TraceFix: TLA+ Verification for LLM Multi-Agent Coordination

Researchers have introduced TraceFix, a verification-centric pipeline designed for the coordination of multi-agent Large Language Models (LLMs). An agent begins by creating a structured intermediate representation (IR) from a task description, which leads to the generation of PlusCal coordination logic. The protocol is then refined iteratively using counterexamples from the TLA+ model checker (TLC) until it is verified. Verified process bodies are transformed into system prompts for each agent and are monitored at runtime to prevent any out-of-topology coordination actions. Across 48 tasks covering 16 scenario families, all tasks achieve complete TLC verification; 62.5% succeed on the first attempt, with no more than four repair iterations needed. Despite state spaces varying by six orders of magnitude, verification is completed in under 60 seconds for each task. A runtime comparison involving 3,456 runs indicates that topology-monitored execution yields the highest task completion rates, averaging 89.4% with 81.5% achieving full completion.