Claude 寫出 239 份『不會當機』的數學證明：AI 驗證軟體，走到量產門口了嗎

Anthropic 與 Theorem 在 10 月 22 日公布的研究中，讓 Claude 為 123 個開源函式庫寫出機器可檢查的形式化證明，總量約 1.8 億行 Rocq 證明碼。

找漏洞與證明沒有漏洞，是兩件難度完全不同的事。Anthropic 在 10 月 22 日與軟體驗證公司 Theorem 共同公布的研究，嘗試把後者交給 AI：Claude 為 123 個開源函式庫的 239 個模糊測試入口，寫出了機器可以逐項檢查的形式化證明，證明這些程式在特定條件下不會因記憶體安全問題或斷言失敗而當機。

從模糊測試出發，把測試變成規格

研究團隊的做法，是把現成的模糊測試當成規格來源。函式庫與測試先被編譯成 RISC-V 執行檔，並以 AddressSanitizer 插樁；接著由 Theorem 的 RISC-V 與 Linux 行程語意，機械式地推導出「不得當機」的規格；Claude 再以 Rocq 證明助手寫出證明，由 Rocq 檢查器驗證證明是否成立。證明一旦失敗，往往指向程式裡的真實缺陷，團隊修補後重新產生規格、再證一次。

整批證明的規模相當驚人：總量約 1.8 億行 Rocq 證明碼，單份證明平均約 60 萬行，對應的二進位檔中位數約 1.8 萬道 RISC-V 指令。團隊表示，這是據其所知首次大規模把 AI 形式化驗證用在生產軟體的組合語言層級；過程中也找出數百個缺陷，包括模糊測試跑了上兆次仍未觸發的隱藏問題，以及某款廣泛使用的 PDF 閱讀器裡潛伏十多年的邏輯錯誤。

「已證明」不等於「沒有任何漏洞”

這份成果的邊界，必須和規模一起讀。首先，證明只涵蓋單執行緒的靜態二進位檔、固定記憶體預算、RISC-V 處理器與 Linux 環境，輸入上限為 64 MB；多數人實際使用的 x86 或 Arm 搭配 glibc 的部署，並不在同一份證明範圍內。其次，證明的是「不會因特定條件當機」，不是整套函式庫在所有面向都正確無誤；呼叫端誤用等情況也不在規格內。最後，證明成本仍然高昂，單份證明可能耗費數億個 token，雖然 Opus 5.5 在 36 項小型驗證任務上比上一代省約四成 token，但距離便宜到隨手可用還有一段路。

儘管如此，這項研究的意義在於把形式化驗證從專家手工藝推向可複製的流程：過去為 seL4 這類核心寫證明要花上數十年人力，如今 AI 能在數週內產出大批機器可驗的證明，並把部分證明、語意模型與未證出的測試規格公開。對軟體供應鏈而言，若驗證成本持續下降，「先證明再上線」有可能從少數關鍵系統的特權，變成開源生態系的常規工序。

資料來源

• Anthropic（2026 年 10 月 22 日研究公布）
• Theorem（oss-verify-proofs，GitHub）
• Unite.AI（2026 年 10 月 22 日研究整理）