Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models

• URL: http://arxiv.org/abs/2607.27964v2
• Date: Sun, 02 Aug 2026 10:30:36 GMT
• Title: Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models
• Abstract summary: 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.
• Score: 2.1311014724439845
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Ensuring behavioural correctness in communication protocols is a central challenge in distributed software systems, as subtle inconsistencies can lead to deadlocks. In such settings, protocol refinement - the safe substitution of a protocol that preserves correctness and compatibility with other components - is essential. Large language models (LLMs) have demonstrated strong capabilities in code generation and program synthesis, yet lack mechanisms to reliably produce outputs with correct behaviour. Formal specification approaches, such as multiparty session types (MPST), offer rigorous guarantees, including deadlock freedom, but provide limited support for automatically constructing protocol refinements. In this paper, we present Syntropy, a framework for synthesising protocol refinements guided by MPST specifications and LLMs. It incorporates refinement constraints directly into the generation process, ensuring the generated variants satisfy these guarantees. Our comprehensive evaluation indicates that Syntropy achieves 95.6%-99.5% validity while maintaining high syntactic correctness, and produces diverse, non-trivial refinements across multiple LLMs.

Related papers

• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
  ZkEVMs generate zero-knowledge that guarantee off-chain execution correctness.<n> subtle implementation bugs can lead to valid proofs certifying semantically faulty states.<n>Formal verification via SMT solvers can prevent this, but is bottlenecked by specification.<n>We propose Veri Synth, a framework that synthesizes executable Python/Z3 verification models from Rust.
  arXiv  Detail & Related papers  (2026-07-22T06:20:36Z)
• LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean [9.293322518056357]
  We present an approach that combines type-based reasoning with trace-based reasoning, enabling modular verification of stateful and unbounded protocols.<n>We implement this framework as the LeanDY library for the Lean proof assistant, building on and extending the design of DY*.<n>We formalize SegWit-style blockchain primitives in LeanDY and demonstrate its expressiveness by carrying out an in-depth formalization of payment channels.
  arXiv  Detail & Related papers  (2026-07-03T15:12:30Z)
• 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)
• SEVerA: Verified Synthesis of Self-Evolving Agents [12.9624447364193]
  Self-evolving agent frameworks provide no formal guarantees of safety or correctness.<n>We formulate agentic code generation as a constrained learning problem, combining hard formal specifications with soft objectives capturing task utility.<n>We present SEVerA, a three-stage framework: Search synthesizes candidate parametric programs containing FGGM calls; Verification proves correctness with respect to hard constraints for all parameter values, reducing the problem to unconstrained learning.
  arXiv  Detail & Related papers  (2026-03-26T07:32:20Z)
• 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)
• Towards Semantic Communication Protocols: A Probabilistic Logic Perspective [69.68769942563812]
  We propose a semantic protocol model (SPM) constructed by transforming an NPM into an interpretable symbolic graph written in the probabilistic logic programming language (ProbLog) By leveraging its interpretability and memory-efficiency, we demonstrate several applications such as SPM reconfiguration for collision-avoidance.
  arXiv  Detail & Related papers  (2022-07-08T14:19:36Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  We study the performance of a practical continuous-variable (CV) quantum key distribution protocol. We focus on the Gaussian-modulated coherent-state protocol with heterodyne detection in a high signal-to-noise ratio regime. This allows us to study the performance for practical implementations of the protocol and optimize the parameters connected to the steps above.
  arXiv  Detail & Related papers  (2022-05-20T12:37:09Z)

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.