Provable Coordination for LLM Agents via Message Sequence Charts
For developers of multi-agent LLM systems, this work provides a method to formally guarantee coordination properties like deadlock freedom, addressing a key challenge in building reliable agent teams.
The paper introduces a domain-specific language based on message sequence charts to specify and verify coordination in multi-agent LLM systems, ensuring deadlock-free execution. The approach separates message-passing structure from LLM actions, enabling formal guarantees independent of LLM nondeterminism.
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.