Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models

• URL: http://arxiv.org/abs/2605.24619v1
• Date: Sat, 23 May 2026 15:06:15 GMT
• Title: Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
• Abstract summary: We present IC3Syn, a neuro-symbolic framework that synthesizes inductive invariants by executing an IC3-style process over TLA+ states.<n>We evaluate IC3Syn on 29 distributed protocols spanning consensus, reconfiguration and client-server systems.
• Score: 10.962435384504301
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 IC3Syn, 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, IC3Syn 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 IC3Syn on 29 distributed protocols spanning consensus, reconfiguration and client-server systems, and compare it against Endive, IC3PO, SWISS and DistAI. IC3Syn discovers candidate invariants for all 29 protocols, including MongoLoglessDynamicRaft (MLDR), an industrial-scale Raft-based reconfiguration protocol for which none of the compared tools reports a solution, as well as one complex Paxos variant. In each case, the invariants synthesized on finite instances are shown in TLAPS to be inductive for the full unbounded protocol, thereby establishing safety.

Related papers

• Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models [2.1311014724439845]
  Syntropy is a framework for synthesising protocol refinements guided by MPST specifications and LLMs.<n>It incorporates refinement constraints directly into the generation process, ensuring the generated variants satisfy these guarantees.<n>Our evaluation indicates that Syntropy achieves 95.6%-99.5% validity while maintaining high syntactic correctness, and produces diverse, non-trivial refinements.
  arXiv  Detail & Related papers  (2026-07-30T10:11:33Z)
• Constraint-Driven Synthesis of Hyper Petri Nets [46.9047309711542]
  This paper addresses the modeling and synthesis of constrained robotic system behaviors using Petri nets (PNs)<n>It investigates how to construct models in which all observable system states satisfy given logical constraints while remaining consistent with executable transition semantics.<n>The proposed method introduces an explicit execution semantics over observable states, induced by admissible (atomic) firing sequences.
  arXiv  Detail & Related papers  (2026-07-24T07:57:19Z)
• EZSMT Version 3, Matured [2.4387391584956]
  This paper presents the design and implementation of EZSMTV3, an SMT-based CASP framework that advances the translational approach to CASP solving.<n>Building upon the foundation of the EZSMT+ system, EZSMTV3 introduces a more expressive input language, supports optimization via weak constraints, and offers foundations for streamlined integration of new constraint types.<n>The paper provides benchmarking results comparing EZSMTV3 with its CASP peers such as CLINGCON, CLINGO[DL], and CLINGO[LP]
  arXiv  Detail & Related papers  (2026-07-15T00:07:15Z)
• When LLMs Develop Languages: Symbolic Communication for Efficient Multi-Agent Reasoning [85.36421257648294]
  Chain-of-Thought (CoT) improves large language models (LLMs) on difficult reasoning tasks.<n>We propose Communicative Language Symbolism Routing (R)<n>R treats each Language Symbolism Framework as a reusable symbolic protocol with compact symbols, usage rules, and a message-passing contract.<n>R reduces latency-oriented generated token completion by $3sim 6times$ compared to standard CoT.
  arXiv  Detail & Related papers  (2026-06-28T12:02:42Z)
• A Technical Taxonomy of LLM Agent Communication Protocols [60.76747983053368]
  This study develops a technical taxonomy to classify and analyze large language models (LLMs) agent communication protocols.<n>The framework guides protocol selection and highlights open research gaps such as privacy and policy enforcement.
  arXiv  Detail & Related papers  (2026-06-17T14:45:20Z)
• Mitigating Bias in Locally Constrained Decoding via Tractable Proposals [73.78736135699953]
  Existing locally constrained decoding approaches enforce constraints by myopically masking out next tokens.<n>Recent work uses sequential Monte Carlo methods to mitigate such biases, but designing effective proposal distributions or potential functions remains a key challenge.<n>We propose a generic approach to construct proposals and potentials for SMC sampling from $p_mathrmlm( cdot mid mathrmconstraint)$.
  arXiv  Detail & Related papers  (2026-06-01T08:58:18Z)
