核心观点 - Specula 是一个开源项目，通过让 coding agent 自动读取代码、编写形式化规约、运行模型检查并复现 bug，将形式化方法从专家工具转变为普通开发者可用的工程工具 [4] - 截至 2026 年 8 月 19 日，Specula 已在 67 个开源系统中发现 382 个 bug，覆盖 MongoDB、Etcd、ScyllaDB、HashiCorp Raft、RabbitMQ/ra、GCC libgomp 和 LLVM libomp 等复杂系统 [1][6] 并发 bug 的难点与形式化方法的价值 - 并发 bug 常由多个线程或节点在罕见顺序下共同导致，普通测试只能覆盖一小部分执行路径，最棘手的问题藏在很少发生却真实可达的路径中 [8] - 以 GCC 死锁为例：只有当其他线程全部停在屏障等待循环后，外部线程才完成一个分离任务，但唤醒路径漏掉了待处理标记，线程被叫醒后又重新睡下，最终形成死锁，该问题自 2021 年引入后潜伏至少五年 [8][26] - TLA+ 形式化方法通过抽象系统行为为状态与转换，让模型检查器系统性探索可达状态，若某条路径打破不变量则返回反例 [8] - 一份可用于找 bug 的规约需过四道关：从代码和历史中提炼正确性性质、保留暴露 bug 的行为同时控制状态空间、确保模型与真实执行一致、让模型反例回到代码中复现 [8] - 此前为 ZooKeeper 和 Asterinas 手写规约需数月，扩展到几十个真实项目人工方式无法承受高昂成本 [10] Specula 的四步工作流程 - **第一步：从系统证据中提炼不变量** - Specula 从代码、注释、文档、测试、issue 和历史修复中总结协议级与实现级不变量，要求 agent 为每条性质给出证据 [13] - 论文统计中，87.35% 的不变量引用了代码或注释，74.34% 引用了 issue、PR 或安全公告 [13] - 以 MongoDB 为例，它根据实现历史识别「多数节点在内存中持有即可提交」的设计选择，而非照搬教科书版 Raft 的持久化假设 [13] - **第二步：围绕关键场景生成模型** - 从文档、测试、issue 和提交历史中提取高风险场景，为每个场景生成定制模型，保留相关变量、动作和故障，抽象无关细节，避免状态空间爆炸 [14] - ScyllaDB Raft 的 voter demotion 曾被连续修复三次，Specula 单独建模新旧配置与 ReadBarrier，最终发现一个在降级期间卡住 read barrier 的新 bug [14] - **第三步：用真实轨迹检查模型** - 自动为程序插桩、收集真实执行轨迹，再逐步检查这些轨迹能否被 TLA+ 模型接受，一旦在某一步分叉就能定位模型与实现之间的差异 [17] - **第四步：把反例带回代码复现** - 模型检查发现不变量被违反后，Specula 把反例转换为确定的事件序列，在真实系统中控制故障与并发顺序重放同样行为，并把复现过程封装成测试 [18] 两条自我演化闭环 - Specula 假设 agent 会犯错，设计了两条相互依赖的自我演化闭环，每次失败必须带回新的代码证据、执行轨迹或反例，推动下一轮判断，而不是简单重试 [20] - **第一条是模型—代码一致性闭环**：轨迹验证确保真实代码行为能在模型中发生，模型检查则阻止 agent 为了迎合轨迹而放宽模型或削弱不变量 [20] - **第二条是 bug 复现闭环**：如果反例无法在代码中重放，系统把分叉状态送回前一条闭环重新检查模型、插桩或不变量；如果复现成功却没有可见后果，则继续判断性质是否过强，或后果是否被系统的恢复机制掩盖 [20][21] 性能对比与效率提升 - 在 5 个代表性系统中，Specula 找到 62 个 bug，原始 Claude Code 找到 2 个，只给 Claude Code 配上 TLA+ 工具找到 3 个 [29] - 差距主要来自场景化建模、模型—代码一致性检查，以及把反例带回代码复现的闭环 [29] - 在论文的 48 个项目上，一次端到端检查耗时 1.43—9.86 小时，中位数 3.69 小时；token 成本为 19—168 美元，中位数 57 美元 [31] - 过去按月计算的规约编写工作，如今可在几个小时内跑完，让批量检查真实项目第一次变成现实 [31] - 目前项目支持 Claude Code、Codex、Copilot CLI、OpenCode 和 Pi 等 agent，用户可用两条命令在自己的系统上跑起来，也可定制自己的场景和形式化模型 [31] 行业影响与意义 - 对基础软件团队，它是在测试、代码审查和静态分析之外，继续追查深层 bug 的一层新防线 [33] - 对形式化方法专家，它把时间从重复建模中释放出来，转向更关键的性质设计与结果判断 [33] - 对更广泛的计算机从业者，它第一次让「用形式化方法检查真实系统」不再是一件遥不可及的事 [33]