Claude 對 123 個開源程式碼庫的 239 個測試入口完成形式化驗證，1.8 億行證明通過核驗

編者按：本文來自微信公眾號新智元（ID：AI_era），編輯：編輯部，創業邦經授權轉載。

全球軟件的bug，要被Claude端掉了？

短短48小時，全球就爆了27起重大網絡攻擊，現在人們都在瘋傳，「最暗十月」來了。

一早，Anthropic前沿紅隊團隊聯手Theorem Labs發佈了一份重量級報告——

他們讓Claude深入到底層彙編指令（RISC-V），向真實的生產級開源代碼庫發起總攻。

短短幾週，Claude拿下了123個開源代碼庫中的239個測試入口的形式化驗證，狂飆1.8億行Rocq數學證明代碼，全部通過機器核驗！

谷歌平台跑了上萬億次都沒撞出來的隱秘漏洞，連同潛伏十餘年的高危邏輯死角，甚至x86處理器硬件本身的真實缺陷，在這場大清剿中悉數現形。

更誇張的是，在一個熱門的PDF閲讀器中，Claude一週挖出的安全漏洞，直接頂得上它通常一整年的報告量。

這一次，Claude把找Bug、修Bug和驗證修復連成一條流程，展開了一場「數學級」Bug清掃。

席捲全球的網絡安全危機，或許真的有救了。

萬億次測試漏掉的Bug，被數學逼了出來

過去十年，開源世界最倚重的防線之一，是谷歌在2016年推出的OSS-Fuzz。

這套方法叫模糊測試，往程序入口裏成批灌半隨機的輸入，看哪一個能把程序搞崩。它累計跑了上萬億次測試。

但模糊測試終究是在迷宮裏碰運氣。它的輸入通常被限制在1MB以內，只要還有一條路沒走過，那裏的Bug就能一直藏下去。

研究團隊這回把測試入口改寫成了一道數學命題，在設定條件下，小於64MiB的任意輸入，都不會觸發約定的崩潰，包括斷言失敗和ASan內存檢測工具能捕捉的錯誤。

Claude要做的，就是證明它。一次跑通不算數，規定範圍內的每一種輸入、每一條能走到的路徑，都必須被證明不會觸發上述錯誤。

證明一旦卡住，要麼是Claude還沒找到證法，要麼是程序裏真有Bug。找到Bug後，Claude會自己打補丁，然後接着往下證。

於是，那些躲在測試夠不着的角落裏的Bug，現形了。

某個解壓器裏藏着一處計數器下溢，會把數據寫到內存邊界之外，可只有喂進約20MB、排布又很罕見的輸入才會觸發。

研究團隊稱，光是嘗試證明的過程，就揪出了數百個Bug。

測試和證明到底差多少，研究人員在Claude用Rust寫的Python解釋器裏，故意埋了7個Bug。

隨機測試放跑了其中5個，最後證明一個都沒放過。

狂跑391行代碼，63萬行證明

這批證明，做在了最底層。

Claude證明的對象，是編譯之後真正在CPU上運行的RISC-V機器碼。源代碼和編譯出來的程序未必完全一致，只有證到機器指令，證明的才是實際跑起來的那個程序。

為此，Theorem先把RISC-V指令和Linux進程的行為寫成了數學模型，目前的證明就建立在這套模型之上，限定在單線程、靜態鏈接、固定內存預算的環境中。

證到這一層，工程量開始爆炸。JSON解析庫cJSON的一個解析入口只有391行C代碼，Claude為它寫了63萬行Rocq證明。

膨脹上千倍，是因為證明要覆蓋整個進程。C程序的啓動、內存分配器、printf、內存檢測工具自己的運行時，全都要一併證明，和cJSON本身有關的只佔十分之一。

整個項目裏，Claude累計寫了約10億行證明，最後約1.8億行通過了檢查。其中超一半，是Claude給自己寫的工具自動生成的。

最後把關的，是Rocq證明檢查器，它按邏輯規則逐步驗算，一份證明要花30分鐘到幾個小時的CPU時間。檢查器確認的是證明符合規範，人類仍要審查規範和機器模型是否對應真實需求。

