Google DeepMind 於 11 月 10 日發表 AlphaProof Code——一套結合人類專家與 AI 代理的**軟體形式驗證（formal verification）**框架，並將其應用於 libsignal，即 Signal 通訊協定的參考實作（該協定同時運行於 WhatsApp 與 Google Messages）。AI 代理為此生成了約 650 萬行 Lean 證明，覆蓋通訊安全的核心保證；同一日 Google 宣布 Gemini 4 Carbon 全面開放，兩者互為表裡。
研究重點
方法：人寫規格，AI 生成證明
- 人類研究員與運行在 Gemini 4 Carbon 及 Claude Opus 5.5 上的代理協作，先撰寫「需證明什麼」的規格（specifications）。
- 之後由 Carbon 驅動的代理生成全部約 650 萬行 Lean 證明；Lean 證明檢查器會自動拒絕任何無效證明，形成嚴格的品質閘門。
- 五人團隊在四週內完成這項工作——DeepMind 表示，這類工作傳統上需要專家耗時數年。
證明涵蓋編譯後的機器碼
- 驗證的保證包括前向保密（forward secrecy）、後洩漏安全（post-compromise security）與認證（authentication）。
- 關鍵差異在於：多數協定驗證只檢查設計層面，而此次證明覆蓋實際編譯後的機器碼。
方法學驗證與研究限制
- 團隊刻意把兩個已修補的歷史漏洞重新植入程式碼，並成功證明這些建置會破壞安全保證——證明該框架有能力抓出真實缺陷。
- 結果涵蓋 Google 自身建置、經由小型命令列包裝執行的版本，並非 Signal 自家應用程式；部分分析亦排除側通道（side channel）。
為何重要
其一，形式驗證的經濟性正被 AI 改寫。研究團隊直言：「結果表明，AI 能讓形式驗證——過往對大多數軟體而言過於昂貴——對真實世界的系統變得可行。」對銀行、關鍵基礎設施與加密通訊等高度敏感的程式碼，這項成本的崩塌意義重大。
其二，「代理人驗證」與 Carbon 的資安定位彼此呼應。Google 同日擴大 Carbon 存取（首發優惠價每百萬輸入 token 2 美元至 11 月 30 日），並稱 Wiz 以 Carbon for cyber 在兩小時內於兩家大型 SaaS 供應商找到 0-day；其 CVR 漏洞研究團隊則用它確認兩個開源專案漏洞可利用，嚴重性堪比已被實際利用的 PHP2Shell 漏洞。「AI 寫程式 + AI 驗證程式」的閉環正在成形。
其三，對軟體供應鏈安全的啟示：當 AI 代理能自主生成數百萬行形式證明，審計成本大幅下降，「證明軟體做了它聲稱的事」可望從學術理想變成常態化執行的工程紀律——但對開源生態而言，也意味著頂級驗證能力可能集中在握有前沿模型的少數實驗室手中。
本文信息來源：SecurityWeek 報導、The Neuron 每日摘要。