  This paper studies specifications and proofs of distributed algorithms when
only message history variables are used, using the Basic Paxos and Multi-Paxos
algorithms for distributed consensus as precise case studies. We show that not
using and maintaining other state variables yields simpler specifications that
are more declarative and easier to understand. It also allows easier proofs to
be developed by needing fewer invariants and facilitating proof derivations.
Furthermore, the proofs are mechanically checked more efficiently.
  We show that specifications in TLA+, Lamport's temporal logic of actions, and
proofs in TLAPS, the TLA+ Proof System (TLAPS) are reduced by a quarter or more
for single-value Paxos and by about half or more for multi-value Paxos. Overall
we need about half as many manually written invariants and proof obligations.
Our proof for Basic Paxos takes about 25% less time for TLAPS to check, and our
proofs for Multi-Paxos are checked within 1.5 minutes whereas prior proofs fail
to be checked by TLAPS.
