Awesome
TLA<sup>+</sup> Examples
This is a repository of TLA<sup>+</sup> 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<sup>+</sup>
- a diverse corpus facilitating development & testing of TLA<sup>+</sup> language tools
- a collection of case studies in the application of formal specification in TLA<sup>+</sup>
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:
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<sup>+</sup> specification you'd like to share with the community? Follow these instructions:
- Fork this repository and create a new directory under
specifications
with the name of your spec - Place all TLA<sup>+</sup> files in the directory, along with their
.cfg
model files - 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
- Ensure name of each
.cfg
file matches the.tla
file it models, or has its name as a prefix; for exampleSpecName.tla
can have the modelsSpecName.cfg
andSpecNameLiveness.cfg
, etc. - 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 - 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:
- Ensure you have Python 3.11+ installed
- It is considered best practice to create & initialize a Python virtual environment to preserve your system package store; run
python -m venv .
thensource ./bin/activate
on Linux & macOS or.\Scripts\activate.bat
on Windows (rundeactivate
to exit) - Run
pip install -r .github/scripts/requirements.txt
- Run
python .github/scripts/generate_manifest.py
- 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/.