Kani: A Model Checker for Rust

arXiv Identifier: 2607.01504 | Submitted: July 1, 2026 Category: Computer Science $\rightarrow$ Software Engineering (cs.SE)

---

📝 Overview

While the ownership-based type system in Rust is highly effective at eliminating memory-related errors within "safe" code, there are critical software properties that the compiler cannot verify on its own. These include the validity of unsafe operations (such as dereferencing raw pointers), the actual functional correctness of the logic, and the total absence of runtime panics.

Kani is an open-source model checker designed to bridge this gap. It moves beyond simple bug-hunting to provide rigorous correctness guarantees for Rust programs.

🎯 Verification Goals

• Ensure soundness of unsafe blocks.
• Prove functional correctness.
• Guarantee the absence of runtime panics.
• Scale to industrial-sized codebases.

---

⚙️ Technical Architecture

Kani operates by transforming Rust code into a format that a bit-precise engine can analyze. The pipeline is as follows:

The Process

1. Compilation: Kani takes proof harnesses written in Rust and compiles them from the Mid-level Intermediate Representation (MIR).
2. Backend: These are translated into the CBMC (C Bounded Model Checker) bit-precise verification engine.
3. Automation: A wide array of safety properties are checked automatically, requiring zero user annotations for basic safety.

Extending to Unbounded Verification

To move from bounded model checking to unbounded proofs, Kani utilizes a specialized specification language:

• Function Contracts: Pre-conditions and post-conditions.
• Loop Contracts: Invariants to prove properties across iterations.
• Quantifiers: Expressing properties like $\forall x \in \text{Set}, P(x)$.
• Function Stubbing: Simplifying complex dependencies.

---

📊 Results and Industrial Impact

The efficacy of Kani was tested against real-world industrial Rust projects. The transition from basic panic-freedom checks to full functional correctness via contracts led to the discovery of six previously undetected bugs.

Performance at Scale

Kani is currently integrated into production Continuous Integration (CI) pipelines.

---

🛠️ Example Logic

If we were to represent a Kani-verified property mathematically, it might look like this: $\text{Safe}(p) \iff \forall \text{ inputs } i, \neg \text{Panic}(f(i)) \land \text{PostCondition}(f(i))$

An example of a conceptual Kani harness might look like this in code:

#[kani::proof]
fn verify_my_logic() {
    let x: u32 = kani::any(); // Symbolic input
    let result = my_complex_function(x);
    assert!(result >= 0); // Property to verify
}

---

📑 Publication Metadata

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

Author Contributions

The following researchers contributed to this work:

• 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

Classification:

• ACM Classes: D.2.4, F.3.1
• Subjects: Software Engineering (cs.SE), Logic in CS (cs.LO), Programming Languages (cs.PL)

(Image: Representation of the arXiv hosting platform)

DOI: https://doi.org/10.48550/arXiv.2607.01504