全球軟體的bug，要被Claude端掉了？
短短48小時，全球就爆了27起重大網路攻擊，現在人們都在瘋傳，「最暗十月」來了。
一早，Anthropic前沿紅隊團隊聯手Theorem Labs發佈了一份重量級報告——
他們讓Claude深入到底層彙編指令（RISC-V），向真實的生產級開放原始碼庫發起總攻。
短短幾周，Claude拿下了123個開放原始碼庫中的239個測試入口的形式化驗證，狂飆1.8億行Rocq數學證明程式碼，全部通過機器核驗！
Google平台跑了上兆次都沒撞出來的隱秘漏洞，連同潛伏十餘年的高危邏輯死角，甚至x86處理器硬體本身的真實缺陷，在這場大清剿中悉數現形。
更誇張的是，在一個熱門的PDF閱讀器中，Claude一周挖出的安全漏洞，直接頂得上它通常一整年的報告量。
這一次，Claude把找Bug、修Bug和驗證修復連成一條流程，展開了一場「數學級」Bug清掃。
席捲全球的網路安全危機，或許真的有救了。
兆次測試漏掉的Bug
被數學逼了出來
過去十年，開源世界最倚重的防線之一，是Google在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公開，任何人都能下載下來，親手驗算一遍。
寫程式碼的機器越來越多，人類也正在把一條路走通，讓支撐數字世界的關鍵程式碼，都帶上一份數學證明。(新智元)