MobilityReadingGroup

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

Yang LI , Ping HOU , Nobuko YOSHIDA

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.

@inproceedings{LHY2026,
  author = {Yang Li and Ping Hou and Nobuko Yoshida},
  title = {{Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models}},
  booktitle = {The 41st IEEE/ACM International Conference on Automated Software Engineering, Munich, Germany},
  pages = {--},
  year = 2026
}

@inproceedings{LHY2026,
  author = {Yang Li and Ping Hou and Nobuko Yoshida},
  title = {{Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models}},
  booktitle = {The 41st IEEE/ACM International Conference on Automated Software Engineering, Munich, Germany},
  pages = {--},
  year = 2026
}