Distributed consensus algorithms such as Paxos have been studied extensively. Many different liveness properties and assumptions have been stated for them, but there are no systematic comparisons for better understanding of these properties.

This paper describes the application of a high-level language and method in developing simpler specifications of more complex variants of the Paxos algorithm for distributed consensus. The specifications are for Multi-Paxos with preemption, replicated state machine, and reconfiguration and optimized with state reduction and failure detection. The language is DistAlgo. The key is to express complex control flows and synchronization conditions precisely at a high level, using nondeterministic waits and message-history queries. We obtain complete executable specifications that are almost completely declarative--updating only a number for the protocol round besides the sets of messages sent and received.