# Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+

arXiv: https://arxiv.org/abs/2205.06360 · HTML: https://mlsanity.com/paper/2205.06360/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 May 2022.

## Built on by (most cited first, 1 of 1)

- [Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2312.10842/) (2023)

## Abstract (arXiv)

We present a new technique for automatically inferring inductive invariants of parameterized distributed protocols specified in TLA+. Ours is the first such invariant inference technique to work directly on TLA+, an expressive, high level specification language. To achieve this, we present a new algorithm for invariant inference that is based around a core procedure for generating plain, potentially non-inductive lemma invariants that are used as candidate conjuncts of an overall inductive invariant. We couple this with a greedy lemma invariant selection procedure that selects lemmas that eliminate the largest number of counterexamples to induction at each round of our inference procedure. We have implemented our algorithm in a tool, endive, and evaluate it on a diverse set of distributed protocol benchmarks, demonstrating competitive performance and ability to uniquely solve an industrial scale reconfiguration protocol.