Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models
Not on the map. Why?
Abstract (arXiv)
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.
Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 27 of its 48 references that are in the map. First posted on arXiv 30 Jul 2026.
Builds on
27 of 48 references.
References · 27
- 2017Attention Is All You Needcited by 59,932
- 2021Evaluating Large Language Models Trained on Codecited by 8,053
- 2021Program Synthesis with Large Language Modelscited by 3,509
- 2023Code Llama: Open Foundation Models for Codecited by 2,105
- 2026DeepSeek-V4: Towards Highly Efficient Million-Token Context Intelligencecited by 877
- 2023Grammar-Constrained Decoding for Structured NLP Tasks without Finetuningcited by 186
- 2024Guiding LLMs The Right Way: Fast, Non-Invasive Constrained Generationcited by 99
- 2021Medically Aware GPT-3 as a Data Generator for Medical Dialogue Summarizationcited by 76
- 2024SynCode: LLM Generation with Grammar Augmentationcited by 66
- 2023Grammar Prompting for Domain-Specific Language Generation with Large Language Modelscited by 58
- 2023Let Models Speak Ciphers: Multiagent Debate through Embeddingscited by 49
- 2024A Scalable Communication Protocol for Networks of Large Language Modelscited by 43
15 more
- 2025Flexible and Efficient Grammar-Constrained Decodingcited by 42
- 2025Type-Constrained Code Generation with Language Modelscited by 32
- 2024FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Provingcited by 22
- 2025ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Modelscited by 12
- 2025ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guaranteescited by 9
- 2024Constrained Decoding for Fill-in-the-Middle Code Language Models via Efficient Left and Right Quotienting of Context-Sensitive Grammarscited by 8
- 2025Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMscited by 8
- 2026LDP: An Identity-Aware Protocol for Multi-Agent LLM Systemscited by 7
- 2025Preguss: It Analyzes, It Specifies, It Verifiescited by 2
- 2016Precise subtyping for synchronous multiparty sessionscited by 1
- 2016On the Preciseness of Subtyping in Session Typescited by 1
- 2016Undecidability of Asynchronous Session Subtypingcited by 1
- 2019A Sound Algorithm for Asynchronous Session Subtyping and its Implementationcited by 1
- 2020Precise Subtyping for Asynchronous Multiparty Sessionscited by 1
- 2021Deadlock-free asynchronous message reordering in Rust with multiparty session typescited by 1
Built on by
Not cited yet.