一句话：提出增量式安全证明系统，融合前向推理、时间反转的后向推理与 prophecy 步骤，将复杂归纳不变式拆解为更简单的证明步骤。
安全性验证常需构造单个归纳不变式，但其布尔结构与量词交替复杂，搜索空间大。本文提出增量式安全证明：把复杂不变式证明分解为多个更简单的步骤，证明系统包含基于归纳不变式的前向推理、基于时间反转系统的后向推理，以及为存在量化性质添加见证的 prophecy 规则。作者证明各规则可靠，并给出从增量证明恢复单一安全归纳不变式的构造，说明单个不变式比增量公式更复杂。在自然限制下每条规则都严格增强证明能力，从而缩减不变式搜索空间。Paxos 变体与 Raft 案例表明，前向-后向步骤消除复杂布尔结构，prophecy 消除量词与量词交替。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FrenkelMPS26,
title = {Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy},
author = {Eden Frenkel and Kenneth L. McMillan and Oded Padon and Sharon Shoham},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808341}
}