Specula 是一个智能体式系统，目标是自动化软件缺陷发现流程。它能够从代码中自动推导 TLA+ 规范，通过轨迹验证检查代码与规范之间的一致性，并对规范进行模型检查以发现并发缺陷；随后，它还会编写具有精确时序的集成测试，在代码层复现缺陷。这篇文章分析了 Specula 的实用价值、主要贡献以及仍未解决的问题。作者认为 Specula 是一个务实且有效的想法，在其目标范围内表现良好，但它回避了真正的难点——组合问题：无法说明各模块的局部保证能否叠加为系统级保证。因此，Specula 更适合发现具体并发缺陷，而在系统级正确性证明上仍有明显边界。