用 TLA+ 验证 LLM Agent 协调协议：从 Prompt 工程到形式化规约

当前 LLM Agent 系统的构建仍停留在 "启发式 Prompt 工程" 阶段 —— 开发者通过反复试错调整指令，直到输出看起来正确。然而，多 Agent 并发场景下的协调失败（死锁、竞态条件、消息丢失）往往只在特定执行交错中暴露，传统测试难以覆盖。2025-2026 年的两项工作（FASTRIC 和 TraceFix）展示了如何将 Prompt 工程转化为可验证的形式化规约，用 TLA+ 模型检测为 Agent 协调协议提供数学级保证。

核心思路：Prompt 即状态机规约

FASTRIC（Prompt Specification Language）的核心洞察是：任何多轮交互协议都隐含一个有限状态机（FSM）。通过显式声明状态、触发器、角色和约束，Prompt 本身成为可执行的行为规约。TraceFix 则更进一步，将 Agent 协调协议编译为 PlusCal（TLA+ 的算法描述语言），利用 TLC 模型检测器进行穷举验证。

这种范式的转变在于：LLM 不再是黑盒的 "智能体"，而是被约束在形式化规约内的 "解释执行器"。规约定义了允许的状态转移，LLM 负责在约束下生成自然语言响应。

TraceFix：生成 - 检测 - 修复闭环

TraceFix 针对多 Agent 协调场景，设计了完整的验证 - 运行时闭环：

协议拓扑 IR：从自然语言任务描述合成协议中间表示，定义 Agent、共享资源（锁 / 计数器）、有向消息通道及其标签词汇。拓扑在编译前通过 JSON Schema 结构验证和语义检查，过滤畸形输入。

PlusCal 协调逻辑：每个 Agent 实现为 PlusCal 公平进程，显式控制发送、接收、获取锁、释放锁等操作。either/or 结构使 LLM 决策点可被模型检测器穷举验证 —— 即使某个分支在实际运行中极少触发，TLC 也会验证其在所有调度交错下的安全性。

反例驱动修复：当 TLC 发现违规时，返回具体的反例轨迹（最小失败执行序列）。修复 Agent 据此修改 PlusCal 源码 —— 典型修复包括强制锁顺序、补全握手信号、重构循环以消除循环等待。在 48 个任务的基准测试中，62.5% 的任务首次尝试即通过验证，其余在最多 4 轮修复后全部通过。

运行时监控：验证后的协议拓扑部署为运行时监控器，拒绝超出拓扑的协调操作（向未声明通道发送、获取未声明资源等）。这保留了 Agent 的领域工具自主权，同时硬化了最易出错的协调原语。

实验数据显示，相比无协调的 "纯聊天" 基线（29.3% 完整完成率），拓扑监控执行达到 89.4% 平均完成率和 81.5% 完整完成率；死锁 / 活锁率从 31.1% 降至 14.1%。

FASTRIC：形式化级别与模型适配

FASTRIC 提出了 "规约形式化级别" 作为设计参数，解决不同模型对指令细节的不同需求：

• L1（隐式）：高层描述如 "根据难度提问"
• L2（结构化）：规定输出格式和基本循环
• L3（显式）：分离状态块，使用跳转 / 停留指令
• L4（算法级）：编号步骤、等待语句、强制约束

关键发现是：最优形式化级别因模型而异。DeepSeek-V3.2（685B）在 L2-L4 达到完美一致性（1.00）；ChatGPT-5（1T+）在 L3 达到峰值（0.90）后在 L4 崩溃至 0.39—— 过度约束反而损害性能；Phi4（14.7B）则无明显最优解。这揭示了 "金发姑娘区"（Goldilocks Zone）的存在：规约需提供足够结构而不致过度约束。

实践落地：可操作的实施路径

对于希望引入形式化验证的团队，建议按以下阶段推进：

阶段一：单 Agent 状态机规约

• 定义状态集合（等待输入、处理中、工具调用、终止）
• 声明不变量（禁止未授权工具调用、禁止重复副作用）
• 使用 FASTRIC L2-L3 级别编写 Prompt
• 通过执行轨迹分析测量 "过程一致性"

阶段二：多 Agent 协调验证

• 识别共享资源和消息通道
• 编写 PlusCal 进程描述协调逻辑
• 运行 TLC 检测死锁和互斥违规
• 迭代修复直至通过 NoDeadlock 检查

阶段三：运行时监控部署

• 将验证后的拓扑编译为系统 Prompt
• 部署拓扑监控器拦截越界操作
• 保留 Agent 领域决策的灵活性

关键设计参数包括：

• 通道深度边界（Bc）：默认 3，可根据协议复杂度调整
• 锁顺序策略：字母序或拓扑序，避免循环依赖
• 重试语义：在模型中简化重试逻辑以保持可验证性，在运行时保留完整重试

局限与边界

TLA+ 验证适用于协调正确性（死锁自由、互斥、通道排空），不验证任务语义正确性（输出质量、业务逻辑）。此外，TLC 在有限边界内穷举搜索，超出边界的不完整性需通过运行时监控弥补。当前运行时监控仅强制拓扑合规，不强制步骤顺序 —— 后者仍依赖 Prompt 约束，存在残余风险。

对于无共享状态、静态依赖明确的场景（如 DAG 工作流），LangGraph 等编排框架更为合适；TLA+ 验证的价值主要体现在并发 Agent、共享可变资源、双向握手无法扁平化的场景。

总结

将 Prompt 工程转化为形式化规约，标志着多 Agent 系统设计从 "艺术" 向 "工程" 的跨越。TraceFix 的生成 - 检测 - 修复闭环和 FASTRIC 的形式化级别框架提供了可落地的路径：先用 TLA+ 验证协调协议消除死锁和竞态，再用运行时监控确保执行不偏离验证过的拓扑。对于安全关键场景（医疗协调、金融交易、工业控制），这种 "验证优先" 的方法论将成为多 Agent 系统的工程基准。

参考来源

• TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples (arXiv:2605.07935v1, 2026)
• FASTRIC: Prompt Specification Language for Verifiable LLM Interactions (arXiv:2512.18940v1, 2025)

ai-systems