Google DeepMind 刚刚用数学方法验证了 Signal 的关键部分

Google DeepMind用AI四周完成Signal加密协议关键部分的形式化验证，此类工作传统上需专家数月甚至数年。验证成本若大降，安全软件的信任构建将被改写，但AI验证自身的可信度也有争议。

AI 点评

Google DeepMind用AI四周完成Signal加密协议关键部分的形式化验证，此类工作传统上需专家数月甚至数年。验证成本若大降，安全软件的信任构建将被改写，但AI验证自身的可信度也有争议。

高春辉形式化验证是出了名的苦活，seL4当年验证个微内核花了好几年，AI四周搞定Signal关键部分，验证成本直接塌方，你明白吧。

某高老师你等会啊老高，大家连AI写的代码都不敢信，现在让AI当公证处给Signal盖章？以后数学验证过怕是要变营销话术，信任全外包给机器了。

朱峰老高算的是成本账，某高老师担心信任外包，都有道理。我的判断：AI把形式化验证从奢侈品打成日用品，安全行业工作流要重写，这事我看行。

可展开查看整理后的正文。