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

TL;DR

This paper introduces a novel technique for automatically inferring inductive invariants directly from TLA+ specifications of distributed protocols, enabling more effective verification of complex systems.

Contribution

It presents the first invariant inference method for TLA+ that combines lemma generation with greedy selection, implemented in the endive tool.

Findings

Successfully infers invariants for diverse distributed protocols

Demonstrates competitive performance against existing methods

Solves an industrial-scale reconfiguration protocol

Abstract

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.