不寫一行證明也能證明 Rust 程式碼正確。幹這活的工具叫做模型檢驗器，目前對 Rust 最實用的一個是 AWS 開發的 Kani。你寫普通的 Rust 斷言，Kani 把它們轉成數學命題，對所有可能的輸入進行檢驗。不需要定理證明器，不需要證明輔助工具，也不需要一頭栽進 Coq 半年出不來。

問題在於，「所有可能的輸入」只有在輸入空間足夠小、可以窮舉的時候才成立。如果你的函式接收一個有百萬個元素的 Vec<u8>，Kani 不會檢查每一種排列。它只會檢查到你指定的邊界為止，或者跑到你的筆記型電腦記憶體耗盡。證明是真的，但它是有界的。

「無證明的證明」到底是什麼意思

形式化驗證通常意味著在 Coq 這樣的證明輔助工具裡寫程式，手工定義不變式，用戰術步驟引導求解器。像 CompCert 這樣的驗證編譯器花了好幾年。大多數團隊沒有好幾年。

模型檢驗不一樣。你寫普通的 Rust。新增一個帶有 #[kani::proof] 註解的驗證函式。在裡面用 kani::any() 產生符號值，呼叫你的程式碼，然後做出斷言。Kani 把你的程式碼編譯成邏輯公式，交給 SMT 求解器。求解器要麼確認該性質在邊界內的所有輸入上都成立，要麼給出一個具體的反例。

你沒寫證明。你寫了一個帶全稱量詞的測試。證明是工具寫的。

Kani 如何把 Rust 變成邏輯

Kani 是一個有界模型檢驗器。它把你的程式碼展開成邏輯公式，問 SMT 求解器：有沒有哪條執行路徑會違反斷言？求解器把變數當成符號處理。普通測試給 x 賦值為 5，Kani 的證明給 x 一個符號，代表所有可能的 u32。

下面是一個 trivial 的例子。我們有一個不應該溢出的函式，想證明這一點。

// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
    x.saturating_mul(2)
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    fn check_saturating_double_never_overflows() {
        let x: u32 = kani::any();
        let result = saturating_double(x);
        if x > u32::MAX / 2 {
            assert_eq!(result, u32::MAX);
        } else {
            assert_eq!(result, x * 2);
        }
    }
}

執行 cargo kani，Kani 在數秒內完成驗證。它不逐個執行，就檢查了 x 的全部 4,294,967,296 種可能取值。SMT 求解器從符號表示出發進行推理，得出結論：不存在反例。

#[cfg(kani)] 守衛意味著這段程式碼只在 Kani 下編譯，不會膨脹你的發布版本。

真實例子：證明一個parser永不崩潰

溢出是簡單的情況。有意思的案例是資料相關的。假設我們有一個解析小型protocol header的函式，想證明無論餵給它什麼位元組，它都絕不會 panic。

// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
    TooShort,
    InvalidVersion,
}

pub struct Header {
    pub version: u8,
    pub length: u16,
}

/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
    if buf.len() < 4 {
        return Err(ParseError::TooShort);
    }
    let version = buf[0];
    if version != 1 {
        return Err(ParseError::InvalidVersion);
    }
    let length = u16::from_be_bytes([buf[2], buf[3]]);
    Ok(Header { version, length })
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)]
    fn check_parse_header_no_panic() {
        let len: usize = kani::any();
        kani::assume(len <= 8);
        let buf: [u8; 8] = kani::any();
        let _ = parse_header(&buf[..len]);
    }
}

Kani 驗證 parse_header 對長度從 0 到 8 的所有輸入 buffer 都不會 panic。它檢查了邊界測試、版本檢查和陣列索引。如果我們沒有先檢查長度就寫了 buf[1]，Kani 會找到一個反例：一個 1 位元組的 buffer，buf[1] 越界。

#[kani::unwind(5)] 註解告訴 Kani 把迴圈展開多少次。由於我們的函式裡沒有迴圈，這個值是保守的。

邊界化問題：模型檢驗撞牆的地方

模型檢驗在邊界內是窮盡的。超出邊界，它一言不發。這是根本的權衡。

迴圈是第一道牆。Kani 必須把每個迴圈固定展開若干次。如果你的函式遍歷一個 Vec，你把展開邊界設為 10，Kani 證明長度為 0 到 10 的向量的正確性。它對長度 11 無話可說。每增加 1，狀態空間就翻倍。展開 50 也許幾分鐘能跑完，展開 500 可能永遠跑不完。

遞迴類似。每次呼叫都會膨脹公式。深度遞迴會讓記憶體使用量爆炸。

資料大小是第二道牆。Kani 擅長處理固定大小的陣列。動態分配的集合除非顯式限制大小，否則它很吃力。

