DeepMind 用 AI 工具形式化验证 Signal 协议安全

Google DeepMind 研究人员借助新 AI 框架 AlphaProof Code，在四周内完成 Signal 协议的形式化验证，确认当前受检协议部分未发现新漏洞，且可正确识别存在已知旧漏洞的旧版 Signal 的问题，判定其无法通过验证。该成果是形式化验证向全球各类软件拓展的里程碑，相关研究人员已公开本次分析开发的规范与证明，为其他形式化验证工作提供助力。