截至 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。触发时，一个外部线程要等到其他线程全部停在屏障等待循环后，才完成一个分离任务；但这条唤醒路径漏掉了 “仍有任务待处理” 的标记。线程被叫醒后看不到任务，又重新睡下，最终所有线程都无法完成屏障。这个问题需要极其特定的线程交错，自 2021 年引入后，在代码库中潜伏了至少五年。
图 3：Specula 在 GCC libgomp 中发现的死锁。一条唤醒路径漏掉待处理标记，违反了「携带唤醒任务的路径必须设置待处理标记」这一活性不变量。来源：Specula 论文 Figure 9 下半部分。
只给 coding agent 装上 TLA + 工具，还远远不够
论文还把 Specula 与两种更直接的做法做了对比：一种是原始 Claude Code，另一种是只给 Claude Code 配上 TLA + 工具。在 5 个代表性系统中，Specula 找到 62 个 bug，前两种方法分别找到 2 个和 3 个。差距主要来自场景化建模、模型 — 代码一致性检查，以及把反例带回代码复现的闭环。
图 4：在同一组 5 个受控实验系统中，Specula 找到 62 个经人工核验的真实 bug，原始 coding agent 与配备 TLA + 工具的 coding agent 分别找到 2 个和 3 个。
更直接的变化是速度。在论文的 48 个项目上，一次端到端检查耗时 1.43—9.86 小时，中位数 3.69 小时；token 成本为 19—168 美元，中位数 57 美元。过去按月计算的规约编写工作，如今可以在几个小时内跑完，让批量检查真实项目第一次变成现实。
目前项目支持 Claude Code、Codex、Copilot CLI、OpenCode 和 Pi 等 agent，其他 agent 也在继续适配中。用户可以只用两条命令就在自己的系统上跑起来，也可以定制自己的场景和形式化模型。
Specula 真正值得关注的地方，是它把长期昂贵、依赖少数专家的形式化方法，变成一条普通开发者也能启动的全自动工程流程。对基础软件团队，它是在测试、代码审查和静态分析之外，继续追查深层 bug 的一层新防线；对形式化方法专家，它把时间从重复建模中释放出来，转向更关键的性质设计与结果判断；对更广泛的计算机从业者，它第一次让 “用形式化方法检查真实系统” 不再是一件遥不可及的事。
作者介绍
本文由程潜、唐瑞泽、黄宇、徐天音共同撰写。
程潜：南京大学计算机系黄宇教授的博士生，研究聚焦面向真实软件系统的形式化方法、模型检查，以及生成式 AI 辅助的规约生成与验证。
唐瑞泽：微软亚洲研究院高级研究员，获南京大学计算机科学博士学位，研究聚焦形式化验证与系统正确性，尤其关注并发与分布式系统及 AI 辅助验证。
黄宇：南京大学计算机系教授、博士生导师，研究方向包括分布式算法与系统、形式化规约与验证、系统软件正确性与可靠性。
徐天音：伊利诺伊大学厄巴纳 — 香槟分校计算机系副教授，研究聚焦操作系统、云计算与数据中心系统，以及大规模系统可靠性和配置管理。
