大型語言模型令更大規模的形式化軟件驗證成為可能

Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross

大部分軟件都充斥錯誤，而 AI 現在可以輕易找出並利用這些錯誤。抵禦網絡攻擊的標準防禦措施已不足夠：我們需要能夠證明程式碼沒有錯誤的方法。形式化軟件驗證或可提供這項保證，但過去需要專家投入多年心力，因此不適用於大部分現實項目。然而，我們與Theorem合作，證明情況已不再如此：LLM 現在能夠大規模產生形式化證明，讓新的軟件開發流程得以納入經證明的安全保證。我們使用 Claude，在超過 100 個現實世界的開源軟件程式庫中，於組合語言（RISC-V）層面證明瞭安全屬性。據我們所知，這是首個大規模運用 AI，在組合語言層面對正式環境軟件進行形式化驗證的工作。在撰寫證明的過程中，Claude 亦發現了多年來一直未被察覺的錯誤，儘管這些軟件曾經過數萬億次測試。隨着模型能力持續提升，我們預期形式化驗證將成為安全軟件開發不可或缺的一環。

引言

即使是成熟、經過大量測試的軟件，仍然包含錯誤，而 LLM 越來越擅長找出這些錯誤。Linux 核心是現今測試最充分的軟件之一，部署於全球數十億部裝置上，但最近仍有超過 1,000 個漏洞被披露。隨着前沿模型越來越有能力將看似無害的錯誤串連起來，形成嚴重漏洞，我們需要能在這些錯誤於實際環境中遭利用之前將其偵測並修復的技術。

理想情況下，這類技術能找出並修補所有錯誤，然後提供證明，確保再沒有其他錯誤。形式化驗證是其中一種方法。在形式化驗證中，開發者會將程式碼轉換成數學模型，再嘗試證明程式碼始終符合一組既定的安全規則。如果無法證明，就表示程式碼可能存在違反規則的錯誤，而證明失敗的情況亦能指出錯誤可能所在。重複這個過程（每次先消除失敗原因），最終便能證明程式碼沒有任何違反這些規則的錯誤。

然而，形式化驗證並不容易。證明的篇幅可能比原本的程式碼長很多倍，而撰寫證明需要付出大量心力，亦需要一套冷門而高度專門的技能。舉例來説，實作 seL4 作業系統核心用了兩人年，但對其進行形式化驗證卻用了20人年。因此，形式化驗證過去只適用於真正攸關任務成敗的應用，例如Airbus 的航空電子系統程式碼。

但大型語言模型令這件事容易得多。如今，前沿模型已能完全自主地為真實世界的軟件產生正確性證明。為了展示這一點，我們要求 Claude 證明 123 個開源程式庫的實用安全屬性，包括證明其中一些可執行檔在特定條件下永遠不會崩潰。具體而言，在若干假設下（即程式以單執行緒靜態二進制檔形式執行，並在使用 Linux 作業系統的 RISC-V¹ CPU 上使用固定的記憶體預算），Claude 證明瞭對所有小於 64 MB 的輸入，以及每一種經建模的 Linux 作業系統回應和記憶體配置，這些程式都會正常結束，不會觸發記憶體安全錯誤或令斷言失敗。這仍與修正所有可能的錯誤相距甚遠，但比以前接近得多，亦為實現這個目標提供了方向。

我們公開了其中一部分證明，讓任何人都可以驗證和重用，並同時公開RISC-V 和作業系統語義。這個項目的合作夥伴 Theorem 亦表示願意為其他開源專案執行相同的流程，並公開了一項Claude 技能，協助開發人員開始驗證自己的程式碼。

形式化驗證是一個涵蓋多種方法的廣泛領域。下文亦會介紹我們如何初步探索運用其他形式化驗證方法，加快其他安全或軟件開發工作，例如評估 zlib 壓縮演算法的安全性、證明以 Rust 編寫的 Python 解譯器在行為上等價，以及找出關鍵軟件中長期存在的錯誤。

