AlphaProof Code：AI 用 600 万行 Lean 证明了 Signal 协议的正确性

11 月 10 日，Google DeepMind 发布 AlphaProof Code——用 multi-LLM agent 框架对 Signal 加密协议的实际代码完成了形式化验证：把保护数十亿人私密对话（Signal、Google Messages）的协议实现，转化为数学上可校验的安全证明。官方称之为「长期公认的安全大挑战」——这是 AI 第一次被用于对广泛部署的加密协议做这个深度的形式化验证，也是这类部署级协议实现的第一次被任何方法（无论有无 AI）形式化验证。HN 首页 562 分。

怎么做到的：像研究团队一样分工

AlphaProof Code 是一个 multi-LLM agent 框架，把形式化验证的工作按研究团队的分工拆开：人类专家与 AI 协作决定「要证明什么」（把 Signal 的安全目标转译成形式化数学规范，每一份规范都经人类专家审阅）；然后由 Gemini Carbon 驱动的 agent 军团完成证明——生成了超过 600 万行 Lean；最后 agent 审计证明、标出需要人工复核的区域——只有 1% 的代码库需要人看，其余由 Lean 自动校验。

效率的关键就在这个「1%」：Lean 机器校验其余 99%，人类判断力被集中到最需要的地方。

三条线的汇合点

把本周的观察连起来看，这不是孤立事件：CFSG（有限简单群分类）4310 万行 Lean 形式化（10/28）、费马大定理被 1000 个 agent 30 小时形式化（11/10）、OpenAI 的数学发布（10 月）与陶哲轩的 Math 2.0 呼吁——「形式化数学的工业化」本周集中落地。而 AlphaProof Code 把这个范式从数学搬进了软件安全：与 FlashProve（密码学防伪，11/5）、GPT-6 Cyber（攻击侧）同场，「证明」正在成为 AI 时代安全与信任的通用语言。

对企业的启示

其一，安全保证的分级标准要更新了。 「我们做了渗透测试」「我们做了代码审计」之上，新增了「我们做了形式化验证」——对金融、医疗、关键基础设施的软件供应商，这个等级的保证第一次变得可获取（AI 把成本压低了一个量级）。采购关键软件时，值得把它写进问询清单。

其二，agent 军团 + 形式化校验的组织模式可以迁移。 「AI 做重复性证明工作、Lean 机器校验 99%、人只审 1%」这个分工结构，适用于任何有客观校验标准的重复性专业工作——合规对照、合同条款核对、配置审计。关键设计是：校验必须独立于生成者（Lean 内核不归 agent 管），这让「1% 人工复核」变得安全。

其三，注意适用边界：官方强调有人类专家全程参与规范制定，且这是密码学协议而非通用软件——形式化验证成本仍高，并非所有代码都值得。但对传输敏感数据的协议层，这道数学防线第一次触手可及。ProMen 在为企业评估高安全需求的集成方案时，已将「形式化验证的可能性」纳入高敏场景的评估框架。

（本文基于 DeepMind 官方博客实抓报道；技术细节以官方技术论文为准。）