4 周时间，650 万行证明，困扰软件安全研究者多年的难题终于破解，还得靠 AI 啊。

Gemini 4 Carbon 一出，谷歌猛猛甩出硬核 Demo，其中，一项名为AlphaProof Code的新方法被 CEO 劈柴推上 C 位：

全球数十亿用户聊天依仗的加密协议，终于被从数学上证明代码可靠了。

领衔研究的 DeepMind 副总裁 Pushmeet Kohli 难掩兴奋：

这是史上头一回！ 无论靠人还是靠 AI，还从来没有人把一款广泛使用的加密协议，直接验证到实际运行的机器码这一层。

Signal 首席技术官 Ehren Kret 也忍不住点赞，称 AI Agent 能够将实际运行的代码转化为有效的 Lean 定理，是一项里程碑式的重大突破。

网友们也纷纷感叹： 

这才是 AI Agent 落地工程的终极示范！把几十年的工作压缩到一个月，自动化验证太强了。

好家伙，AI Agent 这回连代码安全都开始用数学严格证明了。

怎么做到的？

AI 狂写 650 万行数学证明，四周完成多年验证工作

要知道，过去给软件做形式化验证，一般是数学家和形式化验证专家才能干的 " 贵族活 "；

普通安全测试找到一个 Bug 修完就完事了；

但形式化验证却得靠专家写出严密的数学证明，确保软件在特定条件下不会出问题。

所以这项工作不仅烧钱费脑，而且还极其耗时，动辄三五年起步，复杂一点的系统甚至要耗上十年八年。

（比如早在 2004 年，澳大利亚 NICTA 研究团队就开始为 seL4 操作系统内核做数学验证，5 年间累计投入的工作量，足够让一个人连续干上 20 年。）

现在，AlphaProof Code 把这份繁重的证明工作接了过去。

它的工作方式有点像一支AI 数学研究团队。

在这个案例中，首先，5 名 DeepMind 专家会和 AI 一起，把 Signal 需要满足的安全要求写成 Lean 能够理解的数学规范，再由专家逐一审核。

审核通过后，由 Gemini Carbon 驱动的 Agent 小工们就开工了。

有的负责攻克不同部分的数学证明，有的负责检查证明结果。

它们一路追着 Signal 实际编译出来的机器码，一步步把需要证明的安全性质逐项落实到 Lean 代码里。

但这份答卷可不好糊弄。

Agent 写出一段，Lean 就检查一段。

只要证明里存在逻辑错误，Lean 就绝对不会放行。

△AlphaProof Code 工作流程图，图源 DeepMind

就这样，五名研究人员各自守着一台工作站，同时推进任务，让 AI 不停地写、不断地验证。

短短四周内，Agent 们就一口气写出了约 650 万行 Lean 证明代码，把 Signal 底层约14 万条机器指令都纳入了数学验证。

不仅如此，在这项庞大的证明工作完成后，AI 还贴心地帮研究人员筛出了需要重点复核的部分。

谷歌在 Blog 中透露，最终需要专家进一步检查的代码只占约1%。（Woc，1%？！）

但写出 650 万行证明，就真的能证明这群 Agent 真有本事吗？

研究人员们决定再考考它。

于是，他们翻出了 Signal 以前已经修复的两个真实 Bug，并悄悄装回隔离测试版本，看看 AlphaProof Code 能不能察觉。

（一个涉及旧会话与新会话之间的密钥状态处理，另一个涉及密钥交换时缺少必要检查。）

结果，两道陷阱题全被 AlphaProof Code 逮了个正着！

AI 不仅发现了问题，还分别拿出了通过 Lean 检查的数学证明，有理有据地证明带有这些 Bug 的版本确实违反了安全要求。

这下，Agent 不仅真能证明代码符合安全要求，连故意塞进去的旧漏洞，也别想蒙混过关了。

更关键的是，DeepMind 已经将这次研究的规范和约 650 万行 Lean 证明代码全部开源了，感兴趣的小伙伴们可以直接去拿来检查、复现和继续往下研究啦：

