基恩·卢卡斯，艾尔戈斯·林奇，露娜·汤，卢克·Champine，齐吉·斯特拉兹尼卡斯，迪诺·迪斯特法诺，哈希卡·阿格拉瓦尔，埃维亚塔尔·贝恩·阿舍，艾娃·霍维尔，萨米·贾瓦尔，克里斯·罗尔夫，尼克莱·泽尔多维奇，尼古拉斯·卡尔尼，拉贾什里·阿格拉瓦尔，杰森·格罗斯大多数软件充满了漏洞，而人工智能现在可以轻松找到并利用这些漏洞。对网络攻击的标准防御措施已经不再足够：我们需要能够证明代码没有漏洞的方法。正式软件验证可以提供这种保证，但它在历史上需要多年的专家努力，使其在大多数实际项目中不切实际。然而，在与 Theorem 的合作中，我们展示了这种情况不再存在：LLMs 现在可以大规模生成正式证明，从而支持新的软件开发工作流程，并包含经过验证的安全保证。使用 Claude，我们在100多个现实世界的开源软件库中证明了汇编代码级别的安全属性（RISC-V）。据我们所知，这代表了首次大规模努力使用人工智能将正式验证应用于生产软件的汇编代码级别。在编写证明的同时，Claude 还发现了多年未能检测到的漏洞，尽管进行了万亿次的测试运行。随着模型能力的不断提高，我们预计正式验证将成为安全软件开发的一个重要组成部分。引言即使是成熟的、经过严格测试的软件也包含漏洞，而 LLMs 在查找这些漏洞方面越来越擅长。Linux 内核-今天最经过测试的软件之一，已在全球数十亿设备上部署-最近披露了超过 1,000 个漏洞。随着前沿模型能够将表面上无害的漏洞链接成关键利用，我们需要能够在这些漏洞被广泛利用之前检测和修复它们的技术。理想情况下，这些技术可以找到并修补所有漏洞，然后提供某种证据，证明没有更多的漏洞可供发现。正式验证是实现这一目标的一种方法。在正式验证过程中，开发人员将他们的代码转换为数学模型，然后尝试证明它始终遵循某些定义的安全规则。如果他们无法证明这一点，则意味着代码中可能存在违反规则的漏洞，而失败的性质暗示了漏洞可能是什么。重复这个过程（在每次消除失败原因后）最终将产生证明，证明代码没有任何会违反这些规则的漏洞。然而，正式验证并不容易。证明的规模可能远大于原始代码，编写证明需要大量的努力和高度专业化的技能。例如，实现 seL4 操作系统内核需要两人年的时间，而正式验证则需要20人年。因此，正式验证在真正的关键任务应用中才是可行的，例如空客的航空电子代码。但是，LLMs 正在使这一过程变得更加容易。前沿模型现在可以完全自主地为现实世界软件生成正确性证明。为了证明这一点，我们要求 Claude 为 123 个开源库证明有用的安全属性，包括证明它们的一些可执行工件在某些条件下永远不会崩溃。具体来说，Claude 证明这些程序在每个小于 64 MB 的输入和每个建模的 Linux 操作系统（OS）响应和内存布局下，在一定假设（即程序以单线程静态二进制文件与固定内存预算在使用 Linux OS 的 RISC-V 1 CPU 上运行）下将始终正常退出而不会触发内存安全错误或失败断言。这仍然离修复所有可能的漏洞相去甚远，但它确实使我们比以前更接近这一目标，并提供了朝着这一目标的路线图。我们正在发布这些证明的一部分，以便任何人都可以验证和重用它们，连同 RISC-V 和操作系统语义。我们的合作伙伴 Theorem 也提供为其他开源项目运行相同管道的服务，并发布了一个 Claude 技能，以帮助开发人员开始验证自己的代码。正式验证是一个广泛的领域，包含许多方法论。以下，我们还描述了我们使用其他正式验证方法的初步探索，以加速其他安全或软件开发任务，例如评估 zlib 压缩算法的安全性，证明用 Rust 编写的 Python 解释器的行为等价性，以及清除关键软件中的长期存在的漏洞。正式验证的未来前景广阔。随着模型变得越来越智能，编写证明的成本正在下降。此外，随着更多代码的正式化和实现安全保证的方法变得更加标准化，跨代码库重用或修改证明的能力将摊销成本。我们鼓励所有开发人员与 LLMs 探索正式验证——特别是那些以前尝试过能力较低的模型并发现...