Anthropic 稱 Claude 已為 123 個開源程式庫的 239 個模糊測試入口生成安全性形式證明

Anthropic 於 October 22, 2026 發表研究，報告指 Claude 與 Theorem 合作，為 123 個開源程式庫中 239 個模糊測試入口點的 RISC-V 組合語言程式碼，產生經機器檢查的安全屬性形式化證明。

Anthropic 表示，Claude 修補了發現的錯誤，然後證明對於每個小於 64 MB 的輸入，以及每種建模的 Linux 作業系統回應和記憶體配置，程式都會正常結束，不會觸發記憶體安全錯誤或斷言失敗。這些證明假設程式在使用 Linux 的 RISC-V CPU 上，以單執行緒靜態二進制檔執行，並採用固定的記憶體預算。Anthropic 表示，這些證明合共約有 1.8 億行 Rocq 程式碼；典型證明約有 60 萬行，用以涵蓋長度中位數為 18,000 條 RISC-V 指令的二進制檔。該公司表示，據其所知，這是首次大規模運用 AI，在組合語言程式碼層面對生產環境軟件進行形式化驗證。

部分證明及其背後的 RISC-V 和作業系統語義，正透過 GitHub 發佈。Anthropic 表示，亦會公開為此項目建立、但尚未公開的可信組件、無需修補的模糊測試完整證明，以及無法證明的模糊測試規格；可能會揭露未修補錯誤的證明則不會公開。

將模糊測試轉化為形式化證明

這種方法會把每個程式庫現有且可編譯的模糊測試，轉化為一份形式化規格，當中只編碼一條規則：任何小於 64 MB 的輸入都不會令測試崩潰。規格以編譯後的 RISC-V 指令為基礎，採用 Theorem 對 RISC-V 指令集和 Linux 程序的形式語義；Rocq 證明檢查器則會根據規格驗證每份已完成的證明。Anthropic 表示，這代表開發者只需信任三個組件：RISC-V 和 Linux 程序的形式模型、確切的定理陳述，以及 Rocq 檢查器本身。

Anthropic 表示，已將這個流程應用於 Google OSS-Fuzz 計劃中的數百個項目。該計劃為符合資格的開源項目提供持續模糊測試，並會自動為 C 和 C++ 程式加入 AddressSanitizer 檢測；這款工具只要發現記憶體存取不當，就會令程式崩潰。日期為 October 22, 2026 的附錄詳述已證明的完整定理：對於所有小於 64 MiB 的輸入和所有記憶體配置，無論是加入 ASan 檢測的二進制檔還是未加入檢測的二進制檔，都不會發生故障、異常中止或出現未建模行為；兩者產生的讀取和寫入軌跡、結束行為及最終檔案系統狀態亦完全相同。

附錄指出，Claude 在這項工作中編寫了約 10 億行 Rocq 程式碼，當中約 1.8 億行通過證明檢查器；cJSON 的 391 行解析器入口點獲得了一份 630,000 行的證明，而 fftw3 在連結 51,000 行程式碼的情況下，則獲得了一份 480,000 行的證明。由於 Claude 可以在完成證明前修補程式碼，Anthropic 表示會對修補作出扣分，並對證明修補影響哪些輸入提供額外獎勵；同時會記錄及審核修補，以防模型利用獎勵機制漏洞。

證明嘗試期間發現的錯誤

Anthropic 表示，嘗試進行證明揭露了數百個錯誤，當中不少都是模糊測試工具不太可能找到的錯誤。在為一個程式庫的入口點進行證明時，Claude 在一個解壓縮器中發現計數器下溢，導致越界寫入；但只有在輸入約為 20 MB，且具有一種罕見的特定排列時才會發生。其他發現包括：一個影像解碼器中的越界讀取，需輸入 64 MB 並使用超過 2 GB 記憶體；一個需要透過同一檔案的兩個控制代碼，以特定次序呼叫才會出現的越界讀取；以及在 libexpat 中重新發現 CVE-2026-56132，觸發條件是輸入內容有深層巢狀結構。

