Google DeepMind 於 2026 年 11 月 10 日介紹 AlphaProof Code，說明研究人員與 AI Agent 如何合作，對 Signal 參考實作 libsignal 的部分安全性質進行形式驗證。
研究人員定義並審閱 Lean 規格，AI Agent 產生證明，Lean kernel 核對證明。研究團隊將編譯後的 AArch64 機器碼納入驗證流程，檢查 PQXDH handshake 與 Triple Ratchet 等機制中的指定安全性質。
團隊也在隔離的 Signal 複本中重新加入兩個先前已修復的錯誤，並檢查工具能否辨識不安全的程式狀態。研究報告指出，Agent 產生約 650 萬行 Lean 證明程式碼，由 Lean 核心檢查。
這些結果適用於研究者定義並審閱的規格、機器碼模型與程式範圍。形式證明的保證取決於規格與模型涵蓋內容，不能直接推論為整個產品或任意程式都沒有漏洞。
這項研究展示一種分工：人員界定並審閱要證明的性質，Agent 協助產生證明，可信任的 Lean checker 核對證明結果。
想用 Codex 練習程式弱點檢查，可參考「Codex 資安修補實戰」套裝。套裝目前包含 4 門課、37 個已發布單元，影片總長約 1 小時 38 分鐘，售價 NT$590。課堂使用合成 Node.js 專案，練習受控工作區、弱點驗證、身分與授權修補，以及輸入、檔案與機密風險處理。課程不包含 AlphaProof Code、Lean 或 Signal 形式驗證教學。
套裝資訊與目前方案：
https://www.mokoversity.com/courses/bundles/codex-security-remediation
Google DeepMind 官方文章：
https://deepmind.google/blog/introducing-alphaproof-code/
研究論文：
https://deepmind.google/documents/36/Formal_Verification_of_Signal_4.pdf
Google Analytics 使用選擇
網站使用 Google Analytics 了解公開頁面的使用情形。未接受前不會載入分析工具。你可以接受或拒絕，之後也能在隱私權政策調整。