Kani: A Model Checker for Rust

Kani 面向 Rust 中编译器类型系统不覆盖的问题：unsafe 操作是否 sound、函数是否满足规格、运行时 panic 是否可达。它把 Rust MIR 上的 proof harness 编译到 CBMC，并自动检查一组安全属性；进一步用 function contracts、loop contracts、quantifiers 和 stubbing 扩展到更强规格。摘要中的硬事实是工业案例发现 6 个未知 bug，并在 Rust 标准库验证 campaign 中每次代码变更验证 16,000 多个 harness。