Google DeepMind 的研究團隊完成了對 Signal 消息安全性的形式化驗證，並稱這是首次由人工智慧協助構造出證明，將協議層面的安全保證與一款被廣泛使用的密碼學實現相對應。
這項工作依託 AlphaProof Code 完成，這是一個用於軟件形式化規約與驗證的多智能體框架。流程上，先由人工引導的智能體編寫 Lean 規約、評估機器碼語義，再由智能體生成證明，交由 Lean 內核對照規約逐項檢查。
被驗證的對象是 Signal 的後量子 PQXDH 握手和 Triple Ratchet，從而確認了 libsignal 在前向保密、身份認證、密鑰洩露後的恢復能力以及握手保密性方面的設計。這距離有益人工智能基金會今年 4 月提出的構想又近了一步：該基金會希望用 Lean 形式化驗證 Signal 協議與應用。
具體做法是先與多個模型協作，將 Signal 的安全目標轉成經人工審閱的數學規約，再讓 Gemini Carbon 智能體據此生成 Lean 代碼，證明 libsignal 實現的正確性。智能體累計生成 650 萬行代碼，團隊隨後進行了一輪審計，標出需要人工複核的部分。
Google DeepMind 成功驗證 Signal 消息安全性
“這是一套從根本上為人與人工智慧協作而構建的系統，” Google DeepMind 研究科學家、德克薩斯大學奧斯汀分校教授 Swarat Chaudhuri 說。他表示，傳統做法是數學家將定義清晰的問題交給人工智慧去證明，而這次首先要弄清楚該證明什麼。
