形式化驗證中最困難的部分從來不是驗證器本身，而是編寫證明。

給一位資深Rust工程師Verus——微軟研究院開發的基於SMT的驗證器——他可以在一個下午內為函式新增前置條件和後置條件註解。然後驗證器會以機械確定性告訴他，該函式是否對所有可能的輸入滿足這些契約。這部分令人滿意。

接著他遇到了迴圈。驗證器抱怨無法建立後置條件。工程師需要一個不變量——一個在每次迭代前後都成立的邏輯陳述。尋找這個不變量過去需要博士學位，或者至少四十小時的反覆試錯。發表於OOPSLA 2025的AutoVerus利用LLM智慧體網路將這項工作自動化了90%以上。中位數的證明任務在30秒內或三次LLM呼叫內解決。

以下是它的實際運作原理、成本以及仍然失效的地方。

真正的瓶頸是不變量搜尋，而非SMT求解器

Verus透過幽靈程式碼、前置條件和後置條件擴展了Rust。你寫的程式碼類似這樣：

use vstd::prelude::*;

verus! {
    fn sum(arr: &[i32]) -> (result: i32)
        requires
            arr.len() <= 0x40000000,
        ensures
            result == spec_sum(arr@),
    {
        let mut total = 0;
        let mut i = 0;
        while i < arr.len()
            invariant
                0 <= i <= arr.len(),
                total == spec_sum(arr@.subrange(0, i as int)),
        {
            total = total + arr[i];
            i = i + 1;
        }
        total
    }
}

requires子句是前置條件。ensures子句是後置條件。while迴圈內的invariant區塊是讓證明通過的關鍵。它告訴SMT求解器每次迭代中什麼保持為真。

困難的部分是不變量。total == spec_sum(arr@.subrange(0, i as int))並不直觀。人類透過歸納地思考處理前i個元素後什麼保持為真來寫出它。AutoVerus將不變量綜合視為由驗證器回饋引導的搜尋問題，從而自動產生它。

AutoVerus如何將LLM智慧體用作搜尋策略

AutoVerus不是對GPT-4的單一提示。它是一個專業智慧體的流水線，彼此傳遞結構化上下文。

第一個智慧體讀取你的Rust函式及其文件註解。它提取驗證條件並產生requires、ensures和invariant子句的初始草案。

第二個智慧體將這些註解輸入Verus。Verus編譯帶註解的程式碼，並要求其SMT求解器（通常是Z3）消除證明義務。如果求解器回答UNSAT，則性質成立。如果回答SAT，則產生反例。大多數情況下，初稿會失敗。

修復智慧體讀取驗證器錯誤訊息和失敗的證明義務。它建議更強的不變量、更緊的界限或輔助引理。迴圈重複：生成、驗證、修復。AutoVerus報告的中位數收斂為三次LLM呼叫。超過一半的150個非平凡benchmark任務在30秒內完成。

關鍵洞察不是LLM在邏輯上非常出色。證明搜尋是一個區域最佳化問題，而LLM在猜測區域改進方面足夠好，能比手工輸入的人類更快地導航搜尋空間。

90%這個數字實際意味著什麼

AutoVerus在150個非平凡Rust證明任務benchmark上實現了超過90%的證明自動化。這些任務包括陣列邊界推理、迴圈累積和遞迴結構遍歷。benchmark來自真實的Verus程式碼庫。

90%的數字意味著LLM流水線產生了Verus無需人工介入即可接受的證明。這並不意味著規範是程式設計師預期的。LLM從函式名稱、文件註解和型別簽名推斷意圖。如果你的函式名為process，文件註解寫的是”handles the thing”，產生的規範將是通用的，可能是錯誤的。

這與Copilot為程式碼生成引入的分工相同。LLM寫初稿，人類審查領域正確性。區別在於錯誤的證明是沉默的。通過驗證的產生證明可能證明了錯誤的性質。你仍然需要理解函式應該做什麼的人。

AutoVerus不能做什麼

AutoVerus受限於Verus能表達的內容。Verus處理Rust的一個子集。它不支援非同步、閉包或某些標準函式庫集合。如果你的程式碼用tokio產生任務，AutoVerus目前還幫不了你。

