Kani: A Model Checker for Rust
2026/07/01 by Rémi Delmas, Zyad Hassan, Qinheping Hu +9 · 11 voices
#cs.SE #cs.LO #cs.PL
paper · pdf
Abstract
Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties. Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. We demonstrate feasibility through case studies on industrial Rust projects, where contracts upgraded verification from panic-freedom to functional correctness, uncovering six previously unknown bugs. Kani operates at scale in production CI, with over 16,000 harnesses verified per code change in the Rust standard library verification campaign.
Citations
Discussions
- Kani: A Model Checker for Rust [hn, 160 points, 9 comments]
- Kani: A Model Checker for Rust https://arxiv.org/abs/2607.01504 (https://news.ycombinator.com/item?id=48806410) [bsky, 0 points, 0 comments]
- Kani: A Model Checker for Rust https://arxiv.org/abs/2607.01504 (https://news.ycombinator.com/item?id=48806410) [bsky, 0 points, 0 comments]
- Kani: A Model Checker for Rust [bsky, 0 points, 0 comments]
- Kani: A Model Checker for Rust #HackerNews https://arxiv.org/abs/2607.01504 [bsky, 0 points, 0 comments]
- A paper on Kani, a model checker that verifies Rust code, including the soundness of unsafe operations like raw pointer dereferences. Submit to upvote on HN https://news.ycombinator.com/submitlink?u=h [bsky, 0 points, 0 comments]
- Kani: A Model Checker for Rust https://arxiv.org/abs/2607.01504 [bsky, 0 points, 0 comments]
- Kani: A Model Checker for Rust https://arxiv.org/abs/2607.01504 [comments] [37 points] [bsky, 0 points, 0 comments]
- 📰 Kani is a model checker for Rust that aims to ensure safety and correctness of software by automatically verifying properties of programs at compile time. 🔗 https://arxiv.org/abs/2607.01504 #Tech [bsky, 0 points, 0 comments]
- Kani: A Model Checker for Rust https:// arxiv.org/abs/2607.01504 # arxiv # rust [mastodon, 0 points, 0 comments]
- Kani: A Model Checker for Rust https://arxiv.org/abs/2607.01504 https://news.ycombinator.com/item?id=48806410 [bsky, 0 points, 0 comments]
Related