Rust 代码自动证明无 panic 和内存安全
推荐指数 70.0 NO. 012 · 2026.07.07
发布2026/07/06Score86Comments3
为什么值得看
Kani 将 Rust 的 MIR 中间表示编译到 CBMC 模型检查引擎，无需用户注解即可自动验证 unsafe 代码安全性、功能正确性和运行时 panic absence。对写 Rust 系统代码的团队来说，这是目前最接近"编译期即证明正确"的实用工具。
编辑判断
Rust 社区之前做形式化验证主要靠 Prusti（依赖注解）或 Miri（仅检测 UB，不证明正确），Kani 的差异化在于零注解 + 覆盖功能正确性。CBMC 作为后端意味着它继承了对 C 代码验证二十年的工程积累，但 Rust 的所有权模型其实比 C 更适合做自动化验证，这个组合之前没人做成开源产品。
写嵌入式、区块链节点或安全关键 Rust 代码的团队应该优先试用，尤其是有 unsafe 块但不敢上生产的环境。目前 HN 只有 3 条评论，说明工具链成熟度还没到爆发点，但 AWS 已用在生产（Kani 由 AWS 团队维护），早期采用者有时间窗口。
社区反馈
正面 3 条评论
核心争论：Kani 能否替代 Miri 成为 Rust 形式化验证的首选工具
相关内容
Their old paper: https://dl.acm.org/doi/pdf/10.1145/3510457.3513031
The tutorial is helpful: https://model-checking.github.io/kani/kani-tutorial.html Reminds me a bit of hypothesis auto in its simplest applications: https://github.com/timothycrosley/hypothesis-auto/
Is Miri still required? The answer is yes: > Soundness and panic semantics. > (...) > Panics (from assert!, unwrap(), arithmetic overflow, or out- of-bounds access) are translated into assertion violations and are therefore checked as part of the verification. A successful Kani run guarantees both t