Specula：AI 深挖系统隐藏 Bug！在复杂软件系统中，很多隐藏的 Bug 很少会出现在正常流程中。一次寻常的请求、普通任务的执行，并不会触发这些 Bug。一旦遇到诸如并发、重试、超时、失败恢复等等情况，这些 Bug 就会出现。它们的表现有：

- 重复执行同一操作
- 状态卡在中间，流程无法继续
- 不同流程同时修改同一数据，导致状态不一致
……

普通的测试很难发现这些问题。Specula 就是用来解决复杂系统中的此类问题，它会让 AI Agent 协助研发人员理解这些复杂的系统，并进行形式化验证。

Specula 会先分析代码结构，从而理解系统中的模块、状态和关键流程，再把这些行为转换成 TLA+ 规范，并通过 Model Checking 枚举可能的状态变化，寻找违反规则的异常路径。

工作流程如下：

代码仓库 → AI 理解系统 → 生成 TLA+ 规范 → 模型检查 → 发现隐藏 Bug

和传统测试关注“已经想到的场景”不同，Specula 的关注重点是那些容易遗漏的状态组合。

Specula 的核心能力：

0️⃣ 异常发现：通过模型检查寻找隐藏的错误路径；
1️⃣ 代码理解：自动分析大型代码系统，提取关键状态和行为；
2️⃣ 规范生成：将复杂系统行为转换为可验证的 TLA+ 规则；
3️⃣ Agent 验证方向：展示了 AI Agent 从“生成代码”走向“理解和验证系统”的另一种可能；

目前来说，Specula 会更适合分布式系统、基础设施、数据库、消息队列等复杂系统开发场景。

开源项目 AI Agent TLA+ 形式化验证 ModelChecking 开发者工具 Bug