Specification-guided synthesis of deadlock-free communication protocol refinements with large language models

Conference item

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.

Authors: Li, Y; Hou, PH; Yoshida, N

• Publication status: Accepted
• Peer review status: Peer reviewed
• Publisher: IEEE
• Acceptance date: 2026-07-28
• Event title: 41st IEEE/ACM International Conference on Automated Software Engineering (ASE 2026)
• Event location: Munich, Germany
• Event website: https://conf.researchr.org/home/ase-2026
• Event start date: 2026-10-12
• Event end date: 2026-10-16
• Language: English
• Keywords: formal specifications; large language models; protocol refinement; behavioural correctness; constrained generation; session types