Anthropic 用 Claude 為 123 個開源程式庫寫出數學證明
Anthropic 的 Frontier Red Team 10 月 22 日發表研究，與形式驗證公司 Theorem 合作，用 Claude 在數周內為 123 個開源程式庫的 239 個測試入口寫出數學證明，證明這些程式在任何小於 64 MB 的輸入下都不會崩潰。Anthropic 稱，據其所知這是首次大規模用 AI 為生產環境的軟件在組合語言層面做形式驗證。
形式驗證是指把程式碼翻譯成數學模型，再證明它在所有情況下都符合一組既定規則，由程式自動逐步檢查。它一向罕見，因為太慢：Anthropic 指 seL4 作業系統核心花了兩個人年開發，卻花了 20 個人年驗證。
做法：把模糊測試變成可證明的規格
據 Anthropic 報告，團隊由 Google 的 OSS-Fuzz 項目入手。模糊測試（fuzz test）是開發者寫一個入口，再由測試引擎大量產生隨機輸入，看哪一個令程式崩潰；它永遠試不完所有輸入。Claude 改為把每個模糊測試變成一條規格，即「這個測試在任何小於 64 MB 的輸入下都不會崩潰」，然後針對編譯後的 RISC-V 機器碼證明它。
證明用的是 Theorem 的 RISC-V 指令集與 Linux 行程語義模型，再交由 Rocq 證明檢查器機械地核對。Anthropic 表示，這批證明「幾乎不需要人手覆核」，開發者只須信任三樣東西：機器與系統的形式模型、被證明的定理陳述，以及檢查器本身。
項目 | 數字 |
|---|---|
已證明的程式庫 | 123 個 |
已證明的測試入口 | 239 個 |
證明碼總量 | 約 1.8 億行 Rocq |
單一證明的典型長度 | 約 60 萬行 |
被證明程式的中位長度 | 18,000 條 RISC-V 指令 |
寫證明期間找出的漏洞
據 Anthropic 報告，當一條證明寫不下去，原因往往是程式真的有漏洞，團隊容許 Claude 直接修補再繼續，過程中因而找出數百個漏洞，當中不少是模糊測試幾乎不可能碰到的。模糊測試一般把輸入限於 1 MB 以內。
Claude 在一個程式庫內找到的計數器下溢，會導致越界寫入，但只在約 20 MB、而且版面排列極罕見的輸入下才會出現；另一個影像解碼器的越界讀取，需要 64 MB 輸入及逾 2 GB 記憶體；它又重新發現了 libexpat 的 CVE-2026-56132，該漏洞要深層嵌套的輸入才觸發。Claude 亦找到完全不會令程式崩潰的邏輯漏洞：某程式限制應用程式可載入哪些檔案的功能，並非每次都生效。
其他驗證實驗
Anthropic 報告另列出三項實驗。團隊要求 Claude 為 RFC 1950（zlib 壓縮格式的技術文件）寫形式規格，再證明 Linux 核心內的 zlib 實作符合該規格，這次直接證明 x86 編譯出的二進位檔，其後重複用在另外約六個常用程式庫上，發現一些不可被利用的小問題。
另一項實驗是要 Claude 用 Rust 寫一個涵蓋大部分 Python 的直譯器，並用驗證工具 Verus 證明它符合學術論文所述的 CPython 語義；團隊隨機產生逾 170 萬個 Python 程式實測，99.95% 行為與 CPython 一致。報告又指，在驗證一個廣泛使用的 PDF 閱讀器期間，一周內找到的保安漏洞，相當於該軟件通常一年被通報的數量。
成本正在下降
據 Anthropic 報告，LLM 做形式驗證的主要限制是一條證明動輒消耗數以億計的 token。團隊用真實 OSS-Fuzz 程式碼建了 36 項小型驗證任務：Opus 5.5 證出其中一半所用的 token，比 Opus 5 少約 40%。團隊又讓多個代理互相複製對方已完成的證明，結果所用 token 比各自獨立運作少 17%，部分代理在單獨嘗試失敗後，靠共用工作區成功。
「已形式驗證」不等於沒有漏洞
Anthropic 在報告中表明，證明檢查器只能確認證明符合規格，無法判斷規格是否貼近現實；若驗證過的程式仍出事，原因是規格或機器語義與真實機器有出入。報告同時指，現時的證明假設程式以單執行緒靜態二進位檔形式、在固定記憶體上限下，於 RISC-V 處理器及 Linux 上運行。
Anthropic 正公開部分證明及相關語義模型，Theorem 則表示願意為其他開源項目運行同一套流程，並發布一個 Claude skill，供開發者驗證自己的程式碼。
暫時未有留言
提交留言即表示你已閱讀我們的私隱政策。