Anyway，这套新方法当然也有边界，谷歌 Blog 中也有写到： 

这次验证针对的是特定版本的 Signal 核心协议实现及指定安全性质，尚未覆盖整个 Signal App 和所有攻击场景。

但对于软件安全行业来说，AlphaProof Code 意义已经相当直观——

它砍下了过去需要专家们投入大量时间、精力和金钱才能完成的数学验证的门槛。

而且这套办法还可以继续向外延伸。

从银行系统，到医疗设备固件，再到电网软件，那些一旦出错就可能造成严重后果的关键程序，未来都有机会接受同样严格的数学检验。

而站在这套 AlphaProof Code 背后的，是一个坚持了 20 多年的守望者。

一场跨越二十年的科研圆梦

对我个人而言，这一刻意义非凡。

二十多年前，我还只是一名刚刚踏上科研之路，研究如何检查复杂软件系统一致性的实习生。

如今，我有幸能亲自见证现代 AI 让这项艰巨的挑战变得切实可行，实在不可思议…

写下这段话的，正是负责 AlphaProof Code 研究的谷歌云首席科学家、DeepMind 副总裁Pushmeet Kohli。

△Pushmeet Kohli，图源谷歌

他的故事，要从二十多年前说起。

2004 年，Pushmeet 还在印度国立技术学院瓦朗加尔分校读计算机本科，一封突如其来的邮件，让他获得了前往美国微软研究院雷德蒙德实验室实习的机会。

在那里，他跟着团队研究如何验证复杂软件系统的可靠性，也由此正式走上了科研道路。

本科毕业后，他前往英国牛津布鲁克斯大学攻读博士学位，并于 2007 年获得博士学位。

此后，Pushmeet 进入微软研究院，一干就是十年，后来一路做到了认知研究团队负责人。

△Pushmeet 在微软研究院时期所做的演讲《人工智能的前沿——认知》

2017 年，他又转身加入 DeepMind，开始带领团队探索如何用 AI 解决科学难题。

从AlphaFold，到AlphaEvolve、AI Co-Scientist，这些年，他参与推动的项目越来越多，研究版图也从生命科学一路扩展到数学、软件和网络安全。

如今，二十多年过去，当年那个初出茅庐的实习生，已经成了 Google DeepMind 独当一面的科研大将。

而他年轻时研究的难题，也终于在 AI 的帮助下迎来了新的解法。

Pushmeet 之外，AlphaProof Code 背后还站着一群大佬。

比如Swarat Chaudhuri，他既是得克萨斯大学奥斯汀分校计算机科学教授，同时也是 Google DeepMind 研究员，长期研究如何将 AI 与形式化验证结合。

△Swarat Chaudhuri

还有密码学领域的老将Jonathan Katz。

他曾在马里兰大学任教二十多年，担任过该校网络安全中心主任，还是 ACM 和国际密码学研究协会（IACR）的双料 Fellow。

△Jonathan Katz，图源马里兰大学

一群深耕密码学、软件验证和 AI 的研究者，就这样聚到了一起。

而在宣布 AlphaProof Code 取得突破的帖子里，Pushmeet 还特意写下了一句话：

总之，我为我的团队成员感到无比自豪。

是啊，二十多年过去，当年那个埋头钻研解法的年轻人终于等到了答案。

真好。

参考链接：

[ 1 ] https://x.com/pushmeet/status/2120127611137634376

[ 2 ] https://deepmind.google/blog/introducing-alphaproof-code/

[ 3 ] https://github.com/google-deepmind/code-verification?utm_source

[ 4 ] https://google-deepmind.github.io/code-verification/#fig-workflow

[ 5 ] https://www.youtube.com/watch?v=qgEOSO8ZlOg

一键三连「点赞」「转发」「小心心」

欢迎在评论区留下你的想法！

—  完  —

点亮星标

科技前沿进展每日见