Anthropic 驗證123個開源函式庫，證明239個測試入口符合安全條件

Anthropic（Anthropic）運用 Claude，對123個開源函式庫的239個測試入口，以數學方式證明其符合特定安全條件。

Anthropic 前線紅隊（Frontier Red Team）於22日公布的研究指出，團隊與驗證公司 Theorem 合作，將既有測試轉化為驗證條件，再用獨立工具檢查 Claude 撰寫的證明。

驗證對象是 Google 開源錯誤偵測專案 OSS-Fuzz 收錄的函式庫。研究團隊將既有的模糊測試改寫為一項命題：對任何小於64MB的輸入，程式都不會異常終止、發生記憶體安全錯誤，或違反驗證條件。Claude 負責撰寫證明，Rocq 則負責檢查。

研究團隊表示，他們花了數週修正 Claude 找出的錯誤，之後驗證了123個函式庫中的239個測試入口。測試入口是為了測試程式特定功能而設置的輸入路徑。這些證明以編譯後的 RISC-V 指令為驗證對象，而非供人閱讀的原始碼；撰寫出的 Rocq 證明約有1億8000萬行。

形式化驗證是以數學方式確認程式是否遵守明確規則的方法。與透過輸入資料執行程式、找出錯誤的傳統測試不同，形式化驗證會針對符合既定條件的所有輸入證明命題成立。研究團隊在撰寫證明時也發現了既有測試未能找出的錯誤，並依修正後的程式碼重新制定驗證條件。

這次成果僅適用於在 Linux 執行、使用固定記憶體容量的單執行緒靜態連結 RISC-V 程式，並未驗證各函式庫的所有功能，也未涵蓋所有實際部署環境。Anthropic 表示，證明工具能確認命題是否成立，但無法判斷命題是否完整涵蓋實際使用條件。

研究團隊另表示，在獨立實驗中，Claude 以 x86 執行檔層級驗證了 Linux 核心的 zlib 實作。團隊也用超過170萬個隨機生成的程式測試以 Rust 撰寫的 Python 解譯器，結果顯示其行為與 CPython 一致的比例為99.95%。這兩項實驗的對象與方法，均與本次123個函式庫的 RISC-V 驗證不同。

Anthropic 也公布了36項小型驗證任務的比較結果。Claude Opus 5.5 證明其中一半任務時，使用的 token 數量比 Opus 5 少約40%。研究團隊公開了部分證明，供其他開發者檢視與重複使用。