一句话：Kani 是开源 Rust 模型检测器，从 MIR 编译证明 harness 到 CBMC，无需标注即可验证安全性并用契约扩展到无界功能正确性。
Rust 的所有权类型系统可排除安全代码中的内存错误，但 unsafe 操作的健全性、函数正确性与无 panic 等性质仍不在编译保证范围内。Kani 是开源的 Rust 模型检测器，将有界模型检测从缺陷发现推进到对上述性质的正确性保证：它从 Rust 的 Mid-level IR（MIR）编译证明 harness 并交给 CBMC 的位精确验证引擎，无需用户标注即可自动检查一组全面的安全性质；为把验证从有界扩展到无界，Kani 提供了由函数契约、循环契约、量词与函数打桩构成的规约语言。在工业 Rust 项目上的案例研究表明，契约把验证从无 panic 提升到功能正确性，并发现六个此前未知的缺陷；Kani 已在生产 CI 中大规模运行，在 Rust 标准库验证活动中每次代码变更验证超过 16,000 个 harness。
Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties. Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. We demonstrate feasibility through case studies on industrial Rust projects, where contracts upgraded verification from panic-freedom to functional correctness, uncovering six previously unknown bugs. Kani operates at scale in production CI, with over 16,000 harnesses verified per code change in the Rust standard library verification campaign.
@inproceedings{abs-2607-01504,
title = {Kani: A Model Checker for Rust},
author = {Rémi Delmas and Zyad Hassan and Qinheping Hu and Rahul Kumar and Felipe R. Monteiro and Thanh Nguyen and Adrián Palacios and Celina Val and Michael Tautschnig and Justus Adam and Daniel Schwartz-Narbonne and Carolyn Zech},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834499}
}