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.

翻译：我们提出一种增量式安全证明方法，将包含复杂归纳不变量的证明分解为一系列更简单的证明步骤。我们的证明系统结合了以下规则：（i）使用归纳不变量进行前向推理，（ii）使用时间反转系统的归纳不变量进行后向推理，以及（iii）通过预言步骤添加存在量化属性的见证。我们证明了每条规则的合理性，并给出了一种从增量证明中恢复单一安全归纳不变量的构造方法。该不变量构造表明，与增量证明中使用的不变量公式相比，单一归纳不变量具有更高的复杂度，而增量公式可能具有更简单的布尔结构、更少的量词和量词交替。在可用不变量公式的自然约束条件下，每条证明规则均严格增强证明能力——即每条规则允许使用相同的公式集合证明更多安全问题。因此，增量方法能够缩减证明系统安全性所需的不变量公式搜索空间。针对Paxos、其若干变体及Raft的案例研究表明，前向-后向步骤可消除复杂布尔结构，而预言机制能消除量词及量词交替。