AutoVerus也受限於模式。90%的成功率適用於看起來像訓練分佈的程式碼：陣列上的迴圈、算術累積、邊界檢查。如果你的證明需要非顯而易見輔助引理，修復智慧體可能迴圈直到達到迭代限制。那時你就得手寫證明了。

成本也不是零。benchmark任務每個證明花費幾美分。一個完整模組可能花費十到三十美元的API呼叫。這比驗證工程師的時間便宜兩個數量級，但不是免費的。

在實際程式碼上執行AutoVerus

AutoVerus可從微軟研究院取得。儲存庫是GitHub上的microsoft/verus-proof-synthesis。它要求你已安裝Verus。

實際工作流程如下：

# 1. Install Verus
git clone https://github.com/verus-lang/verus.git
cd verus && source ./source/vstd.sh

# 2. Clone AutoVerus
git clone https://github.com/microsoft/verus-proof-synthesis.git
cd verus-proof-synthesis

# 3. Set your API key for the LLM backend
export OPENAI_API_KEY="sk-..."

# 4. Run AutoVerus on a Rust file
python autoverus.py --input src/my_module.rs --output src/my_module_verified.rs

輸出是一個帶requires、ensures和invariant子句註解的Rust檔案。審查每個註解。然後執行Verus：

verus src/my_module_verified.rs

如果Verus報告verification results:: verified，則SMT求解器已消除所有義務。如果報告錯誤，將其回饋回AutoVerus進行另一輪修復，或手動修復。

對於CI整合，將Verus視為僅在帶註解模組上執行的獨立作業。Verus驗證時間隨註解複雜度增長。從你害怕的函式開始：parser、protocol state machine、任何索引到不受信任 buffer的程式碼。

何時使用AutoVerus，何時放棄

當你有適合Verus子集的Rust程式碼且想要無界正確性證明時，AutoVerus值得嘗試。Kani提供無需註解的有界證明，對崩潰自由檢查更快，但無法證明跨越無界迴圈的性質。AutoVerus提供完整的無界證明，代價是需要它主要為你產生的註解。

如果你的程式碼是非同步的、使用複雜閉包，或需要關於活性性質的證明（如”每個請求最終都會得到回應”），請放棄。對於活性，你仍然需要TLA+。如果你的證明需要自訂數學理論，請放棄。LLM智慧體不會發明新數學。它們檢索並適應以前見過的模式。

誠實的底線

AutoVerus並未消除理解程式碼的必要性。它消除了為你已經理解的程式碼花費四十小時編寫不變量的必要性。轉變是從證明工程到提示工程：你描述意圖，智慧體搜尋證明空間，SMT求解器認證結果。

這一轉變足以將形式化驗證從專家小眾領域轉變為CI流水線步驟。對於應用程式與不受信任網路輸入之間的三十行解析程式碼，現在可以實際證明它們不會恐慌。證明在幾秒鐘內產生，在幾分鐘內檢查，由知道parser應該做什麼的人審查。

從一個函式開始。寫Rust。執行AutoVerus。閱讀註解。如果它們符合你的意圖，你就有了一個機器檢查的證明。如果不符合，你有一個比空白頁更好的起點。

Frequently Asked Questions

What is AutoVerus and how does it relate to Verus?

AutoVerus is an automated proof generation system built on top of Verus, a Rust verifier from Microsoft Research. Verus checks whether annotated Rust code satisfies its specifications using an SMT solver. AutoVerus generates those annotations using a network of LLM agents.

How accurate is AutoVerus at generating proofs?

On its benchmark of 150 non-trivial Rust proof tasks, AutoVerus achieved over 90% automation. More than half resolved in under 30 seconds or three LLM calls. Accuracy depends on how closely your code matches the training distribution patterns.

Does AutoVerus eliminate the need to learn formal verification?

No. You still need to understand the annotations to review them for correctness. A generated proof that passes verification may prove the wrong property if the LLM misread your intent. AutoVerus reduces proof writing time from days to minutes, but it does not replace human judgment.

What Rust code works with AutoVerus?

Code that fits the Verus subset: functions with loops, array indexing, arithmetic, and recursive structures. AutoVerus does not support async, closures, or many standard library collections. It is best suited for systems code, parsers, and algorithmic functions.

How much does AutoVerus cost to run?

The benchmark tasks cost cents per proof. A full module might cost ten to thirty dollars in API calls. This is significantly less than the 40 to 80 hours of engineering time required for manual proof writing.