Google DeepMind 用 AlphaProof Code 验证 Signal 协议实际代码的关键安全属性

Google DeepMind 研究人员让 AI 智能体与人类专家协作，对 Signal 协议的实际代码进行形式化验证，证明其符合指定的关键安全属性。研究团队称，验证耗时四周；他们还将两处已修复漏洞重新加入隔离版本，系统均给出了机器可检查的“不安全”证明。该方法的扩大应用仍需研究。