Claude 亦發現了不會導致程式崩潰的邏輯錯誤，包括應用程式可載入哪些檔案的限制並非總是得到執行。Anthropic 表示，在嘗試驗證多個廣泛使用的關鍵應用程式時，發現一個此前未知、已潛藏逾十年的邏輯錯誤；而在驗證一款廣泛使用的 PDF 閲讀器期間，該公司一星期內發現的安全漏洞數量，與通常一年內通報的數量相同。

其他實驗與效率研究結果

除 OSS-Fuzz 外，Anthropic 亦要求 Claude 為 RFC 1950 撰寫形式規格。RFC 1950 是定義 zlib 壓縮格式的技術文件；Claude 隨後證明 Linux 核心的 zlib 實作正確遵循該規格。Claude 直接對 x86 編譯的二進位檔進行證明，並使用由 Claude 生成的 x86 指令集形式語義。Anthropic 表示，該公司亦對另外六個廣泛使用的程式庫重複這個流程，發現了一些輕微且無法利用的邊界情況錯誤，現正向上游提交報告。該公司亦表示，生成 x86 語義時，在官方參考文件中發現數百處錯誤，在硬件本身則發現數量較少的錯誤；以單步方式執行這套語義模型，甚至可以在 Linux 核心上啟動 Ubuntu 用戶空間。

在另一項實驗中，Claude 使用 Rust 為 Python 的一個大型子集建立了解譯器，並利用 Verus 驗證工具證明，該解譯器遵循一篇學術論文所闡述的 CPython 語義。技術附錄指出，解譯器的全部 17 個層級均已獲得證明，定理內容為：「每當解譯器傳回結果，該結果就是形式語義所規定的結果。」Anthropic 表示，對 170 萬個隨機生成的 Python 程式進行實證測試後，發現其中 99.95% 的測試結果與 CPython 行為一致；在七個刻意植入的錯誤中，有五個未被隨機測試發現，但七個全都令證明失效。

為了衡量效率，Anthropic 把真實 OSS-Fuzz 入口點縮減，製作出 36 項小型驗證任務；這些程式包含 283–2,491 條指令，輸入大小上限為 64 bytes，並以約 100 條指令的「mini-ASan」執行階段取代 AddressSanitizer。Anthropic 表示，Opus 5.5 證明一半任務所需的詞元，比 Opus 5 少約 40%。Anthropic 亦表示，獲準在共用工作區互相複製證明的代理，所需詞元比獨自工作的代理少 17%；部分代理在先前獨自工作失敗後，改以協作方式成功，而獨自工作的代理則未能完成其中兩項證明。該公司表示，OSS-Fuzz 專案大規模運作期間亦出現同樣的重用效應：代理團隊會複製已完成的證明並加以修改，因為每項證明大部分內容都涉及共用的 C 執行階段及 AddressSanitizer 初始化程式碼。

已述限制與 OSS Verify 計劃

Anthropic 表示，這些證明並不代表程式庫沒有錯誤：仍有錯誤可能存在於受信任元件內，或超出證明的範圍。這些證明涵蓋以 musl libc 連結的單執行緒靜態 RISC-V 二進制檔；然而，大部分用戶在 x86 或 ARM 上執行這些程式庫，並以動態連結方式連結 glibc，而 AddressSanitizer 亦無法偵測所有記憶體安全漏洞。該公司表示，隨着模型改進，預計這些限制將變得容易處理。

Theorem 透過其 OSS Verify 計劃，向符合資格的開源專案免費提供相同的流程。加入計劃的方式是提交拉取請求，將 project.yaml、Dockerfile 和 build.sh 檔案加入計劃的程式碼庫。Theorem 表示，審核專案的方式與 OSS-Fuzz 相若，並優先考慮廣泛使用的關鍵基礎設施。據 Theorem 表示，維護者會收到一份由 Rocq 核心檢查的 Rocq 證明，證明每個模糊測試目標在任何不超過 64 MiB 的輸入下均不會崩潰；在證明過程中發現的錯誤會透過電郵私下通知維護者，且沒有披露期限，而產生證明可能需要數天。Theorem 的路線圖目標是驗證整個 Nix 生態系統，包括 glibc、OpenSSL 和 cURL 等關鍵基礎設施。