Anthropic 表示，Claude 為 123 個開源函式庫撰寫了形式化證明，證明它們不會崩潰

Anthropic 表示，該公司與 Theorem 合作，使用 Claude 在組合語言層級（RISC-V）證明 100 多個真實世界開源函式庫的安全性質；Anthropic 稱這是 AI 首次大規模用於在該層級形式化驗證正式環境軟體。

Anthropic 表示：

• 證明內容：針對 123 個 OSS-Fuzz 函式庫的 239 個模糊測試入口點，證明無論輸入為何（大小低於 64 MB），程式都會正常結束，不會發生記憶體安全錯誤或斷言失敗。這項結論有前提條件：單執行緒靜態二進位檔、固定記憶體預算，並在執行 Linux 的 RISC-V CPU 上運作。這些證明總計約 1.8 億行 Rocq 程式碼，並經 Rocq 證明檢查器驗證。
• 方法：將每個函式庫既有的模糊測試轉換成規格（「此測試永遠不會崩潰」），再由 Claude 撰寫證明，並在過程中修補發現的錯誤。Anthropic 表示，這找出了數百個錯誤，包括模糊測試不太可能觸及的錯誤，例如必須輸入罕見的 20 MB 輸入資料才會觸發的越界寫入，以及在 libexpat 中重新發現 CVE-2026-56132。
• 其他實驗：Claude 證明 Linux 核心的 zlib 實作在 x86 二進位層級符合 RFC 1950 規格，並建置了一個 Rust Python 直譯器，在 170 萬個隨機程式中，有 99.95% 的行為與 CPython 相符。Anthropic 也表示，對一款廣泛使用的 PDF 閱讀器進行形式化驗證，一週內發現的安全漏洞數量，與該軟體通常一年收到的通報數量相當。
• 成本：證明可能需要數億個 token。Anthropic 表示，在 36 項小型驗證任務中，Opus 5.5 有一半任務能成功證明，且比 Opus 5 少用約 40% 的 token；共享證明的代理程式則少用了 17% 的 token。

Anthropic 正公開部分證明，以及 RISC-V 和 Linux 的語意模型。Theorem 提供服務，可為其他開源專案執行相同流程，並正公開一項 Claude skill，供使用者驗證自己的程式碼。Anthropic 指出，這並不代表這些函式庫沒有錯誤：剩餘的錯誤可能存在於受信任元件中，或落在證明範圍之外。