Kani: A Model Checker for Rust

Authors:Rémi Delmas, Zyad Hassan, Qinheping Hu, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Adrián Palacios, Celina Val, Michael Tautschnig, Justus Adam, Daniel Schwartz-Narbonne, Carolyn Zech View PDF HTML (experimental) 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.

Comments: Accepted at the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2026), Industry Showcase Track

Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO); Programming Languages (cs.PL) ACM classes: D.2.4; F.3.1

Cite as: arXiv:2607.01504 [cs.SE]   (or arXiv:2607.01504v1 [cs.

SE] for this version)   https://doi.org/10.48550/arXiv.2607.01504 arXiv-issued DOI via DataCite (pending registration) Submission history From: Felipe R. Monteiro [view email] [v1] Wed, 1 Jul 2026 22:05:33 UTC (149 KB)