Search papers, labs, and topics across Lattice.
This paper introduces Syntropy, a framework that synthesizes deadlock-free communication protocol refinements by integrating multiparty session types (MPST) specifications with large language models (LLMs). The approach ensures that generated protocol variants not only adhere to behavioral correctness but also maintain compatibility with existing components, addressing a significant challenge in distributed software systems. Evaluation results show that Syntropy achieves a remarkable validity rate of 95.6%-99.5% while producing diverse and syntactically correct refinements across various LLMs.
Syntropy achieves up to 99.5% validity in generating deadlock-free protocol refinements, revolutionizing how we ensure correctness in distributed systems.
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.
