Specula open-source tool finds 382 bugs in 67 systems via coding agents and TLA+
Specula, an open-source tool developed by the team that won the first TLAi+ Challenge, uses coding agents such as Claude Code, Codex, and Copilot CLI to automatically generate TLA+ specificationsable invariants, run model checking, and reproduce counterexamples as tests. As of August 19, 2026, it has found 382 bugs in 67 open-source systems, including MongoDB, Etcd, ScyllaDB, HashiCorp Raft, and LLVM, reducing months of formal verification work to hours.
Coverage timeline
机器之心机器之心
截至 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