形式化驗證的前景令人期待。隨着模型變得更智能，撰寫證明的成本正不斷下降。此外，隨着更多程式碼被形式化，以及取得安全保證的方法日趨標準化，跨不同程式碼庫重用或修改證明，將有助分攤成本。我們鼓勵所有開發人員探索運用大型語言模型進行形式化驗證，尤其是曾使用能力較弱的模型嘗試、但發現行不通的人。

本文其餘部分會更詳細介紹我們的形式化驗證實驗。

將測試轉化為證明

要證明一段軟件正確，我們首先必須説明「正確」究竟代表甚麼。正確性由規格（spec）定義。對於某些程式，我們可以清楚地以形式化方式描述其預期行為。例如，PNG 解碼器會接收一串位元組，並按照 RFC 2083 將這些位元組解碼為相應的圖像。但對大多數程式而言，事情並沒有那麼簡單。文字編輯器或網頁瀏覽器要怎樣才算「正確」？要制定全面且毫無歧義的規格並不容易，這是大規模驗證軟件的一大障礙。

為處理我們希望證明的開源程式庫程式碼，我們採用的方法是自動把它們現有且可編譯的測試套件轉換成規格，並編碼「此測試套件永遠會通過」這條規則；所用的是一個通用模型，描述在 Linux 上執行任何以 RISC-V 編譯的二進制檔代表甚麼。過去，要證明這類規格難以實現，因為要撰寫一份證明，涵蓋並論證數以萬計的組合語言指令在任何輸入下所有可能的行為和互動，本身就極其複雜（而且證明因此往往非常龐大）。這正是現今 LLM 派上用場的地方：LLM 非常擅長為明確定義的目標處理數百萬行程式碼。

這個項目從模糊測試着手。在這類測試中，開發者會在程式碼中撰寫一個入口點²，讓它接收輸入；任何會導致程式崩潰的輸入，都是作者關注的錯誤。接着，模糊測試器這個測試引擎會在入口點產生大量半隨機及經變異的輸入，嘗試找出錯誤（圖 1 有所示意）。模糊測試器執行得越久，就能找出越多錯誤。但這本質上是一個蠻力過程，無論嘗試多少輸入，都無法保證涵蓋所有可能的程式碼路徑。

為了找出模糊測試可能發現的所有錯誤，我們把模糊測試轉換成一份以已編譯的 RISC-V 指令為基礎的規格。規格指出，對於任何小於 64 MB 的輸入，模糊測試都不會令程式崩潰。³如果 Claude 能證明這份規格，那麼在 RISC-V 上進行這項模糊測試便再無必要：對該入口點進行模糊測試，永遠不會找到任何錯誤。

我們在 Google 的 OSS-Fuzz 計劃中，對數百個項目採用了這種做法。該計劃為符合資格的開源項目提供持續模糊測試。OSS-Fuzz 包含數千個由開發者編寫的入口點，透過令程式崩潰來找出程式碼屬性遭違反的情況（例如斷言失敗）。OSS-Fuzz 會自動為 C 和 C++ 程式加入 AddressSanitizer⁴（ASan）插樁，令程式在記憶體遭不當存取時崩潰（這是軟件漏洞的主要成因）。記憶體安全等廣泛適用的規格，幾乎適用於所有軟件。

在短短數星期內，Claude 成功修補了它發現的錯誤，並證明在 123 個不同的 OSS-Fuzz 程式庫中，239 個入口點對任何輸入（上限為 64 MB）都不會發生崩潰。這些證明針對已編譯的 RISC-V 指令（即可執行二進制檔案），合共約有 1.8 億行 Rocq 程式碼；每個證明通常約有 600,000 行，為中位長度為 18,000 條 RISC-V 指令的二進制檔案提供安全保證。這些證明透過使用 Theorem 的 RISC-V 指令語義及 Linux 程序語義，將 RISC-V 組合語言程式碼轉換成數學模型而建立。這表示目前這些證明假設程式在使用 Linux 作業系統的 RISC-V CPU 上，以單執行緒靜態二進制檔案形式運行，並採用固定的記憶體預算。擴大這些證明的適用範圍完全可行，因為只需為更多組合語言架構及其他作業系統程序訂立標準語義。請參閲專家對這些 Claude 所寫證明的看法。

