Welcome to TLA⁺ Examples

The page TLA⁺ Examples is a library of TLA⁺ specifications for distributed algorithms. The webpage supplies the TLA⁺ community with:

• A comprehensive library of the TLA⁺ specifications that are available today, in order to provide an overview of how to specify an algorithm in TLA⁺.
• A comprehensive list of references and other interesting information for each problem.

Do you have your own case study that you like to share with the community? Send a pointer to us and we will include it in the repository. Your specifications will help the community in improving the tools for TLA⁺ analysis.

List of Examples

No	Name	Short description	Spec's authors	TLAPS Proof	TLC Check	Used modules	PlusCal
1	2PCwithBTM	A modified version of P2TCommit (Gray & Lamport, 2006)	Murat Demirbas		✔	FinSet, Int, Seq	✔
2	802.16	IEEE 802.16 WiMAX Protocols	Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou		✔	Int, Seq, FinSet
3	aba-asyn-byz	Asynchronous Byzantine agreement (Bracha & Toueg, 1985)	Thanh Hai Tran, Igor Konnov, Josef Widder		✔	Nat
4	acp-nb	Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993)	Stephan Merz		✔	default theories
5	acp-nb-wrong	Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993)	Stephan Merz		✔	default theories
6	acp-sb	Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993)	Stephan Merz		✔	default theories
7	allocator	Specification of a resource allocator	Stephan Merz		✔	FinSet
8	async-comm	The diversity of asynchronous communication (Chevrou et al., 2016)	Florent Chevrou, Aurélie Hurault, Philippe Quéinnec		✔	Nat
9	bcastByz	Asynchronous reliable broadcast - Figure 7 (Srikanth & Toeug, 1987)	Thanh Hai Tran, Igor Konnov, Josef Widder	✔	✔	Nat, FinSet
10	bcastFolklore	Folklore reliable broadcast - Figure 4 (Chandra and Toueg, 1996)	Thanh Hai Tran, Igor Konnov, Josef Widder	✔	✔	Nat
11	bosco	One-Step Byzantine asynchronous consensus (Song & Renesse, 2008)	Thanh Hai Tran, Igor Konnov, Josef Widder		✔	Nat, FinSet
12	Boulangerie	A variant of the bakery algorithm (Yoram & Patkin, 2015)	Leslie Lamport, Stephan Merz	✔	✔	Int	✔
13	byihive	Based on RFC3506 - Requirements and Design for Voucher Trading System (Fujimura & Eastlake)	Santhosh Raju		✔	default theories
14	byzpaxos	Byzantizing Paxos by Refinement (Lamport, 2011)	Leslie Lamport		✔	Int, FinSet
15	c1cs	Consensus in one communication step (Brasileiro et al., 2001)	Thanh Hai Tran, Igor Konnov, Josef Widder		✔	Int, FinSet
16	Caesar	Multi-leader generalized consensus protocol (Arun et al., 2017)	Giuliano Losa		✔	FinSet, Seq, Int	✔
17	CarTalkPuzzle	A TLA+ specification of the solution to a nice puzzle.			✔	Int
18	CASPaxos	An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov)	Tobias Schottdorf		✔	Int, FinSet
19	cbc_max	Condition-based consensus (Mostefaoui et al., 2003)	Thanh Hai Tran, Igor Konnov, Josef Widder		✔	Int, FinSet
20	cf1s-folklore	One-step consensus with zero-degradation (Dobre & Suri, 2006)	Thanh Hai Tran, Igor Konnov, Josef Widder		✔	Nat
21	ChangRoberts	Leader election in a ring (Chang & Roberts, 1979)	Stephan Merz		✔	Nat, Seq	✔
22	DataPort	Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016)	Geoffrey Biggs, Noriaki Ando			Int, Seq
23	detector_chan96	Chandra and Toueg’s eventually perfect failure detector	Thanh Hai Tran, Igor Konnov, Josef Widder		✔	Int, FinSet
24	DieHard	A very elementary example based on a puzzle from a movie			✔	Nat
25	dijkstra-mutex	Mutual exclusion algorithm (Dijkstra, 1965)			✔	Int	✔
26	diskpaxos	Disk Paxos (Gafni & Lamport, 2003)	Leslie Lamport, Giuliano Losa		✔	Int
27	egalitarian-paxos	Leaderless replication protocol based on Paxos (Moraru et al., 2013)	Iulian Moraru		✔	Nat, FinSet
28	ewd840	Termination detection in a ring (Dijkstra et al., 1986)	Stephan Merz	✔	✔	Nat
70	ewd998	Shmuel safra's version of termination detection	Stephan Merz, Markus Kuppe		✔	Int, FinSet
29	fastpaxos	An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006)	Leslie Lamport			Nat, FinSet
30	fpaxos	A variant of Paxos with flexible quorums (Howard et al., 2017)	Heidi Howard		✔	Int
31	HLC	Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014)	Murat Demirbas		✔	Int	✔
32	L1	Data center network L1 switch protocol, only PDF files (Thacker)	Tom Rodeheffer			FinSet, Nat, Seq
33	lamport_mutex	Mutual exclusion (Lamport, 1978)	Stephan Merz	✔	✔	Nat, Seq
34	leaderless	Leaderless generalized-consensus algorithms (Losa, 2016)	Giuliano Losa		✔	FinSet, Int, Seq	✔
35	losa_ap	The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018)	Giuliano Losa		✔	FinSet, Nat, Seq	✔
36	losa_rda	Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014)	Giuliano Losa			FinSet, Nat, Seq
37	m2paxos	Multi-leader consensus protocols (Peluso et al., 2016)	Giuliano Losa		✔	Int, Seq, FinSet
38	mongo-repl-tla	A simplified part of Raft in MongoDB (Ongaro, 2014)	Siyuan Zhou		✔	FinSet, Nat, Seq
39	MultiPaxos	The abstract specification of Generalized Paxos (Lamport, 2004)	Giuliano Losa		✔	Int, FinSet
40	N-Queens	The N queens problem	Stephan Merz		✔	Nat, Seq	✔
41	naiad	Naiad clock protocol, only PDF files (Murray et al., 2013)	Tom Rodeheffer		✔	Int, Seq, FinSet
42	nbacc_ray97	Asynchronous non-blocking atomic commit (Raynal, 1997)	Thanh Hai Tran, Igor Konnov, Josef Widder		✔	Nat, FinSet
43	nbacg_guer01	On the hardness of failure-sensitive agreement problems (Guerraoui, 2001)	Thanh Hai Tran, Igor Konnov, Josef Widder		✔	Nat, FinSet
44	nfc04	Non-functional properties of component-based software systems (Zschaler, 2010)	Steffen Zschaler		✔	Real, Nat
45	Paxos	Paxos consensus algorithm (Lamport, 1998)	Leslie Lamport		✔	Int, FinSet
46	Prisoners	A puzzle that was presented on an American radio program.			✔	Nat, FinSet
47	raft	Raft consensus algorithm (Ongaro, 2014)	Diego Ongaro		✔	FinSet, Nat, Seq
48	SnapshotIsolation	Serializable snapshot isolation (Cahill et al., 2010)	Michael J. Cahill, Uwe Röhm, Alan D. Fekete		✔	FinSet, Int, Seq
49	spanning	Spanning tree broadcast algorithm in Attiya and Welch’s book	Thanh Hai Tran, Igor Konnov, Josef Widder		✔	Int
50	SpecifyingSystems	Examples to accompany the book Specifying Systems (Lamport, 2002)			✔	all modules
51	Stones	The same problem as CarTalkPuzzle			✔	FinSet, Int, Seq
52	sums_even	Two proofs for showing that x+x is even, for any natural number x.		✔	✔	Int
53	SyncConsensus	Synchronized round consensus algorithm (Demirbas)	Murat Demirbas		✔	FinSet, Int, Seq	✔
54	Termination	Channel counting algorithm (Mattern, 1987)	Giuliano Losa		✔	FinSet, Bags, Nat	✔
55	Tla-tortoise-hare	Robert Floyd's cycle detection algorithm	Lorin Hochstein		✔	Nat	✔
56	tower_of_hanoi	The well-known Towers of Hanoi puzzle.	Markus Kuppe, Alexander Niederbühl		✔	Bit, FinSet, Int, Nat, Seq
57	transaction_commit	Consensus on transaction commit (Gray & Lamport, 2006)	Leslie Lamport		✔	Int
58	TransitiveClosure	The transitive closure of a relation			✔	FinSet, Int, Seq
59	TwoPhase	Two-phase handshaking	Leslie Lamport, Stephan Merz		✔	Nat
60	VoldemortKV	Voldemort distributed key value store	Murat Demirbas		✔	FinSet, Int, Seq	✔
61	Missionaries and Cannibals	Missionaries and Cannibals	Leslie Lamport		✔	FinSet, Int
62	Misra Reachability Algorithm	Misra Reachability Algorithm	Leslie Lamport	✔	✔	Int, Seq, FiniteSets, TLC, TLAPS, NaturalsInduction	✔
63	Loop Invariance	Loop Invariance	Leslie Lamport	✔	✔	Int, Seq, FiniteSets, TLC, TLAPS, SequenceTheorems, NaturalsInduction	✔
64	Teaching Concurrency	Teaching Concurrency	Leslie Lamport	✔	✔	Int, TLAPS	✔
65	Spanning Tree	Spanning Tree	Leslie Lamport		✔	Int, FiniteSets, TLC, Randomization
66	Paxos (How to win a Turing Award)	Paxos	Leslie Lamport		✔	Nat, Int, FiniteSets
67	Tencent-Paxos	PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017)	Xingchen Yi, Hengfeng Wei	✔	✔	Int, FiniteSets
68	Blocking Queue	BlockingQueue	Markus Kuppe	✔	✔ (LiveEnv)	Naturals, Sequences, FiniteSets
69	Paxos	Paxos			✔	Int, FiniteSets
71	Echo Algorithm	Echo Algorithm	Stephan Merz		✔	Naturals, FiniteSets, Relation, TLC	✔
72	Cigarette Smokers problem	Cigarette Smokers problem	Mariusz Ryndzionek		✔	Integers, FiniteSets
73	Conway's Game of Life	Conway's Game of Life	Mariusz Ryndzionek		✔	Integers
74	Sliding puzzles	Sliding puzzles	Mariusz Ryndzionek		✔	Integers
75	Lock-Free Set	PlusCal spec of a lock-Free set used by TLC	Markus Kuppe		✔	Sequences, FiniteSets, Integers, TLC	✔
76	Chameneos	Chameneos, a Concurrency Game	Mariusz Ryndzionek		✔	Integers
77	ParallelRaft	A variant of Raft	Xiaosong Gu, Hengfeng Wei, Yu Huang		✔	Integers, FiniteSets, Sequences, Naturals
78	TLC MC	PlusCal spec of safety checking as implemented in TLC	Markus Kuppe		✔	Integers, FiniteSets, Sequences, TLC	✔
79	TLA+ Level Checking	Level-checking of TLA+ formulas as described in Specifying Systems	Leslie Lamport			Integers, Sequences
80	CRDT-Bug	CRDT algorithm with defect and fixed version	Alexander Niederbühl		✔	FiniteSets, Naturals, Sequences
81	asyncio-lock	Bugs from old versions of Python's asyncio lock	Alexander Niederbühl		✔	Sequences
82	Single Lane Bridge problem	Single Lane Bridge	Younes Akhouayri		✔	Naturals, FiniteSets, Sequences
83	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		✔	Functions, SequencesExt, FiniteSetsExt, TypedBags
84	EWD687a	Detecting termination in distributed computations by Edsger Dijkstra and Carel Scholten	Stephan Merz (PlusCal spec), Leslie Lamport & Markus Kuppe (TLA+ spec)		✔	Integers, Graphs	✔
85	Huang	Termination detection by using distributed snapshots by Shing-Tsaan Huang	Markus Kuppe		✔	DyadicRationals
86	Azure Cosmos DB	Consistency models provided by Azure Cosmos DB	Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe		✔	Integers, Sequences, FiniteSets, Functions, SequencesExt	✔
87	MET for CRDT-Redis	Model-check the CRDT designs, then generate test cases to test CRDT implementations	Yuqi Zhang		✔	Integers, Sequences, FiniteSets, TLC	✔
88	Parallel increment	Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry	Chris Jensen		✔	Integers, FiniteSets, TLC

License

The repository is under the MIT license. However, we can upload your benchmarks under your license.

Support or Contact

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