Anthropic前沿紅隊於10月22日發表研究，用Claude為123個開源函式庫的239個進入點寫出形式化證明：只要輸入小於64 MB，這些程式都不會當機。證明直接落在編譯後的RISC-V執行檔上，合作夥伴是開發形式化工具的Theorem。Anthropic表示，這是AI首次在正式環境軟體的組合語言層面大規模進行形式化驗證。
這批函式庫全部來自Google的OSS-Fuzz專案，也就是長期掛在模糊測試平台上的那批基礎元件，壓縮、影像解碼、HTTP解析都包含在內。整個工程耗時數週。
把模糊測試改寫成定理
做法分三步。第一步，團隊把每個函式庫既有的fuzz測試套件改寫成一條形式化規格，意思是「這段測試程式碼面對任意輸入都不會當機」。規格建立在Theorem提供的RISC-V指令語意與Linux行程語意模型之上。
第二步交給Claude撰寫證明，再由Rocq證明檢查器逐條核對。
"Claude writes the proof; the Rocq kernel checks it against the specification."
（Claude寫證明，Rocq核心拿它對照規格進行檢查。）
第三步處理證不下去的情況。證明卡關，往往代表程式碼裡真的有缺陷，這時Claude會自行修改程式碼，規格重新產生，再接著證明。團隊坦承這一步容易出現「獎勵駭客」，模型可能為了讓證明通過而亂改程式，因此替修補加上懲罰項，要求證明修補所影響的輸入範圍，並逐條記錄、交由人工稽核。
一份典型的證明約60萬行。最終需要信任的部分只剩RISC-V與Linux的語意模型、定理陳述本身，以及Rocq檢查器。
證明過程中挖出的漏洞
證明途中發現並修復的漏洞有數百個，其中一些很難靠模糊測試撞出來。文章舉了幾個例子：某個解壓縮器的計數器下溢，只會在約20 MB的特定輸入下觸發；某個影像解碼器的越界讀取，要64 MB輸入加上2 GB以上記憶體才會出現；還有一個越界讀取，需要兩個控制代碼以特定順序操作同一個檔案。libexpat的CVE-2026-56132也被重新發現了一遍。
cpp-httplib的證明多了一道關卡：std::set解構時的遞迴可能導致堆疊溢位。為排除這種情況，團隊在機器碼層面證明了libc++紅黑樹的平衡演算法能把樹深度壓在對數等級。
同一篇研究還附了幾個旁支實驗。Claude用Rust寫了一個Python子集，並用Verus證明它符合CPython語意，在170萬個隨機程式上與CPython行為一致的比例為99.95%。它還自行產生了一套x86指令語意，單步執行就能啟動Ubuntu使用者空間，順帶查出官方參考文件中數百處錯誤。
拿seL4對照來看
形式化驗證在業界並不新鮮，難處一直是人力。業界常拿seL4微核心舉例：大約一萬行C程式碼，當年的證明投入通常被引述為二十人年左右。CompCert編譯器走的也是類似路線，靠一支小團隊多年打磨。這類專案的共通點是對象少、週期長、專家密集。
Anthropic這次的規模是123個函式庫、幾週時間，粗略對照，單位工作量的成本結構已換了一種形態，人從寫證明退到訂規格、審修補。代價換成了token：文章說一份完整證明可能要消耗數億token。在36個小型任務上，每個任務給單一代理三次嘗試、每次500萬token預算；允許代理彼此重用證明後，所需token又降了17%。
兩邊的保證強度也不在同一個層級。seL4證明的是功能正確性，這次證明的只是「不會當機」，範圍窄得多。
證明之外的空白
Anthropic自己列出的限制相當具體。證明是基於單執行緒、靜態連結、使用musl libc的RISC-V二進位檔，而多數使用者實際執行的是x86或ARM上動態連結glibc的版本。AddressSanitizer本身抓不到所有記憶體安全錯誤，也有進入點沒被涵蓋，呼叫端誤用函式庫而導致的記憶體損毀同樣不在證明範圍內。
"Formally verified" does not mean "bug-free."
（「形式化驗證」不等於「沒有bug」。）
規格與真實機器之間的落差，是這條路線最容易出事的地方。Rocq和那幾套語意模型本身也需要加固，文章說這件事「不是小事」。團隊給出的判斷是，形式化驗證將成為安全軟體開發的常規環節，至於這些證明何時能涵蓋到x86與glibc這類主流部署環境，文章並未說明時間。
參考來源：Anthropic前沿紅隊研究文章、CocoLoop；Anthropic研究頁，用以核對函式庫數量、進入點數、證明行數與token比較口徑。