TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples

Demo

Abstract

Multi-agent LLM systems that share resources and communicate asynchronously are susceptible to coordination failures (races, deadlocks, protocol violations) that prompt engineering alone cannot prevent. We present TraceFix, a framework that automatically synthesizes, verifies, and repairs coordination protocols for multi-agent systems. TraceFix introduces an intermediate representation for protocol topology, generates PlusCal coordination logic, and applies the TLC model checker to exhaustively verify safety properties. When verification fails, TLC counterexamples drive targeted repairs. Verified protocols are compiled into per-agent prompts and enforced at runtime by a topology-conformance monitor. Evaluated on 48 benchmark tasks spanning 16 scenario families, TraceFix achieves 100% TLC verification (62.5% first-attempt), 89.4% average runtime completion, and a 2× degradation buffer when substituting weaker models. Topology-monitored execution matches or exceeds mediator-enforced, prompt-only, and chat-only baselines across all metrics.

Pipeline Overview

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 processes are compiled into per-agent prompts and executed under a topology monitor.

Key Results

48/48

TLC verified

62.5%

First-attempt

89.4%

Mean checkpoint completion

2×

Degradation buffer

Cumulative TLC pass rate: 62.5% first-attempt, 100% by iteration 4.

Runtime architecture comparison — Runtime comparison: topology-monitored outperforms all baselines.

Protocol topology IR

TraceFix separates who may coordinate from how they coordinate. An orchestration agent first emits a protocol topology IR with agents, shared locks and counters, and directed channels with explicit message labels. That structure is validated before any PlusCal or TLC work runs. Behavioral logic (send, receive, acquire, retry loops) is written in PlusCal on top of the topology, then checked by TLC.

The same topology later configures the runtime monitor. Each coordination call must use a declared channel, resource, and label. Operations outside the verified topology are rejected. Design-time verification and runtime enforcement therefore share one artifact instead of drifting apart.

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"]},
    ...
  ]
}

BibTeX

@misc{xia2026tracefixrepairingagentcoordination,
  title         = {TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples},
  author        = {Shuren Xia and Qiwei Li and Taqiya Ehsan and Jorge Ortiz},
  year          = {2026},
  eprint        = {2605.07935},
  archivePrefix = {arXiv},
  primaryClass  = {cs.AI},
  url           = {https://arxiv.org/abs/2605.07935},
}