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

arXiv: https://arxiv.org/abs/2607.27964 · HTML: https://mlsanity.com/paper/2607.27964/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 27 of its 48 references that are in the map.
- First posted on arXiv 30 Jul 2026.

## Builds on (most cited first, 27 of 27)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [DeepSeek-V4: Towards Highly Efficient Million-Token Context Intelligence](https://mlsanity.com/paper/2606.19348/) (2026)
- [Grammar-Constrained Decoding for Structured NLP Tasks without Finetuning](https://mlsanity.com/paper/2305.13971/) (2023)
- [Guiding LLMs The Right Way: Fast, Non-Invasive Constrained Generation](https://mlsanity.com/paper/2403.06988/) (2024)
- [Medically Aware GPT-3 as a Data Generator for Medical Dialogue Summarization](https://mlsanity.com/paper/2110.07356/) (2021)
- [SynCode: LLM Generation with Grammar Augmentation](https://mlsanity.com/paper/2403.01632/) (2024)
- [Grammar Prompting for Domain-Specific Language Generation with Large Language Models](https://mlsanity.com/paper/2305.19234/) (2023)
- [Let Models Speak Ciphers: Multiagent Debate through Embeddings](https://mlsanity.com/paper/2310.06272/) (2023)
- [A Scalable Communication Protocol for Networks of Large Language Models](https://mlsanity.com/paper/2410.11905/) (2024)
- [Flexible and Efficient Grammar-Constrained Decoding](https://mlsanity.com/paper/2502.05111/) (2025)
- [Type-Constrained Code Generation with Language Models](https://mlsanity.com/paper/2504.09246/) (2025)
- [FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving](https://mlsanity.com/paper/2406.14408/) (2024)
- [ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models](https://mlsanity.com/paper/2509.00360/) (2025)
- [ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees](https://mlsanity.com/paper/2504.21022/) (2025)
- [Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs](https://mlsanity.com/paper/2512.17334/) (2025)
- [Constrained Decoding for Fill-in-the-Middle Code Language Models via Efficient Left and Right Quotienting of Context-Sensitive Grammars](https://mlsanity.com/paper/2402.17988/) (2024)
- [LDP: An Identity-Aware Protocol for Multi-Agent LLM Systems](https://mlsanity.com/paper/2603.08852/) (2026)
- [Preguss: It Analyzes, It Specifies, It Verifies](https://mlsanity.com/paper/2508.14532/) (2025)
- [Precise subtyping for synchronous multiparty sessions](https://mlsanity.com/paper/1602.03593/) (2016)
- [On the Preciseness of Subtyping in Session Types](https://mlsanity.com/paper/1610.00328/) (2016)
- [Undecidability of Asynchronous Session Subtyping](https://mlsanity.com/paper/1611.05026/) (2016)
- [A Sound Algorithm for Asynchronous Session Subtyping and its Implementation](https://mlsanity.com/paper/1907.00421/) (2019)
- [Precise Subtyping for Asynchronous Multiparty Sessions](https://mlsanity.com/paper/2010.13925/) (2020)
- [Deadlock-free asynchronous message reordering in Rust with multiparty session types](https://mlsanity.com/paper/2112.12693/) (2021)

## 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.