使用模型檢驗器不需要LTL

使用模型檢驗器不需要學習線性時序邏輯。Kani、CBMC和Alloy等工具讓你能以普通的斷言和關係限制條件來驗證性質。你放棄了證明活性性質的能力，換來的是以小時而非週為單位的學習曲線，而對於大多數軟體錯誤來說，這是一筆值得的交易。

時序邏輯是大多數模型檢驗器要求的守門人

經典的模型檢驗器，SPIN和NuSMV，要求你以時序邏輯公式或計算樹邏輯來表達性質。你寫諸如G(request -> F(response))這樣的東西來表示「全域地，每個請求最終都會得到回應」。這很強大。它可以證明你的protocol永遠不會deadlock，每則訊息最終都會被確認，你的系統是公平的。

這也是大多數在職開發者不具備的專業技能。讀一個時序邏輯公式不像讀程式碼。運算子是模態的，語法定義在無限路徑上，而你在寫單元測試時建立的直覺無法遷移。所以這個問題是合理的：如果你想要模型檢驗的錯誤發現能力，你真的必須先攀登那座高山嗎？

不。另一類工具已經存在數十年，它們用你已經在寫的相同斷言來檢驗程式碼。

有界模型檢驗器將斷言轉化為可滿足性問題

有界模型檢驗器不要求你學習新的邏輯。它要求你編寫測試支架。你宣告非確定性輸入，用假設來限制它們，並在宿主語言中斷言性質。然後該工具將迴圈展開到一個界限，將程式編碼為SAT或SMT公式，並讓求解器尋找反例。

如果求解器回傳UNSAT，那麼你的性質在該界限內的所有路徑上都成立。如果它找到反例，你會得到一個具體的追蹤，準確顯示哪些輸入觸發了錯誤。沒有時間運算子。沒有無限路徑。只有一個帶有可復現輸入向量的失敗斷言。

Kani是Rust最平易近人的有界模型檢驗器。它可以透過cargo install kani-verifier安裝，並在普通Rust程式碼上執行。

真實範例：在Rust中檢驗 state machine

這裡有一個帶錯誤的state machine。它追蹤一個簡單的計數器，每次滴答遞減，直到歸零，然後轉回閒置狀態。

#[derive(Clone, Copy, PartialEq, Debug)]
enum State {
    Idle,
    Running,
    Stopped,
}

struct Machine {
    state: State,
    count: u32,
}

impl Machine {
    fn start(&mut self, initial: u32) {
        if self.state == State::Idle && initial > 0 {
            self.state = State::Running;
            self.count = initial;
        }
    }

    fn tick(&mut self) {
        if self.state == State::Running {
            self.count -= 1;
            if self.count == 0 {
                self.state = State::Idle;
            }
        }
    }

    fn stop(&mut self) {
        if self.state == State::Running {
            self.state = State::Stopped;
        }
    }
}

這個錯誤很微妙。看stop。它將狀態設為Stopped，但讓count保持不變。如果之後有東西假設state == State::Stopped時count == 0，那這個假設就是錯的。

下面是一個能捕捉到它的Kani證明支架：

#[kani::proof]
fn check_stopped_implies_count_zero() {
    let mut machine = Machine {
        state: State::Idle,
        count: 0,
    };

    let initial: u32 = kani::any();
    kani::assume(initial > 0 && initial <= 10);

    machine.start(initial);
    machine.tick();
    machine.stop();

    assert!(
        machine.state != State::Stopped || machine.count == 0,
        "Stopped state should have count == 0"
    );
}

Kani會探索每一條路徑。它發現如果initial == 2，在start之後機器是Running狀態且count == 2。一次tick將count減到1，但狀態保持Running。然後stop將狀態設為Stopped而count仍為1。斷言失敗。Kani會報告這條確切的追蹤。

這就是不用時序邏輯的模型檢驗體驗。你寫Rust。你用Rust寫斷言。工具告訴你哪些輸入會破壞它們。

Alloy用關係邏輯發現設計層面的錯誤

有界模型檢驗器驗證程式碼。Alloy驗證設計。

