  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.