雖然證明程式碼的數量極為龐大，但幾乎完全無需人工審查。Rocq 證明檢查器會確保證明正確滿足規格。因此，開發者只需信任以下項目：

• RISC-V 及 Linux 程序的形式模型；
• 已證明的確切定理陳述；
• Rocq 證明檢查器本身。⁵

這並不表示這些程式庫沒有錯誤。相反，這表示任何仍然存在的錯誤，只可能存在於上述項目中，或屬於 Claude 證明範圍以外。強化這些仍可能有錯誤的可信任元件（Rocq、RISC-V 及 Linux 語義）並非小事，但比起排查大規模擴展的證明所涵蓋的每一行程式碼，這項工作容易處理得多；尤其是這種方法可以保障任意數量的項目，而不增加可信任元件的規模。

我們歡迎對證明進行獨立驗證，亦鼓勵改進我們的方法。為此，我們公開了上述為本項目製作、目前尚未公開的可信任元件；Claude 對無需修補的模糊測試所作的完整 Rocq 證明；以及我們未能證明的其他模糊測試規格。

找出並修正錯誤

上文展示瞭如何將許多開放原始碼程式庫由開發者編寫的測試（模糊測試），轉化為 Claude 可以證明必定通過的規格；有時，還需先修補它發現的剩餘錯誤。因此，嘗試證明這些規格的過程發現了數百個錯誤。

Claude 嘗試證明數百個入口點時，發現了大量錯誤。為確保 Claude 不必每次遇到這種情況都停下來等待人手介入，我們讓 Claude 修正它發現的錯誤：它會修補程式碼，系統隨即以修補後的程式碼重新生成規格，然後 Claude 繼續證明新規格。⁶

我們發現的許多錯誤，都是模糊測試器幾乎不可能找到的。模糊測試器會修改小型輸入，通常上限為 1 MB，並通常依靠程式碼覆蓋率引導測試，以尋找錯誤。在證明某個程式庫的入口點時，Claude 在其版本的解壓縮器中發現計數器下溢，導致越界寫入；但這只會在大小約 20 MB、且採用一種罕見特定排列方式的輸入中發生。其他錯誤包括：圖像解碼器中的越界讀取，需要 64 MB 輸入及超過 2 GB 記憶體；另一個程式庫中的越界讀取，需要按特定次序透過兩個指向同一檔案的控制代碼呼叫；以及在 libexpat 中再次發現 CVE-2026-56132，這個漏洞需要深度巢狀的輸入。Claude 也找到了完全不會導致程式崩潰的邏輯錯誤。例如，在證明某個程式庫具備記憶體安全性時，它注意到一項限制應用程式可載入哪些檔案的功能，並非總是得到強制執行。

這個項目的最終目標，是證明以 RISC-V 編譯的模糊測試已沒有尚待找出的崩潰。不過，上述錯誤顯示，不論能否達成這個目標，這個流程還有另一項好處：單是嘗試這個流程，也能找出確實需要修復的錯誤。

證明的不止是記憶體安全

證明模糊測試已沒有更多崩潰可找，意義比聽起來更重大。現實世界的程式碼經常會用模糊測試，檢查是否違反有意義的高層次屬性，例如編碼與解碼的往返一致性、冪等性、代數定律、差異測試、自我一致性，或與參考實作等價。例如，LZO 壓縮演算法的模糊測試會檢查：若先壓縮輸入，再將其解壓縮，結果是否與原始輸入相同。如果這項屬性不成立，程式就會崩潰，因此證明測試永不崩潰，等同於證明這項屬性本身成立。

