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.
