# TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples

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

## Key facts

- No citing papers in the map yet (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 18 of its 40 references that are in the map.
- First posted on arXiv 8 May 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, 18 of 18)

- [Constitutional AI: Harmlessness from AI Feedback](https://mlsanity.com/paper/2212.08073/) (2022)
- [AutoGen: Enabling Next-Gen LLM Applications via Multi-Agent Conversation](https://mlsanity.com/paper/2308.08155/) (2023)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Why Do Multi-Agent LLM Systems Fail?](https://mlsanity.com/paper/2503.13657/) (2025)
- [NeMo Guardrails: A Toolkit for Controllable and Safe LLM Applications with Programmable Rails](https://mlsanity.com/paper/2310.10501/) (2023)
- [TaskMatrix.AI: Completing Tasks by Connecting Foundation Models with Millions of APIs](https://mlsanity.com/paper/2303.16434/) (2023)
- [ShieldAgent: Shielding Agents via Verifiable Safety Policy Reasoning](https://mlsanity.com/paper/2503.22738/) (2025)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Optimizing Model Selection for Compound AI Systems](https://mlsanity.com/paper/2502.14815/) (2025)
- [RvLLM: LLM Runtime Verification with Domain Knowledge](https://mlsanity.com/paper/2505.18585/) (2025)
- [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025)
- [VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning](https://mlsanity.com/paper/2601.20055/) (2026)
- [Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification](https://mlsanity.com/paper/2510.03469/) (2025)
- [Online Synthesis for Runtime Enforcement of Safety in Multi-Agent Systems](https://mlsanity.com/paper/1910.10380/) (2019)
- [SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems](https://mlsanity.com/paper/2509.23130/) (2025)
- [Automatic Completion of Distributed Protocols with Symmetry](https://mlsanity.com/paper/1505.04409/) (2015)
- [Efficient Synthesis of Symbolic Distributed Protocols by Sketching](https://mlsanity.com/paper/2405.07807/) (2024)
- [ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair](https://mlsanity.com/paper/2602.12058/) (2026)

## Abstract (arXiv)

We present TraceFix, a verification-first pipeline for Large Language Model (LLM) multi-agent coordination. An agent synthesizes a protocol topology as a structured intermediate representation (IR) from a task description, generates PlusCal coordination logic, and iteratively repairs the protocol using counterexamples from the TLA+ model checker (TLC) until verification succeeds. Verified process bodies are compiled into per-agent system prompts and executed under a runtime monitor that rejects out-of-topology coordination operations. On 48 tasks spanning 16 scenario families, all tasks reach full TLC verification; 62.5% pass on the first attempt and none requires more than four repair iterations. State spaces span six orders of magnitude yet verification completes in under 60 s for every task. A 3,456-run runtime comparison shows that topology-monitored execution achieves the highest task completion (89.4% average, 81.5% full) and that runtimes using the verified protocol degrade at roughly half the rate of prompt-only and chat-only baselines when model capability is reduced. A paired ablation under a fixed runtime shows that TLC-verified protocols cut deadlock/livelock (DL/LL) from 31.1% to 14.1%, with the largest separation under fault injection.