About
A simplified TLA+ specification of the Fast Paxos protocol by Leslie Lamport, a consensus algorithm for distributed systems.
TLA+ is a high-level language for modeling programs and systems, especially concurrent and distributed ones, using simple mathematics.
Our main motivation was to simplify the much more complex original specification in Lamport’s paper by including 3 assumptions:
1. There is a unique coordinator in the system. Therefore, Phase 1a and 1b can be omitted.
2. All agents in the system can communicate with one another.
3. Agents must have some stable storage that survives failure and restarts. An agent restores its state from stable storage when it restarts, so failure of an agent is indistinguishable from its simply pausing. There is thus no need to model failures explicitly.
=======================================================
🎉 Our Fast Paxos specification has been accepted in the official TLA+ Examples repository! 🎉
=======================================================