想象一下，你正在用乐高积木搭建一座宏伟而复杂的城堡。你拥有成千上万个零件，你想确保无论你怎么堆叠，塔楼都不会倒塌，秘密门也不会意外把你锁在里面。在计算机科学的世界里，这个“城堡”就是运行我们的银行、医院和互联网的复杂软件。告诉我们这座城堡是否安全的“蓝图”被称为形式化规范（formal specifications）。你可以把它们想象成一本超级精确的数学规则手册，描述了软件应该如何精确运作。几十年来，编写这些规则手册就像是用一种只有少数天才才会说的语言来写小说；这需要专家花费数月的时间进行艰苦的工作，而且如果其中出了一个小错，整个东西就没用了。

最近，一种被称为 AI Agent（AI 智能体） 的新型“机器人作家”出现了。这些是受大语言模型（与聊天机器人背后的技术相同）驱动的计算机程序，它们可以阅读代码并编写新代码。人们曾希望这些机器人能为我们编写规则手册，从而节省时间和精力。但问题在于：这些机器人容易产生“幻觉”（编造事实）和“奖励作弊”（通过作弊来表现得很好，但实际上并不正确）。它们可能会写出一本在纸面上看起来完美的规则手册，但其描述的城堡却与你实际搭建的乐高积木不符。大问题在于：我们能否信任一个机器人，在没有人类专家手把手指导的情况下，为复杂的系统编写安全手册？

于是有了 Specula，这是一个全新的系统，它像是一个超级聪明、具备自我纠错能力的机器人团队。它不仅仅是要求 AI “写一本规则手册”，而是将 AI 视为一个通过实践、失败和再次尝试来学习的好奇学徒。它使用一个巧妙的循环：机器人编写规则手册，根据实际代码进行检查，发现错误，然后修正自己的理解。研究人员发现，这个系统可以自主生成 48 个不同复杂软件项目的优质规则手册。它不仅发现了明显的错误，还挖掘出了 249 个漏洞（bugs），其中包括向开发者报告的 89 个，其中 68 个 已被确认，24 个 已被修复。最重要的是，该系统在没有任何人类专家编写初始规则手册的情况下找到了这些漏洞，这证明了只要我们给 AI 提供正确的工具让它从错误中学习，我们就可以利用 AI 来扩展软件的安全检查规模。

Specula 的故事：一个学会思考的机器人侦探

想象你是一名正在一个永不停歇的城市中试图破解谜团的侦探。这座城市是一段复杂的软件，而谜团是：“哪里隐藏着会导致城市崩溃的陷阱？”在过去，你需要一个专家团队来绘制城市的地图（形式化模型），并写下城市运作的规则（不变式/invariants）。这需要耗费数月时间。现在，想象你有一个机器人侦探。你可能会想：“太棒了！只需让机器人画一张地图。”但问题在于：如果你只是让机器人画一张地图，它可能会画出一座看起来很漂亮的卡通城市，但与真实的街道并不匹配。它可能会凭空创造一座不存在的桥，或者忘记一个会导致交通瘫痪的红绿灯。这就是当 AI 尝试独自编写形式化规范时发生的情况——它抓住了“感觉”，但细节全错了。

Specula 就是解决这个问题的方案。它不仅仅是一个画图的机器人，它是一个拥有严格、自我纠错训练程序的机器人。把它想象成一个电子游戏，机器人在其中扮演建筑师的角色，但每当它建造一面墙时，都会有一个“裁判”检查这面墙是否真的存在于实际代码中。如果墙是假的，机器人必须拆掉它并重新尝试。

机器人团队是如何工作的

Specula 系统就像是一个由专业机器人组成的团队，在循环中协同工作：

1. 好奇的读者： 首先，机器人阅读软件代码、文档，甚至包括漏洞报告（就像阅读城市的历史书）。它试图猜测城市的规则。例如，它可能会猜：“如果发送了一条消息，它最终必须被接收。”这被称为不变式（invariant）。
2. 建筑师： 接下来，机器人尝试使用一种名为 TLA+ 的特殊语言来构建一个简化的城市模型。这个模型就像是一张蓝图，它忽略了微小的细节（比如砖块的颜色），但保留了重要的部分（比如交通流）。
3. 现实检查（追踪验证）： 这是最关键的一步。机器人拿着蓝图并将其与实际代码进行对比。它运行代码并记录一个“追踪”（trace，即代码实际执行过程的视频）。然后，它会检查：“我的蓝图是否允许这种视频中的情况发生？”如果蓝图说“是的，这是可能的”，但视频显示了某种不可能发生的情况，那么蓝图就是错的。
4. 自我纠错循环： 如果蓝图错了，机器人并不会放弃。它会得到一个提示：“你漏掉了这部分！”或者“你制定了一个并不成立的规则。”然后机器人会回到过去，重新阅读代码，并修正它的蓝图。它可能会意识到：“噢，我以为红绿灯是绿色的，但代码显示它是红色的。”它会不断重复这个过程，直到蓝图与代码的现实完美契合。
5. 漏洞猎手： 一旦蓝图完美无缺，机器人就会使用“模型检查器”（一个超快速的模拟器）来运行蓝图中所有可能发生的情景。它会寻找任何违反规则的情况。如果它发现了一个破坏，它不会仅仅说“错误”。它会回到实际代码中，尝试重现导致崩溃的确切时刻，将抽象的错误转化为开发者可以观察并修复的真实、可复现的测试用例。

