TLA⁺ Examples

This is a repository of TLA⁺ specifications and models covering applications in a variety of fields. It serves as:

• a comprehensive example library demonstrating how to specify an algorithm in TLA⁺
• a diverse corpus facilitating development & testing of TLA⁺ language tools
• a collection of case studies in the application of formal specification in TLA⁺

All TLA⁺ 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:

Name	Author(s)	Beginner	TLAPS Proof	PlusCal	TLC Model	Apalache
Teaching Concurrency	Leslie Lamport	✔	✔	✔	✔
Loop Invariance	Leslie Lamport	✔	✔	✔	✔
Learn TLA⁺ Proofs	Andrew Helwer	✔	✔	✔	✔
Boyer-Moore Majority Vote	Stephan Merz	✔	✔		✔
Proof x+x is Even	Stephan Merz	✔	✔		✔
The N-Queens Puzzle	Stephan Merz	✔		✔	✔
The Dining Philosophers Problem	Jeff Hemphill	✔		✔	✔
The Car Talk Puzzle	Leslie Lamport	✔			✔
The Die Hard Problem	Leslie Lamport	✔			✔
The Prisoners & Switches Puzzle	Leslie Lamport	✔			✔
Specs from Specifying Systems	Leslie Lamport	✔			✔
The Tower of Hanoi Puzzle	Markus Kuppe, Alexander Niederbühl	✔			✔
Missionaries and Cannibals	Leslie Lamport	✔			✔
Stone Scale Puzzle	Leslie Lamport	✔			✔
The Coffee Can Bean Problem	Andrew Helwer	✔			✔
EWD687a: Detecting Termination in Distributed Computations	Stephan Merz, Leslie Lamport, Markus Kuppe	✔		(✔)	✔
The Boulangerie Algorithm	Leslie Lamport, Stephan Merz		✔	✔	✔
Misra Reachability Algorithm	Leslie Lamport		✔	✔	✔
Byzantizing Paxos by Refinement	Leslie Lamport		✔	✔	✔
EWD840: Termination Detection in a Ring	Stephan Merz		✔		✔
EWD998: Termination Detection in a Ring with Asynchronous Message Delivery	Stephan Merz, Markus Kuppe		✔	(✔)	✔
The Paxos Protocol	Leslie Lamport		✔		✔
Asynchronous Reliable Broadcast	Thanh Hai Tran, Igor Konnov, Josef Widder		✔		✔
Distributed Mutual Exclusion	Stephan Merz		✔		✔
Two-Phase Handshaking	Leslie Lamport, Stephan Merz		✔		✔
Paxos (How to Win a Turing Award)	Leslie Lamport		✔		✔
Dijkstra's Mutual Exclusion Algorithm	Leslie Lamport			✔	✔
The Echo Algorithm	Stephan Merz			✔	✔
The TLC Safety Checking Algorithm	Markus Kuppe			✔	✔
Transaction Commit Models	Leslie Lamport, Jim Gray, Murat Demirbas			✔	✔
The Slush Protocol	Andrew Helwer			✔	✔
Minimal Circular Substring	Andrew Helwer			✔	✔
Snapshot Key-Value Store	Andrew Helwer, Murat Demirbas			✔	✔
Chang-Roberts Algorithm for Leader Election in a Ring	Stephan Merz			✔	✔
MultiPaxos in SMR-Style	Guanzhou Hu			✔	✔
Resource Allocator	Stephan Merz				✔
Transitive Closure	Stephan Merz				✔
Atomic Commitment Protocol	Stephan Merz				✔
SWMR Shared Memory Disk Paxos	Leslie Lamport, Giuliano Losa				✔
Span Tree Exercise	Leslie Lamport				✔
The Knuth-Yao Method	Ron Pressler, Markus Kuppe				✔
Huang's Algorithm	Markus Kuppe				✔
EWD 426: Token Stabilization	Murat Demirbas, Markus Kuppe				✔
Sliding Block Puzzle	Mariusz Ryndzionek				✔
Single-Lane Bridge Problem	Younes Akhouayri				✔
Software-Defined Perimeter	Luming Dong, Zhi Niu				✔
Simplified Fast Paxos	Lim Ngian Xin Terry, Gaurav Gandhi				✔
Checkpoint Coordination	Andrew Helwer				✔
Finitizing Monotonic Systems	Andrew Helwer				✔
Multi-Car Elevator System	Andrew Helwer				✔
Nano Blockchain Protocol	Andrew Helwer				✔
The Readers-Writers Problem	Isaac DeFrain				✔
Einstein's Riddle	Isaac DeFrain, Giuliano Losa				✔	✔
Asynchronous Byzantine Consensus	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Folklore Reliable Broadcast	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
The Bosco Byzantine Consensus Algorithm	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Consensus in One Communication Step	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
One-Step Consensus with Zero-Degradation	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Failure Detector	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Asynchronous Non-Blocking Atomic Commit	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Asynchronous Non-Blocking Atomic Commitment with Failure Detectors	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
Spanning Tree Broadcast Algorithm	Thanh Hai Tran, Igor Konnov, Josef Widder				✔
The Cigarette Smokers Problem	Mariusz Ryndzionek				✔
Conway's Game of Life	Mariusz Ryndzionek				✔
Chameneos, a Concurrency Game	Mariusz Ryndzionek				✔
PCR Testing for Snippets of DNA	Martin Harrison				✔
RFC 3506: Voucher Transaction System	Santhosh Raju, Cherry G. Mathew, Fransisca Andriani				✔
TLA⁺ Level Checking	Leslie Lamport
Condition-Based Consensus	Thanh Hai Tran, Igor Konnov, Josef Widder
Yo-Yo Leader Election	Ludovic Yvoz, Stephan Merz				✔

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.

