Technical Summary: TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples

1. Problem Statement

Independent Large Language Model (LLM) agents increasingly operate in concurrent, asynchronous environments where they mutate shared external state. In such settings, system failures often stem not from individual agent capability deficits, but from coordination errors arising from complex interleavings, races, deadlocks, and missed handshakes. These hazards are latent; a protocol may succeed in observed runs yet fail under untested schedules.

Prior approaches address LLM coordination through orchestration frameworks (explicit graphs), solver-in-the-loop generation for single-artifact correctness, or runtime guards. However, these often fail to target concurrent protocol correctness specifically. Writing correct concurrent protocols is difficult because edge cases emerge only under specific, unenumerated interleavings. A one-shot specification, whether human or LLM-generated, tends to be plausible but underspecified, lacking a mechanism to systematically discover these edge cases.

2. Methodology: The TraceFix Pipeline

TraceFix introduces a verification-first pipeline that treats protocol design as an iterative loop of synthesis, model checking, and repair. The system operates in two phases: design-time synthesis and runtime enforcement.

2.1 Design-Time Loop

The pipeline consists of four stages driven by an orchestration agent:

1. Topology Synthesis: The agent synthesizes a Protocol Topology Intermediate Representation (IR) from a natural-language task description. This IR declaratively defines agents, shared resources (locks, counters), and directed labeled message channels (FIFO queues). It is structurally validated via JSON schema before proceeding.
2. Logic Generation: The topology is compiled into PlusCal (an algorithmic notation for TLA+). The agent generates per-agent process bodies containing explicit control flow (sends, receives, lock acquisitions) and nondeterministic choices (either/or).
3. Model Checking: The PlusCal code is translated to TLA+ and verified using the TLC model checker. TLC exhaustively explores all reachable states under bounded assumptions (e.g., bounded queue depths) to check safety properties:
   • Deadlock Freedom: No state where no agent can proceed.
   • Mutual Exclusion: No two agents hold the same lock.
   • Orphan Locks: No locks held upon termination.
   • Channel Drainage: All channels are empty when agents terminate.
4. Counterexample-Driven Repair: If TLC finds a violation, it returns a concrete counterexample trace. A repair agent uses this trace to edit the PlusCal source code (e.g., enforcing lock order, adding handshakes, restructuring loops) to eliminate the specific failure witness. The loop repeats until TLC finds no violations.

2.2 Runtime Enforcement

Once a protocol passes verification, the verified process bodies are compiled into system prompts for the agents. A topology monitor runs alongside the agents at runtime. This monitor enforces the coordination interface defined in the topology:

• It validates that every coordination operation (send, receive, acquire, release) targets a declared channel or resource with a valid label.
• It rejects any operation that violates the topology (out-of-topology operations).
• It does not enforce step-ordering or fairness; it only ensures agents stay within the verified structural contract. Agents retain autonomy over domain tools and decision-making within these constraints.

3. Key Contributions

1. TraceFix System: A protocol-design agent that synthesizes a topology IR, generates PlusCal coordination logic, and iteratively repairs protocols using TLC counterexamples until verification succeeds.
2. Coordination Benchmark: A new benchmark of 48 tasks across 16 scenario families (spanning software development, research, manufacturing, and CI/CD) at three difficulty tiers. Ground truth is defined by coordination correctness (deadlock freedom, mutual exclusion) rather than domain semantics.
3. Runtime Topology Enforcement: A monitoring layer that preserves agent autonomy while rejecting coordination operations that deviate from the verified protocol topology.
4. Paired Ablation Study: An experimental isolation of the contribution of counterexample-driven repair by comparing verified vs. unverified protocol variants under identical runtime conditions.

4. Empirical Results

The evaluation was conducted on the 48-task benchmark using Claude Opus 4.6 for protocol design and gpt-5-mini/gpt-5-nano for runtime execution (3,456 total runs).

4.1 Verification Convergence

• 100% Final Pass Rate: All 48 tasks reached full TLC verification.
• Efficiency: 62.5% of tasks passed on the first attempt. No task required more than four repair iterations.
• Scalability: State spaces spanned six orders of magnitude (from 30 to 7.7 million distinct states). Despite this, verification completed in under 60 seconds for every task (median <1s).
• Failure Taxonomy: Of the 29 repair attempts required, 69% were deadlocks. The dominant failure patterns were structural coordination hazards (e.g., nondeterministic receives before channel checks, hub agents terminating before satellite agents completed retry loops) rather than fundamental design flaws. Lock-only tasks passed 100% on the first attempt, indicating that channel semantics are the primary source of complexity.

4.2 Runtime Performance

A comparison of four runtime architectures (Topology-monitored, Mediator-enforced, Prompt-only, Chat-only) revealed:

• Highest Completion: Topology-monitored execution achieved the highest task completion (89.4% average, 81.5% full completion).
• Safety: It reduced Deadlock/Livelock (DL/LL) rates significantly compared to baselines.
• Model Degradation: When model capability was reduced (gpt-5-mini to gpt-5-nano), runtimes using the verified protocol degraded at roughly half the rate of prompt-only or chat-only baselines. The verified protocol acts as a "capability buffer."
• Fault Tolerance: Under injected faults, the verified protocol maintained high completion rates, whereas baselines suffered severe performance drops.

4.3 Ablation Study

Under a fixed Topology-monitored runtime, comparing verified vs. unverified protocols showed that counterexample-driven repair reduced DL/LL rates from 31.1% to 14.1%. The improvement was most pronounced under fault injection, confirming that the repair process removes concrete coordination hazards that amplify under adverse conditions.

5. Significance and Claims

The paper claims that TraceFix demonstrates the viability of a generate/check/repair paradigm for LLM multi-agent coordination.

• Necessity of Repair: The loop is necessary, as over one-third of initial attempts fail, but sufficient, as all converge within a small iteration budget.
• Tractability: Bounded model checking remains tractable even for large state spaces, decoupling verification time from state-space magnitude.
• Runtime Benefit: Verified protocols provide measurable, tangible improvements in task completion and robustness against model degradation and faults.
• Scope Limitation: The system verifies coordination safety (deadlock, mutual exclusion) under bounded assumptions. It does not verify task semantics, output quality, or liveness properties (e.g., guaranteed termination), as LLM protocols often contain valid nondeterministic loops that would be rejected by strict liveness checks.

The work positions itself as a concrete instantiation of integrating formal methods with LLM systems, specifically targeting the "specification and orchestration gaps" identified as dominant failure modes in multi-agent systems. It complements existing optimization frameworks (like DSPy) by verifying how agents coordinate rather than what they produce.