🎊 This TLA+ specification has been merged into the Official TLA+ Examples Repository! 🎊
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.
Please, make sure to install Visual Studio Code and its TLA+ Extension, following the instructions on the linked pages. Also, consider adding the following command to your VSCode setting to parse your TLA+ code automatically.
After installing the TLA+ extension for VSCode, Simply open FastPaxos.tla or Paxos.tla in VSCode, right click anywhere in the file editor, and click "Check model with TLC".
The following timings were achieved on a 6-core, 12-thread CPU:
- Paxos.tla: 4 seconds
- FastPaxos.tla: 1 minute 2 seconds