[2605.07935] TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples

Computer Science > Artificial Intelligence arXiv:2605.07935 (cs) [Submitted on 8 May 2026] Title:TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples Authors:Shuren Xia, Qiwei Li, Taqiya Ehsan, Jorge Ortiz View a PDF of the paper titled TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples, by Shuren Xia and 3 other authors View PDF HTML (experimental) Abstract: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 reduc...