DeepMind用AlphaProof Code四周內形式化驗證Signal協議

金色財經報道，11月10日，據WIRED報道，Google DeepMind研究人員使用名爲AlphaProof Code的新AI框架，在四周內形式化驗證了Signal協議按預期運行。該分析未在已檢查的協議部分發現新漏洞，但在含已知舊漏洞的舊版Signal上正確識別出已知問題，並顯示該版本無法通過形式化驗證。DeepMind研究科學家Swarat Chaudhuri表示，這是把形式化驗證擴展至全球所有軟件目標的一個里程碑，仍有很長的路要走。研究人員同時公開了爲此次分析開發的規範與證明，以協助其他形式化驗證工作。