Anthropic用Claude形式化驗證123個開源庫，發現潛伏多年漏洞

金色財經報道，10月23日，據Anthropic研究博客，Anthropic與Theorem合作，使用Claude在RISC-V彙編層面對123個開源庫進行形式化驗證，證明其在特定假設下（單線程靜態二進制、固定內存預算、RISC-V CPU及Linux系統、輸入小於64MB）對任意輸入均不會出現內存安全錯誤或斷言失敗，相關證明涵蓋239個入口點、約1.8億行Rocq代碼。Anthropic稱，這是在彙編層面對生產軟件進行AI形式化驗證的首次大規模嘗試。過程中Claude還發現並修補了潛伏多年、即便經歷數萬億次測試運行也未被檢出的漏洞。Anthropic同時提示，形式化驗證不等於無漏洞，其結論依賴於對RISC-V及Linux語義等可信組件的假設。