TLA+ is a formal specification and verification language to help engineers design, specify, reason about, and verify complex software and hardware systems. It is widely used to verify the algorithms in distributed systems.
- Homepage: https://lamport.azurewebsites.net/tla/tla.html
- Learn TLA+: https://learntla.com/introduction/
- reddit: https://www.reddit.com/r/tlaplus/
- google groups: https://groups.google.com/forum/#!forum/tlaplus
- TLA+ example：https://github.com/tlaplus/Examples
| name | description |
|---|---|
| AWS and TLA+ | Use of Formal Methods at Amazon Web Services |
| Batch Installer (H) | Sending async batches of commands. |
| Redux (H) | Redux reducers with verifying a temporal property. |
| Zero Downtime Deployments (H) | A simple model of a deploying new code to servers where at least one server is always available to clients, and all available servers show the same code version. |
| Trading Algorithm | Trading boths executing trades in a simulated market, showing how it’s susceptible to flash crashes. |
| Detecting Linked-List Cycles | Finding cycles in linked lists. |
| Replicated Storage | Replicated storage system with a quorum. |
| Rate Limiter (H) | Independent workers hitting a rate-limited API. |
| Thread Pool (T) | Multiple reader and writer threads sharing a bounded queue, discovering deadlocks. |
| Bank Transfer (H) | Specifying a bank transfer with overdraft protection. |
| Finding bugs in systems through formalization | Ensuring distributed jobs go from “pending” to “completed”. |
| TLA+ in TIDB | verify the distributed consensus algorithm : Raft & the implementation of distributed transaction. |
-
Specification of a resource allocator, written by Stephan Merz.
-
A TLA+ specification of the solution to a nice puzzle.
-
A PlusCal specification of the algorithm by Chang and Roberts (1979) for electing a leader on a unidirectional ring.
-
A very elementary example based on a puzzle from a movie. It provides a good first introduction to TLA+.
-
A PlusCal version of the first published mutual exclusion algorithm, written by Edsger Dijkstra.
-
ewd840 A TLA+ specification of an algorithm due to Dijkstra, Feijen, and van Gasteren for detecting distributed termination on a unidirectional ring, together with a safety proof.
-
lamport_mutex A TLA+ specification of the distributed mutual-exclusion algorithm that appeared as an example in Lamport's classic paper "Time, Clocks and the Ordering of Events in a Distributed System", together with a hierarchical proof of mutual exclusion.
-
N-Queens TLA+ and PlusCal descriptions of a solution to the N queens problem. Written by Stephan Merz.
-
A high-level specification of the Paxos consensus algorithm, consisting of a specification of consensus, a very high level spec of the algorithm (with no messages) that implements consensus and is implemented by the Paxos algorithm.
-
A simple specification that solves a puzzle that was presented on an American radio program. The solution is rather subtle, and hence it's not so easy to understand why the solution is correct.
-
Specifying Systems Examples to accompany the book Specifying Systems.
-
Another specification that solves the same proble as CarTalkPuzzle.
-
Two proofs for showing that x+x is even, for any natural number x.
-
The well-known Towers of Hanoi puzzle.
-
TLA+ specifications underlying the paper "Consensus on Transaction Commit" by Gray and Lamport (2006).
-
Someone once posted on TLAPlus.net a question asking how the transitive closure of a relation can be defined in TLA+. This answers the question by giving several equivalent definitions. Reading them might help you when you have to define some mathematical operation that requires a recursive definition.
-
A specification of a very simple hardware protocol and of the problem it solves. This is a nice example of the use of instantiation to describe a refinement mapping, and of the use of constant operator parameters to describe unspecified actions. There is also a TLA+ proof of correctness that has been checked by the TLAPS proof system.
enjoy it! 😄