TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples

TL;DR

TraceFix is a verification pipeline that synthesizes, repairs, and verifies multi-agent coordination protocols for LLMs using TLA+ counterexamples, ensuring high success rates and robustness.

Contribution

It introduces a method to automatically repair multi-agent protocols with TLA+ counterexamples, achieving verified, efficient coordination in diverse tasks.

Findings

All tasks verified within 60 seconds despite large state spaces.

62.5% of tasks pass verification on the first attempt.

Verified protocols significantly reduce deadlock and livelock occurrences.

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 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.