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 benchmarks

No	Name	Short description	Spec's authors	TLAPS Proof	TLC Check	Used modules
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
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		✔	FinSet, Nat, Bit
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

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? Please contact Thanh-Hai Tran.