3 months ago
- Kani 是一个开源的 Rust 模型检查器，它通过有界模型检查来验证安全属性和功能正确性。
- 它将 Rust 代码从中级中间表示（MIR）编译到 CBMC 的验证引擎中，无需用户标注即可自动检查安全属性。
- Kani 提供了一种规范语言，具有函数合约、循环合约、量词和函数存根等特性，可将验证从有界域扩展到无界域。
- 针对工业 Rust 项目的案例研究表明了其可行性，验证范围从恐慌自由升级到功能正确性，并发现了六个先前未知的错误。
- 它在生产持续集成中具有可扩展性，在 Rust 标准库验证活动中，每次代码更改可验证超过 16,000 个测试套件。