Scalable, Interpretable Distributed Protocol Verification by Inductive Proof Slicing

TL;DR

The paper tackles the challenge of scalable and interpretable safety verification for large-scale distributed protocols by introducing inductive proof slicing. It frames inductive invariants as a conjunction of lemmas organized in an inductive proof graph, and accelerates invariant synthesis via local, grammar- and state-based slicing that focuses on small state projections. A central contribution is the formalization of inductive proof graphs, along with an automated inference algorithm that builds these graphs from a target safety property and discharges them through localized subproblems. The approach is implemented in Scimitar and evaluated on benchmarks including Raft, TwoPhase, and other distributed protocols, demonstrating significant scalability improvements and providing interpretable failure diagnosis that guides grammar repair. Overall, inductive proof slicing delivers scalable automated invariant inference with explicit, human-readable proof structure that aids diagnosis and repair in complex distributed systems.

Abstract

Many techniques for automated inference of inductive invariants for distributed protocols have been developed over the past several years, but their performance can still be unpredictable and their failure modes opaque for large-scale verification tasks. In this paper, we present inductive proof slicing, a new automated, compositional technique for inductive invariant inference that scales effectively to large distributed protocol verification tasks. Our technique is built on a core, novel data structure, the inductive proof graph, which explicitly represents the lemma and action dependencies of an inductive invariant and is built incrementally during the inference procedure, backwards from a target safety property. We present an invariant inference algorithm that integrates localized syntax-guided lemma synthesis routines at nodes of this graph, which are accelerated by computation of localized grammar and state variable slices. Additionally, in the case of failure to produce a complete inductive invariant, maintenance of this proof graph structure allows failures to be localized to small sub-components of this graph, enabling fine-grained failure diagnosis and repair by a user. We evaluate our technique on several complex distributed and concurrent protocols, including a large scale specification of the Raft consensus protocol, which is beyond the capabilities of modern distributed protocol verification tools, and also demonstrate how its interpretability features allow effective diagnosis and repair in cases of initial failure.

Figures (9)

• Figure 1: State variables, initial states (Init), transition relation (Next), and safety property (NoConflictingValues) for the SimpleConsensus protocol. Definitions of the protocol actions are shown on the right.
• Figure 2: Complete inductive invariant, Ind, for proving the NoConflictingValues safety property of the SimpleConsensus protocol from Figure \ref{['fig:simple-consensus-spec']}. Selected lemma definitions from Ind are also shown.
• Figure 3: Example progression of inductive proof graph for SimpleConsensus during execution of our inference algorithm. Nodes in orange with ✗ are those with remaining inductive proof obligations to be discharged, and those in green with ✓ represent those with all obligations discharged.
• Figure 4: A complete inductive proof graph for SimpleConsensus protocol inductive invariant and NoConflictingValues safety property (the root node). Local variable slices are shown as $V_{slice}$, along with the size of the explored state set slice at that node, indicated as $|R|$, along with the reduction factor over the full set of explored states computed during inference runs of SimpleConsensus.
• Figure 5: Full grammar and some grammar slices for SimpleConsensus protocol. Predicate sets in red indicate predicates removals that lead to inductive invariant inference failure for SimpleConsensus.

Theorems & Definitions (9)

• definition 1
• definition 2: Local Action Validity
• definition 3: Local Lemma Validity
• definition 4: Inductive Proof Graph Validity
• lemma 1
• theorem 1
• definition 5
• definition 6
• theorem 2