kani

Kani 是 Rust 程序的位精确模型检查器，由 model-checking 组织开发。它旨在帮助开发者检查 Rust 代码的安全性与正确性。 在安全性方面，Kani 会自动检查多种未定义行为。这使其在验证 Rust 中的 unsafe 代码块时尤为有价值，因为编译器在这些代码块中不会强制执行通常的安全保证。在正确性方面，它会自动检查 panic（例如对 None 调用 unwrap()）、算术溢出，以及以断言（assert!(...)）或函数契约形式表达的自定义正确性属性。 使用方式遵循类似测试的工作流。开发者编写带有 #[kani::proof] 注解的 harness，并使用 kani::any() 创建非确定性输入。随后 Kani 尝试证明所有输入都会产生满足规范的结果，而不会 panic 或表现出意外行为。Kani book 中提供了教程和参考文档。 安装通过 Cargo 完成：先执行 cargo install --locked kani-verifier，然后执行 cargo kani setup。该工具支持 Linux 或 macOS 上的 Rust 1.58+。GitHub Action（model-checking/kani-github-action）可将其集成到 CI 流水线中。 该项目在 MIT 和 Apache 2.0 双重许可下分发，并包含来自 Rust 项目的代码。它有一篇学术引用（ASE 2026 论文），并为贡献者提供开发者文档。