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

1. Problem Statement

Ensuring behavioural correctness in distributed software systems is a critical challenge, as subtle inconsistencies in communication protocols often lead to deadlocks. While Large Language Models (LLMs) have demonstrated proficiency in generating syntactically correct code and satisfying local semantic properties (e.g., type safety), they lack mechanisms to guarantee global behavioural correctness, particularly in complex interaction scenarios.

Conversely, Multiparty Session Types (MPST) provide rigorous formal guarantees, including communication safety and deadlock freedom, through asynchronous multiparty subtyping (AMS). AMS allows a protocol (subtype) to safely replace another (supertype) while preserving these properties. However, the automatic synthesis of such subtypes is non-trivial. The problem is compounded by the fact that AMS is generally undecidable, and existing toolchains offer limited support for automatically constructing valid protocol refinements.

The core research question addressed is: How can protocol refinements be systematically synthesised while retaining behavioural correctness (specifically deadlock freedom) under asynchronous multiparty subtyping?

2. Methodology: The Syntropy Framework

The authors propose Syntropy, a framework that bridges LLMs and formal specifications to synthesise valid protocol refinements. The framework consists of two complementary modules: Syntropy-Train and Syntropy-Gen.

2.1 Syntropy-Train: Learning Subtype Generation

• Fine-Tuning: The authors fine-tune open-source LLMs (e.g., Qwen2.5-Coder-7B) using LoRA (Low-Rank Adaptation).
• Data Construction: The training dataset comprises pairs of (supertype, subtype) derived from MPST literature and synthetic benchmarks. Subtypes are generated via heuristic procedures based on asynchronous subtyping algorithms and validated by a formal checker.
• Representation: Session types are converted into a model-friendly, BNF-style syntax (e.g., explicit p!m; T for sends, p?m; T for receives, and REC_X_OPEN/CLOSE for recursion) to reduce ambiguity.
• Prompting: Prompts include theoretical context describing transformation rules (Identity, RefA, RefB, RefIn, RefOut, Unfold) to guide the model toward structurally valid transformations.
• Loss Function: A weighted token-level loss is used, prioritizing the generation of valid subtype sequences over auxiliary labels.

2.2 Syntropy-Gen: Constrained Generation with Two-Level Monitoring

To ensure semantic correctness beyond what the LLM can guarantee by construction, Syntropy-Gen employs a two-level monitoring strategy during the beam search generation process:

• Level 1: Token-Level Derivative Check (Prefix Filtering):
  • At every decoding step, the current prefix is parsed into a partial session tree.
  • A lightweight, coinductive derivative check verifies if the prefix can still be extended to a valid subtype of the supertype.
  • If the check fails (i.e., no valid completion exists), the beam is pruned immediately. This acts as a coarse over-approximation to eliminate infeasible paths early.
• Level 2: Widening-Based Fixpoint Checker (Final Verification):
  • When a candidate sequence reaches the End-of-Sequence (EOS) token, it is parsed into a complete session tree.
  • A full subtype checker (based on derivative reasoning and widening operators to handle recursion) verifies if the complete tree is a valid subtype of the supertype.
  • This step is conservative; it accepts valid subtypes but may reject some valid ones due to the undecidability of the general problem.

This two-level design balances computational efficiency (Level 1) with semantic rigor (Level 2), ensuring that only candidates satisfying the asynchronous subtyping relation are retained.

3. Key Contributions

1. LLM Generation with Behavioural Guarantees: A novel approach enabling LLMs to synthesise MPST protocol refinements with guaranteed deadlock freedom and communication safety.
2. Specification-Guided Protocol Refinement: A systematic encoding of MPST specifications that guides and constrains LLM generation, moving beyond local syntactic correctness to global behavioural properties.
3. Constraint-Integrated Generation: A two-level generation workflow that integrates constraint validation directly into the synthesis process via prefix filtering and subsequent verification.
4. Syntropy Framework and Evaluation: Implementation and comprehensive evaluation demonstrating high validity and the ability to generate diverse, non-trivial refinements.

4. Experimental Results

The framework was evaluated on two datasets (literature-derived and synthetic) using multiple LLMs (7B to 32B parameters).

• Validity: Syntropy achieves 95.6%–99.5% semantic validity across all models when using Two-Level Monitoring, compared to significantly lower rates (e.g., 60.4%) for direct generation without monitoring. Syntactic validity remains high (95.4%–98.1%).
• Diversity: The framework produces structurally distinct refinements, including reordering (RefA, RefB) and variance (RefIn, RefOut) transformations, rather than trivial variations.
• Data Scale: Performance saturates around 9,500 training pairs; increasing data beyond this yields marginal gains.
• Ablation Studies:
  • Removing Two-Level Monitoring causes a drastic drop in semantic validity (to ~60%), confirming its necessity for correctness.
  • Removing Prompting reduces structural diversity and slightly lowers semantic validity, indicating its role in guiding transformation coverage.
• Comparison with Frontier Models: While frontier models (e.g., GPT-5.5, DeepSeek-V4-Pro) can generate valid subtypes with high validity on the few cases they cover, their coverage is extremely limited (4%–18% of benchmarks). In contrast, Syntropy provides full coverage across the benchmark suite.

5. Significance and Claims

The paper claims that Syntropy successfully addresses the gap between the generative capabilities of LLMs and the rigorous requirements of distributed system correctness. By integrating formal specifications (MPST) directly into the generation loop, the framework ensures that the synthesized protocol refinements are deadlock-free and behaviourally compatible.

The authors emphasize that while frontier LLMs show promise, they currently lack the systematic coverage required for comprehensive protocol refinement. Syntropy demonstrates that fine-tuned models, when coupled with formal verification constraints, can reliably produce diverse and correct protocol variants that are difficult to construct manually. The work positions itself as a step toward applying LLMs to safety-critical software engineering tasks where behavioural guarantees are non-negotiable.

Limitations Acknowledged:

• The semantic validity metric relies on a checker that is sound but incomplete (due to the undecidability of AMS); thus, rejected candidates are not definitively proven incorrect.
• The evaluation is currently focused on subtype generation within MPST, and generalization to other formalisms or generation tasks remains future work.