Home

Awesome

TLA<sup>+</sup> Examples

Gitpod ready-to-code Validate Specs & Models

This is a repository of TLA<sup>+</sup> specifications and models covering applications in a variety of fields. It serves as:

All TLA<sup>+</sup> specs can be found in the specifications directory. The table below lists all specs and their features, such as whether they are suitable for beginners, come with an additional PlusCal variant (✔), or use PlusCal exclusively. The manifest.json file is the source of truth for this table, and is a detailed human- & machine-readable description of the specs & their models. Its schema is manifest-schema.json. All specs in this repository are subject to CI validation to ensure quality.

Examples Included Here

Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:

NameAuthor(s)BeginnerTLAPS ProofPlusCalTLC ModelApalache
Teaching ConcurrencyLeslie Lamport
Loop InvarianceLeslie Lamport
Learn TLA⁺ ProofsAndrew Helwer
Boyer-Moore Majority VoteStephan Merz
Proof x+x is EvenStephan Merz
The N-Queens PuzzleStephan Merz
The Dining Philosophers ProblemJeff Hemphill
The Car Talk PuzzleLeslie Lamport
The Die Hard ProblemLeslie Lamport
The Prisoners & Switches PuzzleLeslie Lamport
Specs from Specifying SystemsLeslie Lamport
The Tower of Hanoi PuzzleMarkus Kuppe, Alexander Niederbühl
Missionaries and CannibalsLeslie Lamport
Stone Scale PuzzleLeslie Lamport
The Coffee Can Bean ProblemAndrew Helwer
EWD687a: Detecting Termination in Distributed ComputationsStephan Merz, Leslie Lamport, Markus Kuppe(✔)
The Boulangerie AlgorithmLeslie Lamport, Stephan Merz
Misra Reachability AlgorithmLeslie Lamport
Byzantizing Paxos by RefinementLeslie Lamport
EWD840: Termination Detection in a RingStephan Merz
EWD998: Termination Detection in a Ring with Asynchronous Message DeliveryStephan Merz, Markus Kuppe(✔)
The Paxos ProtocolLeslie Lamport
Asynchronous Reliable BroadcastThanh Hai Tran, Igor Konnov, Josef Widder
Distributed Mutual ExclusionStephan Merz
Two-Phase HandshakingLeslie Lamport, Stephan Merz
Paxos (How to Win a Turing Award)Leslie Lamport
Dijkstra's Mutual Exclusion AlgorithmLeslie Lamport
The Echo AlgorithmStephan Merz
The TLC Safety Checking AlgorithmMarkus Kuppe
Transaction Commit ModelsLeslie Lamport, Jim Gray, Murat Demirbas
The Slush ProtocolAndrew Helwer
Minimal Circular SubstringAndrew Helwer
Snapshot Key-Value StoreAndrew Helwer, Murat Demirbas
Chang-Roberts Algorithm for Leader Election in a RingStephan Merz
MultiPaxos in SMR-StyleGuanzhou Hu
Einstein's RiddleIsaac DeFrain, Giuliano Losa
Resource AllocatorStephan Merz
Transitive ClosureStephan Merz
Atomic Commitment ProtocolStephan Merz
SWMR Shared Memory Disk PaxosLeslie Lamport, Giuliano Losa
Span Tree ExerciseLeslie Lamport
The Knuth-Yao MethodRon Pressler, Markus Kuppe
Huang's AlgorithmMarkus Kuppe
EWD 426: Token StabilizationMurat Demirbas, Markus Kuppe
Sliding Block PuzzleMariusz Ryndzionek
Single-Lane Bridge ProblemYounes Akhouayri
Software-Defined PerimeterLuming Dong, Zhi Niu
Simplified Fast PaxosLim Ngian Xin Terry, Gaurav Gandhi
Checkpoint CoordinationAndrew Helwer
Finitizing Monotonic SystemsAndrew Helwer
Multi-Car Elevator SystemAndrew Helwer
Nano Blockchain ProtocolAndrew Helwer
The Readers-Writers ProblemIsaac DeFrain
Asynchronous Byzantine ConsensusThanh Hai Tran, Igor Konnov, Josef Widder
Folklore Reliable BroadcastThanh Hai Tran, Igor Konnov, Josef Widder
The Bosco Byzantine Consensus AlgorithmThanh Hai Tran, Igor Konnov, Josef Widder
Consensus in One Communication StepThanh Hai Tran, Igor Konnov, Josef Widder
One-Step Consensus with Zero-DegradationThanh Hai Tran, Igor Konnov, Josef Widder
Failure DetectorThanh Hai Tran, Igor Konnov, Josef Widder
Asynchronous Non-Blocking Atomic CommitThanh Hai Tran, Igor Konnov, Josef Widder
Asynchronous Non-Blocking Atomic Commitment with Failure DetectorsThanh Hai Tran, Igor Konnov, Josef Widder
Spanning Tree Broadcast AlgorithmThanh Hai Tran, Igor Konnov, Josef Widder
The Cigarette Smokers ProblemMariusz Ryndzionek
Conway's Game of LifeMariusz Ryndzionek
Chameneos, a Concurrency GameMariusz Ryndzionek
PCR Testing for Snippets of DNAMartin Harrison
RFC 3506: Voucher Transaction SystemSanthosh Raju, Cherry G. Mathew, Fransisca Andriani
Yo-Yo Leader ElectionLudovic Yvoz, Stephan Merz
TCP as defined in RFC 9293Markus Kuppe
TLA⁺ Level CheckingLeslie Lamport
Condition-Based ConsensusThanh Hai Tran, Igor Konnov, Josef Widder
Buffered Random Access FileCalvin Loncaric
DisruptorNicholas Schultz-Møller

