Anthropic正嘗試讓AI不只寫程式碼，還能用數學方法證明程式碼正確。該公司前沿紅隊與合作伙伴Theorem合作，利用Claude對現有開源軟體進行形式化驗證，在數週內為123個開源庫生成了約1.8億行數學證明程式碼，並在此過程中發現並自行修復了數百個常規測試未能捕捉的缺陷。

形式化驗證長期被視為成本極高的手段。此前，一個專家團隊需要20人年才能完成小型作業系統核心seL4的完整驗證，因此這類方法通常只用於空中客車航電軟體等極端關鍵場景。Anthropic此次的思路是讓Claude接管證明工作：模型不寫新程式碼，而是把Google OSS-Fuzz安全專案中的測試程式轉化為數學問題，分析編譯後的機器碼，並生成大量證明。獨立驗證程式Rocq會自動檢查這些證明，Anthropic稱整個過程幾乎不需要人工複核。

在生成證明的過程中，Claude遇到了數百個缺陷，並被允許自行修復。研究團隊表示，許多缺陷只有在非常特定的條件下才會暴露，例如異常大的輸入檔案或特定的訪問順序，因此常規測試很難發現。在驗證一款廣泛使用的PDF閱讀器時，團隊在一週內發現的安全缺陷數量，與該專案通常一整年報告的數量相當。另一個應用案例中，Claude捕捉到一個隱藏了十多年的邏輯錯誤。Anthropic還指出，即使最終證明失敗，嘗試過程本身也能暴露真實缺陷。

不過，Anthropic明確承認，“形式化驗證”並不等於“沒有錯誤”。這些證明只在嚴格條件下成立：特定的處理器架構、單執行緒程式，以及輸入小於64MB。現實中，這些庫執行在不同的硬體和配置上。計算成本也相當高，單個證明可能消耗數億個token，Anthropic未披露專案總成本。

從行業角度看，這項實驗的意義在於把AI程式設計的討論從“AI能否寫程式碼”推進到“AI能否證明自己寫的程式碼安全”。如果開發者能更信任AI生成的軟體，並減少人工審查時間，節省的將不只是驗證成本，還包括整個編碼流程的開銷。Anthropic還提到，較小規模的測試顯示證明具有可複用性，且新模型效率在提升：Opus 5.5完成一半證明所需的token比Opus 5少約40%。

Anthropic預計，AI形式化驗證很快會變得像標準測試一樣實用。Theorem的路線圖已瞄準glibc、OpenSSL和cURL等關鍵基礎設施。但這一願景能否落地，取決於證明條件能否覆蓋真實世界的複雜執行環境，以及算力成本能否降到可規模化複用的水平。