The Paxos algorithm of Lamport is a classic consensus protocol for state machine replication in environments that admit crash failures. New versions of this protocol are constantly springing that compete with each other for better performance, widening the gap between the description of the Paxos algorithm and the real-world systems. We tackle the challenge of verifying these increasingly complex protocols by applying modular reasoning, this is, by verifying parts of the protocol separately instead of verifying the whole protocol in one go. To this end, we consider the abstractions from an existing decomposition of Paxos by Boichat et al. and we provide highly non-deterministic, atomic specifications of these abstractions that are strong enough to prove the algorithm correct.

In this talk I will present our advances in proving that the implementations of Boichat et al. refine (i.e., are linearizable with respect to) our non-deterministic specifications. We conjecture that variants of Paxos and other consensus algorithms, like Multi-Paxos, ZAB and Viewstamped Replication, could be verified in a similar fashion.