Paxos algorithm specified and proved in TLA+/PlusCal, with separate processes and invariants for proposers and acceptors.

The Dutch national flag problem is a partitioning problem proposed and solved by E. Dijkstra in the 1970s. The problem is solved in +CAL in TLA.

Experimenting with formal methods using TLA+ and Pluscal

Compared the specifications and correctness of Distributed Mutex Algorithms and compared the efficiency, max clock values, max states reached using TLA+

A TLA+ specification for the Xen vchan protocol

A TLA+ verification of the Go-Back-N ARQ protocol

How to use TLA+ / TLA+ specification of the ClickHouse replication protocol

A collection of TLA+ specifications of varying complexities

Learning and experimenting with TLA toy models

TLA+ model checking and TLAPS theorem proving for the Paxos implementation in PaxosStore by WeChat

A TLA+ Specification of Peterson's Algorithm

Parse the trace of TLC output and generate HTML with better format.

TLA+ examples and modelling

A formally verified implementation of a bolt-on security device for ICS networks. Designed with TLA+ and written/proved in F*

A TLA+ module for animating TLC traces.

When a process is betrayed and sent into a limbo by a fellow process, it regains its majority and comes back for consensus.

Applying TLA+/TLC/TLAPS to Source Code

Formal models of vac protocols