Provable Coordination for LLM Agents via Message Sequence Charts

Benedikt Bollig, Matthias Függer, Thomas Nowak

cs.PL Apr 19, 2026 · v3 cs.AI

verification formalization ai-agents logic

Read PDF arXiv abstract Code

TL;DR

All definitions of the MSC-based coordination DSL and the projection's correctness and deadlock-freedom results are formalized and machine-checked in Lean 4.

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 calls, tool calls, and human control points, whose outcomes 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.

Problem

LLM-based multi-agent systems are prone to coordination errors such as deadlocks and type-mismatched messages, which testing rarely uncovers. Existing agent frameworks provide no formal coordination guarantees.

Approach

The authors define a domain-specific language based on message sequence charts. It separates message-passing structure from opaque LLM, tool, and human actions, and gives the language a formal syntax and MSC semantics. A syntax-directed projection turns global workflows into local agent programs, using explicit control broadcasts from the owner of each decision. All definitions and correctness results are machine-checked in Lean 4, and the framework is implemented in Python as ZipperGen, including a runtime planning extension where an LLM generates the workflows.

Results

The projection is always defined, needs no realizability check, and is deadlock-free by construction. This is illustrated on a medical diagnosis consensus protocol. In the runtime-planning experiment, GPT-4.1 and GPT-4.1 mini had all 10 generated workflows accepted and executed, while small local models and GPT-4o mini produced none that were accepted.

Model	Accepted first	Accepted within 8	Executed	Correct
qwen2.5:14b (local)	0	0	0	0
GPT-4o mini	0	0	0	0
GPT-4.1 mini	0	10	10	9
GPT-4o	7	8	8	7
GPT-4.1	10	10	10	6

Runtime planning: LLM-generated workflows (10 cases each)

Papers With

Provable Coordination for LLM Agents via Message Sequence Charts