標準函式庫是第三道牆。Kani 建模了其中很大一部分，但不是全部。如果你呼叫了 Kani 不理解的東西，證明會因為缺少函式定義而失敗。

Kani 能證明什麼、短板在哪裡

Kani 擅長在有界程式碼中發現 panic、整數溢位和斷言違反。它對密碼學原語、protocol parser和small state machine特別出色。這些地方的特點是：一個壞輸入就能釀成災難，而且程式碼天然有界。

Kani 不擅長證明活性性質，比如「每個請求最終都會得到回應」。這需要對無限執行進行推理，而有界模型檢驗明確不做這件事。對於活性，你需要像 TLA+ 這樣的時序模型檢驗器。

Kani 也不能替代測試。通過證明意味著邊界內不存在反例。通過測試意味著程式碼在你關心的某個具體輸入上行為正確。Kani 抓住你想不到的邊界情況。測試抓住 Kani 看不見的整合問題。

在 CI 裡跑 Kani，別把 runner 跑崩

一個針對小函式的 Kani 證明只需數秒。一個真實 crate 的完整套件需要數分鐘。展開邊界高的證明可能跑上數小時。你不會想讓 CI 管線等一個兩小時的 SMT 求解。

保持 Kani 證明小而快。去證明安全攸關的函式——那些出了 bug 就是事故的函式。別試圖證明你的整個 Web 框架。設定逾時，比如每個證明 5 分鐘，並且把逾時視為「未能證明」，而不是「證明失敗」。

以下是一個有效的 Makefile 模式：

# Makefile
kani:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 300 --all-functions --enable-unstable

kani-fast:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 60 --all-functions --enable-unstable

kani-fast 在每個 pull request 時跑 CI。kani 每晚跑。如果證明出現退化，你一天內就能發現，而不是在出貨之後。

如果你暴露了公共 API，為每個公共函式寫一個 Kani 證明，用完全符號化的輸入去呼叫它。這是最接近形式化契約測試的東西。它不證明實作正確，但證明實作在任意有效輸入上都不會崩潰。

什麼時候該換真正的證明輔助工具

如果你需要證明關於無界資料結構的性質，比如「這條鏈結串列永遠無環」，Kani 幫不了你。展開邊界會推翻這個論斷。這時候你需要 Creusot 這樣的工具，它把 Rust 翻譯成 WhyML，再用證明輔助工具。工作量更大，但能處理無界結構。

如果你需要等價性證明或未定義行為偵測，MIRI 或 KLEE 這樣的工具位於工作量與覆蓋率的譜系上不同位置。Kani 是「我有有界程式碼，想知道它會不會 panic」的甜蜜點。parser、解碼器、序列化器和配置驗證器都適用。Rust 的型別系統已經消滅了整個類別的 bug。Kani 消滅的是型別系統夠不到的那些。

先嘗試什麼

如果你有一個 Rust crate，裡面有個讓你心裡發毛的函式，加上 Kani。讓你發毛的通常是解析不可信輸入、做位元運算、或者對陣列做索引的函式。寫一個證明框架，用 kani::any() 呼叫它。執行 cargo kani。通過了，你就得到了一個有界的崩潰自由證明；失敗了，你就得到了一個具體的反例——那本來會是一個 bug 回報。

你不需要學一門新語言。你不需要理解序貫演算。你寫 Rust 斷言，求解器告訴你它們是否成立。這不是學術意義上的形式化證明，而是實用意義上的機械證明。而對大多數軟體來說，實用恰恰就是你需要的。

常見問題

軟體驗證中的模型檢驗是什麼

模型檢驗是一種自動化技術，它窮舉系統的所有可能狀態，以驗證指定性質是否成立。對於 Rust，Kani 這樣的工具使用有界模型檢驗來證明在限定邊界內所有可能輸入上的斷言，無需手工構造證明。

Kani 與寫單元測試有什麼不同

單元測試檢查一個具體輸入。Kani 的證明檢查邊界內的每一個輸入。如果 Kani 的證明通過，你就知道有界狀態空間內不存在反例。證明更強，但受你設定的邊界限制。

Kani 能證明我的整個 Rust 應用程式都正確嗎

不能。Kani 最適合小型、有界的函式。狀態空間隨迴圈迭代次數、遞迴深度和資料大小指數成長。把 Kani 用在parser、protocol handler這類安全攸關的元件上，而不是應用層邏輯。

當 Kani 遇到沒有固定邊界的迴圈時會發生什麼

Kani 需要為迴圈指定展開邊界。如果迴圈可能執行的次數超過邊界允許，Kani 會插入一個失敗的展開斷言。你必須提高邊界，或者重構程式碼使其具有靜態已知的迭代次數。這是有界模型檢驗的主要限制。