Google DeepMind 表示，已使用 AlphaProof Code 對 Signal 協定的機器碼進行正式驗證

Google DeepMind 的 Pushmeet Kohli 宣布，他的團隊已證明 Signal 訊息協定底層機器碼的關鍵安全性質。DeepMind 表示，這是首次有人以任何方法、在如此深入的層次，對廣泛部署的協定正式環境程式碼進行形式化驗證。以上皆為 DeepMind 自身的說法。

這項工作使用了 AlphaProof Code。DeepMind 將其描述為一種新的代理式形式化驗證框架，採用包括 Gemini Carbon 在內的 LLM。DeepMind 表示，驗證深入至裝置上執行的程式碼，約耗時一個月；類似工作原本可能需要多個團隊合計投入數十年。DeepMind 也將 Signal 團隊列為合作夥伴。

DeepMind 正以開源方式釋出其形式化規格和驗證產物，供其他人據此繼續開發。截至 11 月 10 日上午，該貼文在 X 上獲得 1,297 個讚。