AlphaProof Code完成Signal加密实现形式化验证
谷歌DeepMind称，AlphaProof Code已对Signal协议关键代码完成形式化验证，并向社区开放证明材料。
发生了什么
谷歌DeepMind发布AlphaProof Code，一套面向深层形式化验证的智能体框架，并用它验证了Signal即时通信协议底层实现中的关键安全属性。此次对象不是停留在抽象层面的协议描述，而是广泛部署的真实加密代码。研究团队称，这是人工智能首次在如此深度上验证广泛使用的密码协议实现。
这套系统由人工专家与多个AI智能体协同完成，后者由Gemini Carbon驱动。研究人员先把Signal的安全目标转化为Lean形式化规范，再让智能体生成超过600万行Lean证明代码。最终结论并不由模型自行裁定，而是必须通过Lean的机器检查。
为检验系统能否识别真实缺陷，团队还在Signal代码的隔离版本中重新植入两处已修复漏洞。AlphaProof Code均判断对应实现不安全，说明它不只是生成看似合理的证明，而是能够区分正确与错误代码。
为什么重要
形式化验证被视为安全关键软件最严格的保障手段，但长期以来成本高、专业门槛高，通常只能覆盖较小的软件组件。AlphaProof Code显示，智能体或许能把定理证明扩展到规模更大的生产代码库。未来，医疗设备、工业控制系统和关键基础设施软件都可能成为受益对象。
当然，这一成果仍有边界。安全规范由人类专家制定并审核，论文验证的也是Signal实现中的特定范围，而非整个应用的所有属性。即便如此，真实协议、机器可检验证明以及开源材料的组合，使它明显超越了普通基准测试演示。
猫叔判断
600万行Lean证明很亮眼，但真正昂贵的环节仍是定义“安全”本身；AI能加速证明，却还替不了规范审查。