TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples
For developers of LLM-based multi-agent systems, TraceFix provides a verification-first approach that significantly improves coordination reliability and reduces coordination failures.
TraceFix uses TLA+ model checking to verify and repair LLM multi-agent coordination protocols, achieving 100% verification across 48 tasks with 62.5% passing on first attempt, and reducing deadlock/livelock from 31.1% to 14.1% in runtime execution.
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.