• From I/O to Code with Discovery Agent [103.88427301265669]
  We propose DIO-Agent, a discovery agent for IO2Code.<n>Our method frames IO2Code as an evolutionary search over discrete program space.<n>Extensive experiments show that DIO-Agent consistently outperforms both traditional program-by-example method and SOTA evolution-agent baselines.
  arXiv  Detail & Related papers  (2026-05-14T18:57:32Z)
• CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
  CktFormalizer is a framework that redirects hardware generation through a dependently-typed HDL embedded in Lean 4.<n>On VerilogEval (156 problems), RTLLM (50 problems), and ResBench (56 problems), CktFormalizer achieves simulation pass rates competitive with direct Verilog generation.
  arXiv  Detail & Related papers  (2026-05-08T14:20:06Z)
• Beyond Structure: Revolutionising Materials Discovery via AI-Driven Synthesis Protocol-Property Relationships [0.0]
  We argue that closing this gap demands a pivot to a synthesis-first paradigm in which executable synthesis protocols are treated as primary design variables.<n>We outline a roadmap built on three pillars: (i) representing synthesis procedures as machine-readable protocols, (ii) deploying generative and inverse-design models to propose actionable reaction pathways and recipes, and (iii) integrating closed-loop optimisation to refine protocols against experimental realities and sustainability constraints.
  arXiv  Detail & Related papers  (2026-05-01T00:48:39Z)
• Multigrain-aware Semantic Prototype Scanning and Tri-Token Prompt Learning Embraced High-Order RWKV for Pan-Sharpening [46.94213480279033]
  We propose a Multigrain-aware Semantic Prototype Scanning paradigm for pan-sharpening.<n>We use a high-order RWKV architecture and a tri-token prompting mechanism derived from semantic clustering.<n> Experimental results demonstrate the superiority of our method.
  arXiv  Detail & Related papers  (2026-04-16T05:10:03Z)
• TermiGen: High-Fidelity Environment and Robust Trajectory Synthesis for Terminal Agents [70.68963723787424]
  TermiGen is an end-to-end pipeline for synthesizing verifiable environments and resilient expert trajectories.<n>Our TermiGen-Qwen2.5-Coder-32B achieves a 31.3% pass rate on TerminalBench.
  arXiv  Detail & Related papers  (2026-02-06T23:56:50Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  We propose an unsupervised conformal inference framework for generation.<n>Our gates achieve close-to-nominal coverage and provide tighter, more stable thresholds than split UCP.<n>The result is a label-free, API-compatible gate for test-time filtering.
  arXiv  Detail & Related papers  (2025-09-26T23:40:47Z)
• LLM-Assisted Model-Based Fuzzing of Protocol Implementations [9.512044399020514]
  Faults in protocol behavior can lead to vulnerabilities and system failures.<n>A common approach to protocol testing involves constructing Markovian models that capture the state transitions and expected behaviors of the protocol.<n>We propose a novel method that leverages large language models (LLMs) to automatically generate sequences for testing network protocol implementations.
  arXiv  Detail & Related papers  (2025-08-03T13:16:18Z)
• ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
  We introduce ProtocolLLM, the first benchmark suite specifically targeting widely used SystemVerilog protocols.<n>We observe that most of the models fail to generate SystemVerilog code for communication protocols that follow timing constrains.
  arXiv  Detail & Related papers  (2025-06-09T17:10:47Z)
• Squeezeformer: An Efficient Transformer for Automatic Speech Recognition [99.349598600887]
  Conformer is the de facto backbone model for various downstream speech tasks based on its hybrid attention-convolution architecture. We propose the Squeezeformer model, which consistently outperforms the state-of-the-art ASR models under the same training schemes.
  arXiv  Detail & Related papers  (2022-06-02T06:06:29Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.