Many techniques for the automated verification of distributed protocols have been developed over the past several years, but their performance is still unpredictable and their failure modes can be opaque for industrial scale verification tasks. Thus, in practice, large-scale verification efforts typically require some amount of human guidance. In this paper, we present inductive proof decomposition, a new methodology for interactive safety verification that provides a compositional, interactive approach to inductive invariant development. Our approach guides the human-aided development of inductive invariants via a novel structure, an inductive proof graph, which is built incrementally by a human verifier, working backwards from a target safety property. A user is guided by induction counterexamples that are localized to specific nodes of this graph, and nodes of this proof graph are further decomposed based on logical actions that appear in a protocol's transition relation. Our decomposition also enables a localized variable slicing technique that hides irrelevant protocol state at each sub-component of an inductive proof, allowing a user to focus on fine-grained sub-problems rather than a large, monolithic inductive invariant. We present our technique and experience applying it to develop inductive safety proofs of several complex distributed protocols, including the Raft consensus protocol, which is beyond the capabilities of modern automated verification tools. We also demonstrate how the developed proof graphs provide additional insight into the structure of a protocol proof and its correctness.

翻译：在过去几年中，分布式协议自动化验证技术得到了广泛发展，但其性能仍难以预测，且针对工业级验证任务，其失效模式往往难以直观理解。因此，在实际大规模验证工作中，通常需要一定程度的人工引导。本文提出归纳证明分解方法——一种新型的交互式安全性验证方法，通过组合式交互途径实现归纳不变量的构建。该方法借助一种新型结构——归纳证明图，引导人工辅助构建归纳不变量：验证者从目标安全属性出发逆向操作，逐步构建该图。用户通过定位于图中特定节点的归纳反例获得引导，同时根据协议转换关系中的逻辑动作对证明图节点进行进一步分解。该分解技术还支持局部变量切片，能够隐藏归纳证明各子组件中不相关的协议状态，使验证者可以专注于细粒度子问题，而非处理庞大单一的归纳不变量。我们展示了该方法的技术细节及应用经验，成功为多个复杂分布式协议（包括现代自动化验证工具无法处理的Raft共识协议）构建了归纳安全性证明。同时证明，所生成的证明图能够为协议证明结构及其正确性提供更深入的洞见。