Lib.rs

Kani Rust Verifier 是一个针对 Rust 的位精确模型检查器。

Kani特别适用于验证 Rust 中的不安全代码块，其中编译器未检查 "不安全超级功能"。

Kani验证

• 内存安全（例如，空指针解引用）
• 用户指定的断言（即 assert!(...)）
• 无 panic（例如，在 None 值上使用 unwrap()）
• 某些类型的意外行为不存在（例如，算术溢出）

安装

要安装 Kani 的最新版本（Rust 1.58+; Linux 或 Mac），运行

cargo install --locked kani-verifier
cargo kani setup

查看 安装指南 以获取更多详细信息。

如何使用 Kani

类似于测试，您编写一个 harness，但使用 Kani 您可以使用 kani::any() 检查所有可能的值

use my_crate::{function_under_test, meets_specification, precondition};

#[kani::proof]
fn check_my_property() {
   // Create a nondeterministic input
   let input = kani::any();

   // Constrain it according to the function's precondition
   kani::assume(precondition(input));

   // Call the function under verification
   let output = function_under_test(input);

   // Check that it meets the specification
   assert!(meets_specification(input, output));
}

然后 Kani 将尝试证明所有有效输入都能产生可接受的输出，而不会恐慌或执行意外的行为。否则，Kani 将生成一个指向失败的轨迹。我们建议参考 教程 了解更多关于如何使用 Kani 的信息。

GitHub Action

在您的 CI 中使用 Kani，请使用以下命令：model-checking/kani-github-action@VERSION。有关详细信息，请参阅 Kani 书籍中的 GitHub Action 部分。

安全

有关更多信息，请参阅 SECURITY。

贡献

如果您有兴趣为 Kani 贡献，请参阅 开发者文档。

许可

Kani

Kani 在 MIT 许可证和 Apache 许可证（版本 2.0）的条款下分发。

有关详细信息，请参阅 LICENSE-APACHE 和 LICENSE-MIT。

Rust

Kani 包含 Rust 项目的代码。Rust 主要在 MIT 许可证和 Apache 许可证（版本 2.0）的条款下分发，部分内容受各种类似 BSD 的许可证保护。

有关详细信息，请参阅 Rust 仓库。