  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.
