# Provable Coordination for LLM Agents via Message Sequence Charts

arXiv: https://arxiv.org/abs/2604.17612 · HTML: https://mlsanity.com/paper/2604.17612/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in General LLM agent frameworks and benchmarks, one of 16 directions in LLM agents and tool use.
- Builds on 8 of its 42 references that are in the map.
- First posted on arXiv 19 Apr 2026.

## Placed in

- LLM agents and tool use / [General LLM agent frameworks and benchmarks](https://mlsanity.com/agents/general-llm-agent-frameworks-and-benchmarks/)

## Builds on (most cited first, 8 of 8)

- [A Trace-Based Assurance Framework for Agentic AI Orchestration: Contracts, Testing, and Governance](https://mlsanity.com/paper/2603.18096/) (2026)
- [HasChor: Functional Choreographic Programming for All (Functional Pearl)](https://mlsanity.com/paper/2303.00924/) (2023)
- [Pirouette: Higher-Order Typed Functional Choreographies](https://mlsanity.com/paper/2111.03484/) (2021)
- [Statically Verified Refinements for Multiparty Protocols](https://mlsanity.com/paper/2009.06541/) (2020)
- [Asynchronous Multiparty Session Type Implementability is Decidable -- Lessons Learned from Message Sequence Charts](https://mlsanity.com/paper/2302.11272/) (2023)
- [Complete Multiparty Session Type Projection with Automata](https://mlsanity.com/paper/2305.17079/) (2023)
- [Characterizing Implementability of Global Protocols with Infinite States and Data](https://mlsanity.com/paper/2411.05722/) (2024)
- [High-Level Message Sequence Charts: Satisfiability and Realizability Revisited](https://mlsanity.com/paper/2504.19814/) (2025)

## Built on by (most cited first, 1 of 1)

- [Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows](https://mlsanity.com/paper/2605.20923/) (2026)

## Abstract (arXiv)

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.