Google DeepMind于2026年11月10日发布AlphaProof Code，使用Gemini Carbon驱动的多Agent系统，对Signal协议核心代码进行了机器级形式化验证。系统生成约650万行Lean证明，并由Lean内核检查。重点不是AI“看起来认为代码安全”，而是证明能被独立的形式化工具验证。
普通测试与形式化验证的区别
单元测试只能覆盖选定输入，静态扫描寻找已知模式，形式化验证则先写出必须满足的数学性质，再证明实现对所有规定状态成立。它仍依赖规格是否正确：如果人类写错了安全目标，证明再完整也不能覆盖遗漏的风险。
AlphaProof Code的流程
第一步由人类专家和模型共同把Signal安全目标转成Lean规格，并逐条审批；第二步多个Agent生成证明；第三步可信的Lean内核验证证明；第四步系统标出约1%需要人工重点检查的区域。研究还把两个已修复漏洞重新放入隔离版本，验证系统能证明错误版本不安全。
为什么验证到机器代码
协议设计正确，不代表编译后的实现没有偏差。编译器优化、内存布局和底层指令都可能引入问题。AlphaProof Code对AArch64机器代码建模，试图缩小设计与真实运行代码之间的鸿沟。企业落地时也要明确验证的是源代码、编译中间表示还是最终二进制。
普通团队怎么开始
不要直接挑战整个系统。先选择权限判断、金额计算、加密封装或状态机等边界清晰模块，写出输入、不变量和禁止状态。让AI协助补充证明，再由熟悉业务和形式化方法的人审核规格。证明文件纳入版本控制，代码改变后自动重新验证。
站内AI数学成果与Lean验证介绍了机器检查思路，GPT-6 Cyber漏洞修复则属于发现与修补路线，两者可以互补。
不能忽略的边界
形式化证明不会自动覆盖密钥管理、社会工程、部署配置、侧信道和业务流程。规格编写仍需要专家，生成证明也可能消耗大量算力。对高风险系统，应把形式化验证、代码审计、渗透测试和运行监控组合使用。
结论
AlphaProof Code展示了AI最可靠的一类用途：生成复杂工作，再交给确定性验证器检查。它不是让模型替代密码专家，而是把专家精力集中到规格与少量关键区域。
