1.8 億行證明寫完之後，才是審查的開始：Claude 的形式化驗證到底證明了什麼

2026 年 10 月 23 日，Anthropic 發布與 Theorem 合作的形式化驗證實驗報告：Claude 為 OSS-Fuzz 的 123 個開源函式庫、239 個模糊測試入口產生 Rocq 證明，總量約 1.8 億行。數字很大，但對開發團隊來說，真正有用的問題有兩個：這些證明保障了什麼，以及證明框不到的地方在哪裡。

先弄清楚證明的單位

入口數、函式庫數、證明行數是三種不同的單位，很容易在新聞標題裡被混在一起。這次實驗的證明對象是特定的模糊測試入口：證明某個入口在指定條件下，對小於 64 MB 的輸入會正常結束，不觸發該測試定義的崩潰、記憶體安全錯誤或斷言失敗。一個函式庫可能有多個入口，一個入口對應一份典型約 60 萬行的證明。證明行數既不是函式庫數量，也不是找到的漏洞數量。

用日常比喻：模糊測試像是派一羣猴子隨機亂敲鍵盤，看程式會不會當機。猴子敲得再多，也敲不完所有可能。形式化驗證換一條路，先把「不當機」寫成數學規格，再用邏輯推導證明程式在任何符合範圍的輸入下都成立。猴子找反例，證明找通例。

分工：模型寫證明，檢查器驗證

流程的關鍵在於 Claude 與 Rocq 的分工。程式先編譯成 RISC-V 執行檔，配上形式化的指令集與 Linux 程序模型，再加上「所有小於 64 MB 的輸入都不讓測試崩潰」的規格，交給 Claude 推導證明。Rocq 的核心檢查器再獨立確認這份證明符合規格。Anthropic 的描述很直白：「Claude 撰寫證明；Rocq 核心檢查器依規格檢查證明。」

這個分工有實務意義：模型可能出錯，但證明成立與否由獨立檢查器決定，不靠模型的自我宣稱。這與 OpenAI 把安全主張變成可查核文件 的思路相通，把「我相信它安全」換成「這裡有一份可被機器檢查的論證」。

推導失敗也有價值。一個解壓縮程式的計數器在罕見輸入下發生下溢、導致越界寫入，這個問題就是 Claude 在嘗試證明時暴露的反例。該輸入約 20 MB 且帶特定排列，傳統模糊測試很難剛好撞上。

證明通過，為什麼還不能說程式安全

這是整份報告最值得開發團隊細讀的部分。證明只保證程式符合已寫明的規格，而規格本身依賴一組執行假設：單執行緒、靜態連結的 RISC-V 執行檔、固定記憶體預算、Linux 模型。實際服務常跑在 x86 或 ARM 上、動態連結、搭配不同函式庫，平臺差異直接形成缺口。

範圍問題同樣具體。證明涵蓋某個模糊測試入口，不代表正式產品透過其他 API 呼叫同一個函式庫時也受保護。呼叫端若沒遵守函式的前置條件，錯誤照樣發生。要把保證延伸到實際服務，還得另外寫出呼叫端責任與跨模組互動的規格。Anthropic 在限制說明中寫得明白：「形式化驗證不代表沒有漏洞。」剩餘風險可能來自規格、機器語意模型，或證明未涵蓋的程式行為。

規格本身也要被審。既有測試只把崩潰視為失敗，證明就無法回答輸出是否正確、權限是否合理這類沒寫進規格的問題。AddressSanitizer 能抓部分越界存取，但 Anthropic 指出它偵測不了所有記憶體安全問題。

團隊審查的四個檢查點

從這份報告可以整理出把此類證明納入流程時，審查者實際要看的東西。

一是定理敘述。Rocq 檢查的是推理是否符合定理，不會判斷定理是否回答了正確的產品需求。定理寫錯方向，證明再嚴謹也沒用。

二是版本對應。修補後的程式要重新產生規格與證明；對應修補前二進位檔的證明，不能替修補後的版本背書。Anthropic 也說明，為避免模型用「把程式改成永不崩潰」的捷徑讓定理變容易，他們對程式修改做了限制與稽核。審查者應把補丁與證明一併檢視，確認修補保留了原功能。

三是機器模型與檢查器。執行假設是否貼近實際部署，RISC-V 模型與真實平臺的差距有多大，都影響證明能外推多遠。

四是審查範圍要對照產品實際呼叫路徑。未被測試入口觸及的程式碼、函式庫的其他路徑、呼叫端的錯誤使用，都在證明之外。

值得注意的是，這是 Anthropic Frontier Red Team 與 Theorem 的合作報告，尚未由獨立團隊重現。成果數字屬研究團隊公布的實驗結果，須按各證明的範圍逐一解讀。同樣面對「AI 產出如何取信於人」的問題，OpenJDK 把 AI 生成程式碼擋在門外 選擇了相反方向：不是拒絕 AI 的產出，而是要求產出通過獨立機器檢查。兩條路線的差異，值得基礎軟體維護者放在同一張桌上比較。

對一般團隊的啟示收斂成一句話：這類證明是可查核的證據，不是安全保證。它把「這段程式在這些條件下不會崩潰」從口頭承諾變成文件，而文件的價值，取決於審查者有沒有把規格、版本與呼叫路徑逐一對上實際部署。