AI coding · 四周，六百万行证明：Signal 密码学实现第一次被机器逐行验收

测试这门手艺有一句老实话：它只能证明错误存在，永远证不了错误缺席。对聊天软件，这只是体验问题；对端到端加密协议，这直接关系安全本身。形式化验证——把"代码正确"写成一条数学定理，交给机器逐行核对——几十年来被公认为最彻底的路线，也是最贵的一条：专家团队熬上数年，覆盖到的往往还只是设计文档；实际跑在几十亿部手机上的那份实现，通常不在验证名单里。

11 月 10 日，Google DeepMind 发布 AlphaProof Code，一份针对这道题的答卷：给 Signal 协议的核心密码学实现配上机器可查的证明。Signal 是现代端到端加密的地基之一，WhatsApp 等覆盖几十亿用户的聊天应用都踩在它上面。按 DeepMind 的口径，这是广泛部署的加密协议实现在这个深度上的首次完整形式化验证，此前被该领域视作 grand challenge。

流程分四步。第一步，人类专家与模型一起把安全目标翻译成形式规约，每一条规约都由人批准；第二步，由 Gemini Carbon 驱动的各 agent 在 Lean 定理证明器里生成证明；第三步，Lean 逐条机器验收——证明对了就是对了，没有中间态；第四步，agent 审计全部证明，把剩余风险压缩到约百分之一的代码量，交回人类。产出是六百多万行 Lean，用时四周。这种工程在历史上的报价单是"年"。

为防这套流程自说自话，团队做过一次反向实验：把两个已修复的真实漏洞重新塞进一份隔离副本，系统都在机器可查的证明里给出判定——这两个版本不安全。连"验证器自己灵不灵"这个问题，也顺手验了一遍。

另一个卖点是深度。证明的对象是实际部署到设备上的那份代码，设计文档与实现之间的缝被填上了——包括设备被临时攻破时的消息保护性质。验证产物开源，论文同步挂出，合著者名单里有密码学家 Jonathan Katz；Signal 的 CTO Ehren Kret 给了一句克制的好评，大意是把活代码翻译成成立的 Lean 定理，是件大事。

这条产品线有家谱可查。2024 年 7 月 AlphaProof 在 IMO 摸到银牌线，2025 年推进到研究级数学，2026 年 10 月 Gemini Carbon 发布，一个月后这套框架落在软件上。对写代码的 AI 来说，这是一次岗位扩张：生成代码各家都在做，验收代码这门生意刚刚开张。安全审计行业里最贵的那种审计，报价单正在被重写。

密码学的形式化验证曾是一门靠奖学金和耐心支撑的手艺。现在它有了产能。剩下的悬念只有一个：下一份被逐行验收的代码，会是哪家的基础设施。