Provable Coordination for LLM Agents via Message Sequence Charts

TL;DR

This paper presents a domain-specific language and framework for designing and verifying coordination protocols for LLM-based multi-agent systems, ensuring deadlock-free interactions despite LLM nondeterminism.

Contribution

It introduces a message sequence chart-based language and a syntax-directed projection method to generate deadlock-free agent programs from global specifications.

Findings

Successfully applied to a diagnosis consensus protocol

Establishes coordination properties independently of LLM nondeterminism

Provides an open-source implementation called ZipperGen

Abstract

Multi-agent systems built on large language models (LLMs) are difficult to reason about. Coordination errors such as deadlocks or type-mismatched messages are often hard to detect through testing. We introduce a domain-specific language for specifying agent coordination based on message sequence charts (MSCs). The language separates message-passing structure from LLM actions, whose outputs remain unpredictable. We define the syntax and semantics of the language and present a syntax-directed projection that generates deadlock-free local agent programs from global coordination specifications. We illustrate the approach with a diagnosis consensus protocol and show how coordination properties can be established independently of LLM nondeterminism. We also describe a runtime planning extension in which an LLM dynamically generates a coordination workflow for which the same structural guarantees apply. An open-source Python implementation of our framework is available as ZipperGen.