Specula在67个开源系统中找到382个深层bug，数月形式化验证缩短到几小时

截至 2026 年 8 月 19 日，Specula 已经在 67 个开源系统中找出 382 个 bug，并被多个公司和开源社区的开发者使用。 如今，coding agent 已经能写功能、补测试、提 PR，但一碰到形式化规约，它仍然很难摆脱专家手把手指导。TLA+ Foundation 与 NVIDIA 举办首届 TLAi+ Challenge，希望借助 AI 降低规约编写的门槛。Specula 团队拿下第一名。如今，我们把比赛中的思路做成了真正可以跑起来的系统：coding agent 会自己读代码、写规约、运行模型检查，再追出那些只在极端交错下出现的问题。过去，专家要反复读代码、提炼性质、手写模型，再一轮轮校准；仅为一个复杂系统建立可用规约，就可能花上数月。 开源项目 Specula 瞄准的正是这件事。它让 Claude Code、Codex、Copilot CLI 等 coding agent 阅读目标系统的代码、文档、测试与历史提交，自动生成 TLA + 模型和正确性不变量，运行模型检查，再把找到的反例带回真实代码复现并封装成测试。整个过程可以全自动运行，开发者不需要先学会 TLA + 或模型检查，这让长期困在专家圈里的形式化方法，第一次有机会变成普通开发者拿来就能用的工程工具。 Specula 官网：https://specula.info Specula 论文：https://arxiv.org/abs/2607.25333 Specula GitHub：https://github.com/specula-org/Specula Specula Bug 追踪表：https://docs.google.com/spreadsheets/d/1AVXdKjNfD4952hZqyB-_wTdrzeTw0SD73f3F0zWJ0as/edit?gid=996176958 #gid =996176958 TLAi+ Challenge：https://foundation.tlapl.us/challenge/index.html 截至 8 月 19 日，Specula 已经在 67 个开源系统中发现 382 个 bug，覆盖 MongoDB、Etcd、ScyllaDB、HashiCorp Raft、RabbitMQ/ra、GCC libgomp 和 LLVM libomp 等复杂系统。 并发 bug 为什么难找 形式化规约为什么更难写？ 所谓并发 bug，常常不是某一行代码直接写错，而是多个线程或节点各自做着看似正确的事，却在一个罕见顺序下共同把系统推向错误。线程交错、消息顺序、节点故障和磁盘延迟一组合，可能形成数量巨大的执行路径。普通测试通常只能抽到其中一小部分，最棘手的问题恰恰藏在很少发生、却真实可达的路径里。比如本文后面会讲到的 GCC 死锁：只有当其他线程全部停在屏障等待循环后，外部线程才完成一个分离任务；此时唤醒路径漏掉了待处理标记，线程被叫醒后又重新睡下，最终形成死锁。 TLA+ 形式化方法的思路是先把系统行为抽象成状态与转换，再让模型检查器系统性探索可达状态：如果某条路径打破了「提交索引不能倒退」、「多数派确认的数据不能丢失」这类不变量，工具就返回一条反例。 真正困难的是，一份可用于找 bug 的规约必须同时过四道关：从庞杂代码和历史中提炼系统真正承诺的正确性性质；保留足以暴露 bug 的行为，同时控制状态空间；确保模型与真实执行一致；还要让模型反例回到代码中复现，排除只存在于抽象模型里的假 bug。任何一环出错，后续都可能建立在错误前提上。论文团队此前为 ZooKeeper 和 Asterinas 手写规约时，这件事需要数月；把它扩展到几十个真实项目，人工方式无法承受其高昂的成本。 核心原则： 判断和决策来自 artifact，agent 在推进中学习 Specula 不是让大模型一次生成一份 TLA + 文件就结束。它把工作拆成四个彼此衔接、可以独立验收的环节：理解正确性性质、生成有效模型、检查模型与代码的一致性、在真实代码中复现异常行为。每一环都会留下明确的 artifact，下一环既使用它，也检查它；agent 的关键判断还必须附上代码、issue、提交或执行轨迹等证据。 第一步：从系统证据中提炼不变量 Specula 从代码、注释、文档、测试、issue 和历史修复中总结协议级与实现级不变量，并要求 agent 为每条性质给出证据。以 MongoDB 为例，它不会照搬教科书版 Raft 的持久化假设，而会根据实现历史识别「多数节点在内存中持有即可提交」的设计选择。论文统计中，87.35% 的不变量引用了代码或注释，74.34% 引用了 issue、PR 或安全公告。 第二步：围绕关键场景生成模型 不变量决定什么必须保留，Specula 再从文档、测试、issue 和提交历史中提取高风险场景，为每个场景生成定制模型：保留相关变量、动作和故障，抽象无关细节，避免状态空间爆炸。ScyllaDB Raft 的 voter demotion 曾被连续修复三次，Specula 因此单独建模新旧配置与 ReadBarrier，最终发现一个在降级期间卡住 read barrier 的新 bug。 图 1：Specula 为 ScyllaDB Raft 库生成的简化建模计划：从历史修复和代码证据中提炼场景、变量、动作与不变量。 第三步：用真实轨迹检查模型 模型能运行，不代表它忠于代码。Specula 自动为程序插桩、收集真实执行轨迹，再逐步检查这些轨迹能否被 TLA + 模型接受；一旦在某一步分叉，就能定位模型与实现之间的差异。 第四步：把反例带回代码复现 模型检查发现不变量被违反后，Specula 会把反例转换为一条确定的事件序列，在真实系统中控制故障与并发顺序，重放同样的行为，并把复现过程封装成测试。 两条自我演化闭环 让 agent 在失败中纠错与进化 上述四步并不是一条只向前走的流水线。Specula 假设 agent 会犯错，因此专门设计了两条相互依赖的自我演化闭环。每次失败都必须带回新的代码证据、执行轨迹或反例，推动下一轮判断，而不是简单重试。 第一条是模型 — 代码一致性闭环：轨迹验证确保真实代码行为能在模型中发生，模型检查则阻止 agent 为了迎合轨迹而放宽模型或削弱不变量。第二条是 bug 复现闭环：如果反例无法在代码中重放，系统就把分叉状态送回前一条闭环，重新检查模型、插桩或不变量；如果复现成功却没有可见后果，则继续判断性质是否过强，或后果是否被系统的恢复机制掩盖。 图 2：Specula 的两条自我演化闭环。模型与代码一致性循环在轨迹验证与模型检查之间往返；bug 复现循环把无法重放的反例重新送回模型修正。 67 个开源系统，382 个 bug 从数据库、分布式系统到编译器运行时，Specula 都找到了可以在真实代码中复现的问题。下面这个 GCC 案例最能说明，这些罕见的并发 bug 为什么会逃过常规测试。 一个躲了五年的 GCC 死锁 论文给出的案例来自 GCC 的 OpenMP 运行时库 libgomp。触发时，一个外部线程要等到其他线程全部停