Kani：Rust 的模型检查器

Kani 是一个开源的 Rust 模型检查器，旨在为 Rust 编译器的所有权类型系统无法验证的属性提供形式化的正确性保证，例如 unsafe 操作的健全性、功能正确性以及运行时 panic 的不存在。通过将 Rust 的中间层中间表示（MIR）编译到 CBMC 位精确验证引擎，Kani 使开发者能够自动验证安全属性，而无需用户注释。

有界与无界验证

Kani 提供两种验证层级：有界模型检查和无界验证。有界模型检查允许工具在无需用户干预的情况下自动检查一套全面的安全属性。对于需要无界验证的更复杂属性，Kani 引入了一种规范语言，包含函数合约、循环合约、量词以及函数存根。

技术实现

Kani 的架构将来自 Rust 的中间层中间表示（MIR）的证明 harness 编译为 ƒBMC 位精确验证引擎使用的逻辑。此过程使 Kani 能够在定义的边界内位精确地验证代码在所有可能输入下的行为，用于检查 unsafe 代码中的内存错误、原始指针解引用以及运行时 panic。

工业应用与规模

Kani 已被证明能够适用于工业规模的 Rust 项目。在具体案例研究中，使用合约将验证从简单的无 panic 提升到完整的功能正确性，进而发现了六个此前未知的 bug。

Kani 目前已在生产 CI 环境中大规模运行。在 Rust 标准库验证活动中，Kani 每次代码变更可验证超过 16,000 个 harness，展示了其在现代软件开发工作流中大规模集成的能力。

学术认可

Kani 背后的研究已被第 39 届 IEEE/ACM 国际自动化软件工程会议（ASE 2026）工业展示轨道录用。