Alloy是一個模型搜尋器，不是傳統的模型檢驗器，但區別不如工作流程重要。你將系統描述為一組關係，將狀態不變式描述為一階邏輯限制條件，然後讓Alloy尋找反例。它搜尋使用者定義範圍內的所有可能實例，並向你展示失敗示意圖。

下面是一個簡單有向圖性質的Alloy模型：

sig Node {
    next: set Node
}

pred reachable[n1, n2: Node] {
    n2 in n1.^next
}

assert symmetric_reachability {
    all n1, n2: Node |
        reachable[n1, n2] implies reachable[n2, n1]
}

check symmetric_reachability for 3

該斷言聲稱可達性是對稱的。Alloy檢驗所有不超過三個節點的圖，並立即畫出一個反例：n1指向n2但n2沒有出邊的圖。沒有任何地方出現G、F或U運算子。

你放棄的東西：活性與無限行為

這種便利性是有代價的。有界模型檢驗器只驗證到迴圈界限或路徑長度為止的行為。它不能證明請求最終會得到回應，只能證明壞事不會在前N步內發生。Alloy只檢驗其範圍內的實例。它不能為任意大的系統證明性質，只能證明界限以下不存在反例。

如果你需要證明你的共識protocol永遠不會遺失已提交的寫入，或每則訊息最終都會被投遞，你仍然需要時序邏輯和無界模型檢驗。像TLA+這樣的工具將時序邏輯包裝在更像數學而非模態邏輯的語法中，但底層語義仍然是時序的。

對於資料結構不變式、API契約強制，以及尋找只在第47條執行路徑上觸發的race condition，有界工具通常已經足夠。它們捕捉到單元測試遺漏的錯誤，而且用的是不用教科書就能讀懂的斷言。

五分鐘上手Kani

如果你已經安裝了Rust，有界模型檢驗只需一個命令之遙。

cargo install kani-verifier
cargo kani setup

建立一個新的crate，寫一個帶有微妙錯誤的函式，然後新增一個#[kani::proof]支架。執行cargo kani。如果Kani找到反例，它會印出觸發失敗的具體輸入。如果它回報VERIFICATION SUCCESSFUL，你的性質在預設界限內的所有路徑上都成立。

從狀態空間小且不變式清晰的函式開始。state machine、parser驗證和protocol狀態轉移都是理想的首選目標。不要一開始就試圖驗證整個HTTP伺服器。SAT求解器有限度，你的耐心也是。

常見問題：有界與無界、活性以及從何處開始

有界模型檢驗真的是模型檢驗嗎？

從技術上講，它是一種變體，將問題編碼為可滿足性查詢，而非明確探索狀態圖。對於試圖發現錯誤的開發者來說，這種區別只是學術上的。它系統地探索所有路徑，這正是實踐中模型檢驗的含義。

我能用Kani或CBMC證明活性嗎？

不能直接證明。活性性質需要對無限行為進行推理，而有界工具明確限制了搜尋範圍。有時你可以透過展開足夠多的步驟以達到不動點來編碼有界活性檢查，但那是進階技巧。

TLA+呢？它需要時序邏輯嗎？

TLA+使用時序動作邏輯，所以從技術上講是的。但Leslie Lamport設計的語法讀起來像普通數學。大多數TLA+規格將90%的篇幅花在狀態不變式和資料結構限制條件上，而非時序運算子。如果你確實需要無界時序推理，它是最易接近的路徑。

我應該用Alloy還是Kani？

如果你有Rust程式碼而且想驗證實作細節，用Kani。如果你還在設計系統，想在寫程式碼之前探索你的不變式是否甚至可行，用Alloy。

選擇匹配你問題的工具，而非匹配你野心的工具

時序邏輯優美而強大，但它不是形式驗證的先決條件。有界模型檢驗器和關係模型搜尋器讓你用已經會的語言表達性質。它們不會證明你的系統最終終止，但會發現那個破壞資料庫state machine的差一錯誤。對於大多數團隊來說，那才是要緊的錯誤。

從一個有狀態的函式開始用Kani。寫一個斷言。讓求解器告訴你遺漏了什麼。