N環球 
Claude 寫出 1.8 億行數學證明：Anthropic 首次大規模驗證開源軟件底層安全
Anthropic 官方研究：與 Theorem 合作，用 Claude 在 RISC-V 彙編層面對 123 個開源庫、239 個程序入口做安全性形式化驗證，證明過程還挖出數百個潛伏多年的 bug。
為何重要
形式化驗證過去是專家花數年才能做成的奢侈品——寫 seL4 微內核用了 2 個人年，驗證它卻用了 20 個人年。Anthropic 證明：大模型幾週就能對上百個真實開源庫做完這件事，還順手挖出躲過「數萬億次」自動化測試的漏洞。
全文
Anthropic 10 月 22 日在官方研究頁面公布：與軟件驗證公司 Theorem 合作，用 Claude 在 RISC-V 彙編層面對 123 個取自 Google OSS-Fuzz 的真實開源庫、239 個程序入口做了安全性形式化驗證。據其稱，這是「AI 對生產級軟件做彙編級形式化驗證的首次大規模嘗試」。
規模驚人：共生成約 1.8 億行 Rocq 證明，典型證明約 60 萬行，覆蓋中位數 1.8 萬條 RISC-V 指令的二進制文件；全部在幾週內完成。證明由 Rocq 內核獨立校驗，無需人工逐行審查。
方法是把現有的 fuzz 測試轉成數學規範：64MB 以下任意輸入、單線程靜態鏈接的 RISC-V 二進制、Linux 環境下必須正常退出、無內存安全違規。證明過程中若發現疑似 bug，Claude 直接打補丁再重新證明。
挖出的 bug 有數百個：包括在某解壓器的拷貝中發現計數器下溢導致的越界寫入（需約 20MB 特定佈局輸入才能觸發）、圖像解碼器中的越界讀取，以及 libexpat 中 CVE-2026-56132 的重新發現——有些漏洞已潛伏多年。
Anthropic 自己也承認局限：「形式化驗證通過」不等於沒有 bug——證明只覆蓋單線程靜態 RISC-V 二進制，而多數代碼實際跑在 x86/ARM 上。不過它已把部分證明發佈到 GitHub 供獨立驗證，Theorem 也表示願為其他開源項目跑同樣的流水線。
副成果同樣亮眼：證明了 Linux 內核 zlib 實現在 x86 二進制層符合 RFC 1950；用 Rust 寫的 Python 解釋器大子集與 CPython 在 170 萬＋隨機程序上行為一致率達 99.95%。
💬 留言
暫時還沒有留言，來搶沙發！