Search papers, labs, and topics across Lattice.
This paper introduces a novel incremental proof system for safety properties that decomposes complex inductive invariants into simpler, sequential proof steps. The system combines forward reasoning, backward reasoning (on a time-reversed system), and prophecy steps to introduce witnesses for existential properties. The authors prove the soundness of each rule and demonstrate that a single, complex inductive invariant can be recovered from the incremental proof, highlighting the reduced complexity of invariants used in the incremental approach.
Decomposing safety proofs into forward, backward, and prophecy steps dramatically simplifies the search for inductive invariants, enabling verification of complex systems like Paxos and Raft.
We propose an incremental approach for safety proofs that decomposes a proof with a complex inductive invariant into a sequence of simpler proof steps. Our proof system combines rules for (i) forward reasoning using inductive invariants, (ii) backward reasoning using inductive invariants of a time-reversed system, and (iii) prophecy steps that add witnesses for existentially quantified properties. We prove each rule sound and give a construction that recovers a single safe inductive invariant from an incremental proof. The construction of the invariant demonstrates the increased complexity of a single inductive invariant compared to the invariant formulas used in an incremental proof, which may have simpler Boolean structures and fewer quantifiers and quantifier alternations. Under natural restrictions on the available invariant formulas, each proof rule strictly increases proof power. That is, each rule allows to prove more safety problems with the same set of formulas. Thus, the incremental approach is able to reduce the search space of invariant formulas needed to prove safety of a given system. A case study on Paxos, several of its variants, and Raft demonstrates that forward-backward steps can remove complex Boolean structure while prophecy eliminates quantifiers and quantifier alternations.
