DeepMind用AlphaProof Code四周内形式化验证Signal协议

Cointime 消息， Google DeepMind研究人员使用名为AlphaProof Code的新AI框架，在四周内形式化验证了Signal协议按预期运行。该分析未在已检查的协议部分发现新漏洞，但在含已知旧漏洞的旧版Signal上正确识别出已知问题，并显示该版本无法通过形式化验证。DeepMind研究科学家Swarat Chaudhuri表示，这是把形式化验证扩展至全球所有软件目标的一个里程碑，仍有很长的路要走。研究人员同时公开了为此次分析开发的规范与证明，以协助其他形式化验证工作。