AI花四周给Signal加密做了一次“数学体检”：关键安全性质首次在真实代码层被证明 ↗
保护数十亿人私密聊天的Signal加密协议，过去只能“在设计图上”被数学证明安全，真正跑在手机里的代码一直没人能完整证明。谷歌DeepMind 11月10日称，其AI框架AlphaProof Code用约四周，对Signal实际代码的关键安全性质完成了形式化证明——过去这类工作往往要专家团队花上数年。把两个已修复的真实漏洞重新放回测试副本后，系统也都证明了“这个版本不安全”。注意：被证明的是专家审定的那几项关键性质，并不等于整个Signal应用绝对没有漏洞；以上均为DeepMind自己公布的结果。