Kani: Rust 的模型檢查器

Kani 是一個開源的 Rust 模型檢查器，旨在為 Rust 編譯器所有權類型系統無法驗證的屬性提供形式化正確性保證，例如 unsafe 操作的健全性、功能正確性以及避免運行時恐慌（runtime panics）。透過將 Rust 的 Mid-level Intermediate Representation (MIR) 編譯成 CBMC 位元精確（bit-precise）驗證引擎，Kani 使開發者能夠在不需要使用者註解的情況下，自動驗證安全性屬性。

邊界與無界驗證

Kani 提供兩個層級的驗證：邊界模型檢查（bounded model checking）與無界驗證（unbounded verification）。邊界模型檢查允許工具在無需使用者干預的情況下，自動檢查一組全面的安全性屬性。對於需要無界驗證的更複雜屬性，Kani 引入了一種規範語言，其中包含函數合約（function contracts）、迴圈合約（loop contracts）、量詞（quantifiers）以及函數存根（function stubbing）。

技術實作

Kani 的架構將證明腳手架（proof harnesses）從 Rust 的 Mid-level Intermediate Representation (MIR) 編譯成 ƒBMC 位元精確驗證引擎所使用的邏輯。這個過程允許 Kani 在定義的邊界內，以位元精確的方式驗證程式碼行為於所有可能的輸入，它被用於檢查 unsafe 程式碼中的記憶體錯誤、原始指標解引用（raw pointer dereferences）以及運行時恐慌。

工業應用與規模

Kani 已被證明適用於工業規模的 Rust 專案。在特定的案例研究中，使用合約（contracts）將驗證從簡單的恐慌自由（panic-freedom）提升到了完整的功能正確性，這進而發現了六個先前未知的錯誤。

Kani 目前已大規模應用於生產環境的 CI 環境中。在 Rust 標準函式庫的驗證活動中，Kani 在每次程式碼變更時會驗證超過 16,000 個腳手架，展現了其大規模整合進現代軟體開發工作流的能力。

學術認可

Kani 背後的研究已被 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2026) 的 Industry Showcase Track 接收。