Examples Elsewhere

Here is a list of specs stored in locations outside this repository, including submodules. They are not covered by CI testing so it is possible they contain errors, the reported details are incorrect, or they are no longer available. Ideally these will be moved into this repo over time.

SpecDetailsAuthor(s)BeginnerTLAPS ProofTLC ModelPlusCalApalache
Blocking QueueBlockingQueueMarkus Kuppe(✔)
IEEE 802.16 WiMAX Protocols2006, paper, specsPrasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, Hai Zhou
On the diversity of asynchronous communication2016, paper, specsFlorent Chevrou, Aurélie Hurault, Philippe Quéinnec
CaesarMulti-leader generalized consensus protocol (Arun et al., 2017)Giuliano Losa
CASPaxosAn extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov)Tobias Schottdorf
DataPortDataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016)Geoffrey Biggs, Noriaki Ando
egalitarian-paxosLeaderless replication protocol based on Paxos (Moraru et al., 2013)Iulian Moraru
fastpaxosAn extension of the classic Paxos algorithm, only PDF files (Lamport, 2006)Leslie Lamport
fpaxosA variant of Paxos with flexible quorums (Howard et al., 2017)Heidi Howard
HLCHybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014)Murat Demirbas
L1Data center network L1 switch protocol, only PDF files (Thacker)Tom Rodeheffer
leaderlessLeaderless generalized-consensus algorithms (Losa, 2016)Giuliano Losa
losa_apThe assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018)Giuliano Losa
losa_rdaApplying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014)Giuliano Losa
m2paxosMulti-leader consensus protocols (Peluso et al., 2016)Giuliano Losa
mongo-repl-tlaA simplified part of Raft in MongoDB (Ongaro, 2014)Siyuan Zhou
MultiPaxosThe abstract specification of Generalized Paxos (Lamport, 2004)Giuliano Losa
naiadNaiad clock protocol, only PDF files (Murray et al., 2013)Tom Rodeheffer
nfc04Non-functional properties of component-based software systems (Zschaler, 2010)Steffen Zschaler
raftRaft consensus algorithm (Ongaro, 2014)Diego Ongaro
SnapshotIsolationSerializable snapshot isolation (Cahill et al., 2010)Michael J. Cahill, Uwe Röhm, Alan D. Fekete
SyncConsensusSynchronized round consensus algorithm (Demirbas)Murat Demirbas
TerminationChannel-counting algorithm (Kumar, 1985)Giuliano Losa
Tla-tortoise-hareRobert Floyd's cycle detection algorithmLorin Hochstein
VoldemortKVVoldemort distributed key value storeMurat Demirbas
Tencent-PaxosPaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017)Xingchen Yi, Hengfeng Wei
PaxosPaxos
Lock-Free SetPlusCal spec of a lock-Free set used by TLCMarkus Kuppe
ParallelRaftA variant of RaftXiaosong Gu, Hengfeng Wei, Yu Huang
CRDT-BugCRDT algorithm with defect and fixed versionAlexander Niederbühl
asyncio-lockBugs from old versions of Python's asyncio lockAlexander Niederbühl
Raft (with cluster changes)Raft with cluster changes, and a version with Apalache type annotations but no cluster changesGeorge Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts
MET for CRDT-RedisModel-check the CRDT designs, then generate test cases to test CRDT implementationsYuqi Zhang
Parallel incrementParallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetryChris Jensen
The Streamlet consensus algorithmSpecification and model-checking of both safety and liveness properties of Streamlet with TLCGiuliano Losa
Petri NetsInstantiable Petri Nets with liveness propertiesEugene Huang
CRDTSpecifying and Verifying CRDT ProtocolsYe Ji, Hengfeng Wei
Azure Cosmos DBConsistency models provided by Azure Cosmos DBDharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe

