diff --git a/.github/scripts/format_markdown_table.py b/.github/scripts/format_markdown_table.py index 16db0300..9008f5a0 100644 --- a/.github/scripts/format_markdown_table.py +++ b/.github/scripts/format_markdown_table.py @@ -66,7 +66,7 @@ def format_document(document): # Gets table of local specs local_table, remote_table = [child for child in document.children if isinstance(child, Table)] #format_table(local_table) - format_table(remote_table) + #format_table(remote_table) # Read, format, write # Need to both parse & render within same MarkdownRenderer context to preserve other formatting diff --git a/README.md b/README.md index 8b80bf87..f3f453c6 100644 --- a/README.md +++ b/README.md @@ -16,121 +16,121 @@ 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](specifications/TeachingConcurrency) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | | -| [Loop Invariance](specifications/LoopInvariance) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | | -| [Learn TLA⁺ Proofs](specifications/LearnProofs) | Andrew Helwer | ✔ | ✔ | ✔ | ✔ | | -| [Boyer-Moore Majority Vote](specifications/Majority) | Stephan Merz | ✔ | ✔ | | ✔ | | -| [Proof x+x is Even](specifications/sums_even) | Stephan Merz | ✔ | ✔ | | ✔ | | -| [The N-Queens Puzzle](specifications/N-Queens) | Stephan Merz | ✔ | | ✔ | ✔ | | -| [The Dining Philosophers Problem](specifications/DiningPhilosophers) | Jeff Hemphill | ✔ | | ✔ | ✔ | | -| [The Car Talk Puzzle](specifications/CarTalkPuzzle) | Leslie Lamport | ✔ | | | ✔ | | -| [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | | | ✔ | | -| [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | | -| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | | | ✔ | | -| [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi) | Markus Kuppe, Alexander Niederbühl | ✔ | | | ✔ | | -| [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | | | ✔ | | -| [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | ✔ | | -| [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | | | ✔ | | -| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | | -| [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | | -| [Byzantizing Paxos by Refinement](specifications/byzpaxos) | Leslie Lamport | | ✔ | ✔ | ✔ | | -| [EWD840: Termination Detection in a Ring](specifications/ewd840) | Stephan Merz | | ✔ | | ✔ | | -| [EWD998: Termination Detection in a Ring with Asynchronous Message Delivery](specifications/ewd998) | Stephan Merz, Markus Kuppe | | ✔ | | ✔ | | -| [The Paxos Protocol](specifications/Paxos) | Leslie Lamport | | ✔ | | ✔ | | -| [Asynchronous Reliable Broadcast](specifications/bcastByz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | | ✔ | | -| [Distributed Mutual Exclusion](specifications/lamport_mutex) | Stephan Merz | | ✔ | | ✔ | | -| [Two-Phase Handshaking](specifications/TwoPhase) | Leslie Lamport, Stephan Merz | | ✔ | | ✔ | | -| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward) | Leslie Lamport | | ✔ | | ✔ | | -| [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex) | Leslie Lamport | | | ✔ | ✔ | | -| [The Echo Algorithm](specifications/echo) | Stephan Merz | | | ✔ | ✔ | | -| [The TLC Safety Checking Algorithm](specifications/TLC) | Markus Kuppe | | | ✔ | ✔ | | -| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | | | ✔ | ✔ | | -| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | | ✔ | ✔ | | -| [The Slush Protocol](specifications/SlushProtocol) | Andrew Helwer | | | ✔ | ✔ | | -| [Minimal Circular Substring](specifications/LeastCircularSubstring) | Andrew Helwer | | | ✔ | ✔ | | -| [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | | ✔ | ✔ | | -| [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts) | Stephan Merz | | | ✔ | ✔ | | -| [Resource Allocator](specifications/allocator) | Stephan Merz | | | | ✔ | | -| [Transitive Closure](specifications/TransitiveClosure) | Stephan Merz | | | | ✔ | | -| [Atomic Commitment Protocol](specifications/acp) | Stephan Merz | | | | ✔ | | -| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos) | Leslie Lamport, Giuliano Losa | | | | ✔ | | -| [Span Tree Exercise](specifications/SpanningTree) | Leslie Lamport | | | | ✔ | | -| [The Knuth-Yao Method](specifications/KnuthYao) | Ron Pressler, Markus Kuppe | | | | ✔ | | -| [Huang's Algorithm](specifications/Huang) | Markus Kuppe | | | | ✔ | | -| [EWD 426: Token Stabilization](specifications/ewd426) | Murat Demirbas, Markus Kuppe | | | | ✔ | | -| [Sliding Block Puzzle](specifications/SlidingPuzzles) | Mariusz Ryndzionek | | | | ✔ | | -| [Single-Lane Bridge Problem](specifications/SingleLaneBridge) | Younes Akhouayri | | | | ✔ | | -| [Software-Defined Perimeter](specifications/SDP_Verification) | Luming Dong, Zhi Niu | | | | ✔ | | -| [Simplified Fast Paxos](specifications/SimplifiedFastPaxos) | Lim Ngian Xin Terry, Gaurav Gandhi | | | | ✔ | | -| [Checkpoint Coordination](specifications/CheckpointCoordination) | Andrew Helwer | | | | ✔ | | -| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer | | | | ✔ | | -| [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | | -| [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | | -| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | | -| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain | | | | ✔ | | -| [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | -| [Folklore Reliable Broadcast](specifications/bcastFolklore) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | -| [The Bosco Byzantine Consensus Algorithm](specifications/bosco) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | -| [Consensus in One Communication Step](specifications/c1cs) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | -| [One-Step Consensus with Zero-Degradation](specifications/cf1s-folklore) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | -| [Failure Detector](specifications/detector_chan96) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | -| [Asynchronous Non-Blocking Atomic Commit](specifications/nbacc_ray97) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | -| [Asynchronous Non-Blocking Atomic Commitment with Failure Detectors](specifications/nbacg_guer01) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | -| [Spanning Tree Broadcast Algorithm](specifications/spanning) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | -| [The Cigarette Smokers Problem](specifications/CigaretteSmokers) | Mariusz Ryndzionek | | | | ✔ | | -| [Conway's Game of Life](specifications/GameOfLife) | Mariusz Ryndzionek | | | | ✔ | | -| [Chameneos, a Concurrency Game](specifications/Chameneos) | Mariusz Ryndzionek | | | | ✔ | | -| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | ✔ | | +| Name | Author(s) | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache | +| --------------------------------------------------------------------------------------------------- | --------------------------------------------------- | :------: | :---------: | :-----: | :-------: | :------: | +| [Teaching Concurrency](specifications/TeachingConcurrency) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | | +| [Loop Invariance](specifications/LoopInvariance) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | | +| [Learn TLA⁺ Proofs](specifications/LearnProofs) | Andrew Helwer | ✔ | ✔ | ✔ | ✔ | | +| [Boyer-Moore Majority Vote](specifications/Majority) | Stephan Merz | ✔ | ✔ | | ✔ | | +| [Proof x+x is Even](specifications/sums_even) | Stephan Merz | ✔ | ✔ | | ✔ | | +| [The N-Queens Puzzle](specifications/N-Queens) | Stephan Merz | ✔ | | ✔ | ✔ | | +| [The Dining Philosophers Problem](specifications/DiningPhilosophers) | Jeff Hemphill | ✔ | | ✔ | ✔ | | +| [The Car Talk Puzzle](specifications/CarTalkPuzzle) | Leslie Lamport | ✔ | | | ✔ | | +| [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | | | ✔ | | +| [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | | +| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | | | ✔ | | +| [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi) | Markus Kuppe, Alexander Niederbühl | ✔ | | | ✔ | | +| [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | | | ✔ | | +| [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | ✔ | | +| [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | | | ✔ | | +| [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | | +| [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | | +| [Byzantizing Paxos by Refinement](specifications/byzpaxos) | Leslie Lamport | | ✔ | ✔ | ✔ | | +| [EWD840: Termination Detection in a Ring](specifications/ewd840) | Stephan Merz | | ✔ | | ✔ | | +| [EWD998: Termination Detection in a Ring with Asynchronous Message Delivery](specifications/ewd998) | Stephan Merz, Markus Kuppe | | ✔ | | ✔ | | +| [The Paxos Protocol](specifications/Paxos) | Leslie Lamport | | ✔ | | ✔ | | +| [Asynchronous Reliable Broadcast](specifications/bcastByz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | | ✔ | | +| [Distributed Mutual Exclusion](specifications/lamport_mutex) | Stephan Merz | | ✔ | | ✔ | | +| [Two-Phase Handshaking](specifications/TwoPhase) | Leslie Lamport, Stephan Merz | | ✔ | | ✔ | | +| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward) | Leslie Lamport | | ✔ | | ✔ | | +| [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex) | Leslie Lamport | | | ✔ | ✔ | | +| [The Echo Algorithm](specifications/echo) | Stephan Merz | | | ✔ | ✔ | | +| [The TLC Safety Checking Algorithm](specifications/TLC) | Markus Kuppe | | | ✔ | ✔ | | +| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | | | ✔ | ✔ | | +| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | | ✔ | ✔ | | +| [The Slush Protocol](specifications/SlushProtocol) | Andrew Helwer | | | ✔ | ✔ | | +| [Minimal Circular Substring](specifications/LeastCircularSubstring) | Andrew Helwer | | | ✔ | ✔ | | +| [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | | ✔ | ✔ | | +| [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts) | Stephan Merz | | | ✔ | ✔ | | +| [Resource Allocator](specifications/allocator) | Stephan Merz | | | | ✔ | | +| [Transitive Closure](specifications/TransitiveClosure) | Stephan Merz | | | | ✔ | | +| [Atomic Commitment Protocol](specifications/acp) | Stephan Merz | | | | ✔ | | +| [SWMR Shared Memory Disk Paxos](specifications/diskpaxos) | Leslie Lamport, Giuliano Losa | | | | ✔ | | +| [Span Tree Exercise](specifications/SpanningTree) | Leslie Lamport | | | | ✔ | | +| [The Knuth-Yao Method](specifications/KnuthYao) | Ron Pressler, Markus Kuppe | | | | ✔ | | +| [Huang's Algorithm](specifications/Huang) | Markus Kuppe | | | | ✔ | | +| [EWD 426: Token Stabilization](specifications/ewd426) | Murat Demirbas, Markus Kuppe | | | | ✔ | | +| [Sliding Block Puzzle](specifications/SlidingPuzzles) | Mariusz Ryndzionek | | | | ✔ | | +| [Single-Lane Bridge Problem](specifications/SingleLaneBridge) | Younes Akhouayri | | | | ✔ | | +| [Software-Defined Perimeter](specifications/SDP_Verification) | Luming Dong, Zhi Niu | | | | ✔ | | +| [Simplified Fast Paxos](specifications/SimplifiedFastPaxos) | Lim Ngian Xin Terry, Gaurav Gandhi | | | | ✔ | | +| [Checkpoint Coordination](specifications/CheckpointCoordination) | Andrew Helwer | | | | ✔ | | +| [Finitizing Monotonic Systems](specifications/FiniteMonotonic) | Andrew Helwer | | | | ✔ | | +| [Multi-Car Elevator System](specifications/MultiCarElevator) | Andrew Helwer | | | | ✔ | | +| [Nano Blockchain Protocol](specifications/NanoBlockchain) | Andrew Helwer | | | | ✔ | | +| [The Readers-Writers Problem](specifications/ReadersWriters) | Isaac DeFrain | | | | ✔ | | +| [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain | | | | ✔ | | +| [Asynchronous Byzantine Consensus](specifications/aba-asyn-byz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | +| [Folklore Reliable Broadcast](specifications/bcastFolklore) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | +| [The Bosco Byzantine Consensus Algorithm](specifications/bosco) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | +| [Consensus in One Communication Step](specifications/c1cs) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | +| [One-Step Consensus with Zero-Degradation](specifications/cf1s-folklore) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | +| [Failure Detector](specifications/detector_chan96) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | +| [Asynchronous Non-Blocking Atomic Commit](specifications/nbacc_ray97) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | +| [Asynchronous Non-Blocking Atomic Commitment with Failure Detectors](specifications/nbacg_guer01) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | +| [Spanning Tree Broadcast Algorithm](specifications/spanning) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | ✔ | | +| [The Cigarette Smokers Problem](specifications/CigaretteSmokers) | Mariusz Ryndzionek | | | | ✔ | | +| [Conway's Game of Life](specifications/GameOfLife) | Mariusz Ryndzionek | | | | ✔ | | +| [Chameneos, a Concurrency Game](specifications/Chameneos) | Mariusz Ryndzionek | | | | ✔ | | +| [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | ✔ | | | [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | | | ✔ | | -| [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | -| [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | +| [TLA⁺ Level Checking](specifications/LevelChecking) | Leslie Lamport | | | | | | +| [Condition-Based Consensus](specifications/cbc_max) | Thanh Hai Tran, Igor Konnov, Josef Widder | | | | | | ## 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 | Author(s) | TLAPS Proof | TLC Model | PlusCal | Apalache | -| ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------ | :---------: | :-------: | :-----: | :------: | -| IEEE 802.16 WiMAX Protocols (2006, [paper](https://users.cs.northwestern.edu/~ychen/Papers/npsec06.pdf), [specs](http://list.cs.northwestern.edu/802.16/)) | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, Hai Zhou | | | | | -| On the diversity of asynchronous communication (2016, [paper](https://dl.acm.org/doi/10.1007/s00165-016-0379-x), [specs](http://hurault.perso.enseeiht.fr/asynchronousCommunication/)) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | | | | -| [Caesar](specifications/Caesar) | Multi-leader generalized consensus protocol (Arun et al., 2017) | Giuliano Losa | | ✔ | ✔ | | -| [CASPaxos](specifications/CASPaxos) | An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov) | Tobias Schottdorf | | ✔ | | | -| [DataPort](specifications/DataPort) | Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016) | Geoffrey Biggs, Noriaki Ando | | | | | -| [egalitarian-paxos](specifications/egalitarian-paxos) | Leaderless replication protocol based on Paxos (Moraru et al., 2013) | Iulian Moraru | | ✔ | | | -| [fastpaxos](specifications/fastpaxos) | An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006) | Leslie Lamport | | | | | -| [fpaxos](specifications/fpaxos) | A variant of Paxos with flexible quorums (Howard et al., 2017) | Heidi Howard | | ✔ | | | -| [HLC](specifications/HLC) | Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014) | Murat Demirbas | | ✔ | ✔ | | -| [L1](specifications/L1) | Data center network L1 switch protocol, only PDF files (Thacker) | Tom Rodeheffer | | | | | -| [leaderless](specifications/leaderless) | Leaderless generalized-consensus algorithms (Losa, 2016) | Giuliano Losa | | ✔ | ✔ | | -| [losa_ap](specifications/losa_ap) | The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018) | Giuliano Losa | | ✔ | ✔ | | -| [losa_rda](specifications/losa_rda) | Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014) | Giuliano Losa | | | | | -| [m2paxos](specifications/m2paxos) | Multi-leader consensus protocols (Peluso et al., 2016) | Giuliano Losa | | ✔ | | | -| [mongo-repl-tla](specifications/mongo-repl-tla) | A simplified part of Raft in MongoDB (Ongaro, 2014) | Siyuan Zhou | | ✔ | | | -| [MultiPaxos](specifications/MultiPaxos) | The abstract specification of Generalized Paxos (Lamport, 2004) | Giuliano Losa | | ✔ | | | -| [naiad](specifications/naiad) | Naiad clock protocol, only PDF files (Murray et al., 2013) | Tom Rodeheffer | | ✔ | | | -| [nfc04](specifications/nfc04) | Non-functional properties of component-based software systems (Zschaler, 2010) | Steffen Zschaler | | ✔ | | | -| [raft](specifications/raft) | Raft consensus algorithm (Ongaro, 2014) | Diego Ongaro | | ✔ | | | -| [SnapshotIsolation](specifications/SnapshotIsolation) | Serializable snapshot isolation (Cahill et al., 2010) | Michael J. Cahill, Uwe Röhm, Alan D. Fekete | | ✔ | | | -| [SyncConsensus](specifications/SyncConsensus) | Synchronized round consensus algorithm (Demirbas) | Murat Demirbas | | ✔ | ✔ | | -| [Termination](specifications/Termination) | Channel-counting algorithm (Kumar, 1985) | Giuliano Losa | ✔ | ✔ | ✔ | ✔ | -| [Tla-tortoise-hare](specifications/Tla-tortoise-hare) | Robert Floyd's cycle detection algorithm | Lorin Hochstein | | ✔ | ✔ | | -| [VoldemortKV](specifications/VoldemortKV) | Voldemort distributed key value store | Murat Demirbas | | ✔ | ✔ | | -| [Tencent-Paxos](specifications/TencentPaxos) | PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017) | Xingchen Yi, Hengfeng Wei | ✔ | ✔ | | | -| [Paxos](https://github.com/neoschizomer/Paxos) | Paxos | | | ✔ | | | -| [Lock-Free Set](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.tla) | PlusCal spec of a lock-Free set used by TLC | Markus Kuppe | | ✔ | ✔ | | -| [ParallelRaft](specifications/ParalleRaft) | A variant of Raft | Xiaosong Gu, Hengfeng Wei, Yu Huang | | ✔ | | | -| [CRDT-Bug](https://github.com/Alexander-N/tla-specs/tree/main/crdt-bug) | CRDT algorithm with defect and fixed version | Alexander Niederbühl | | ✔ | | | -| [asyncio-lock](https://github.com/Alexander-N/tla-specs/tree/main/asyncio-lock) | Bugs from old versions of Python's asyncio lock | Alexander Niederbühl | | ✔ | | | -| [Raft (with cluster changes)](https://github.com/dranov/raft-tla) | 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](https://github.com/elem-azar-unis/CRDT-Redis/tree/master/MET/TLA) | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | ✔ | ✔ | | -| [Parallel increment](https://github.com/Cjen1/tla_increment) | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | ✔ | | | -| [The Streamlet consensus algorithm](https://github.com/nano-o/streamlet) | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | ✔ | ✔ | | -| [Petri Nets](https://github.com/elh/petri-tlaplus) | Instantiable Petri Nets with liveness properties | Eugene Huang | | ✔ | | | -| [CRDT](https://github.com/JYwellin/CRDT-TLA) | Specifying and Verifying CRDT Protocols | Ye Ji, Hengfeng Wei | | ✔ | | | -| [Azure Cosmos DB](https://github.com/tlaplus/azure-cosmos-tla) | Consistency models provided by Azure Cosmos DB | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe | | ✔ | ✔ | | -| [Blocking Queue](https://github.com/lemmy/BlockingQueue) | BlockingQueue | Markus Kuppe | ✔ | ✔ | | | +| Spec | Details | Author(s) | TLAPS Proof | TLC Model | PlusCal | Apalache | +| --------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------- | :---------: | :-------: | :-----: | :------: | +| IEEE 802.16 WiMAX Protocols | 2006, [paper](https://users.cs.northwestern.edu/~ychen/Papers/npsec06.pdf), [specs](http://list.cs.northwestern.edu/802.16/) | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, Hai Zhou | | | | | +| On the diversity of asynchronous communication | 2016, [paper](https://dl.acm.org/doi/10.1007/s00165-016-0379-x), [specs](http://hurault.perso.enseeiht.fr/asynchronousCommunication/) | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec | | | | | +| [Caesar](specifications/Caesar) | Multi-leader generalized consensus protocol (Arun et al., 2017) | Giuliano Losa | | ✔ | ✔ | | +| [CASPaxos](specifications/CASPaxos) | An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov) | Tobias Schottdorf | | ✔ | | | +| [DataPort](specifications/DataPort) | Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016) | Geoffrey Biggs, Noriaki Ando | | | | | +| [egalitarian-paxos](specifications/egalitarian-paxos) | Leaderless replication protocol based on Paxos (Moraru et al., 2013) | Iulian Moraru | | ✔ | | | +| [fastpaxos](specifications/fastpaxos) | An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006) | Leslie Lamport | | | | | +| [fpaxos](specifications/fpaxos) | A variant of Paxos with flexible quorums (Howard et al., 2017) | Heidi Howard | | ✔ | | | +| [HLC](specifications/HLC) | Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014) | Murat Demirbas | | ✔ | ✔ | | +| [L1](specifications/L1) | Data center network L1 switch protocol, only PDF files (Thacker) | Tom Rodeheffer | | | | | +| [leaderless](specifications/leaderless) | Leaderless generalized-consensus algorithms (Losa, 2016) | Giuliano Losa | | ✔ | ✔ | | +| [losa_ap](specifications/losa_ap) | The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018) | Giuliano Losa | | ✔ | ✔ | | +| [losa_rda](specifications/losa_rda) | Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014) | Giuliano Losa | | | | | +| [m2paxos](specifications/m2paxos) | Multi-leader consensus protocols (Peluso et al., 2016) | Giuliano Losa | | ✔ | | | +| [mongo-repl-tla](specifications/mongo-repl-tla) | A simplified part of Raft in MongoDB (Ongaro, 2014) | Siyuan Zhou | | ✔ | | | +| [MultiPaxos](specifications/MultiPaxos) | The abstract specification of Generalized Paxos (Lamport, 2004) | Giuliano Losa | | ✔ | | | +| [naiad](specifications/naiad) | Naiad clock protocol, only PDF files (Murray et al., 2013) | Tom Rodeheffer | | ✔ | | | +| [nfc04](specifications/nfc04) | Non-functional properties of component-based software systems (Zschaler, 2010) | Steffen Zschaler | | ✔ | | | +| [raft](specifications/raft) | Raft consensus algorithm (Ongaro, 2014) | Diego Ongaro | | ✔ | | | +| [SnapshotIsolation](specifications/SnapshotIsolation) | Serializable snapshot isolation (Cahill et al., 2010) | Michael J. Cahill, Uwe Röhm, Alan D. Fekete | | ✔ | | | +| [SyncConsensus](specifications/SyncConsensus) | Synchronized round consensus algorithm (Demirbas) | Murat Demirbas | | ✔ | ✔ | | +| [Termination](specifications/Termination) | Channel-counting algorithm (Kumar, 1985) | Giuliano Losa | ✔ | ✔ | ✔ | ✔ | +| [Tla-tortoise-hare](specifications/Tla-tortoise-hare) | Robert Floyd's cycle detection algorithm | Lorin Hochstein | | ✔ | ✔ | | +| [VoldemortKV](specifications/VoldemortKV) | Voldemort distributed key value store | Murat Demirbas | | ✔ | ✔ | | +| [Tencent-Paxos](specifications/TencentPaxos) | PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017) | Xingchen Yi, Hengfeng Wei | ✔ | ✔ | | | +| [Paxos](https://github.com/neoschizomer/Paxos) | Paxos | | | ✔ | | | +| [Lock-Free Set](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.tla) | PlusCal spec of a lock-Free set used by TLC | Markus Kuppe | | ✔ | ✔ | | +| [ParallelRaft](specifications/ParalleRaft) | A variant of Raft | Xiaosong Gu, Hengfeng Wei, Yu Huang | | ✔ | | | +| [CRDT-Bug](https://github.com/Alexander-N/tla-specs/tree/main/crdt-bug) | CRDT algorithm with defect and fixed version | Alexander Niederbühl | | ✔ | | | +| [asyncio-lock](https://github.com/Alexander-N/tla-specs/tree/main/asyncio-lock) | Bugs from old versions of Python's asyncio lock | Alexander Niederbühl | | ✔ | | | +| [Raft (with cluster changes)](https://github.com/dranov/raft-tla) | 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](https://github.com/elem-azar-unis/CRDT-Redis/tree/master/MET/TLA) | Model-check the CRDT designs, then generate test cases to test CRDT implementations | Yuqi Zhang | | ✔ | ✔ | | +| [Parallel increment](https://github.com/Cjen1/tla_increment) | Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry | Chris Jensen | | ✔ | | | +| [The Streamlet consensus algorithm](https://github.com/nano-o/streamlet) | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | ✔ | ✔ | | +| [Petri Nets](https://github.com/elh/petri-tlaplus) | Instantiable Petri Nets with liveness properties | Eugene Huang | | ✔ | | | +| [CRDT](https://github.com/JYwellin/CRDT-TLA) | Specifying and Verifying CRDT Protocols | Ye Ji, Hengfeng Wei | | ✔ | | | +| [Azure Cosmos DB](https://github.com/tlaplus/azure-cosmos-tla) | Consistency models provided by Azure Cosmos DB | Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe | | ✔ | ✔ | | +| [Blocking Queue](https://github.com/lemmy/BlockingQueue) | BlockingQueue | Markus Kuppe | ✔ | ✔ | | | ## License The repository is under the MIT license and you are encouraged to publish your spec under a similarly-permissive license.