DeepMind 釋出 AlphaProof Code：4 周完成 Signal 程式碼數學驗證

我們每天在手機上傳送端到端加密訊息時，總是下意識地相信通訊絕對安全。但在網路安全的世界裡，最殘酷的現實往往是：哪怕數學上的加密演算法設計得天衣無縫，只要程式設計師在敲程式碼時漏掉一個邊界檢查，整座防禦大廈就會瞬間坍塌。

長期以來，消除這種隱患的終極手段叫「形式化驗證」，也就是用純粹的數學邏輯證明程式碼完全沒有漏洞。然而這種驗證極其耗時費力，通常只有航天或晶片級專案才勉強用得起。

Google DeepMind 拿出了 AlphaProof Code。這個多智慧體框架直接對 Signal 加密協議底層正在執行的生產程式碼完成了形式化驗證，而 Signal 正是守護著 Signal 和 Google Messages 中數十億人私密對話的核心技術。

4 周啃完人類團隊數年的活

以往的形式化驗證大多停留在協議設計層面，根本不敢碰跑在裝置上的真實程式碼，因為設計和實現之間的鴻溝往往藏著無數細節漏洞，證明覆雜度會呈指數級飆升。

傳統方式下，讓人類專家團隊手動把生產程式碼翻譯成數學定理並完成嚴密證明，往往需要好幾年時間。而 AlphaProof Code 把整個週期壓縮到了短短 4 周。

AlphaProof Code 的協作模式很像一個分工明確的研究小組。人類專家先與多種模型合作，把 Signal 的安全目標翻譯成形式化數學規範，並由人類逐條嚴格審查。

隨後，由 Gemini Carbon 驅動的智慧體負責主力證明工作，一口氣生成了超過 600 萬行 Lean 語言程式碼。Lean 是一種能夠以數學精度檢驗程式碼正確性的計算機證明語言。

更聰明的是後續審計流程。智慧體自動篩出其中最關鍵、需要人類二次把關的部分，這部分僅佔整個程式碼庫的 1%。其餘 99% 全部交由 Lean 編譯器自動核驗，讓人類專家把精力完全集中在最具判斷力的核心節點上。

為了驗證這套系統是不是真有辨別力，研究人員還故意往隔離環境的程式碼裡重新塞回了兩個曾經修好的真實歷史漏洞。結果，系統兩次都給出了機器證明，明確判定帶有漏洞的程式碼不安全。

DeepMind 已經宣佈將開源這次驗證的相關產物，供社群研究使用。

為什麼重要

我們認為，AlphaProof Code 的突破不僅僅在於證明了 Signal 程式碼的安全性，更在於它改變了高規格安全防禦的成本結構。

過去形式化驗證之所以沒能普及，純粹是因為人力成本過於昂貴。現在 AI 智慧體把幾年的專家工作壓縮到一個月，意味著這項原本屬於極少數航天或特種領域的「核級防禦」技術，終於有機會下放到醫療裝置韌體、電網控制軟體等關乎現實民生的關鍵基礎設施中。

從技術實現上看，DeepMind 這一步走得相當務實。他們沒有讓大模型直接自由發揮去判定安全，因為模型會產生幻覺；他們把模型限制在嚴格的 Lean 形式化語言環境中，讓確定性的編譯器去當終審裁判，AI 只負責尋找證明路徑。這種「智慧體生成證明 + 嚴謹編譯器驗證」的組合，才是工業級落地的正確解法。

不過，這也並不意味著軟體安全從此高枕無憂。形式化驗證證明的是「程式碼符合人類寫下的數學規範」，如果人類專家一開始對安全目標的描述就存在盲區或疏漏，那麼程式碼依然可能在規範之外被攻破。但無論如何，能把數以億計裝置執行的加密程式碼在數學層面夯死，安全攻防的門檻已經被永久性地拔高了。