License

The repository is under the MIT license and you are encouraged to publish your spec under a similarly-permissive license. However, your spec can be included in this repo along with your own license if you wish.

Support or Contact

Do you have any questions or comments? Please open an issue or send an email to the TLA+ group.

Contributing

Do you have your own case study or TLA<sup>+</sup> specification you'd like to share with the community? Follow these instructions:

  1. Fork this repository and create a new directory under specifications with the name of your spec
  2. Place all TLA<sup>+</sup> files in the directory, along with their .cfg model files
  3. You are encouraged to include at least one model that completes execution in less than 10 seconds, and (if possible) a model that fails in an interesting way - for example illustrating a system design you previously attempted that was found unsound by TLC
  4. Ensure name of each .cfg file matches the .tla file it models, or has its name as a prefix; for example SpecName.tla can have the models SpecName.cfg and SpecNameLiveness.cfg, etc.
  5. Consider including a README.md in the spec directory explaining the significance of the spec with links to any relevant websites or publications, or integrate this info as comments in the spec itself
  6. Add an entry to the table of specs included in this repo, summarizing your spec and its attributes

Adding Spec to Continuous Integration

To combat bitrot, it is important to add your spec and model to the continuous integration system. To do this, you'll have to update the manifest.json file with machine-readable records of your spec files. If this process doesn't work for you, you can alternatively modify the .ciignore file to exclude your spec from validation. Modifying the manifest.json can be done manually or (recommended) following these directions:

  1. Ensure you have Python 3.11+ installed
  2. It is considered best practice to create & initialize a Python virtual environment to preserve your system package store; run python -m venv . then source ./bin/activate on Linux & macOS or .\Scripts\activate.bat on Windows (run deactivate to exit)
  3. Run pip install -r .github/scripts/requirements.txt
  4. Run python .github/scripts/generate_manifest.py
  5. Locate your spec's entry in the manifest.json file and ensure the following fields are filled out:
    • Spec title: an appropriate title for your specification
    • Spec description: a short description of your specification
    • Spec sources: links relevant to the source of the spec (papers, blog posts, repositories)
    • Spec authors: a list of people who authored the spec
    • Spec tags:
      • "beginner" if your spec is appropriate for TLA<sup>+</sup> newcomers
    • Model runtime: approximate model runtime on an ordinary workstation, in "HH:MM:SS" format
    • Model size:
      • "small" if the model can be executed in less than 10 seconds
      • "medium" if the model can be executed in less than five minutes
      • "large" if the model takes more than five minutes to execute
    • Model mode:
      • "exhaustive search" by default
      • {"simulate": {"traceCount": N}} for a simulation model
      • "generate" for model trace generation
    • Model result:
      • "success" if the model completes successfully
      • "assumption failure" if the model violates an assumption
      • "safety failure" if the model violates an invariant
      • "liveness failure" if the model fails to satisfy a liveness property
      • "deadlock failure" if the model encounters deadlock
    • (Optional) Model state count info: distinct states, total states, and state depth
      • These are all individually optional and only valid if your model uses exhaustive search and results in success
      • Recording these turns your model into a powerful regression test for TLC
    • Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the manifest-schema.json file)

Before submitted your changes to run in the CI, you can quickly check your manifest.json for errors and also check it against manifest-schema.json at https://www.jsonschemavalidator.net/.