Specula 自动形式化验证：已在 67 个开源系统发现 382 个 bug
Specula 用 AI 自动生成形式化规约并验证并发 bug，把专家数月的工作压缩到几小时，已发现 382 个真实缺陷。
Specula 是一个开源工具，它让 AI 编码代理自动阅读代码、编写 TLA+ 形式化规约并运行模型检查，从而找出普通测试难以触达的并发 bug。目前它已在 67 个开源系统中发现 382 个 bug，而过去这类验证需要专家手动完成，往往要耗费数月。
正文摘录
.jpg)  截至 2026 年 8 月 19 日，Specula 已经在 67 个开源系统中找出 382 个 bug，并被多个公司和开源社区的开发者使用。  如今，coding agent 已经能写功能、补测试、提 PR，但一碰到形式化规约（formal specification，用数学语言精确描述系统行为的定义），它仍然很难摆脱专家手把手指导。TLA+ Foundation 与 NVIDIA 举办首届 TLAi+ Challenge，希望借助 AI 降低规约编写的门槛。Specula 团队拿下第一名。