2026/10/30 · Weekly Radar
Anthropic Frontier Red Team 與 Theorem 讓 Claude 把 OSS-Fuzz 的 fuzz test 改寫成規格，在 RISC-V 機器碼層級替 123 個開源函式庫、239 個 entry point 證明「64 MB 以內任何輸入都不會 crash」，產出約 1.8 億行 Rocq 證明，沿途抓出數百個 bug。
這是 Anthropic Frontier Red Team 與 Theorem 合作發表的研究文章，主張 LLM 正讓形式化軟體驗證能以過去無法想像的規模落地。Claude 在 RISC-V 組合語言層級，替超過 100 個真實世界的開源函式庫寫出安全性質的形式證明。作者表示，就他們所知，這是第一次大規模用 AI 對生產級軟體做這個層級的形式驗證。過程中 Claude 也找到一些經過多年測試仍沒被發現的 bug，其中包括 OSS-Fuzz 跑了「數兆次」都沒抓到的問題。
Linux kernel 最近一口氣揭露了超過 1,000 個漏洞，LLM 找 bug、串成 exploit 的能力也在快速提升。形式驗證可以證明程式碼遵守定義好的規則，但成本極高：seL4 實作約花 2 人年，驗證卻花了約 20 人年，因此過去多半只用在 Airbus 航電這類安全關鍵領域。這次 Claude 證明了 123 個開源函式庫在任何小於 64 MB 的輸入下都能正常結束，不會出現記憶體安全錯誤或 assertion 失敗。前提是單執行緒靜態連結 binary、固定記憶體預算、RISC-V CPU 與 Linux。團隊公開了部分證明、RISC-V 與作業系統語意，以及一個幫開發者驗證自己程式碼的 Claude skill；Theorem 也提供替其他專案跑這條 pipeline 的服務。
核心想法是把現有的 fuzz test 轉成規格：「這個 fuzz entry point 在任何小於 64 MB 的輸入下都不會 crash」。只要在編譯後的 RISC-V 程式碼上證明了這件事，fuzz 這個 entry point 就變得多餘。這套方法涵蓋 Google OSS-Fuzz 裡的數百個專案，而 ASan 偵測的 crash 正好針對記憶體安全違規，也就是漏洞的主要來源。幾週內，Claude 修補了自己找到的 bug，並對 123 個函式庫的 239 個 entry point 證明不會 crash，證明總計約 1.8 億行 Rocq。一份典型證明約 60 萬行，對應的 binary 中位數約 1.8 萬條 RISC-V 指令。可信基礎只有 RISC-V 與 Linux process 模型、定理陳述本身，以及 Rocq proof checker；由 checker 驗證證明，審查者不必逐行讀證明程式碼。附錄另附一位專家對這批證明的評估。
證明過程挖出數百個 bug。Claude 會修補程式碼、重新產生規格、重新證明，全程不需人工介入。註腳也承認這會留下 reward hacking 的空間，團隊用「懲罰修補」加上人工稽核來壓制。舉例包括：解壓縮器的計數器下溢，在約 20 MB 輸入時造成越界寫入；影像解碼器需要 64 MB 輸入加 2 GB 以上記憶體才會觸發的越界讀取；需要對同一檔案開兩個 handle 才觸發的越界讀取；重新找到 libexpat 的深層巢狀輸入 bug（CVE-2026-56132）；以及一個檔案限制功能並非總是生效。除了記憶體安全，fuzz test 常會檢查 roundtrip、idempotence 或與參考實作等價，所以證明不 crash 就等於證明了這些性質，例如 LZO 的「壓縮後再解壓等於原文」。cpp-httplib 還需要排除 std::set 解構子遞迴造成的 stack overflow，等於要在機器碼上證明 libc++ 紅黑樹的再平衡能讓樹高維持對數級。
zlib：Claude 寫了 RFC 1950 的形式規格，用 Claude 自己生成的 x86 語意，在 x86 binary 層級證明 Linux kernel 的 zlib 正確；另外約六個函式庫也照做，只找到不可利用的小角落 bug。Python：Claude 用 Rust 寫了一個大型 Python 子集直譯器，再用 Verus 證明它符合學術論文中的 CPython 語意，在 170 萬個隨機程式上與 CPython 行為一致的比例達 99.95%。PDF 閱讀器：一週驗證找到的安全 bug，相當於平常一年的回報量；另一款廣泛使用的應用程式中，有個邏輯 bug 潛伏了十多年。
一份證明可能耗掉數億 token。在 36 個小型 OSS-Fuzz 任務上，Opus 5.5 證完一半，token 用量比 Opus 5 少約 40%。共用工作區的 agent 比單獨作業少用 17% token，34 份完成的證明中有 30 份是單獨作業比較貴，還有兩個任務只有協作才完成。規模化之後，libcups、freerdp、libzmq 等可以直接複製既有證明，因為每份證明大部分都在處理共用的 runtime 和 sanitizer 程式碼。對照組是 Mathlib：700 多名貢獻者累積了近 30 萬條定理。Theorem 的路線圖是驗證 Nix 生態系，包括 glibc、OpenSSL 和 cURL。由於依賴關係呈冪律分布，只要驗證一小組共用函式庫，大量軟體就有機會被證明。
「已形式驗證」不等於沒有 bug，證明的品質只取決於規格和機器模型。目前模型涵蓋的是 musl 靜態連結的 RISC-V binary，但多數使用者跑的是 x86 或 ARM 加動態 glibc；ASan 也抓不到所有記憶體安全 bug；並非每個 entry point 都驗證過，dead code 也不在 entry-point 證明的範圍內；呼叫端仍可能誤用函式庫，在自己那一側破壞記憶體，要補上這塊就得替每個公開函式寫出呼叫者義務。
Anthropic 認為，過去只用在安全關鍵程式碼的形式驗證，很快就會像 fuzzing 一樣成為多數生產軟體的例行工作，從「事後外掛」變成「內建」，並鼓勵曾經用舊模型嘗試失敗的開發者再試一次。
seL4 驗證花了 20 人年，這裡幾週就跑完 123 個函式庫，聽起來像魔法；但限制欄寫得很清楚：musl 靜態連結的 RISC-V，而你機器上跑的是 x86 加動態 glibc。「已證明」證的是作者自己定義的那台機器。