Towards an Automatic Proof of Lamport's Paxos

TL;DR

This paper presents an approach to automatically verify the safety of Lamport's Paxos protocol by leveraging structural features in its specification, successfully inferring an inductive invariant with a novel model checking algorithm.

Contribution

It introduces IC3PO, a new model checking algorithm that automatically infers inductive invariants for Paxos, reducing manual effort and demonstrating general applicability.

Findings

Successfully inferred the original Paxos invariant automatically.

First automatic proof of Lamport's Paxos safety properties.

IC3PO can be applied to other protocols with similar structural features.

Abstract

Lamport's celebrated Paxos consensus protocol is generally viewed as a complex hard-to-understand algorithm. Notwithstanding its complexity, in this paper, we take a step towards automatically proving the safety of Paxos by taking advantage of three structural features in its specification: spatial regularity in its unordered domains, temporal regularity in its totally-ordered domain, and its hierarchical composition. By carefully integrating these structural features in IC3PO, a novel model checking algorithm, we were able to infer an inductive invariant that identically matches the human-written one previously derived with significant manual effort using interactive theorem proving. While various attempts have been made to verify different versions of Paxos, to the best of our knowledge, this is the first demonstration of an automatically-inferred inductive invariant for Lamport's original Paxos specification. We note that these structural features are not specific to Paxos and that IC3PO can serve as an automatic general-purpose protocol verification tool.