Spec	Details	Author(s)	Beginner	TLAPS Proof	TLC Model	PlusCal	Apalache
Blocking Queue	BlockingQueue	Markus Kuppe	✔	✔	✔	(✔)
IEEE 802.16 WiMAX Protocols	2006, paper, specs	Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, Hai Zhou
On the diversity of asynchronous communication	2016, paper, specs	Florent Chevrou, Aurélie Hurault, Philippe Quéinnec
Caesar	Multi-leader generalized consensus protocol (Arun et al., 2017)	Giuliano Losa			✔	✔
CASPaxos	An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov)	Tobias Schottdorf			✔
DataPort	Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016)	Geoffrey Biggs, Noriaki Ando
egalitarian-paxos	Leaderless replication protocol based on Paxos (Moraru et al., 2013)	Iulian Moraru			✔
fastpaxos	An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006)	Leslie Lamport
fpaxos	A variant of Paxos with flexible quorums (Howard et al., 2017)	Heidi Howard			✔
HLC	Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014)	Murat Demirbas			✔	✔
L1	Data center network L1 switch protocol, only PDF files (Thacker)	Tom Rodeheffer
leaderless	Leaderless generalized-consensus algorithms (Losa, 2016)	Giuliano Losa			✔	✔
losa_ap	The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018)	Giuliano Losa			✔	✔
losa_rda	Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014)	Giuliano Losa
m2paxos	Multi-leader consensus protocols (Peluso et al., 2016)	Giuliano Losa			✔
mongo-repl-tla	A simplified part of Raft in MongoDB (Ongaro, 2014)	Siyuan Zhou			✔
MultiPaxos	The abstract specification of Generalized Paxos (Lamport, 2004)	Giuliano Losa			✔
naiad	Naiad clock protocol, only PDF files (Murray et al., 2013)	Tom Rodeheffer			✔
nfc04	Non-functional properties of component-based software systems (Zschaler, 2010)	Steffen Zschaler			✔
raft	Raft consensus algorithm (Ongaro, 2014)	Diego Ongaro			✔
SnapshotIsolation	Serializable snapshot isolation (Cahill et al., 2010)	Michael J. Cahill, Uwe Röhm, Alan D. Fekete			✔
SyncConsensus	Synchronized round consensus algorithm (Demirbas)	Murat Demirbas			✔	✔
Termination	Channel-counting algorithm (Kumar, 1985)	Giuliano Losa		✔	✔	✔	✔
Tla-tortoise-hare	Robert Floyd's cycle detection algorithm	Lorin Hochstein			✔	✔
VoldemortKV	Voldemort distributed key value store	Murat Demirbas			✔	✔
Tencent-Paxos	PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017)	Xingchen Yi, Hengfeng Wei		✔	✔
Paxos	Paxos				✔
Lock-Free Set	PlusCal spec of a lock-Free set used by TLC	Markus Kuppe			✔	✔
ParallelRaft	A variant of Raft	Xiaosong Gu, Hengfeng Wei, Yu Huang			✔
CRDT-Bug	CRDT algorithm with defect and fixed version	Alexander Niederbühl			✔
asyncio-lock	Bugs from old versions of Python's asyncio lock	Alexander Niederbühl			✔
Raft (with cluster changes)	Raft with cluster changes, and a version with Apalache type annotations but no cluster changes	George Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts			✔		✔
MET for CRDT-Redis	Model-check the CRDT designs, then generate test cases to test CRDT implementations	Yuqi Zhang			✔	✔
Parallel increment	Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry	Chris Jensen			✔
The Streamlet consensus algorithm	Specification and model-checking of both safety and liveness properties of Streamlet with TLC	Giuliano Losa			✔	✔
Petri Nets	Instantiable Petri Nets with liveness properties	Eugene Huang			✔
CRDT	Specifying and Verifying CRDT Protocols	Ye Ji, Hengfeng Wei			✔
Azure Cosmos DB	Consistency models provided by Azure Cosmos DB	Dharma 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⁺ 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⁺ 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. Otherwise, follow these directions:

1. Ensure you have Python 3.11+ installed
2. Download & extract tree-sitter-tlaplus (zip, tar.gz) to the root of the repository; ensure the extracted folder is named tree-sitter-tlaplus
3. Open a shell and navigate to the repo root; ensure a C++ compiler is installed and on your path
   • On Windows, this might entail running the below script from the visual studio developer command prompt
4. 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)
5. Run pip install -r .github/scripts/requirements.txt
6. Run python .github/scripts/generate_manifest.py
7. 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⁺ 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/.