Claude 形式驗證 123 個開源函式庫，過程挖出數百個錯誤
Anthropic 10 月 22 日在 Frontier Red Team 部落格發表研究，與新創公司 Theorem 合作，用 Claude 對 123 個開源函式庫的 239 個進入點做形式驗證，證明這些程式在任何小於 64 MB 的輸入下都不會當機。Anthropic 表示，就他們所知，這是首次大規模用 AI 在組合語言層級，對實際上線的軟體做形式驗證。Claude 在寫證明的過程中，也找出一些多年來沒被發現的錯誤。
形式驗證是把程式碼轉成數學模型，再證明它永遠遵守一組設定好的安全規則；證明不出來，就代表程式可能有違反規則的錯誤。這套方法過去很難普及，證明往往比原始程式碼大好幾倍，也需要極少數專家才有的技能。Anthropic 舉例，作業系統核心 seL4 的開發花了 2 人年，形式驗證卻花了 20 人年，因此過去只用在空中巴士航電程式這類攸關安全的系統。
把 Google OSS-Fuzz 的模糊測試轉成證明，產出 1.8 億行
這次研究的對象是 Google OSS-Fuzz 計畫裡的開源專案。OSS-Fuzz 為開源專案持續做模糊測試，也就是在程式的進入點丟進大量半隨機的輸入，看哪些輸入會讓程式當機。模糊測試跑越久找到的錯誤越多，但輸入有無限多種，永遠無法保證走遍每條程式路徑。
廣告 - 內文未完請往下捲動
研究團隊把開發者寫好的模糊測試轉成規格：只要輸入小於 64 MB，測試就永遠不會當機，再讓 Claude 對編譯成 RISC-V 指令的執行檔寫證明，由 Rocq 證明檢查器確認證明是否符合規格。Claude 在幾週內修補了找到的錯誤，完成 239 個進入點的證明，總共約 1.8 億行 Rocq 程式碼；典型的證明約 60 萬行，對應的執行檔中位數約 18,000 道 RISC-V 指令。
Anthropic 說，這麼大量的證明幾乎都不用人工審查，因為檢查器會確認證明滿足規格。開發者只需要信任三樣東西：RISC-V 與 Linux 程序的形式模型、被證明的定理陳述，以及 Rocq 檢查器本身。Anthropic 已公開部分證明，Theorem 也提供讓其他開源專案跑同一套流程的服務，並發布一個 Claude 技能協助開發者驗證自己的程式碼。
證明過程挖出數百個錯誤，PDF 閱讀器一週找到一年份漏洞
Anthropic 表示，嘗試證明的過程找到數百個錯誤，其中很多是模糊測試不太可能找到的。模糊測試通常把輸入上限設在 1 MB，Claude 卻在一個解壓縮程式裡找到計數器下溢，會導致越界寫入，但只有在約 20 MB、特定罕見結構的輸入下才會觸發。其他例子包括一個影像解碼器的越界讀取，需要 64 MB 的輸入和超過 2 GB 記憶體才會出現，以及重新找到 libexpat 的已知漏洞 CVE-2026-56132。
Anthropic 也嘗試用其他形式驗證方法處理資安任務。研究團隊在幾個廣泛使用的關鍵應用程式裡找到問題，其中一個是潛伏超過十年、先前沒人發現的邏輯錯誤；驗證一款常用 PDF 閱讀器時，一週內找到的資安漏洞數量，和這款軟體通常一年被回報的數量一樣多。
「通過形式驗證不代表沒有錯誤」，證明只涵蓋單執行緒 RISC-V
Anthropic 也列出限制。證明檢查器只能確認程式符合規格，無法判斷規格是否符合真實世界。這次的證明假設程式是單執行緒、靜態連結 musl libc 的 RISC-V 執行檔，但多數人是在 x86 或 ARM 上、動態連結 glibc 執行這些函式庫。研究也沒有驗證每個函式庫的所有進入點，用來偵測記憶體錯誤的 AddressSanitizer 也抓不到所有記憶體安全問題。
成本是另一個限制，一次證明可能要用掉數億個 token。Anthropic 用 36 個來自 OSS-Fuzz 的小型驗證任務測試，Claude Opus 5.5 證明其中一半所用的 token 比 Opus 5 少約 40%；讓多個代理共用彼此的證明時，所需 token 比各自作業少 17%。Anthropic 表示，形式驗證過去只用在最關鍵的程式，未來很快會像現在的模糊測試一樣，能套用到幾乎所有上線軟體。
風險提示
加密貨幣投資具有高度風險，其價格可能波動劇烈，您可能損失全部本金。請謹慎評估風險。
