  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.