模型寫得再流暢，過不了檢查器，就一行都不算數。寫出這樣規模的證明，放在過去是一個不敢想的工程量。

傳奇微內核seL4，寫代碼只用了2人年，給它做完形式化驗證卻花了整整20人年。所以幾十年來，這種級別的安全保證，只有空客飛控這類人命關天的代碼才用得起。

而這一次，123個開源庫，Claude只用了幾週。

Claude給芯片寫了一套數學，順手揪出硬件Bug

要説Claude證明能挖得有多深，看一眼cpp-httplib就知道了。

為了排除遞歸太深、撐爆棧內存的可能，Claude追進了C++標準庫libc++的紅黑樹，在機器碼上證明這棵樹的高度始終被壓在對數級別。樹的高度受控，銷燬時的遞歸層數才有上限，才能繼續證明棧空間不會被耗盡。

它先把zlib壓縮格式的標準寫成形式化規範，再證明Linux內核自帶的zlib實現完全符合它。

這一回，證明做在了x86機器碼上。而x86指令集的數學模型，是Claude完全自主寫出來的。

這套模型準到什麼程度呢？在模型裏一條指令一條指令地單步推演，能在Linux內核上把Ubuntu的用戶態完整啓動起來。

寫模型的過程中，Claude找出了x86官方參考文檔裏的數百處錯誤，還發現了少量藏在CPU硬件本身裏的Bug。

從軟件一路證到芯片，AI已經在幫人類重新核對整台計算機的地基。

證明速度兩個月翻一番，1.34億美元的驗證路線圖

形式化驗證最大的門檻是貴，一份證明往往要燒掉數億token。如今這筆賬，正在飛快變小。

Anthropic用36個小型驗證任務做了測試，Opus 5.5完成其中一半所需的token，比Opus 5少了約40%。

Theorem測了今年5月到9月發佈的7款前沿模型，驗證速度大約每兩個月翻一番。

而且，證明可以複用。

Agent們共享工作區之後，同一組任務少花了17%的token。libcups、freerdp、libzmq這幾個八竿子打不着的項目，共用了運行庫等底層代碼，因此大段證明都是從別人證好的部分抄過來，改一改就用上了。

順着這個思路，Theorem算了一筆以Nix軟件生態為樣本的總賬。

在Nix軟件生態裏，只要9MB的共享基礎庫，就是三分之二機器碼的全部依賴。光是OpenSSL一個庫，就出現在近1.6萬個軟件包的運行依賴裏。

按今天的價格，把OpenSSL證穿一次約22萬美元，攤到每個下游軟件包，只要14美元左右。

Theorem推算，如果驗證能力保持兩個月翻倍，並按每年1億美元的預算推進，到2027年底，總成本約1.34億美元，就有望把Nix生態95%的機器碼納入證明。

作為對照，GovAI估計，全球網絡犯罪相關損失、應對和防禦支出，每年合計約5000億美元。

全球網安至暗48小時，讓數學來兜底

Linux內核是全世界測試得最狠的軟件之一，9月的一份Debian內核安全公告，就列出了1000多個漏洞。前沿大模型已經能把幾個看似無害的小Bug，串成一條致命的攻擊鏈。

找Bug的AI越來越強，靠人類一個個打補丁，已經追不上它的速度。

論文作者之一Aengus Lynch寫道，「對互聯網來説，這是一段可怕的日子。我相信，這是一束希望之光。」

他還相信，終有一天，Theorem會把所有關鍵軟件都形式化驗證一遍。

現在，首批25個庫、60個入口的證明已經在GitHub公開，任何人都能下載下來，親手驗算一遍。

寫代碼的機器越來越多，人類也正在把一條路走通，讓支撐數字世界的關鍵代碼，都帶上一份數學證明。

參考資料：https://x.com/AnthropicAI/status/2113390212911083894?s=20

本文為專欄作者授權創業邦發表，版權歸原作者所有。文章系作者個人觀點，不代表創業邦立場，轉載請聯繫原作者。如有任何疑問，請聯繫editor@cyzone.cn。