Kani：让Rust代码从防错到正确

Kani: A Model Checker for Rust

Rust的所有权系统虽然能防止内存错误，但无法保证unsafe操作、功能正确性或无运行时panic。Kani作为开源模型检查器，将Rust的MIR编译到CBMC引擎，自动验证这些关键属性，无需人工注解。通过函数契约和循环契约等规范语言，Kani将验证从有界扩展到无界，在工业级项目中发现了6个未知bug，并在Rust标准库的CI中规模化运行，每次代码变更验证超16000个测试桩。

"Kani将验证从有界扩展到无界，通过函数契约、循环契约和量化器，让Rust代码从防错迈向功能正确。"