[2604.17612] Provable Coordination for LLM Agents via Message Sequence Charts

Computer Science > Programming Languages arXiv:2604.17612 (cs) [Submitted on 19 Apr 2026 (v1), last revised 29 Apr 2026 (this version, v2)] Title:Provable Coordination for LLM Agents via Message Sequence Charts Authors:Benedikt Bollig, Matthias Függer, Thomas Nowak View a PDF of the paper titled Provable Coordination for LLM Agents via Message Sequence Charts, by Benedikt Bollig and 2 other authors View PDF HTML (experimental) 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. Comments: Subjects: Programming Languages (cs.PL); Artificial Inte...