2026 年 11 月 10 日，Google DeepMind 在官方網站介紹了 AlphaProof Code。這是一個把人類專家與 AI agent 結合起來、用於形式化驗證的框架，不是新的聊天模型上架。

研究人員用它證明了 libsignal（Signal 協議參考實現）的選定關鍵安全性質，並把證明做到編譯後的機器碼／AArch64 層面。官方網站博文把所涉技術寫成保護 Signal 與 Google Messages 中海量私密對話的技術。論文寫明，結果針對本次 libsignal-cli 構建，不是 Signal 自家應用。

論文與產物頁寫，agents 生成了約 650 萬行經機器檢查的 Lean 證明程式碼；官方網站博文正文則寫超過六百萬行 Lean。

論文寫，證明覆蓋 Signal 的後量子 PQXDH 握手與 Triple Ratchet，並建立前向保密、認證、失陷後安全與握手保密。論文把這些結果表述為：把協議層安全保證連接到廣泛使用的密碼協議實現之未修改程式碼的首次證明。

證明由 Gemini Carbon（論文作 Gemini 4 Carbon）驅動的 agent 完成。規格由人類與模型協作起草，並由人類專家逐條審閱。論文還寫，規格階段使用了 Claude Opus 5.5，但證明是由 Gemini 4 Carbon 的 agent 團隊寫出的，作者沒有手寫證明程式碼。該模型的既有介紹發布於 2026 年 10 月 28 日；這並不構成 Carbon 的新一次 API 或價表發布。證明所用模型的既有介紹（不是今天發布）見：Google 發布 Gemini 4 Carbon：下一代前沿模型。

官方網站博文寫，驗證過程用了四周；論文補充為五人團隊用四周完成證明工作。

官方網站把「首次」限定為：AI 首次在這一深度對廣泛部署的密碼協議做形式化驗證；也是像這樣廣泛部署的協議實現首次被任何方法（無論是否使用 AI）形式化驗證。這不是聲稱整個 Signal 應用，或全部可能的失敗模式，都已得到驗證。

為確認該框架能區分正確程式碼與有缺陷的程式碼，研究人員把兩個此前已修復的真實漏洞再引入隔離版本。兩種情況下，系統都給出了「有漏洞版本不安全」的機器檢查證明。這是迴歸測試，不是發現 Signal 的新漏洞。

Signal 技術長 Ehren Kret 在官方網站博文中表示：「此前的形式化驗證主要針對程式碼中較小的部分，Google DeepMind 的方法使範圍得以顯著擴展。用 AI agent 把實際運行的程式碼翻譯成有效的 Lean 定理，是一項重大突破。隨著 AI 驅動的安全威脅增加，嚴格驗證 Signal 協議實現，讓我們對其程式碼的隱私保證更有信心。」

驗證產物與技術論文已公開。