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. To contribute a spec of your own, see CONTRIBUTING.md.

The table below lists all specs and indicates whether a spec is beginner-friendly, includes an additional PlusCal variant (✔), or uses PlusCal exclusively. Additionally, the table specifies which verification tool—TLC, Apalache, or TLAPS—can be used to verify each specification.

Space contraints limit the information displayed in the table; detailed spec metadata can be found in the manifest.json files in each specification's directory. You can search these files for examples exhibiting a number of features, either using the GitHub repository search or locally with the command ls specifications/*/manifest.json | xargs grep -l $keyword, where $keyword can be a value like:

• pluscal, proof, or action composition (the \cdot operator)
• Specs intended for trace generation (generate), simulate, or checked symbolically with Apalache (symbolic)
• Models failing in interesting ways, like deadlock failure, safety failure, liveness failure, or assumption failure

It is also helpful to consult model files using specific TLC features. For this, run ls specifications/*/*.cfg | xargs grep -l $keyword, where $keyword can be a feature like SYMMETRY, VIEW, ALIAS, CONSTRAINT, or DEADLOCK.

Validated Examples Included Here

Here is a list of specs included in this repository which are validated by the CI, 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 | Martin Riener | ✔ | ✔ | | ✔ | | | 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 | ✔ | | | ✔ | | | The Prisoners & Switch Puzzle | Florian Schanda | ✔ | | | ✔ | | | 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 Moving Cat Puzzle | Florian Schanda | ✔ | | | ✔ | | | The Boulangerie Algorithm | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | | | Misra Reachability Algorithm | Leslie Lamport | | ✔ | ✔ | ✔ | | | Byzantizing Paxos by Refinement | Leslie Lamport | | ✔ | ✔ | ✔ | | | Barrier Synchronization | Jarod Differdange | | ✔ | ✔ | ✔ | | | Peterson Lock Refinement With Auxiliary Variables | Jarod Differdange | | ✔ | ✔ | ✔ | | | 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 | | (✔) | | ✔ | | | Finitizing Monotonic Systems | Andrew Helwer, Stephan Merz, Markus Kuppe | | ✔ | | ✔ | | | Dijkstra's Mutual Exclusion Algorithm | Leslie Lamport | | | ✔ | ✔ | | | The Echo Algorithm | Stephan Merz | | | ✔ |