即使開發者沒有直接指定這些屬性，也可能出現這種情況。例如，為了完成對 cpp-httplib 的 OSS-Fuzz 證明，Claude 必須排除 std::set 解構函式因遞迴過深而導致堆疊溢位的可能性。遞迴深度受樹的最大深度限制，因此 Claude 必須在機器碼層面證明：libc++ 的紅黑樹重新平衡演算法已正確最佳化，能將樹的深度限制在對數級範圍內。

其他形式化驗證案例研究

形式化驗證的範疇十分廣泛。上述從模糊測試到證明的例子，是大型語言模型直接將證明應用於機器碼，令形式化驗證更廣泛易用的一個案例。

我們亦在其他方面成功結合大型語言模型與形式化驗證。例如，我們請 Claude 為 RFC 1950 撰寫形式化規格。RFC 1950 是定義 zlib 壓縮檔案格式的技術文件。之後，我們請 Claude 證明 Linux 核心中的 zlib 實作正確實作了該規格。與上述例子一樣，Claude 在二進制層面證明瞭這項性質；不過，這次 Claude 並非針對 RISC-V，而是直接證明以 x86 編譯的二進制檔，並使用由 Claude 生成（且經過大量測試）的 x86 ISA 形式化語義。⁷ 接着，我們以同樣方法處理另外六個廣泛使用的程式庫。過程中，我們在一些邊界情況發現了輕微（無法利用）的錯誤，目前正把這些問題提交至上游。這項工作帶來兩個結論：(1) 這些經過極充分測試的程式碼庫，已經幾乎完全正確；(2) 有可能為現有的真實程式碼庫證明端對端正確性屬性。

在另一項實驗中，我們請 Claude 用 Rust 開發一個支援 Python 大部分功能的直譯器，並使用 Verus（一種用於 Rust 的驗證工具）證明它遵循一篇學術論文所述的 CPython 語義。之後，我們透過執行超過 1.7 million 個隨機生成的 Python 程式，實際測量它遵循 CPython 行為的程度；結果顯示，在 99.95% 的測試中，它的行為與 CPython 完全一致，其餘測試的差異則是意料之中的已知邊界情況。

我們亦透過嘗試形式化驗證一些簡單的安全屬性，在數個廣泛使用且重要的應用程式中發現問題。其中一個問題是此前未被發現、潛藏超過十年的邏輯錯誤。在驗證一款廣泛使用的 PDF 閲讀器時，我們一星期內發現的安全漏洞，數量與通常一年內報告的數量相同。

如要進一步瞭解部分相關工作，請參閲附錄。

這只是開始

LLM 輔助形式化驗證的主要限制之一，是產生證明可能需要數億個 token。若要讓整個軟件生態系統都能使用這些方法，成本效益便至關重要。幸好，有充分理由相信效率會有所提升。

較新的模型所需 token 較少

我們根據真實 OSS-Fuzz 程式碼建立了 36 項小型驗證任務。Opus 5.5 能證明其中一半，所需 token 比 Opus 5 少約 40%。我們預期，隨着模型以長篇驗證任務進行訓練，這個趨勢會持續。

證明可以重用

Agent 分開工作時，往往會重複付出大量努力。證明和軟件一樣，都是由較小的證明遞迴構建而成；證明越小，通常越容易重用。為了衡量這種做法的影響，我們讓 Agent 在證明各自目標的過程中互相複製對方的證明。使用這個共享工作區時，Agent 所需 token 比單獨工作時少 17%；有些 Agent 更在先前單獨嘗試失敗後，最終成功。

我們在 OSS-Fuzz 證明工作中，也大規模觀察到同一現象。大部分證明涉及每個程式都包含的程式碼（尤其是 C 執行環境的初始化和 AddressSanitizer），因此差異很大的程式，最終也可能有大量重疊的證明。Agent 團隊利用這一點，複製另一個團隊已完成的證明，再按自己的程式加以修改（圖 6）。

