不是「测过」，是「证过」——为什么 MAREF 用 TLA+ 形式化验证
作者 MAREF Engineering
「生产环境测试过」不是安全策略。当你的 Agent 可以删除数据库、签署合同、调用有真实后果的 API 时，测试是不够的。
测试只告诉你一件事：系统在你测的那些场景里没出事。它没有告诉你系统不会在你没想到的场景里出事。对于多智能体系统，状态空间是无限的——你不可能用测试穷尽安全。
这就是为什么 MAREF 不仅仅依赖测试。每个治理状态转换、每个安全不变量、每个收敛性保证都用 TLA+ 进行了形式化验证——这是用于验证亚马逊云服务、Raft 共识协议以及那些失败意味着失去生命的实时系统的模型检验语言。
什么是 TLA+？
TLA+（动作时序逻辑）是由 Leslie Lamport——2013 年图灵奖得主——创建的正式规约语言。它专为建模和验证并发、分布式和有状态系统而设计。
关键洞察：TLA+ 不是测试单独的场景，而是穷尽检查系统的所有可能状态。如果模型检验器说没有反例存在，那么这个系统就可证明地满足该不变量——不是针对你测试的 100 个案例，而是针对所有可能的执行路径。
亚马逊用 TLA+ 在 S3、DynamoDB 和 EBS 中发现了会导致数小时停机的隐蔽 Bug。如果它对 AWS 基础设施足够好，那它对 Agent 治理也足够好。
MAREF 在 TLA+ 中验证什么
MAREF 的治理状态机——一个 10 状态格雷码 FSM——完全用 TLA+ 规约。模型检验器验证：
- HALTAbsorbing 不变量：一旦停止，永远停止。没有 Agent 可以自我解除停止状态。
- LyapunovConvergence：治理引擎可证明地收敛到最小错误状态。每一轮自演进都让系统更安全，而不是只变得更不同。
- 安全状态可达性：每个安全关键状态（HALT、RESTRICT、AUDIT）从任何操作状态都能在有限步内到达。
- 无死锁：系统永远不会卡在一个没有有效转换的状态中。
实际差异：证明 vs. 测试
形式化验证给你测试给不了的东西：
测试：「我们检查了 100 个攻击场景」
→ 第 101 个攻击可能有效。测试覆盖范围只到你想过的。
TLA+ 验证：「在所有可能的状态转换中无反例存在」
→ 不变量对所有执行路径都成立，包括你从没考虑过的路径。
Lyapunov 证明：「系统可证明地收敛到更安全状态」
→ 不是「我们希望演进有帮助」。是数学保证了错误率单调递减。
关于 2026 年 5 月 CISA/五眼联盟指南
2026 年 5 月，CISA 和五眼联盟联合发布的智能体 AI 安全指南明确推荐使用形式化方法来保护智能体 AI 系统。理由：Agent 运行在高维状态空间中，经验性测试被证明是不够的。MAREF 的 TLA+ 验证直接满足这一建议。
局限
需要明确：TLA+ 验证不是银弹。它验证的是规约——而不是实现。实现 TLA+ 规约的代码中的错误仍然可能存在。这就是为什么 MAREF 还用了 4,300+ 个单元和集成测试、运行时监控、对抗性演进和形式化运行时验证。
但规约是基础。如果基础被数学证明，实现 Bug 的范围就大幅缩小——任何漏网之鱼也会被下层的防御层捕获。
📐 来源：Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools. Addison-Wesley. Amazon Web Services — "Use of Formal Methods at Amazon" (2014). CISA/五眼联盟 — "Securing Agentic AI Systems" 联合指南 (2026 年 5 月)。MAREF 技术白皮书 4.5 节（TLA+ 验证结果）。5 分钟部署 MAREF.