Google AI 首度證明 Signal 實際程式碼安全，四週完成
Google DeepMind 11 月 10 日在官方部落格發表 AlphaProof Code，用一組 AI 代理以數學方式證明，Signal 加密協定在裝置上實際執行的程式碼，符合專家設定的主要安全性質。Signal 協定除了 Signal 本身，也用在 Google Messages 等通訊軟體，保護數十億則私人對話。
DeepMind 說，這是 AI 第一次在這個深度，形式驗證一套廣泛使用的加密協定；不論用不用 AI，這類協定的「實作」被完整形式驗證，也是第一次。整個驗證花了四週，DeepMind 說傳統上要專家團隊花好幾年。
過去只驗設計圖，這次驗到編譯後的程式碼
形式驗證是用數學證明程式照規格運作，沒有漏洞，被視為最高等級的資安保證，但非常耗人力。DeepMind 說，大多數協定驗證只做到設計層，證明「設計」是安全的；真實世界的漏洞，卻常藏在設計和實作之間的落差。
廣告 - 內文未完請往下捲動
這次 AI 代理一路證明到編譯後的程式碼，例如裝置暫時被入侵前後，訊息仍受保護這類性質，都驗證到裝置上實際執行的那一層，證明難度也因此大幅提高。
600 萬行 Lean 證明，人只需看其中 1%
AlphaProof Code 把工作拆成研究團隊的分工：人類專家和 AI 一起決定「要證明什麼」，再交給一群 AI 代理去證明。
第一步，研究人員和多個模型合作，把 Signal 的安全目標翻成形式化的數學規格，每一條都由人類專家審過。接著由 Gemini 4 Carbon 驅動的代理動手證明，寫出超過 600 萬行 Lean。Lean 是一種用來寫數學證明的程式語言，電腦會自動檢查每一步。
最後，代理自己稽核證明，標出需要人類再看一次的地方，只占整份程式碼的 1%；其餘部分由 Lean 自動檢查，專家只需把時間花在真正需要判斷的地方。
把兩個已修好的舊漏洞放回去，系統都抓得出來
為了確認 AlphaProof Code 分得出正確和有問題的程式碼，研究人員在隔離環境中的 Signal 程式碼裡，重新放回兩個過去真實存在、已經修掉的漏洞。兩次系統都產出經機器檢查的證明，指出有漏洞的版本不安全。
Signal 技術長 Ehren Kret 在部落格中說，過去的形式驗證只能涵蓋較小範圍，要確認正式上線的程式碼嚴格符合加密設計，需要大量人工；用 AI 代理把線上程式碼自動翻成有效的 Lean 定理是「很大的突破」。他說，AI 驅動的資安威脅越來越多，核心協定經過嚴格驗證，讓 Signal 對自家程式碼的隱私保證「更有信心」。
證明檔已開源，下一步瞄準醫療設備與電網
DeepMind 已把這次的形式驗證成果開源，並附上技術論文。DeepMind 說，同一套方法可以用在醫療設備韌體、電網軟體等關鍵系統，但要擴大規模還需要更多研究。
用 AI 做形式驗證，近期不只 DeepMind 在做。Anthropic 10 月與 Theorem 合作，用 Claude 形式驗證 123 個開源函式庫，過程中找出數百個錯誤。以太坊共同創辦人 Vitalik Buterin 在 Devcon 8 開幕演講中，也主張以開源、可驗證取代單純信任，點名晶片、通訊、AI 等領域都需要可以被驗證。
風險提示
加密貨幣投資具有高度風險，其價格可能波動劇烈，您可能損失全部本金。請謹慎評估風險。
