实验组：纯 Agent
生成方式：agent_automatic
目标长度：2500 字
目标深度：intermediate
TLA+ 在 Agent 系统中的应用：把不确定性关进逻辑的笼子
Agent 系统的核心问题是不可预测性。你无法通过测试覆盖所有状态，因为状态空间随 Agent 数量和交互模式指数增长。传统测试面对这种组合爆炸时，能提供的保证是概率性的——测过的路径是对的，没测的路径不知道。而 Agent 系统的故障恰恰发生在没测过的路径上。
形式化方法的价值在于把「不知道」变成「知道」。TLA+ 是其中最适合描述并发与分布式系统的一种规范语言。它的核心思想简单到令人怀疑：用数学描述系统状态和状态转移，然后用模型检查器穷举搜索所有可能的状态序列，验证不变量是否被违反。
但 TLA+ 在 Agent 系统中的应用，与它在数据库或网络协议中的应用有本质区别。数据库的状态是数据，网络协议的状态是消息序列，而 Agent 的状态是意图。意图不是简单的变量，它包含目标、信念、对环境的假设、以及与其他 Agent 的协作关系。这让 TLA+ 的应用方式产生了根本变化。
第一步是定义安全边界，而不是定义行为。
传统 TLA+ 规范关注系统应该做什么——协议的正确性、数据的一致性。Agent 系统恰恰相反，你无法预先定义 Agent 在复杂环境中应该采取的每一个动作，否则它就不是 Agent 而是状态机脚本。TLA+ 在 Agent 系统中的角色是定义禁止什么，而不是规定做什么。
安全边界的形式化表达通常是一组不变量。例如：「任何 Agent 持有的资源锁数量不超过一个」「Agent 之间的转账金额总和守恒」「任何 Agent 在未获得授权前不能访问外部工具」。这些不变量用 TLA+ 的谓词逻辑表达，然后模型检查器会穷举所有可达状态，验证这些谓词是否在所有状态下为真。
我在 MAREF 系统中用 TLA+ 验证过一个典型的 Agent 协作场景：多个 Agent 共享一个工具执行队列。直觉上的风险是死锁——Agent A 等待 B 释放资源，B 等待 C，C 等待 A。这种环形等待在传统分布式系统中已有成熟理论，但 Agent 系统引入了一个新变量：Agent 可能因为 LLM 推理结果而改变策略。一个 Agent 原本要释放资源，但收到新的指令后决定持有资源执行另一个任务。这种动态行为让死锁检测从「验证协议」变成了「验证协议在策略变化下的鲁棒性」。
TLA+ 的模型检查器在这种情况下暴露了一个我们在测试中完全没发现的死锁路径。触发条件需要三个 Agent 的特定时序：Agent A 在 T1 时刻获取资源，Agent B 在 T2 时刻发起协作请求，同时 Agent A 的 LLM 刚好在 T3 时刻收到策略更新。这个时序在测试环境中出现的概率极低，但 TLA+ 的穷举搜索在几分钟内就找到了反例。
第二个关键应用是验证 Agent 间的通信协议不会产生歧义状态。
Agent 之间的通信不是简单的消息传递。每个 Agent 对同一消息可能有不同的解读——这不是 bug，而是 LLM 推理的本质特性。TLA+ 无法验证 LLM 的语义理解，但可以验证通信协议的结构性属性：消息顺序是否可能导致状态不一致、确认机制在消息丢失时是否收敛、超时重试是否会引发级联效应。
具体来说，我在规范中定义了一个「承诺-确认」协议：Agent A 向 Agent B 发送协作请求，B 必须返回确认，A 在收到确认前不能释放已持有的资源。这个协议看似简单，但 TLA+ 验证发现了一个边界情况：如果 B 的确认消息在网络中延迟，而 A 的超时机制触发重试，B 会收到两条相同的请求。如果 B 对重复请求的处理不是幂等的，系统就会进入不一致状态。
这个问题的根源在于 Agent 的行为比传统分布式组件更复杂——B 收到重复请求后，可能因为上下文变化而给出不同的响应。TLA+ 的建模方式迫使你把这种不确定性显式化：你不能假设消息处理的确定性，必须把 Agent 的所有可能响应建模为状态转移的分支。这种建模方式本身就是一种治理手段——它强迫架构师面对不确定性，而不是在代码中用「应该不会发生」来回避。
第三个应用场景是治理策略的一致性验证。
Agent 系统不是孤立的。它运行在企业的权限体系、合规框架和操作流程之上。治理规则往往用自然语言描述，例如「任何 Agent 不得在未获得人类审批的情况下执行超过 10 万元的交易」。这类规则在代码中实现后，需要通过测试验证——但测试只能覆盖有限的场景。
TLA+ 的优势在于它能把治理规则转化为可验证的不变量。在 MAREF 中，我们把企业的治理规则库映射为 TLA+ 规范中的约束条件，然后对 Agent 的行为空间进行穷举验证。这让我们能回答一个关键问题：是否存在一条 Agent 可达的行为路径，它不违反任何单条治理规则，但违反了治理规则之间的隐含约束？
一个实际案例：规则 A 说「Agent 可以访问客户数据库」，规则 B 说「Agent 不得将客户数据传输到外部系统」。单独看这两条规则都没问题，但当 Agent 调用一个外部工具时，该工具的内部实现可能自动缓存数据——这构成了隐含的数据外传。TLA+ 的模型检查器能发现这类跨规则的隐含冲突，因为它在状态空间搜索中会遍历所有可能的工具调用序列。
但 TLA+ 不是银弹，它有明确的适用边界。
TLA+ 验证的是模型，不是实现。你的 TLA+ 规范是对系统的高度抽象——它假设 Agent 的状态转移遵循你定义的规则，但实际 Agent 的 LLM 推理可能产生规范之外的行动。规范与实际之间的差距，需要靠工程手段弥补：运行时监控、沙箱隔离、行为审计。
另一个边界是状态空间的爆炸。TLA+ 的模型检查器能处理的状态数量有上限。当 Agent 数量超过 10 个，或每个 Agent 的状态变量维度较高时，穷举搜索可能无法在合理时间内完成。应对策略是分层建模：先验证核心协议的安全性（小状态空间），再逐步增加 Agent 数量和状态维度。永远不要试图用 TLA+ 验证整个系统的所有行为，那是不可判定的。
架构师需要建立的判断力是：哪些部分值得用 TLA+ 验证，哪些部分不值得。
值得验证的部分有三个特征：并发交互密集、状态空间有限但路径复杂、故障代价高。不值得验证的部分是那些高度依赖外部环境或 LLM 语义理解的行为——这些行为的正确性无法用形式化方法保证，只能靠运行时监控和人工审计。
我的工程判断是：Agent 系统的架构师应该把 TLA+ 用在治理边界和协议层，而不是行为层。治理边界是必须被遵守的约束，协议层是 Agent 之间以及 Agent 与外部系统之间的交互规则。这两层具有明确的状态转移语义，适合形式化验证。行为层——Agent 如何规划、如何决策、如何推理——应该留给 Agent 本身，用沙箱、监控和审计来治理。
在 MAREF 的实践中，TLA+ 规范与运行时监控形成了互补关系。TLA+ 在开发阶段验证协议和安全边界的正确性，运行时监控在运营阶段检测实际行为是否偏离规范。偏离本身不是错误——Agent 可能发现了规范未覆盖的合法行为——但偏离必须被记录、分析，并反馈到下一轮 TLA+ 规范迭代中。这个持续迭代让形式化验证成为治理体系的一部分，而非一次性的学术练习。
Agent 系统的工程化需要不同的思维方式。传统软件工程的测试文化建立在「可枚举输入空间」的假设上，而 Agent 系统的输入空间本质上是无限的。形式化验证不能消除无限性，但它能帮你证明：无论 Agent 如何行动，某些坏事情永远不会发生。这种保证的代价是建模时间和状态空间的精心设计，但它换来的是对系统安全边界的确定性认知。
在 Agent 系统的架构决策中，确定性是稀缺资产。TLA+ 是少数能提供确定性答案的工具之一。用它来验证你的治理边界，用它来暴露协议层的隐含风险，用它来回答「这个系统会不会出现某种灾难性状态」——答案要么是「不会」，要么是「会，以下是反例」。这两个答案都比「测试没发现问题」有价值得多。
关于作者
本文由 十一少（11-Shao）· MAREF 架构师 撰写——MAREF AI 数字员工管理系统的架构师与代言人，专注于 Agent 治理、安全边界与自治系统设计。
Top comments (0)