发生了什么
谷歌 DeepMind 11 月 10 日公开 AlphaProof Code，一套由多个智能体协作、把形式化证明写进 Lean 的验证框架。首个应用对象不是示例工程，而是 Signal 协议的参考实现 libsignal：团队用 libsignal-protocol 0.105.4 与抗量子扩展 SPQR 1.6.0，配自研测试程序，经 rustc 1.98.1 编译出面向 Linux AArch64 的静态二进制，约 560 KB、约 14 万条指令，验证直接落在这份机器码上。
分工是「人定规格、机器写证明、内核做检查」。研究人员先把 Signal 的安全目标翻译成 Lean 可理解的数学规格并逐条人工审核，再由 Gemini Carbon 驱动的智能体自动构造证明；整个周期四周，产出约 650 万行 Lean 证明，建立在大约 2.6 万行形式化规格与机器码语义之上。智能体还会主动标出需要人工再看的部分，约 1% 的代码库进入复核。
为什么值得看
- 验证层级：不是只证协议设计，而是证编译后真正跑在设备上的机器码，把「设计安全、实现有洞」这段缝隙纳了进来。
- 反例能力：团队把两个历史上真实存在、后来已修复的漏洞重新植入隔离副本，框架都生成了机器可检查的反例证明，认定该版本不满足原有安全要求。
- 覆盖面：限于一对一通信中 PQXDH 的会话建立与 Triple Ratchet 的收发行为，涉及前向保密、妥协后安全等若干项明确列出的属性。
- 可复现：DeepMind 表示把规格与证明工件对外开源，供社区检查与复用。
边界在哪
三条限制必须写清。第一，证明只说明代码满足已经写出来的规格，规格之外的安全需求不在覆盖范围；那 2.6 万行可信规格与处理器语义本身仍要专家评估，它们是整套论证的地基，地基错了，结论再严密也没有意义。第二，验证对象是单个 Linux 二进制加一组明确的密码学假设与运行环境前提，不等于 Signal 应用整体安全。第三，目前没有独立第三方审计；「首次对广泛部署的密码协议实现做到这一深度」属于企业口径，且官方博客写的「六百万行以上」与媒体转述的三百万行存在差异，尚无法从公开材料对齐。
对工程团队的意义
形式化验证过去是成本最高的一档保障手段，重要系统常需专家团队数年。这条路径可复制的部分，是把规格定义、证明搜索、机器检查三段拆开：人只保留最容易出错也最需要判断的规格与复核，Agent 承担人力最密集的中间段。短期它不会替掉测试与代码审计，但对密码、支付、车控这类容错空间极小的模块，多了一种可机器复查、可交付给审计方的证据形式。