正是這種證明的可重用性，令 Mathlib——Lean 中的形式數學共用程式庫——發展至收錄近 300,000 條定理，由 700 多名貢獻者提交：每項新證明都建基於既有成果。我們在 OSS-Fuzz 工作過程中也累積了類似規模的證明，其中部分會納入此次發布（我們不會發布可能暴露開源軟件中未修補錯誤的證明）。

當我們從這些初步實驗邁向下一階段，就需要制定策略來驗證大量現有軟件，首先處理最關鍵的依賴項。正如我們所示，使用通用規格並在二進制層面工作，便能大規模做到這一點，無須將整個程式碼庫改寫成另一種語言。

這種做法亦方便以套件層級重用證明，意味着每個依賴項只需驗證一次。依賴項呈現冪律分佈：只要證明少量共用程式庫，就能令大範圍軟件的形式驗證變得可行。詳情請參閲 Theorem 的路線圖，瞭解如何驗證整個 Nix 生態系統；當中包括 glibc、OpenSSL 和 cURL 等關鍵基礎設施。

限制

實際上，形式驗證有時能證明的程式碼安全性，可能不如我們所期望。

「形式上已驗證」不代表「沒有錯誤」。Claude 可以撰寫證明，説明編譯後程式的行為符合形式規格的要求（並由外部證明檢查器驗證）。然而，證明檢查器無法判斷規格是否符合現實。要符合現實，規格必須正確涵蓋並建模已驗證程式所運行的真實機器的一切，包括 CPU 和作業系統。經驗證的程式碼若出現錯誤，原因就在於規格或對機器語義的假設與現實不符。幸好，這也代表我們知道應在哪裏尋找剩餘錯誤，以及如何設計系統，將那些仍可能存在錯誤的缺口減至最低。以下説明這些問題如何適用於我們的證明，並提出未來可用來彌補這些缺口的工作構想。

實際機器的行為，有些並非模型所描述。我們的證明針對以 musl libc 連結的單執行緒靜態 RISC-V 二進制檔。不過，大多數人會在 x86 或 ARM 上使用這些程式庫，並以動態方式連結至 glibc。要縮小這個差距，我們需要更貼近實際部署系統的系統模型。例如，為 x86 建立準確的語義，便是邁向這個目標的一步。

這項主張未必涵蓋所有我們關注的情況。我們已證明，對於 Google OSS-Fuzz 中許多模糊測試入口點，任何大小低於 64 MB 的輸入都不會觸發崩潰，包括 ASan 崩潰。不過，ASan 並不能偵測所有記憶體安全漏洞，而且我們沒有驗證每個程式庫的所有入口點。即使我們驗證了所有入口點，也不能因此涵蓋整個程式庫（尤其是存在死程式碼時）。此外，實際程式可能會錯誤使用程式庫，導致呼叫端發生記憶體損毀。要縮小這個差距，我們需要規定呼叫端使用每個公開函式時必須遵守的事項，而呼叫端亦必須嚴格遵守這些規定。

我們預期，隨着我們更瞭解如何運用 LLM 進行形式化方法研究，以及模型持續改進，這些限制將變得可以克服，讓我們能夠驗證所依賴程式碼中更大比例的部分。

結論

發展方向已十分明確：過去，形式驗證只適用於安全關鍵程式碼中由專家量身打造的保證；不久之後，它將像今天的模糊測試一樣，適用於幾乎所有正式環境軟件。就像靜態型別、測試框架及其他正確性工具一樣，驗證將由「後加」走向「內建」；推動這項轉變的不僅是 LLM，還有語言設計和開發工作流程方面的創新。

在當今世界，LLM 正自動掃描並找出愈來愈多程式碼漏洞，我們必須採用能夠保證程式碼安全屬性的流程。由 LLM 擴展規模的形式驗證，是一種很有希望的方法，讓我們能在以往無法達到的範圍和規模上提供這些保證。我們鼓勵其他人進行實驗，讓我們共同建設一個穩健軟件廣泛普及、而軟件錯誤既少見、又廣為理解並能迅速處理的世界。

閲讀完整附錄。