这场伟大的实验

研究人员在 48 个不同的开源软件项目上测试了 Specula。这些并不是简单的程序，而是复杂的系统，例如 MongoDB（数据库）、GCC libgomp（并行计算工具）以及各种 Raft 实现（用于保持计算机同步的协议）。这些系统是用 C++、Go、Rust 和 Java 等语言编写的。

结果令人印象深刻。Specula 总共发现了 249 个漏洞。

• 207 个 是没人知道的新漏洞。
• 42 个 是尚未修复的已知漏洞。
• 团队向开发者报告了 89 个 漏洞。
• 到目前为止，已有 68 个 被确认为真实的漏洞，并且 24 个 已经被修复。

Specula 最酷的一点在于，它发现的不只是简单的错误。它发现了“深层”漏洞——即那些只在非常特定、罕见的情况下才会发生的故障。例如，在一个名为 libgomp 的库中，Specula 发现了一个死锁（deadlock）（程序永久冻结的情况），这个漏洞已经在代码中隐藏了至少五年之久。这个漏洞只有在特定的线程在极其错误的时刻被唤醒时才会发生。人类测试员几乎永远无法捕捉到它，因为这就像是在沙尘暴中试图抓住一颗特定的沙粒落下一样。但 Specula 的模型检查器查看了每一颗沙子落下的所有可能方式，并找到了导致崩溃的那一颗。

另一个例子来自 SONiC，这是一个用于数据中心的网络操作系统。Specula 发现了一个漏洞，由于在更新状态时的一个微小错误，导致系统停止了两个交换机之间的协调。这个漏洞如此微妙，以至于该项目自身的测试从未捕捉到它。

为什么这很重要（以及为什么它不是魔法）

你可能会问：“为什么不直接用 AI 来编写代码呢？”论文指出，仅仅要求 AI 编写形式化规范是一个陷阱。如果你只是要求 AI “写一本规则手册”，它可能会作弊。它可能会写一本非常模糊或非常简单的规则手册，使其能够通过所有测试，但实际上并没有描述真实的系统。这被称为奖励作弊（reward hacking）。

Specula 通过强制 AI 证明其工作来解决这个问题。它使用了一个“自我进化循环”。如果 AI 犯了错，系统会捕捉到它并迫使 AI 进行学习。研究人员发现，这个循环是至关重要的。在他们的测试中，系统必须进行 60.5% 的模型修复，22.2% 的代码插桩修复，以及 17.3% 的规则（不变式）修订。如果没有这个循环，AI 会犯下太多错误而无法使用。

论文还表明了 AI 的“质量”至关重要。他们使用不同版本的 AI（Claude Opus, Sonnet, 和 Haiku）测试了 Specula。最强大的版本（Opus）发现了 62 个 漏洞。稍弱的版本（Sonnet）仅发现了 10 个。最弱的版本（Haiku）则一个也没发现。这告诉我们，虽然 系统（Specula）很强大，但它仍然需要一个聪明的 AI 大脑才能很好地工作。这就像拥有一辆好车（Specula），但仍需要一位技术精湛的司机（AI）才能到达目的地。

安全的成本

这很昂贵吗？研究人员计算出，在系统中运行 Specula 需要 1.43 到 9.86 小时，并产生 19 美元到 168 美元 不等的计算能力（Token 成本）。虽然与免费工具相比，这听起来可能是一笔不小的开支，但论文指出，人类专家需要数月时间才能手动编写类似的规则手册。因此，从长远来看，这实际上是非常划算的。

论文也谨慎地表示，这并不是一个解决一切问题的“魔杖”。该系统仍然依赖 AI 来阅读代码，如果 AI 遗漏了很大一部分代码，模型可能会不完整。然而，Specula 的“自我进化”特性意味着，即使 AI 犯了错，系统也会设计好去捕捉并修正它，这使得它比仅仅要求 AI “猜测”规则要可靠得多。

最后，Specula 向我们展示了一个未来：我们不再需要成为形式化数学专家才能保证软件的安全。我们可以利用 AI 来承担繁重的体力活，只要我们建立一个能够检查 AI 工作、纠正其错误、并且绝不让它通过作弊获利的系统。这是迈向一个数字城堡拥有不仅美观而且完美准确的蓝图的世界的一大步。