A collection of TLA⁺ specifications of varying complexities.

writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+

Dr. TLA+ series - learn an algorithm and protocol, study a specification

TLA+ specification for the Raft consensus algorithm

Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

Azure Cosmos TLA+ specifications

Learn TLA+ for free! No prior experience necessary!

PGo is a source to source compiler from Modular PlusCal specs into Go programs.

A TLA+ specification of the Apache BookKeeper replication protocol

TLA+ specification of the Kafka replication protocol

Pluscal/TLA+ modeling of distributed systems/protocols

A TLA+ module for animating TLC traces.

Specifying and Verifying CRDT Protocols using TLA+

TLA+ specification of the Ceph consensus algorithm

Azure Cosmos TLA+ specifications

TLA+ specification for the Raft consensus algorithm (with Pre-Vote)

TLA+ description for the CAS-Paxos algorithm

Modeling snapshot isolation in TLA+

Verifying the correctness of CRDTs using TLA+/PlusCal

Verification tool for distributed protocols based on inductive proof decomposition.

TLA+ specification of the Practical BFT protocol

TLA+ specs for ViewStampedReplication

Modeling B-trees in TLA+

Some TLA+ specs that I wrote

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