Research

TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples

May 2026

Shuren Xia, Qiwei Li, Taqiya Ehsan, and Jorge Ortiz

ACM CAIS 2026 Best Paper Award (Outstanding Solution Paper) · arXiv · Code · Project Page

Independent LLM agents that share resources and communicate asynchronously inherit the coordination hazards of distributed systems. Races, deadlocks, missed handshakes, and premature termination emerge from interleavings that designers rarely enumerate. TraceFix is a verification-first pipeline that uses TLA+ counterexamples to debug and repair LLM multi-agent coordination protocols before deployment.

TraceFix pipeline: IR synthesis, PlusCal generation, TLC verification, counterexample repair, prompt compilation, runtime monitoring — TraceFix pipeline. An orchestration agent synthesizes a protocol topology IR, generates PlusCal coordination logic, and iteratively repairs it using TLC counterexamples. Verified process bodies are compiled into per-agent prompts and executed under a topology monitor.

Coordination hazards

Centralized workflow engines (LangGraph, ADK) avoid coordination hazards by construction but limit agent autonomy. When agents run independently, correctness depends on interleavings that designers rarely enumerate. A protocol can succeed in every observed run and stall under an untested schedule.

Adding locks reshapes failures rather than removing them. Underspecified lock discipline trades races for deadlocks. Message passing introduces symmetric hazards when agents wait on messages that will never be sent. These bugs are latent. They depend on rare schedules and appear only at scale.

Design

Generating a correct concurrent protocol is hard. Checking one is mechanical. TLC exhaustively explores all interleavings and nondeterministic choices within bounded assumptions. When it finds a violation, it returns a concrete, minimal counterexample trace. TraceFix treats the initial protocol as a hypothesis to be attacked. The pipeline generates a candidate, uses TLC to find edge cases, repairs from the counterexample, and repeats until the checker finds no violation.

The pipeline has four design-time stages and two runtime stages.

Topology synthesis. An orchestration agent produces a protocol topology IR that declares agents, shared resources (locks, counters), and directed labeled FIFO channels. The topology is validated structurally before any model checking.
PlusCal generation. Per-agent process bodies are written as PlusCal coordination code with explicit control flow over sends, receives, and resource acquisition. Nondeterministic either/or branches make decision points visible to the checker.
TLC verification. PlusCal compiles to TLA+. TLC checks deadlock freedom, mutual exclusion, orphan locks, and channel drainage under bounded queue depths.
Counterexample repair. When TLC finds a violation, the counterexample trace is fed to the repair agent, which edits PlusCal processes to eliminate the failure. The loop repeats until verification passes.
Prompt compilation. Verified process bodies are embedded verbatim into per-agent system prompts.
Runtime monitoring. A topology monitor validates that each coordination operation targets a declared channel or resource with a valid label. Out-of-topology operations are rejected.

Concrete repairs

Counterexample repair often fixes two coordination bugs that usually pass manual testing. Circular lock dependencies and agents that exit before the workflow is finished. The snippets below are simplified from repaired protocols in the benchmark.

Circular lock dependency. A developer and a CI runner each hold a different lock and wait on the other. TLC produces the circular-wait counterexample. The repair removes cross-lock acquisition.

(* failed, circular wait *)
DEVELOPER_A:
  acquire_lock(REPO); ... acquire_lock(BUILD_SERVER);
CI_RUNNER:
  acquire_lock(BUILD_SERVER); ... acquire_lock(REPO);

(* repaired, disjoint lock ownership *)
DEVELOPER_A:
  acquire_lock(REPO); ... release_lock(REPO);
CI_RUNNER:
  acquire_lock(BUILD_SERVER); ... release_lock(BUILD_SERVER);

Premature reviewer termination. The reviewer exits after a fixed count, but developers re-enter review after CI setbacks. The repair replaces counting with per-developer completion flags.

(* failed, exits after 3 approvals *)
while (rvCount < 3) {
  receive(review_request);
  send(approved or revise);
};
goto Done;

(* repaired, waits for all devs to signal done *)
receive_any(ch_a_review, ch_b_review, ch_c_review);
if (msg = "review_done") { mark_done(agent); }
if (a_done /\ b_done /\ c_done) {
  goto Done;
} else {
  goto rev_loop;
};

Protocol topology IR

Most multi-agent frameworks encode coordination implicitly in prompts or workflow graphs. TraceFix makes the coordination contract explicit. The protocol topology IR states which agents exist, which shared resources they may acquire, and which labeled messages may flow on which channels. Behavioral logic comes later, in PlusCal.

Structural validation. The topology is checked against a JSON schema and semantic invariants (valid endpoints, explicit labels) before TLC explores interleavings.

Repair scope. When TLC fails, repairs edit PlusCal process bodies. The topology defines the coordination interface that repairs must preserve.

Runtime contract. After verification, the same topology configures the monitor. Coordination calls outside the declared channels, resources, or labels are rejected at execution time.

Fragment from Task 14H (Drug Discovery Pipeline, 7 agents, 4 locks, 1 counter, 12 channels).

{
  "agents": [
    {"id": "BIOLOGIST"}, {"id": "CHEMIST"},
    {"id": "CLINICAL_LEAD"}, {"id": "FORMULATION_SCIENTIST"},
    {"id": "PROJECT_DIRECTOR"}, {"id": "REGULATORY_SPECIALIST"},
    {"id": "TOXICOLOGIST"}
  ],
  "resources": [
    {"id": "HPLC", "type": "Lock"},
    {"id": "MASS_SPEC", "type": "Lock"},
    {"id": "CELL_LAB", "type": "Lock"},
    {"id": "BIOLOGICAL_SAMPLES", "type": "Counter",
     "config": {"initial": 8}}
  ],
  "channels": [
    {"id": "ch_chem_to_form", "from": "CHEMIST",
     "to": "FORMULATION_SCIENTIST",
     "labels": ["compound", "retry_compound"]},
    {"id": "ch_reg_to_director", "from": "REGULATORY_SPECIALIST",
     "to": "PROJECT_DIRECTOR",
     "labels": ["approval", "conditional_approval"]},
    ...
  ]
}

