AI 用 600 万行 Lean 证明，把 Signal 的加密代码算明白了

这段代码没有漏洞——这句话在安全行业里几乎没人敢说。但数学可以。形式化验证就是用数学证明代码的行为符合规格，它是安全保证的最高标准，也是最贵的标准。

一分钟速览

• DeepMind 发布 AlphaProof Code，一个用于深度形式化验证的多 LLM 智能体框架；
• 研究对象是 Signal 协议的实际代码，也就是保护数十亿次私密对话的那套技术；
• 智能体由 Gemini Carbon 驱动，生成超过 600 万行 Lean 证明；
• 智能体自审后只标出约 1% 的代码库需要人工复核；
• 这是 AI 首次对广泛部署的加密协议实现如此深度的形式化验证。

它到底做了什么

形式化验证的流程分两步：先把你希望系统满足的安全目标翻译成数学规格，再证明代码实现符合这些规格。第一步需要人，因为什么才算安全是业务判断；第二步极其枯燥，过去靠少数专家一行行推。

AlphaProof Code 的分工很像一个研究团队：人类专家和多个模型协作，把 Signal 的安全目标写成形式化规格，每一条都经人工审核；然后由 Gemini Carbon 驱动的智能体去做证明，产出 600 万行以上的 Lean 代码；最后智能体再回头审计自己的证明，把可疑之处标出来交给人类。

DeepMind 特别强调，这是首次有广泛部署的协议实现被任何方法形式化验证——不管用不用 AI。

为什么这件事比 benchmark 更有分量

模型跑分的意义，在于相对排序；形式化验证的意义，在于结论可以被机器检查。Lean 的证明只要通过编译器，就不存在模型胡编的空间——错一步就过不了。这恰好补上了大模型最被诟病的短板：不可验证。

对安全行业来说，这条路如果走通，意味着关键基础设施——加密库、通信协议、支付清算、航电飞控——的验证成本可能下降一个数量级。过去需要数年、数百万美元的验证项目，也许能压缩到数月。

别急着宣布漏洞绝迹

三点必须说清楚。第一，验证的是代码符合规格，如果规格本身写错了，证明再漂亮也没用，而规格仍然依赖人类专家。第二，DeepMind 没有公布这次验证覆盖了 Signal 协议的多大范围，1% 的人工复核比例是在什么基线上得出的，也需要更多细节。第三，AlphaProof Code 目前是研究框架，不是开箱即用的产品。

但方向已经很清楚：AI 不再只是写代码的工具，也开始承担证明代码是对的这一类高信任度工作。当生成代码的速度远超人类审核速度时，可验证性会变成比生成能力更稀缺的资源。