從模糊測試到數學證明：自動化規格轉換機制
傳統上，形式化驗證需要開發者手動將程式碼轉換為數學模型並撰寫證明，這過程極其耗時且需要高度專業的技能。例如，驗證seL4作業系統核心曾花費20人年，遠超過實作該核心的時間。
為了克服規格定義的困難，研究團隊採用了一種自動化方法：將現有的模糊測試（Fuzz Tests）轉換為形式化規格。具體來說，他們將「測試套件永遠通過」這一規則編碼為規格，並基於RISC-V指令集和Linux作業系統的一般執行模型進行驗證。
這種方法繞過了為複雜軟體（如文字編輯器或瀏覽器）定義完整行為規格的難題，轉而關注更廣泛且可自動生成的屬性，例如記憶體安全性和斷言不失敗。Claude被要求證明這些程式在任何小於64 MB的輸入下，都不會觸發記憶體安全錯誤或斷言失敗。
驗證範圍與技術限制：RISC-V組語層級的邊界
此次驗證並非針對原始碼，而是直接針對編譯後的RISC-V組語指令（可執行二進位檔）。這意味著證明涵蓋了編譯器可能引入的錯誤，但也引入了對特定硬體架構和作業系統模型的依賴。
目前的驗證假設程式以單執行緒、靜態連結的二進位檔形式運行，並使用固定的記憶體預算。此外，輸入大小被限制在64 MB以內，且僅針對Google OSS-Fuzz專案中的特定入口點進行驗證，並未涵蓋整個函式庫的所有程式碼路徑或死代碼。
研究團隊指出，雖然ASan（AddressSanitizer）能檢測許多記憶體錯誤，但它並非萬能，無法檢測所有記憶體安全問題。此外，若呼叫者誤用函式庫導致記憶體損壞，這類問題也不在當前證明的涵蓋範圍內。
發現長期潛伏的錯誤與邏輯缺陷
在嘗試生成證明的過程中，Claude不僅修復了導致測試失敗的錯誤，還發現了一些傳統模糊測試難以捕捉的深層問題。例如，在某個解壓縮器中發現了一個計數器下溢導致的越界寫入錯誤，該錯誤僅在約20 MB且具有特定罕見佈局的輸入下才會觸發。
其他發現包括一個需要64 MB輸入和超過2 GB記憶體才能觸發的影像解碼器越界讀取錯誤，以及libexpat中一個需要深度巢狀輸入才能重現的CVE漏洞（CVE-2026-56132）。
Claude還發現了一些不會導致崩潰但存在邏輯錯誤的情況。例如，在某個函式庫中，限制應用程式可載入檔案的功能並未總是得到強制執行。這些發現表明，即使未能完成最終的無崩潰證明，嘗試進行形式化驗證的過程本身也能揭示真實且重要的軟體缺陷。
成本效率與證明重用：未來擴展的可能性
生成形式化證明的主要障礙之一是高昂的Token成本。然而，研究顯示較新的模型（如Opus 5.5）在處理驗證任務時所需的Token數量比舊版本減少約40%，且完成速度更快。
透過讓多個代理共享工作區並重用彼此生成的證明片段，團隊發現所需Token數量可進一步減少17%。這是因為許多程式碼（如C運行時初始化和ASan檢查）在不同專案間具有高度相似性，使得證明可以模組化重用。
這種重用機制類似於數學庫Mathlib的發展模式，隨著更多程式碼被形式化，驗證成本將因證明的累積和標準化而攤銷。Theorem公司表示將提供工具協助開發者對自己的程式碼進行驗證，並計劃擴展至x86架構和其他作業系統環境。
社群回饋與技術質疑
部分開發者對該方法的實用性提出質疑，認為將ASan檢測的二進位檔與非檢測版本進行行為等價性驗證是一種「聰明但彆扭」的Hack方法。他們擔心這種間接驗證可能無法完全反映真實環境中的記憶體安全問題。
另有評論指出，形式化驗證的核心挑戰在於如何驗證「驗證器本身」以及規格模型是否準確反映了現實世界的硬體和作業系統行為。若底層語義模型存在錯誤，則基於該模型的證明將失去意義。
儘管存在這些技術限制，社群中也出現了實際應用案例。例如，有開發者利用LLM輔助形式化驗證來比對Rust重寫的PostgreSQL與原始C代碼的行為一致性，目前已驗證約12%的程式碼（約7萬行C代碼）在單執行緒下行為相同。
