2026 年 11 月 10 日，Google DeepMind 的 Pushmeet Kohli 與 Swarat Chaudhuri 在官方部落格發布了〈Introducing AlphaProof Code: a breakthrough in verifying complex software at depth〉。這篇 AlphaProof Code 解讀，要回答的是：當 AI 替 Signal 的密碼協定程式碼寫出安全性證明，我們究竟多知道了什麼，又有哪些問題仍在證明範圍之外？
先看原文的工作方法，再對照論文與既有研究，最後判斷它對軟體安全的真正意義。先給結論：值得重視的是把協定安全性連到特定編譯結果的證明工程；信任仍落在規格、假設與執行環境上。
一、AlphaProof Code 把什麼接起來：安全設計與實際程式碼
測試像拿幾把鑰匙試門；形式驗證則先把「哪些人、在什麼條件下，應該打不開哪扇門」寫成精確命題，再證明所有符合模型的情況都滿足它。力量來自這個全稱範圍，限制也來自同一個地方：門、鑰匙與攻擊者如何定義，會決定證明回答了哪一題。
原文的核心訴求是跨過設計與實作之間的落差。協定論文可以描述一套安全的密鑰更新規則；真正交付的程式仍要處理狀態儲存、訊息順序、錯誤分支與編譯結果。這次團隊把未為了驗證而改寫的 libsignal 程式碼，接進小型命令列測試框架，編譯成 AArch64 Linux 執行檔，再以 Lean 描述的機器執行語意進行推論。
這裡的「機器碼層級」有具體對象。技術論文第 4 節列出 libsignal-protocol v0.105.4 與 spqr v1.6.0 的一對一會話程式碼；底層密碼原語等部分被替換為具有契約的呼叫模型。讀成某個建置及其假設下的保證，才能保留這項成果的精確性。
二、誰出題、誰證明、誰驗收？三種角色不能混在一起
AlphaProof Code 將工作拆成三層。人類專家與模型反覆討論規格，決定安全命題及假設；證明 Agent 團隊嘗試完成它；最後由 Lean 核心與比較工具檢查證明，以及它是否仍對應核准的命題。研究論文說，規格工作使用不同模型家族交叉審查，證明部分由 Gemini 4 Carbon Agent 團隊產生。
Every proof is checked by Lean to verify the agents’ work.
中文：每份證明都交給 Lean 檢查，以核對 Agent 的工作。
Google DeepMind 原文
圖中的分工很關鍵。即使 Agent 會出錯，完成的形式證明仍可以交給另一套明確規則檢查。然而，Lean 檢查的是「這個命題是否被合法推出」；命題是否夠強、是否描述了你在意的風險，還需要審查。這也是研究採用獨立保留規格副本與 comparator 的理由：避免 Agent 為了交卷，悄悄把題目改簡單。
論文第 7 節也記錄了防止弱化規格的流程：在乾淨環境重放證明，拒絕以 sorry 等方式跳過證明，並審查規格修正。這種「生成者與驗收者分工」的想法，可接著讀 Agent Harness 的角色與邊界；只是這裡的驗收標準，是形式定理及其完整依賴。
三、四週與 650 萬行：要把成績的分母一起讀
依論文第 7 節，這次證明工作由五人團隊，在四週內平行推進；約 650 萬行 Lean 證明碼，依賴約 18,000 行需要審閱信任的陳述與定義，再加上約 8,000 行 AArch64 語意。這些數字是作者對本次研究的報告。本篇查閱公開論文、規格與程式庫，未執行完整的本機重建與核心重驗。
650 萬行表示生成與檢查的工程規模，不直接衡量安全保證有多廣。規格中的一項前提改變，就可能比新增一百萬行證明更影響結論。同樣，四週是這組團隊在這次任務的經過時間；它建立在既有協定研究、工具與人工指導上。把它直接換算成「任何安全驗證都能加速幾十倍」，缺少同條件比較。
原文把應用方向延伸到醫療設備、電網與關鍵基礎設施。這是值得追蹤的研究願景；每種系統仍須重新定義環境、故障與安全條件。若要評估模型是否適合自己的工程任務，模型排行榜的交叉判讀可以補足另一個觀念：單一數字總要回到它實際回答的問題。
四、Signal 的哪些安全性被討論，哪些量子保證要分開？
先把三個常見名詞分開。前向保密希望未來的密鑰洩漏，不會回頭解開已受保護的過去訊息；入侵後安全性希望攻擊者取得某次狀態後，會話仍能在符合條件的新密鑰交換後恢復保護；身分驗證則約束訊息或會話能否被冒充。每一項都要連同論文對攻擊者與洩漏時點的定義一起讀。
Signal 在 2025 年 10 月的 SPQR 說明中，解釋了 PQXDH 用於啟動會話，而 Triple Ratchet 結合既有 Double Ratchet 與稀疏後量子棘輪。這是一手背景，但「協定設計想提供什麼」與「本次研究已證到什麼」仍有距離。
DeepMind 論文提供兩條證明路線。符號模型把密碼運算理想化，並把機器碼執行連到協定事件；計算模型則把攻擊成功率，連到密碼假設與明確的機率上界。兩種模型的假設、攻擊者及範圍不同，不能把各自最強的句子拼成一張無條件保證。
量子這一點尤其要讀小字。第 5.1.6 節明說，棘輪定理顯示的是 Triple Ratchet 不弱於 Double Ratchet，並未證明 SPQR 新增的後量子恢復能力；第 5.2.5 節也明說，計算模型的上界不提供對量子攻擊者的保證。符號路線中的部分握手保密結果，不能擴大成「整個 Signal 的抗量子安全都已由 AI 證明」。
五、兩個舊漏洞與公開成果：能檢查，比漂亮的成功宣告更重要
原文說，團隊把兩個已修復的真實漏洞重新放回隔離版本，再證明錯誤版本不滿足安全定理。這是對規格強度的測試：如果好程式和帶缺陷程式都能過關，可能是題目訂得太弱。
這兩個問題有獨立的研究前史。Cheval、Jacomme 與 Richards 的 原始研究介紹記錄了協定分析、實作中確認的問題及後續修復；DeepMind 論文第 6 節則交代，將上游修復反向套用到指定版本後，再建立反例證明。因此，這個展示應讀成對已知缺陷的回歸檢驗，不能改寫成 AlphaProof Code 新發現兩個 Signal 漏洞。
截至 2026 年 11 月 11 日，公開程式庫及審閱網站已可讀取。README 提供建置、二進位檔指紋與 comparator 驗證步驟，也指出 comparator 流程依賴 Linux 沙箱。這讓外部研究者有具體材料可以挑戰；公開材料的存在，和外部團隊已完成重現，是兩種不同證據。
六、安全證明的邊界：論文自己列出的限制
讀第 5.1.6、5.2.5 與 5.3 節，可以把最容易被標題省略的條件放回來：
- 對象有界：結果針對研究團隊建置的 libsignal-cli；計算模型採固定長度訊息，且未包含多裝置狀態。它不是 Signal 應用程式各層功能的總驗收。
- 攻擊情境有界：符號模型將旁通道及記憶體中其他祕密列在範圍外；計算模型則對部分初始握手訊息注入與洩漏時點有限制。
- 信任仍有底座：Lean 核心、AArch64／Linux 執行模型、被掛接函式的契約，以及密碼原語的假設，都是理解結論的一部分。
- 機率界線有適用規模：作者指出，在幾乎每則訊息都啟動新 epoch 的情境，單一會話約 25,000 則訊息時，計算上界可能失去有效約束。這是該證明上界的限制，不能推成 Signal 在那一刻就會被破解。
這些限制不會抹去已成立的命題，卻會改變讀者能做的推論。密碼協定核心的形式保證，可以和應用程式測試、平台安全及部署審查相互補充；把其中一層當成全部，反而失去形式驗證最有價值的精確性。
七、AlphaLab 的判讀：證明成本下降後，出題能力更值錢
once proofs become cheap, the hard question is what to prove.
中文：當證明變得便宜，難題就變成該證明什麼。
研究論文第 7 節
我同意的，是這種分工值得擴大。讓模型承擔大量推導，再交給可檢查的形式系統驗收，比只相信一段「我已檢查安全」的自然語言回答，多了一條可追查的證據鏈。把鏈條延伸到指定機器碼，也直接碰到實作與設計可能分離的問題。
我存疑的，是把這個案例直接換成普遍成本與普遍安全承諾。五人四週的成果，仍包含專家的選題、反覆修規格、安排證明策略與維護 Agent 工作流程。論文也記錄，早期小幅程式或二進位變動曾需要大量修補證明。要評估能否進入日常開發，下一張成績單應該是版本更新後，維護同一套保證要花多少時間與資源。
更值得警惕的是驗收者也被生成者一起改掉。若讓 Agent 同時改程式、改安全定義，再自己宣告完成，形式系統可能精確證明了一個已經被削弱的題目。把規格副本、修正權限與最終檢查分開，才是這項研究對一般 AI 工程最可移植的啟發。
八、現在能做什麼：把「安全嗎」改成可逐項回答的問題
讀到下一則「AI 證明某軟體安全」的消息時，先問四件事：哪個版本與建置？哪條命題？哪些假設與排除情境？誰能用公開材料重新檢查？這四個答案，比證明碼行數更適合拿來判斷保證的價值。
如果你在做開發，先挑一個範圍小、失敗後果清楚的元件，寫下正常執行應滿足的條件，再放入一個已知錯誤版本，觀察驗收是否真的拒絕它。AI Evals 入門能幫你先建立可重跑的測例；要把生成、工具執行與驗收串起來，最小 Agent Harness則提供另一個起點。測例與形式證明各有用途，選擇時要說清楚它們涵蓋哪些失敗。
對一般讀者，這項消息適合增加一份對研究進展的理解，而不是把自己的風險判斷全部交給一個「已驗證」標籤。最值得追蹤的下一步，是外部重建、信任底座的審查，以及新版本能否持續維持同一組安全命題。
接著閱讀
左右滑動查看更多推薦