Papers › Formal Verification of Multi-Paxos for Distributed Consensus
Formal Verification of Multi-Paxos for Distributed Consensus
Saksham Chand, Yanhong A. Liu, Scott D. Stoller
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
Paxos is an important algorithm for a set of distributed processes to agree on a single value or a sequence of values, for which it is called Basic Paxos or Multi-Paxos, respectively. Consensus is critical when distributed services are replicated for fault-tolerance, because non-faulty replicas must agree on the state of the system or the sequence of operations that have been performed. Unfortunately, consensus algorithms including Multi-Paxos in particular are well-known to be difficult to understand, and their accurate specifications and correctness proofs remain challenging, despite extensive studies ever since Lamport introduced Paxos. This article describes formal specification and verification of Lamport's Multi-Paxos algorithm for distributed consensus. The specification is written in TLA+, Lamport's Temporal Logic of Actions. The proof is written and automatically checked using TLAPS, the TLA+ Proof System. The proof is for the safety property of the algorithm. Building on Lamport, Merz, and Doligez's specification and proof for Basic Paxos, we aim to facilitate the understanding of Multi-Paxos and its proof by minimizing the difference from those for Basic Paxos, and to demonstrate a general way of proving other variants of Paxos and other sophisticated distributed algorithms. We also discuss our general strategies and results for proving complex invariants using invariance lemmas and increments, for proving properties about sets and tuples to help the proof check succeed in significantly reduced time, and for overall proof improvement leading to considerably reduced proof size.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections