不是又一個 AI 抓 bug 的故事

Anthropic 在 10 月 22 日發表〈LLMs are making formal software verification feasible at a much larger scale〉，說明它和 Theorem 合作，讓 Claude 替 OSS-Fuzz 裡 123 個開源函式庫、共 239 個進入點，寫出由機器檢查過的 Rocq 證明。過程中找到的 bug，Claude 也自己修補，再重新證明。

如果你維護 C/C++ 函式庫，或負責軟體供應鏈的資安，這件事值得看的不是「AI 又找到 bug」，而是形式化驗證過去要專家花大量人力，現在被做成可以大批產出的東西。這篇文章在 Hacker News 上約三天累積 460 points、310 則留言，前排留言問的多半不是 bug 數量，而是「證明的到底是什麼」。

這也是讀者最容易誤會的地方：「formally verified」不等於沒有 bug。Anthropic 和 Theorem 都自己把這點講清楚了，我們接下來就照著他們寫下的邊界，一條一條看。

fuzzing 試很多輸入，證明管所有輸入

先看他們做了什麼。OSS-Fuzz 上的函式庫本來就有 fuzz test，也就是一段把隨機輸入餵進函式庫的測試程式。fuzzer 會試非常多輸入，但永遠試不完。Anthropic 的做法是把同一個 fuzz test 改寫成一個要證明的命題：對任何小於 64 MB 的輸入，這個 fuzz test 都不會崩潰。

接著把函式庫和 fuzz test 編譯成 RISC-V 執行檔，由 Claude 寫證明，再交給 Rocq 的證明檢查器核對。OSS-Fuzz 原本就用 AddressSanitizer（ASan）編譯，記憶體錯誤會讓程式直接崩潰，所以「證明不會崩潰」也就涵蓋了 ASan 能抓到的這類記憶體錯誤。

依 Anthropic 的說法，證明的內容是：在輸入小於 64 MB 時，這些編譯後的程式會正常結束，不會觸發記憶體安全錯誤或斷言失敗。全部證明約 1.8 億行 Rocq，一份典型證明約 60 萬行，對應的執行檔中位數是 18,000 條 RISC-V 指令。這些數字都是 Anthropic 自己報的。

最值得注意的是信任範圍。Anthropic 說，開發者需要信任的只有三樣：RISC-V 與 Linux process 的形式模型、被證明的定理陳述本身，以及 Rocq 證明檢查器。也就是說，證明雖然是 Claude 寫的，但讀者不必相信 Claude；證明成不成立，由檢查器決定。

證明過程順手找到的 bug

Anthropic 說過程中找到「數百個」bug，但沒有附逐一清單，所以這個數字只能當官方自述。文章舉的例子都很難靠一般測試撞到：一個解壓縮器要約 20 MB、特定結構的輸入，才會因為 counter underflow 造成越界寫入；一個影像解碼器要 64 MB 輸入、超過 2 GB 記憶體，才會出現越界讀取；另一個函式庫要對同一個檔案開兩個 handle、照特定順序呼叫，才會越界讀取。還有一個不會崩潰的邏輯 bug：限制可載入檔案的功能，不是每次都會生效。

其中一個我們可以自己核對。Anthropic 說 Claude 重新發現了 libexpat 的 CVE-2026-56132。我們去看了 MITRE 的 CVE 記錄，它在 6 月 19 日公開，描述 libexpat 2.8.2 之前，doProlog 在跨 parser 共享資料結構時，重新配置 scaffold 陣列處理錯誤，造成 heap-based buffer overflow，CVSS 3.1 分數 6.9（MEDIUM）。這個漏洞確實存在，也確實是記憶體安全問題。不過 Anthropic 說觸發條件是深度巢狀的輸入，這一點 CVE 記錄裡沒有寫，目前只有 Anthropic 這麼說。

讓 Claude 自己修補，也帶來另一個問題：它大可把程式改成怎樣都不會崩潰，定理就輕鬆成立了。Anthropic 在註腳說，為了防止這種 reward hacking，他們對任何 patch 扣分，對能證明「改到哪些輸入、改得多少」的 patch 加分，並記錄審查這些 patch。

證明 repo 裡寫明了「沒說什麼」

Anthropic 說會公開信任元件（RISC-V 與 Linux process 語意）、不需修補就能證明的完整證明，以及沒能證明的規格；可能洩漏未修補 bug 的證明則不放。我們讀了 Theorem 發布的 證明 repo README，10 月 25 日更新的版本列出 25 個函式庫、60 個進入點有證明，用 Rocq 9.2.0 檢查，MIT 授權。它和 239／123 之間的差距，Anthropic 沒有給公開子集的確切數字，我們只能說 README 當時列的是這些。

這份 README 最有用的是一段「證明沒說什麼」，我們自己轉述重點：

  • 不代表函式庫正確。 sanitizer 偵測不到的錯誤，例如算出錯的結果、記憶體洩漏，都不在證明範圍內。
  • 只涉及一個進入點能走到的程式碼，不是整個函式庫。
  • 證明的對象是執行檔，不是原始碼。 而且是用 clang 20.1.8 加 musl 編出的靜態 riscv64 執行檔，不是 OSS-Fuzz 平常跑的 x86-64 版本。
  • 模型和真實 Linux 不一致的地方，證明可能不適用。
  • README 也提醒，其中的「agreement」陳述不排除程式永遠不結束，這個版本也沒有任何 halts 陳述。Anthropic 文章把性質描述成「會正常結束」，要確認哪些證明包含終止，得看 repo 裡實際的定理。

Anthropic 自己列的限制也差不多：真實的 CPU 和作業系統可能和模型不一致，ASan 抓不到所有記憶體安全 bug，不是每個進入點都驗過，呼叫端誤用函式庫也還是可能破壞記憶體。它也提到，多數人實際是在 x86 或 ARM、動態連結 glibc 的環境上跑這些函式庫，這不是證明涵蓋的環境。

HN 上的質疑也落在這裡。有人問證明的是不是你真正想要的性質，也就是規格和現實貼不貼近；有人認為流程其實是 fuzz 找 crash、修掉、再寫證明；也有人引附錄說證明風格很冗長，能不能擴到更複雜的程式還要再看。這些是個人意見，但問的都是同一件事：規格與假設。

成本還很高，但有在往下掉

Anthropic 說一份證明可能要用掉數億 token。它也給了兩個下降的訊號：在 36 個用 OSS-Fuzz 程式碼建的小任務上，Opus 5.5 解出一半所需的 token，比 Opus 5 少約 40%；讓多個 agent 共用工作區、互相複製證明，token 用量又比各自作業少 17%。原因之一是證明裡很多內容都在處理 C runtime 和 ASan 初始化，這些每個程式都有，可以重用。這是 36 題的內部實驗，不能推成所有程式都能省這麼多。

文章另外提到幾個案例，例如替 RFC 1950 寫形式規格，證明 Linux 核心的 zlib 實作（x86 二進位）符合規格，也都是 Anthropic 自述。

看到「已驗證」，先問三件事

對維護者和資安團隊來說，這次結果改變的是可行性：形式化證明不再只屬於少數專家長期投入的專案，現在可以拿既有的 fuzz test 當起點，大批產出並由機器檢查。Theorem 也在 OSS Verify 頁面表示，對符合條件的開源專案免費跑這套流程，並發布了 Claude skill 讓開發者自己試。條件細節我們還沒讀到，維護 C/C++ 函式庫、已有 OSS-Fuzz 整合的專案，可以先去看自己符不符合。

但它沒有改變的是：證明只對它寫下的規格和假設成立。以下是我們的判讀建議，不是 Anthropic 或 Theorem 的說法。之後在 release note、供應商文件或資安報告裡看到「formally verified」，先問三件事：

  • 證明的規格是什麼？ 是「不崩潰、不觸發 ASan」，還是「結果正確」？兩者差很多。
  • 假設的機器是什麼？ 這次是單執行緒、靜態連結 musl 的 RISC-V 執行檔，固定記憶體預算。你在 x86 上跑動態連結 glibc 的版本，就不在範圍內。
  • 信任哪些元件？ 形式模型、定理陳述和證明檢查器，任何一個有問題，證明就不保證什麼。

所以「已驗證」可以信到這裡：在那份規格、那台假設的機器上，那個進入點對所有小於 64 MB 的輸入不會出現 ASan 抓得到的錯誤，而且這件事已經由檢查器核對過，不必相信寫證明的模型。這是 fuzzing 只試有限輸入給不了的保證，但它不是「這個函式庫沒有 bug」。接下來值得觀察的，是公開的證明數量會不會增加、Theorem 計畫實際收哪些專案，以及證明能不能擴到 x86、glibc 這些多數人真正部署的環境。