Original post · AI translation
Google DeepMind 取得了一项重大成就：展示了一个无需信任 AI、就能从数学上证明软件安全的 AI 系统。
他们刚刚利用 AI 智能体，从数学上证明了 Signal 实际运行的代码能保守消息秘密。
谷歌的 AI 智能体编写了 650 万行数学证明，证明 Signal 的编译后代码能保护聊天隐私。
检验深入到了处理器实际执行的指令层面。该实验室表示，此前还没有人对任何广泛使用的协议做到这一点。
常规测试会尝试许多输入，寄希望于碰到有问题的那个。证明则表明安全规则在所有情况下都成立，而 Lean 证明检查器会拒绝 AI 写出的任何错误步骤。
真正的漏洞往往在设计转化为代码时悄然出现，因此检查处理器层面的代码弥补了这一环节的漏洞。Rust 编译器也不需要被信任，所以编译器犯的错误同样会被发现。
这项工作耗时 4 周，而过去专家团队需要数年。由 40 至 80 个 Gemini Carbon 智能体组成的团队编写了约 650 万行 Lean 代码；人类则设定安全目标，并审查智能体标记出的 1%。
为了检验该系统不会对任何代码都给出认可，研究人员在一个副本中重新引入了 2 个早已修复的 Signal 漏洞。两次它都生成了经机器检查的证明，证实代码不安全。
更大的转变在于成本：如今 AI 能在数周内生成经机器检查的证明，使原本需要耗时数年的项目有望成为设备固件、电网软件及其他关键代码的常规检查。
宣布我的 @GoogleDeepMind 团队取得的一项重大里程碑：我们证明了 Signal 消息协议底层机器代码的关键安全性质。这是首次有人对广泛部署的协议的实际生产代码进行形式化验证——无论采用何种方法、是否使用 AI，在这一验证深度上都是如此。
这不仅是一项研究突破，也是前沿 AI 如何发挥倍增作用、应对现代网络威胁的速度和规模的一个典型例子。
形式化验证提供了更高的安全标准；然而，它极其复杂且耗时，因此在许多情况下被认为不切实际。类似的工作可能需要团队累计投入数十年。我们在 1 个月内完成了。
我们使用 Google DeepMind 新推出的形式化验证智能体框架 AlphaProof Code，将 Signal 协议验证到了设备上实际运行的代码层面；该框架运行在包括 Gemini Carbon 在内的大语言模型上。这一里程碑为未来奠定了基础：从医疗设备固件到电网软件的重要系统，都能在交付时附带数学证明，证实其防护措施有效。
要实现这样的未来，还需要研究界持续开展研究。秉持这一精神，我们正在开源形式化规格说明和验证产物，让其他人能够在这项工作的基础上继续推进。
就我个人而言，这一刻对我意义深远。20 多年前，我以实习生身份开始自己的研究之路，当时的工作是检查复杂软件系统的一致性。看到这一重大挑战借助现代 AI 变得切实可行，实在非同寻常。
我为团队成员 Swarat Chaudhuri、Andrew Ferraiuolo、Anton Kovsharov、Tej Chajed、Sam Schlesinger、Karn Seth、Jonathan Katz 和 Charles Sutton 接受并完成这一重大挑战而感到无比自豪，也感谢 Signal 团队的合作。
https://t.co/kN1eRYQ8fF
Original
Announcing a major milestone achieved by my team @GoogleDeepMind: we have proven key security properties of the machine code underlying the Signal messaging protocol. This is the first time the actual production code of a widely deployed protocol has been formally verified – by any method, with or without AI – and at this depth. More than a research breakthrough, it’s a prime example of how frontier AI can be a force multiplier to counter the speed and scale of modern cyber threats. Formal verification offers a higher standard of security; however, it’s extremely complex and time consuming, which is why in many cases it’s considered to be impractical. Similar efforts could take teams decades of combined effort. We did it in a month’s time. Using AlphaProof Code, Google DeepMind's new agentic framework for formal verification that runs on LLMs including Gemini Carbon, we verified the Signal protocol down to the actual code running on devices. This milestone lays the groundwork for a future in which vital systems, from medical device firmware to power grid software, ship with mathematical proof that their protections work. Reaching that future will take continued research from our community. In that spirit, we're open-sourcing our formal specifications and verification artifacts so others can build on this work. On a personal note, this moment is of deep significance to me. I started my own research journey more than two decades ago as an intern working on checking the consistency of complex software systems. Seeing this grand challenge made practical with modern AI is extraordinary. I'm extremely proud of my team members: Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, and Charles Sutton for taking on this grand challenge and delivering, and grateful to the Signal team for their partnership. https://t.co/kN1eRYQ8fF