I3DP: Neuro-Symbolic Inductive Invariant Inference for Distributed Protocols

Abstract

Distributed protocols are notoriously difficult to verify correctly. Proving safety typically requires inductive invariants that both imply the desired property and are preserved by every protocol transition; yet inferring such invariants remains a major bottleneck: existing approaches either restrict the protocol models to a decidable fragment of first-order logic or demand expert-crafted templates. We present I3DP, a neuro-symbolic framework that synthesizes inductive invariants by executing an IC3-style process over TLA+ states with the assistance of large language models (LLMs). At large, I3DP combines a symbolic IC3 controller which decomposes invariant synthesis into focused blocking tasks, and an LLM which provides protocol-level reasoning that IC3 alone lacks for TLA+ specifications. This integration enables a disciplined yet flexible search for invariants without imposing logical restrictions or requiring manual templates. We evaluate I3DP on 29 distributed protocols spanning consensus, reconfiguration, and client-server systems, and compare it against Endive, IC3PO, SWISS, DuoAI, and P-FOLIC3. I3DP discovers candidate invariants for all 29 protocols. Among them, MongoLoglessDynamicRaft models the core mechanism of an industrial-scale Raft-based reconfiguration protocol, and none of the compared tools reports a solution for it. In each case, the invariants synthesized on finite instances are shown in TLAPS to be inductive for the full unbounded protocol, thereby establishing safety.