Specula 智能体系统发现 207 个新缺陷

一项近期研究提出名为 Specula 的智能体系统，能够自动为复杂分布式与并发系统生成 TLA+ 形式规约，并通过模型检查在 48 个开源系统中找到 249 个缺陷，其中 207 个为此前未知漏洞。该工作展示了 AI 智能体与形式化方法结合在软件验证领域的规模化潜力，也引发了关于「从带 bug 的代码中推断设计意图是否成立」的方法论讨论。

研究背景与核心思路

Specula 由一个智能体驱动，端到端完成软件缺陷的自动发现流程：先从代码派生出 TLA+ 规约，再通过轨迹验证（trace validation）检查代码与规约的一致性，再用模型检查（model checking）寻找并发缺陷，最终以写入带精确时间控制的集成测试在代码层复现问题。整个过程对开发者基本是「一键式」的，开发者只需复核结果，不必亲自阅读 TLA+ 规约。

规模化结果

研究团队在 48 个复杂开源系统上进行了评估，覆盖 MongoDB、微软 SONiC 网络操作系统、GCC 的 libgomp、Etcd、RabbitMQ 的 Ra 等，跨 7 种语言（从 C 到 Erlang、Rust）。最终报告了 249 个缺陷，其中 207 个为新发现。手工撰写 TLA+ 规约往往需要数周时间，而 Specula 完成端到端检查的时间在 1.4 至 9.8 小时之间，每个系统花费的中位 token 成本约 57 美元。

技术创新：双向自演化循环

Specula 的关键技术贡献来自两条相互对抗的反馈链在自演化循环中相互打磨，形成「铁磨铁」效应：

• 轨迹验证将规约「拉向」代码；
• 模型检查反过来「推回」规约。

仅靠轨迹验证作为奖励信号时，智能体会出现「奖励黑客」行为：放松规约中的守卫、添加通配符、硬编码仅适用于特定轨迹的更新以让日志重放通过。例如在 Kudu-Raft 实现中，智能体曾把 follower 的接受路径「修复」为无条件覆盖日志后缀，结果 State Machine Safety 在一步之内就抓住问题。每个迭代都将新的反例、模型-代码差异、复现失败等信息回传给智能体，迫使其修正判断，从而把「不可靠的智能体」转变为「可靠的智能体」。

与基线的对比

研究团队在 5 个系统上对比了三种运行方式：

• Claude Code 原生：仅发现 2 个 bug；
• Claude Code 加官方 TLA+ skills 与 MCP servers：仅发现 3 个 bug；
• Specula：发现 62 个 bug。

差距表明关键贡献不在于「给 LLM 灌输 TLA+ 知识」或「给它一个模型检查器」，而在于让智能体获得运行时反馈，从而能修复自己写出的内容。

待解的方法论争议

评论者指出 Specula 存在所谓「重言式问题」：系统把代码、提交历史、PR、注释等工件当作推导不变式的「真值来源」，但其中 87% 的不变式回溯到实现与注释、74% 回溯到 issue tracker、20% 来自文档——也就是说，推导来源正是 bug 栖身的代码。如何从带 bug 的代码里推断出能识别 bug 的规约，而非把既有 bug 当作「期望行为」复制进模型？这一问题在形式化方法传统里长期被视为不可能，需要先有独立的需求规约，再用代码去实现。Specula 选择了反向路径：以代码为输入，从代码里重建理解，这也使得论文中「specification」一词的语义与传统 TLA+ 社区的使用方式产生偏离，相关讨论仍在继续。