今日 · 研究文章 10 月 22 日

Claude 證明 239 個入口不會崩潰。成立有前提

Anthropic 寫，Claude 對 123 個開源函式庫的 239 個模糊測試入口，在編譯成 RISC-V 機器碼的執行檔上證明 64 MB 以內任何輸入都不會崩潰，證明成立有前提。 模糊測試是用大量隨機輸入去撞程式、找會讓程式崩潰的輸入。Anthropic 與合作方 Theorem 把這些測試改寫成要證明的命題：任何輸入都撞不出崩潰。證明是用數學推導涵蓋所有輸入，測試只能說明測過的那些輸入沒出錯。原文寫「Claude successfully patched the bugs it found and then proved that there are no crashes on any input (up to 64 MB) for 239 entry points across 123 different OSS-Fuzz libraries.」（Anthropic，2026-10-22）。前提是程式以單執行緒靜態執行檔、固定記憶體預算跑在 RISC-V 的 Linux 上。證明約 1.8 億行，由證明檢查器 Rocq 機器檢查，不靠人工審。Anthropic 寫，需要信任的只剩 RISC-V 與 Linux 程序的形式模型、命題本身與 Rocq。Anthropic 也寫明這不代表這些函式庫沒有臭蟲。證明過程中找到數百個臭蟲，Claude 先修補再證明。成本是證明要用掉數億 token。數字全是 Anthropic 自報，Anthropic 公開了部分證明供獨立核對。模糊測試只能說測過的輸入沒崩潰。這種證明能說清楚要信任哪幾個元件，證的性質是不崩潰，不是程式做對了事。能不能普及，要看這數億 token 的成本，這是本報的讀法。怎麼查的 →

黑色邊框內的概念插圖：左邊一台機蓋寫著 FUZZING 的深色筆電旁堆著許多米色小方塊，方塊呈弧形往上連到中央一個高高的米色視窗面板，面板頂欄有三個圓點、內有灰色文字線條，後方襯著淡粉紅色圓形。從面板底部，多條印有深色線條、摺成鋸齒狀的紅色紙帶橫過桌面，延伸到右邊一台機蓋寫著 CLAUDE 的深色筆電；右下角一塊淺色牌子寫著 ANTHROPIC，後面接著一個小標記。

出處與查證

這則刊在2026年10月23日的晨報，同一期還有 6 則。查證經過、引句核對與當天缺的資料，記在那一期的本日驗證。

引用這則

SecondSource（2026），〈Claude 證明 239 個入口不會崩潰。成立有前提〉，https://secondsource.io/research/2026-10-23-1/，取用日期取用。