Google DeepMind 宣布用新的智能体框架 AlphaProof Code 完成 Signal 消息协议底层机器码关键安全属性的形式化验证，覆盖 libsignal 的 PQXDH 握手与 Triple Ratchet，并称这是首次对广泛部署协议的生产代码做到这一深度的验证。该框架由负责编写 Lean 规范的引导智能体和一组自主证明智能体组成，证明须通过 Lean 内核检查，共生成约 650 万行机器校验的 Lean 证明，基于约 26000 行可信规范与 AArch64 语义。团队称同类工作原本可能需要数十年合力，此次用时一个月，并已开源形式化规范与验证产物。Andrew Curran 转发该消息时提到 Gemini 4 Carbon 参与其中，并称有用户报告 Carbon 已上线，Google 可能在当天上午发布公告。
DeepMind 用 AlphaProof Code 在约一个月内完成 Signal 协议机器码级形式化验证，并开源规范与验证产物。
Gemini 4 Carbon contributed to this. There are multiple reports of Carbon going live for some people right now, and we may get a release announcement from Google later this morning.
【引用 @pushmeet】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://deepmind.google/blog/formal-verification-signal-protocol
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://deepmind.google/blog/formal-verification-signal-protocol在 X 查看被引用的帖子
来源：Andrew Curran · x.com