Results

The benchmark contains 48 tasks drawn from 16 scenario families (shared codebase development, dining philosophers, semiconductor fabrication, CI/CD pipelines, drug discovery, and others) at Easy, Medium, and Hard tiers. Protocol design uses Claude Opus 4.6. Runtime evaluation uses gpt-5-mini and gpt-5-nano across four architectures, three fault-injection levels, and three repetitions per configuration (3,456 runs total).

48/48

TLC verified

62.5%

First-attempt pass

89.4%

Mean checkpoint completion

<60s

All verifications

Verification convergence. 30 of 48 tasks pass on the first attempt (62.5%). The remaining 18 converge after 1–4 repair iterations. Deadlocks dominate (20 of 29 repair attempts, 69%). Every lock-only task passes first-attempt. Channel semantics are the primary source of verification complexity. Easy tasks pass first-attempt in 14/16 cases (87.5%), Hard in 4/16 (25%).

Cumulative TLC verification pass rate by repair iteration — Cumulative TLC pass rate by repair iteration, stratified by difficulty. No task requires more than four iterations.

State-space tractability. Distinct states range from 30 (Task 16E, 3-agent CI/CD) to 7.7M (Task 3H, 7-agent survey with 17 channels). TLC completes in under 60 seconds for every task (median <1s). Verification time does not track state-space size. The decoupling is characteristic of BFS model checking with efficient state hashing.

TLC distinct states and verification time vs topology size — TLC distinct states (circles, log scale) and verification time (triangles, linear) vs. topology size. Six-order-of-magnitude range in states. Verification stays flat.

Runtime comparison

Each benchmark task has a simulation harness with task-specific objectives (checkpoints). Examples include a successful build, a completed review, or a drained coordination channel. We report two completion measures on 3,456 runs (48 tasks, four architectures, two models, three fault levels, three repetitions).

Mean checkpoint completion. Average share of objectives satisfied in a run. Partial progress counts. The paper labels this Avg Sim %.

All objectives met. Share of runs where every checkpoint is satisfied (Sim 100% in the paper). Deadlock or livelock rate. Share of runs that end stuck in coordination failure (DL/LL in the paper).

Four runtime architectures span full enforcement to no coordination infrastructure. Results below use gpt-5-mini (432 runs per condition).

Topology-monitored. Verified protocol with a topology-aware monitor that rejects out-of-topology operations. 89.4% mean checkpoint completion, 81.5% all objectives met, 8.8% deadlock or livelock.
Prompt-only. Same protocol-derived prompts, no topology monitoring. 86.2% mean, 69.7% all objectives met, 21.1% deadlock or livelock. The 12-point drop on all objectives met shows that prompts alone do not prevent failures under rare interleavings.
Mediator-enforced. The mediator manages all lock and channel operations and structurally prevents violations. 78.4% mean, 44.7% all objectives met, 4.5% deadlock or livelock, but stalls on domain-tool failures.
Chat-only. Shared chat, no coordination tools. 75.0% mean, 29.3% all objectives met. 61% of tool calls hit resource conflicts.

Mean checkpoint completion and all objectives met by runtime architecture — Mean checkpoint completion and all objectives met across four runtime architectures (gpt-5-mini, 432 runs per condition).

Model degradation. Switching from gpt-5-mini to gpt-5-nano, runtimes using the verified protocol lose about 15 points of mean checkpoint completion. Prompt-only and chat-only lose about 30 to 36 points. The verified protocol absorbs roughly half the performance loss from a weaker model.

Fault injection. All runtimes degrade from S0 (no injected faults) through S2 (two injected faults), but rankings stay stable. Topology-monitored drops from 94.8% to 84.5% mean checkpoint completion on gpt-5-mini. The verified protocol's explicit branch structure supports retries and fallback paths.

Mean checkpoint completion for Topology-monitored across difficulty and fault injection — Mean checkpoint completion for Topology-monitored (gpt-5-mini) by difficulty and fault-injection level. Easy with no faults reaches 97.1%. Hard with two faults reaches 75.0%.

Ablation. Holding the runtime fixed (Topology-monitored) and varying only protocol quality, verified protocols cut deadlock or livelock from 31.1% to 14.1% and raise mean checkpoint completion from 72.6% to 82.1%. The difference is smallest without faults and largest under S1 and S2.

Scope and limitations

What is verified. Deadlock freedom (TLC's NoDeadlock), mutual exclusion over locks, no orphan locks at termination, and channel drainage. TLC explores exhaustively within bounded queues (default B_c = 3). Liveness properties are not checked because LLM agents routinely contain nondeterministic loops that are valid business logic.

What is not enforced at runtime. The topology monitor rejects out-of-topology operations and enforces mutual exclusion. It does not enforce step order, lock order, handshake discipline, or receive patterns. Agents can reintroduce deadlock through step-order deviations that topology checks cannot catch. The residual 8.8% deadlock or livelock rate in Topology-monitored runs comes from this limitation. Closing it with lightweight per-agent program counters is the most immediate open direction.

Semantic drift. Timeout-driven repair can simplify branching to fit the checker budget, weakening fidelity to the original task intent. The paired ablation confirms this concentrates in timeout-labeled tasks.

Model coverage. The pipeline uses Claude Opus 4.6 for protocol design. Generalization to other design-time models is not evaluated.