Claude給123個開源庫寫出1.8億行數學証明，找出數百個Bug

BiRun 訊，Anthropic 聯閤形式化驗証公司 Theorem，讓 Claude 用數學方法檢査軟件漏洞。傳統測試通常靠不斷輸入隨機數據，看看程序會不會崩潰。但無論測試多少次，都無法保証沒有遺漏。這次 Claude 直接為程序編寫數學証明，試圖從根本上排除特定類型的錯誤。

幾週內，Claude 為 123 個開源庫的 239 個測試入口完成驗証，生成約 1.8 億行証明代碼，並交給 Rocq 數學証明工具檢査。結果表明，在指定運行環境下，這些程序面對小於 64 MB 的任意輸入，都不會觸發測試所檢査的崩潰。

証明過程中，Claude 還發現並脩復了數百個 Bug。比如，一段解壓程序只有遇到約 20 MB、結構極其特殊的數據，才會發生內存越界寫入。另一處圖像解碼漏洞需要 64 MB 輸入和超過 2 GB 內存才能觸發。常規隨機測試很難碰到這些情況。

這類數學驗証過去極其費時。比如 seL4 操作系統內覈，開發累計投入約 2 年的全職人力，數學驗証卻需要約 20 年，是開發工作量的 10 倍。

信源

動察 Beating 頻道 · 動察 Beating 交流羣。