Kani: A Model Checker for Rust

# Kani: A Model Checker for Rust
Source: [https://arxiv.org/html/2607.01504](https://arxiv.org/html/2607.01504)
Rémi Delmas, Zyad Hassan, Qinheping Hu, Rahul Kumar, Felipe R\. Monteiro, Thanh Nguyen, Adrián Palacios,Celina ValAmazon Web ServicesVancouverBCCanada,Michael TautschnigAmazon Web ServicesSeattleWAUSAQueen Mary UniversityLondonUnited Kingdom,Justus AdamBrown UniversityProvidenceRIUSA,Daniel Schwartz\-NarbonneDatadogNew YorkNYUSAandCarolyn ZechMassachusetts Institute of TechnologyCambridgeMAUSA

\(2026\)

###### Abstract\.

Rust’s ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness ofunsafeoperations \(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\.

model checking, Rust, formal verification, specification language

††conference:39th IEEE/ACM International Conference on Automated Software Engineering; October 12–16, 2026; Munich, Germany††journalyear:2026††copyright:none††ccs:Software and its engineering Software verification and validation††ccs:Software and its engineering Formal software verification## 1\.Introduction

Rust has become the language of choice for safety\-critical systems software, from embedded operating systems\(Levyet al\.,[2017](https://arxiv.org/html/2607.01504#bib.bib7); Booset al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib6)\)and cryptographic protocols\(Bhargavanet al\.,[2025b](https://arxiv.org/html/2607.01504#bib.bib5)\)to cloud infrastructure\(Agacheet al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib68)\)\. Its ownership type system statically prevents data races and many classes of memory errors\(Junget al\.,[2017](https://arxiv.org/html/2607.01504#bib.bib3)\), but there are three classes of correctness properties that the compiler cannot prove: \(1\) the correctness ofunsafeoperations \(e\.g\., raw pointer dereferences, calls tounsafefunctions, access to mutable statics,unsafetrait implementations, andunionfield access\) where the compiler still enforces borrow checking and type safety but the developer assumes responsibility for the additional safety invariants these operations require\(Astrauskaset al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib62); Cuiet al\.,[2024](https://arxiv.org/html/2607.01504#bib.bib63)\); \(2\) functional correctness properties such as algorithmic correctness and protocol conformance; and \(3\) absence of runtime panics from operations likeunwrap\(\), integer overflow, and out\-of\-bounds access, in contexts where panics are undesirable\. Testing and fuzzing can expose some of these failures, but they explore only a finite sample of the input space and provide no completeness guarantee\.

Deductive verification tools for Rust, including Prusti\(Astrauskaset al\.,[2022](https://arxiv.org/html/2607.01504#bib.bib34)\), Creusot\(Deniset al\.,[2022](https://arxiv.org/html/2607.01504#bib.bib21)\), and Verus\(Lattuadaet al\.,[2023](https://arxiv.org/html/2607.01504#bib.bib67)\), can prove rich functional properties\. However, they require substantial proof engineering \(e\.g\., separation logic or ghost state\) that limits adoption outside specialist teams\(Huanget al\.,[2026](https://arxiv.org/html/2607.01504#bib.bib11)\)\. At the other end of the spectrum, dynamic tools like Miri\(Junget al\.,[2026](https://arxiv.org/html/2607.01504#bib.bib59)\)detect undefined behavior at runtime but cannot prove its absence\. There is a gap between these extremes: developers need a verification approach that can start with high automation and low annotation cost, then scale incrementally toward stronger correctness guarantees as the verification need grows\.

Bounded model checking fills the automated end of this gap\. A bounded model checker encodes default safety properties \(e\.g\., arithmetic overflow, division by zero, null dereferences, assertion violations\) and checks them exhaustively up to a bound, requiring minimal manual proof construction\. This makes it an effective entry point for verification: developers write proof harnesses that resemble unit tests, and the tool proves properties over all inputs within the bound\. The limitation is that bounded analysis alone cannot guarantee correctness beyond the unwinding depth\. To push model checking from bug\-finding toward correctness proofs, the technique must be extended with specification constructs that enable unbounded reasoning while preserving the low annotation overhead that makes bounded checking accessible\.

This paper presents Kani, an open\-source model checker for Rust that realizes this progression from bounded analysis to unbounded correctness guarantees\. Kani builds on the code\-level model checking methodology\(Chonget al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib18),[2021](https://arxiv.org/html/2607.01504#bib.bib19)\), which demonstrated that bounded model checking with CBMC\(Kroening and Tautschnig,[2014](https://arxiv.org/html/2607.01504#bib.bib10)\)can be integrated into continuous development workflows for industrial C codebases\. Kani extends this methodology to Rust, operating on the Mid\-level Intermediate Representation \(MIR\) to preserve Rust\-specific type invariants, and adds a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing\. These constructs allow developers to incrementally annotate their code: Kani first proves default safety properties with no annotation, then, as contracts are added, extends the same verification engine to unbounded functional correctness proofs\. We demonstrate the feasibility of this approach through a case study on the Hifitime time\-management library, where adding contracts upgraded guarantees from panic\-freedom to functional correctness at low specification overhead, with AI\-assisted specification drafting via an AI coding assistant\. Kani is deployed in production CI at scale: proof harnesses run on every code change in Firecracker\(Agacheet al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib68)\), the virtual machine monitor behind AWS Lambda and AWS Fargate; in s2n\-quic, Amazon’s Rust implementation of the IETF QUIC transport protocol; in Hifitime\(Rabotin,[2024](https://arxiv.org/html/2607.01504#bib.bib70)\), a time\-management library used in aerospace applications; and in the Rust standard library verification campaign\(Cooket al\.,[2026](https://arxiv.org/html/2607.01504#bib.bib66)\), where over 16,000 harnesses are verified per code change\.

We make the following contributions:

1. \(1\)We evaluate Kani on multiple industrial Rust projects, where it uncovered eleven bugs missed by testing and fuzzing\. Through a detailed case study on the Hifitime library, we show that contract\-based verification extends Kani’s default safety checks to unbounded functional correctness proofs at low specification overhead \(§[5](https://arxiv.org/html/2607.01504#S5)\)\.
2. \(2\)We formalize Kani’s specification language for function contracts, loop contracts, quantifiers, and function stubbing, grounding the semantics in Floyd\-Hoare logic and connecting them to the underlying bounded model checking engine \(§[4](https://arxiv.org/html/2607.01504#S4)\)\.
3. \(3\)We present Kani’s architecture, its MIR\-level design, and its integration with the Rust toolchain \(§[3](https://arxiv.org/html/2607.01504#S3)\)\.

## 2\.Kani by Example

We illustrate Kani’s verification workflow using Euclid’s greatest common divisor \(GCD\) algorithm and its use in Firecracker\(Agacheet al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib68)\),an open\-source virtual machine monitor that runs workloads in lightweight microVMs\. Firecracker powers AWS Lambda and AWS Fargate, making the correctness of its Rust codebase a security\-critical concern\. The GCD function is used in Firecracker’s rate limiter to simplify token\-bucket refill ratios, and its iterative loop makes it a natural target for both bounded and unbounded verification\.

### 2\.1\.Bounded Verification

Consider the iterative GCD implementation from Firecracker’srate\_limitermodule:

fngcd\(x:u64,y:u64\)\-\>u64\{

letmuta=x;

letmutb=y;

whileb\!=0\{

lett=b;

b=a%b;

a=t;

\}

a

\}

A developer can write a Kani*proof harness*, analogous to a unit test but over all possible inputs, to verify thatgcdreturns a common divisor:

\#\[kani::proof\]

\#\[kani::unwind\(94\)\]

fncheck\_gcd\(\)\{

letx:u64=kani::any\(\);

lety:u64=kani::any\(\);

kani::assume\(x\>0&&y\>0\);

letd=gcd\(x,y\);

assert\!\(d\!=0&&x%d==0&&y%d==0\);

\}

The callkani::any\(\)produces a nondeterministic value of the given type, andkani::assumeconstrains the input space\. A note of caution: an incorrect assumption \(e\.g\.,assume\(false\)\) makes the proof vacuously true, so assumptions must be reviewed as carefully as the code itself\. Kani unwinds the loop, converts the result to SSA form, and encodes all assertions as a propositional formula \(§[4\.1](https://arxiv.org/html/2607.01504#S4.SS1)\) that is checked using a SAT solver\.

The\#\[kani::unwind\(94\)\]annotation sets the loop unwinding bound\. For 64\-bit inputs, the worst\-case number of iterations of Euclid’s algorithm is 93 \(the largest Fibonacci number below2642^\{64\}isF93F\_\{93\}\); the bound is set conservatively to 94\. If the bound is insufficient, Kani reports an*unwinding assertion failure*, alerting the developer that the verification result is inconclusive beyond the given depth\. Even with a sufficient bound, the resulting formula is very large: in our experiments, bounded verification ofgcdover the fullu64range did not terminate within a one\-hour timeout\. Moreover, the bound is specific to 64\-bit integers; changing the input type requires recomputing it\.

### 2\.2\.Unbounded Verification with Contracts

We annotategcdwith a function contract \(precondition and postcondition\) and a loop contract \(invariant and decreases clause\)\. The loop contract eliminates the dependence on the unwinding bound by abstracting the loop via an inductive invariant:

\#\[kani::requires\(x\>0&&y\>0\)\]

\#\[kani::ensures\(\|&result\|result\>0\)\]

fngcd\(x:u64,y:u64\)\-\>u64\{

letmuta=x;

letmutb=y;

\#\[kani::loop\_invariant\(

a\>0

&&kani::forall\!\(\|d:u64

in\(1,a\.saturating\_add\(1\)\)\|

d==0

\|\|\(\(x%d==0&&y%d==0\)

==\(a%d==0&&b%d==0\)\)\)

\)\]

\#\[kani::loop\_decreases\(b\)\]

whileb\!=0\{

lett=b;

b=a%b;

a=t;

\}

a

\}

Therequiresclause states the precondition: both inputs must be positive\. Theensuresclause states the postcondition: the result is positive\. Inside the loop,loop\_invariantasserts two properties across all iterations: \(1\)aremains positive, and \(2\) for every candidate divisord,ddivides the original inputs\(x, y\)iff it divides the current values\(a, b\), i\.e\., the set of common divisors is preserved\. Thesaturating\_addavoids overflow when computing the upper bound of the quantifier range\. Theloop\_decreasesclause specifies thatbis a well\-founded decreasing measure \(sinceamodb<ba\\bmod b<bon each iteration\), proving termination \(§[4\.4](https://arxiv.org/html/2607.01504#S4.SS4)\)\.

The natural postcondition is the full divisibility property \(x % result == 0 && y % result == 0\), which the invariant implies at loop exit; however, Z3 cannot automatically instantiate the quantifier atd=𝑟𝑒𝑠𝑢𝑙𝑡d=\\mathit\{result\}over nonlinear 64\-bit bitvector remainder \(§[4\.5](https://arxiv.org/html/2607.01504#S4.SS5)\), so we use the weakerresult \> 0\. Verification passes all 202 checks in 0\.54 s with Z3, exercising the full pipeline: quantified loop invariant, termination proof, and all automatically generated safety checks\.

This invariant is nontrivial: it requires a universally quantified statement over nonlinear arithmetic\. In practice, many verification tasks require only simple contracts, which Kani checks automatically with no annotations\. The GCD example demonstrates the expressiveness of Kani’s specification language when functional correctness is desired\.

##### Verifying the contract\.

A dedicatedproof\_for\_contractharness sets nondeterministic inputs viakani::any\(\)and callsgcd; Kani assumes the precondition, executes the function, and asserts the postcondition\. The\#\[kani::solver\(z3\)\]attribute selects the Z3 SMT solver, required for the quantified invariant\. The loop invariant is verified inductively \(§[4\.4](https://arxiv.org/html/2607.01504#S4.SS4)\): the loop body executes exactly twice in a single BMC query, regardless of input size\.

##### What failure looks like\.

When a postcondition is violated, Kani reports the contract expression and source location\. For example, a sign error in Hifitime’stotal\_nanoseconds\(\)\(§[5\.2](https://arxiv.org/html/2607.01504#S5.SS2)\) produced:

Check1:\.\.\.total\_nanoseconds::\{closure\#2\}

\-Status:FAILURE

\-Description:"\|result\|\{\*result==

i128::from\(self\.centuries\)\*

i128::from\(NPC\)\+

i128::from\(self\.nanoseconds\)\}"

VERIFICATION:\-FAILED\(0\.26s\)

##### Using the verified contract\.

Once verified, the contract serves as a sound abstraction for compositional reasoning\. In Firecracker,TokenBucket::newcallsgcdto simplify token\-bucket refill ratios\. Using\#\[kani::stub\_verified\(gcd\)\], the harness replacesgcdwith its contract: the precondition is asserted at the call site, and a nondeterministic return value satisfying the postcondition \(result \> 0\) is assumed\. No loop is unrolled, and verification completes in seconds over all 64\-bit inputs using a sound abstraction\.

## 3\.Architecture

Kani is an open\-source verification tool that integrates with the standard Rust toolchain\. It can be invoked viacargo kanion Cargo111[https://doc\.rust\-lang\.org/cargo/](https://doc.rust-lang.org/cargo/)packages \(analogous tocargo test\) or viakanion individual crates\. Internally, Kani reuses the entirerustcfrontend and replaces the code\-generation backend: instead of emitting machine code via LLVM, it translates Rust programs into GOTO programs\(Kroeninget al\.,[2023](https://arxiv.org/html/2607.01504#bib.bib46)\)that CBMC can model\-check\. A key design decision is to operate on Rust’s Mid\-level Intermediate Representation \(MIR\) rather than LLVM IR\. MIR preserves monomorphized type information, enum discriminant layouts, and Rust’s validity invariants \(e\.g\., that aboolis 0 or 1, that acharis a valid Unicode scalar\) in a form that LLVM IR discards\. This enables Kani to automatically check Rust\-specific safety properties and to reason about dynamic trait objects and closures, which are erased at the LLVM level\(VanHattumet al\.,[2022](https://arxiv.org/html/2607.01504#bib.bib2)\)\. As shown in Figure[1](https://arxiv.org/html/2607.01504#S3.F1), the pipeline flows from Rust source through the Kani compiler to CBMC and a SAT/SMT solver, with thekani\-driverorchestrating each stage\.

![Refer to caption](https://arxiv.org/html/2607.01504v1/x1.png)Figure 1\.Kani verification pipeline\. Blue boxes are Kani components; gray boxes are external tools; green is the orchestrator\. White boxes denote input/output\. Dashed arrows indicate orchestration control flow\.##### Compilation\.

A verification session starts withcargo kani, which invokes*kani\-driver*, the orchestrator \(green box in Figure[1](https://arxiv.org/html/2607.01504#S3.F1)\)\. The driver calls*kani\-compiler*, arustcplugin that hooks into the compiler via therustc\_privateinterface after MIR generation\. The standardrustcfrontend performs parsing, name resolution, type checking, trait resolution, and monomorphization, producing typed MIR\. Kani then applies MIR\-to\-MIR transformations: reachability analysis, contract and loop\-contract instrumentation \(§[4](https://arxiv.org/html/2607.01504#S4)\), stubbing, and safety\-check insertion\.

##### Code generation\.

The transformed MIR is lowered to a GOTO program by the*codegen*backend, which translates MIR statements, rvalues, places, and types into GOTO expressions using the*cprover\-bindings*library available in CBMC\. Calls to the Kani API \(e\.g\.,kani::any\(\),kani::assume\(\),kani::assert\(\),forall\!, orexists\!\) are intercepted by codegen hooks and translated into their CBMC counterparts: nondeterministic values, assumptions, assertions, and quantified expressions\. Quantifier bodies are inlined to produce single CBMC\-compliant expressions \(§[4\.5](https://arxiv.org/html/2607.01504#S4.SS5)\)\. The resulting GOTO program is serialized to CBMC’s binary IRep format\.

##### Verification\.

The driver optionally invokes*goto\-instrument*to apply Dynamic Frame Condition Checking222[https://diffblue\.github\.io/cbmc/contracts\-dev\-spec\-dfcc\.html](https://diffblue.github.io/cbmc/contracts-dev-spec-dfcc.html)\(DFCC\) for function and loop contracts, instrumenting write\-set enforcement\. It then invokes CBMC, which performs symbolic execution of the GOTO program, unwinds loops, converts the result to SSA form, and encodes all assertions as a propositional formula \(§[4\.1](https://arxiv.org/html/2607.01504#S4.SS1)\), which it dispatches to a solver\. Kani supports multiple solver backends: MiniSat\(Eén and Sörensson,[2003](https://arxiv.org/html/2607.01504#bib.bib53)\)\(default\), Kissat and CaDiCaL\(Biereet al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib54)\)for SAT, and Z3\(de Moura and Bjørner,[2008](https://arxiv.org/html/2607.01504#bib.bib56)\), cvc5\(Barbosaet al\.,[2022](https://arxiv.org/html/2607.01504#bib.bib57)\), and Bitwuzla\(Niemetz and Preiner,[2023](https://arxiv.org/html/2607.01504#bib.bib58)\)for SMT\. CBMC returns a verdict per property \(e\.g\., assertion, overflow check, memory safety check\), which the driver maps back to Rust source locations and presents to the user\.

##### Default properties\.

Beyond user\-specified assertions, Kani automatically verifies a comprehensive set of properties333Full list at[https://github\.com/model\-checking/kani](https://github.com/model-checking/kani)\.without any annotation from the developer\. These fall into three categories:*absence of undefined behavior*\(i\.e\., invalid or dangling pointer dereferences, misaligned casts, invalid enum discriminants\),*absence of runtime panics*\(e\.g\., arithmetic overflow, division by zero, undefined shift, out\-of\-bounds indexing,unwrap\(\)onNone\), and*resource properties*\(e\.g\., float\-to\-integer cast finiteness\)\. The Kani compiler instruments the code during MIR transformations and code generation with Rust\-semantic checks; CBMC contributes additional C\-level memory safety checks\. Two optional MIR passes provide deeper checks: the*valid\-value pass*asserts that unsafe type coercions produce valid inhabitants, and the*uninit\-memory pass*uses shadow memory to verify that every dereference accesses initialized memory\. Both are opt\-in due to solver overhead\.

## 4\.Specification Language and Verification Methodology

Kani’s verification model follows a deliberate progression: bounded model checking provides push\-button safety analysis for any Rust program; loop and function contracts extend this to*unbounded*verification when loops or recursion make a finite bound insufficient\. This section formalizes that progression, beginning with the bounded foundation, then showing how each specification construct extends it\. Rust’s ownership model introduces subtleties, particularly around type invariants and memory havocking, that do not arise in C\-level model checking; we identify these precisely and explain how Kani addresses them\. Throughout, we ground the formalism in the GCD–TokenBucketexample of Section[2](https://arxiv.org/html/2607.01504#S2)\.

### 4\.1\.Bounded Model Checking Foundations

Kani’s verification engine is CBMC\(Kroening and Tautschnig,[2014](https://arxiv.org/html/2607.01504#bib.bib10); Kroeninget al\.,[2023](https://arxiv.org/html/2607.01504#bib.bib46)\), a bit\-precise bounded model checker \(BMC\)\. Unlike classical BMC formulations defined over explicit transition systems\(Biereet al\.,[1999](https://arxiv.org/html/2607.01504#bib.bib55)\), CBMC operates directly on programs: given a loopwhileGG\{B\}\\\{B\\\}with guardGGand bodyBB, CBMC syntactically unwinds it up to a boundkk, inserting an*unwinding assertion*¬G\\neg Gafter the last copy\. The result is a loop\-free programPkP\_\{k\}\. CBMC then convertsPkP\_\{k\}to Static Single Assignment \(SSA\) form and encodes all assertions as a propositional formula\(Chonget al\.,[2021](https://arxiv.org/html/2607.01504#bib.bib19); Clarkeet al\.,[2004](https://arxiv.org/html/2607.01504#bib.bib47)\)\. If the formula is satisfiable, the satisfying assignment yields a concrete counterexample; if unsatisfiable, all assertions hold for every execution ofPkP\_\{k\}\.

##### SSA encoding\.

CBMC convertsPkP\_\{k\}to SSA form, introducing a fresh variable versionx\(i\)x\_\{\(i\)\}at each assignment pointiiand encoding branching with path\-condition guardsgjg\_\{j\}\. The result is a conjunction of guarded equations whereeje\_\{j\}is the right\-hand\-side expression at assignmentjj:

𝑆𝑆𝐴​\(Pk\)=⋀j\(gj→xnj=ej\)\.\\mathit\{SSA\}\(P\_\{k\}\)\\;=\\;\\bigwedge\_\{j\}\\;\\bigl\(g\_\{j\}\\;\\rightarrow\\;x\_\{n\_\{j\}\}=e\_\{j\}\\bigr\)\.The propositional formula CBMC constructs is:

\(1\)ψk=𝑆𝑆𝐴​\(Pk\)∧⋁p∈𝐴𝑠𝑠𝑒𝑟𝑡𝑠​\(Pk\)¬φp\\psi\_\{k\}\\;=\\;\\mathit\{SSA\}\(P\_\{k\}\)\\;\\wedge\\;\\bigvee\_\{p\\,\\in\\,\\mathit\{Asserts\}\(P\_\{k\}\)\}\\neg\\,\\varphi\_\{p\}where𝐴𝑠𝑠𝑒𝑟𝑡𝑠​\(Pk\)\\mathit\{Asserts\}\(P\_\{k\}\)includes user assertions, automatically inserted safety checks, and unwinding assertions\.

##### Completeness\.

The bounded guarantee becomes practically complete when all unwinding assertions pass, meaningPkP\_\{k\}covers all reachable paths\. For programs with input\-independent loop bounds this is tractable: in our running example, Euclid’s algorithm iterates at most 93 times, so\#\[kani::unwind\(94\)\]is a sound, complete bound, but the unwound formula \(O​\(k⋅\|𝑏𝑜𝑑𝑦\|\)O\(k\\cdot\|\\mathit\{body\}\|\)SSA equations over 64\-bit bitvectors\) exceeds practical solver limits\. For programs with input\-dependent bounds, no tractablekkmay suffice\. Function and loop contracts \(§[4\.4](https://arxiv.org/html/2607.01504#S4.SS4)\) address this gap by replacing exhaustive unrolling with inductive reasoning, achieving unbounded guarantees with a single BMC query\.

Kani compiles Rust’s MIR into CBMC’s GOTO program representation, inheriting bit\-precise arithmetic and memory reasoning\. In the remainder of this section, we useσ\\sigmafor program states and standard Hoare\-logic notation\. The specification constructs below extend this foundation\.

### 4\.2\.Specification Language

Kani’s specification language extends Rust boolean expressions with contract annotations\. All specification expressions must be deterministic and side\-effect free \(i\.e\., no I/O, mutation, or heap allocation\), a restriction enforced by a MIR traversal at compile time\.

##### Syntax\.

The grammar of contract annotations is:

func\-spec::=::=requires\(P\)∣ensures\(\|r\|Q\)\\texttt\{requires\}\(P\)\\mid\\texttt\{ensures\}\(\|r\|\\;Q\)∣modifies\(e\)\\mid\\;\\texttt\{modifies\}\(e\)loop\-spec::=::=loop\_invariant​\(I\)\\texttt\{loop\\\_invariant\}\(I\)∣loop\_modifies​\(e\)∣​loop\_decreases​\(d\)\\mid\\;\\texttt\{loop\\\_modifies\}\(e\)\\mid\\texttt\{loop\\\_decreases\}\(d\)P,Q,IP,Q,I::=::=𝑟𝑢𝑠𝑡​\-​𝑒𝑥𝑝𝑟𝑏𝑜𝑜𝑙∣P∧Q\\mathit\{rust\\text\{\-\}expr\}\_\{\\mathit\{bool\}\}\\mid P\\wedge Q∣forall\(\|x:τin\(l,h\)\|P\)\\mid\\;\\texttt\{forall\}\(\|x\{:\}\\tau\\;\\texttt\{in\}\\;\(l,h\)\|\\;P\)∣exists\(\|x:τin\(l,h\)\|P\)\\mid\\;\\texttt\{exists\}\(\|x\{:\}\\tau\\;\\texttt\{in\}\\;\(l,h\)\|\\;P\)QQ::=::=⋯∣old​\(e\)\\cdots\\mid\\texttt\{old\}\(e\)\(ensures only\)ee::=::=𝑟𝑢𝑠𝑡​\-​𝑒𝑥𝑝𝑟𝑝𝑢𝑟𝑒\\mathit\{rust\\text\{\-\}expr\}\_\{\\mathit\{pure\}\}Multiplerequiresandensuresclauses are implicitly conjoined\. The pseudo\-functionold​\(e\)\\texttt\{old\}\(e\)evaluateseein the pre\-state and is valid only withinensuresclauses; quantifiers range over a bounded domain\[l,h\)\[l,h\)\(inclusive lower bound, exclusive upper bound\) or, if bounds are omitted, over all values of typeτ\\tau\(with backend implications discussed in Section[4\.5](https://arxiv.org/html/2607.01504#S4.SS5)\)\.

##### Validity invariants and safety invariants\.

A Rust\-specific challenge is that types carry two classes of invariant\. A*validity invariant*𝑣𝐼𝑛𝑣​\(τ\)\\mathit\{vInv\}\(\\tau\)must hold at all times \(e\.g\.,bool∈\{0,1\}\\in\\\{0,1\\\}, valid enum discriminants\); the compiler assumes it unconditionally\. A*safety invariant*𝑠𝐼𝑛𝑣​\(τ\)\\mathit\{sInv\}\(\\tau\)is a semantic property that safe code may assume but the type system does not enforce \(e\.g\.,Duration’s nanosecond field<109<10^\{9\}\)\. Kani’skani::any::<T\>\(\)respects𝑣𝐼𝑛𝑣​\(τ\)\\mathit\{vInv\}\(\\tau\)by construction but does not automatically enforce𝑠𝐼𝑛𝑣​\(τ\)\\mathit\{sInv\}\(\\tau\)\. TheInvarianttrait allows types to express𝑠𝐼𝑛𝑣​\(τ\)\\mathit\{sInv\}\(\\tau\)programmatically; when arequiresclause includes anInvariantcheck, inputs are constrained accordingly\. We write𝐴𝑟𝑏​\(τ\)\\mathit\{Arb\}\(\\tau\)for the set of values producible bykani::any::<T\>\(\)\.

##### Semantic domains\.

We writeσ∈Σ\\sigma\\in\\Sigmafor program states \(mappings from locations to values\),f​\(x¯\)f\(\\bar\{x\}\)for a function with parametersx¯\\bar\{x\}and bodyBfB\_\{f\}, and𝑀𝑜𝑑​\(f\)⊆𝐿𝑜𝑐\\mathit\{Mod\}\(f\)\\subseteq\\mathit\{Loc\}for the write set offf\. We writeσ​\[L←ℎ𝑎𝑣𝑜𝑐τ\]\\sigma\[L\\leftarrow\\mathit\{havoc\}\_\{\\tau\}\]for the state obtained by*havocking*LL: replacing every location inLLwith a nondeterministic value drawn from𝐴𝑟𝑏​\(τ\)\\mathit\{Arb\}\(\\tau\), thereby preserving𝑣𝐼𝑛𝑣​\(τ\)\\mathit\{vInv\}\(\\tau\)while leaving𝑠𝐼𝑛𝑣​\(τ\)\\mathit\{sInv\}\(\\tau\)unconstrained unless the precondition specifies otherwise\.

### 4\.3\.Function Contracts

A function contract is a triple⟨𝑃𝑟𝑒,𝑃𝑜𝑠𝑡,𝑀𝑜𝑑⟩\\langle\\mathit\{Pre\},\\,\\mathit\{Post\},\\,\\mathit\{Mod\}\\ranglewhere𝑃𝑟𝑒​\(x¯\)\\mathit\{Pre\}\(\\bar\{x\}\)is the precondition,𝑃𝑜𝑠𝑡​\(x¯,r\)\\mathit\{Post\}\(\\bar\{x\},r\)the postcondition over the return valuerr, and𝑀𝑜𝑑\\mathit\{Mod\}the write set\. All contract expressions must be deterministic and side\-effect free \(enforced at compile time\)\. In the postcondition, bare parameter names refer to their*post\-state*values; theold\(ee\)construct \(described below\) is required to reference pre\-state values\. For parameters passed by value, the post\-state and pre\-state values coincide \(the caller’s copy is unaffected\); for parameters passed by mutable reference \(&mut T\), the post\-state value reflects modifications made through the reference\. The contract establishes the Hoare triple:

\(2\)\{𝑃𝑟𝑒​\(x¯\)\}r←f​\(x¯\)\{𝑃𝑜𝑠𝑡​\(x¯,r\)∧𝑓𝑟𝑎𝑚𝑒​\(σ,σ′,𝑀𝑜𝑑\)\}\\bigl\\\{\\ \\mathit\{Pre\}\(\\bar\{x\}\)\\ \\bigr\\\}\\quad r\\leftarrow f\(\\bar\{x\}\)\\quad\\bigl\\\{\\ \\mathit\{Post\}\(\\bar\{x\},r\)\\;\\wedge\\;\\mathit\{frame\}\(\\sigma,\\sigma^\{\\prime\},\\mathit\{Mod\}\)\\ \\bigr\\\}where𝑓𝑟𝑎𝑚𝑒​\(σ,σ′,𝑀𝑜𝑑\)\\mathit\{frame\}\(\\sigma,\\sigma^\{\\prime\},\\mathit\{Mod\}\)asserts that every location outside𝑀𝑜𝑑\\mathit\{Mod\}is unchanged between the pre\-stateσ\\sigmaand post\-stateσ′\\sigma^\{\\prime\}\. In our running example, the GCD contract has𝑃𝑟𝑒≡\(x\>0∧y\>0\)\\mathit\{Pre\}\\equiv\(x\>0\\wedge y\>0\)and𝑃𝑜𝑠𝑡≡\(r\>0\)\\mathit\{Post\}\\equiv\(r\>0\); the write set is empty sincegcdis a pure function\. The loop invariant establishes the stronger property that the set of common divisors is preserved, but the postcondition is simplified to avoid intractable quantifier instantiation over nonlinear bitvector arithmetic; see Section[2](https://arxiv.org/html/2607.01504#S2)\. In practice, contract precision involves a trade\-off: a precondition that is too strong prevents the contract from being applied at call sites that do not establish the full condition, while a postcondition that is too weak may leave call\-site verification unable to prove the desired property\. Developers must balance precision against annotation effort\.

##### Contract checking\.

A contract is verified in a harness annotated with\#\[kani::proof\_for\_contract\(ff\)\]\. Kani instruments the harness to establish \([2](https://arxiv.org/html/2607.01504#S4.E2)\):

1. \(1\)construct arbitrary inputsx¯\\bar\{x\}via𝐴𝑟𝑏​\(τi\)\\mathit\{Arb\}\(\\tau\_\{i\}\), respecting Rust’s ownership invariants \(e\.g\., no two&mut Targuments alias the same memory\);
2. \(2\)assume𝑃𝑟𝑒​\(x¯\)\\mathit\{Pre\}\(\\bar\{x\}\);
3. \(3\)symbolically executer←f​\(x¯\)r\\leftarrow f\(\\bar\{x\}\);
4. \(4\)assert𝑃𝑜𝑠𝑡​\(x¯,r\)\\mathit\{Post\}\(\\bar\{x\},r\); and
5. \(5\)verify𝑤𝑟𝑖𝑡𝑒𝑠​\(f\)⊆𝑀𝑜𝑑\\mathit\{writes\}\(f\)\\subseteq\\mathit\{Mod\}via CBMC’s frame condition checker\.

The instrumented harness is discharged by BMC \([1](https://arxiv.org/html/2607.01504#S4.E1)\): CBMC searches for an execution that satisfies the precondition but violates the postcondition or frame condition\. If loop contracts are also present, the loop body executes only twice in a single BMC query \(c\.f\. Section[4\.4](https://arxiv.org/html/2607.01504#S4.SS4)\), decoupling verification time from iteration count\.

##### Contract replacement\.

Once \([2](https://arxiv.org/html/2607.01504#S4.E2)\) is established, the contract soundly replacesffat call sites via\#\[kani::stub\_verified\(ff\)\], applying a*contract abstraction rule*that combines the verified contract with frame reasoning:

\(3\)\{𝑃𝑟𝑒\}​r←f​\(x¯\)​\{𝑃𝑜𝑠𝑡∧𝑓𝑟𝑎𝑚𝑒\}\{P∧𝑃𝑟𝑒\}​r←f​\(x¯\)​\{P\|𝑀𝑜𝑑¯∧𝑃𝑜𝑠𝑡\}\\frac\{\\displaystyle\\bigl\\\{\\ \\mathit\{Pre\}\\ \\bigr\\\}\\;r\\leftarrow f\(\\bar\{x\}\)\\;\\bigl\\\{\\ \\mathit\{Post\}\\wedge\\mathit\{frame\}\\ \\bigr\\\}\}\{\\displaystyle\\bigl\\\{\\ P\\wedge\\mathit\{Pre\}\\ \\bigr\\\}\\;r\\leftarrow f\(\\bar\{x\}\)\\;\\bigl\\\{\\ P\|\_\{\\overline\{\\mathit\{Mod\}\}\}\\wedge\\mathit\{Post\}\\ \\bigr\\\}\}wherePPis the caller’s context andP\|𝑀𝑜𝑑¯P\|\_\{\\overline\{\\mathit\{Mod\}\}\}retains the conjuncts ofPPthat do not depend on locations in𝑀𝑜𝑑\\mathit\{Mod\}; conjuncts that do are discarded as part of the over\-approximation\. The rule is admissible, justified by the BMC\-verified premise: the replacement body havocs𝑀𝑜𝑑\\mathit\{Mod\}and then assumes𝑃𝑜𝑠𝑡\\mathit\{Post\}, which narrows the nondeterministic values to those satisfying the postcondition\. No computation offfis performed, soff’s internal loops need not be unrolled at call sites\. In theTokenBucketverification of Section[2](https://arxiv.org/html/2607.01504#S2), this reduction drops verification of the caller from hours \(i\.e\., the time required to unroll all 64\-bit GCD iterations in context\) to seconds, while providing an unbounded guarantee over all 64\-bit inputs\.

##### History expressions\.

Theold\(ee\) construct captures the pre\-state value ofeefor two\-state postconditions, essential when a function receives&mut T\. For example,ensures\(\|r\| \*v == old\(\*v\) \+ 1\)asserts that the referent was incremented by exactly one\. Kani rewritesensures​\(\|r\|​Q​\(old​\(e\),x¯,r\)\)\\texttt\{ensures\}\(\|r\|\\;Q\(\\texttt\{old\}\(e\),\\bar\{x\},r\)\)into\{v←⟦e⟧σ\}r←f\(x¯\)\{Q\(v,x¯,r\)\}\\\{v\\leftarrow\\llbracket e\\rrbracket\_\{\\sigma\}\\\}\\;r\\leftarrow f\(\\bar\{x\}\)\\;\\\{Q\(v,\\bar\{x\},r\)\\\}, whereσ\\sigmais the pre\-state\.

##### Write sets and havocking\.

For functions taking&mut T, Kani infers𝑀𝑜𝑑\\mathit\{Mod\}from the signature: all memory reachable through mutable references\. The havoc useskani::any\(\)\(preserving𝑣𝐼𝑛𝑣​\(τ\)\\mathit\{vInv\}\(\\tau\)\), and themodifiesmacro converts references to raw pointers*after*borrow checking viauntracked\_deref\. Explicitmodifiesclauses narrow the inferred set when the reachable state is too large, improving solver completeness\. For raw pointers,modifiesis required: Kani cannot infer which memory is reachable through a raw pointer, so without an explicit clause the write set defaults to empty and any write triggers a DFCC verification failure\. The frame condition in \([2](https://arxiv.org/html/2607.01504#S4.E2)\) assumes that locations inside and outside𝑀𝑜𝑑\\mathit\{Mod\}do not alias\. Rust’s borrow checker guarantees this for safe code; forunsafecode, the user must ensure𝑀𝑜𝑑\\mathit\{Mod\}is closed under aliasing\.

##### Recursive functions\.

Contracts support unbounded verification of*self\-recursive*functions via induction on call depth, implementing the standard proof rule\(Aptet al\.,[2009](https://arxiv.org/html/2607.01504#bib.bib1)\):

\(4\)\{𝑃𝑟𝑒\}​f​\(x¯\)​\{𝑃𝑜𝑠𝑡\}⊢\{𝑃𝑟𝑒\}​Bf​\{𝑃𝑜𝑠𝑡\}⊢\{𝑃𝑟𝑒\}​f​\(x¯\)​\{𝑃𝑜𝑠𝑡\}\\frac\{\\displaystyle\\bigl\\\{\\ \\mathit\{Pre\}\\ \\bigr\\\}\\;f\(\\bar\{x\}\)\\;\\bigl\\\{\\ \\mathit\{Post\}\\ \\bigr\\\}\\;\\vdash\\;\\bigl\\\{\\ \\mathit\{Pre\}\\ \\bigr\\\}\\;B\_\{f\}\\;\\bigl\\\{\\ \\mathit\{Post\}\\ \\bigr\\\}\}\{\\displaystyle\\vdash\\bigl\\\{\\ \\mathit\{Pre\}\\ \\bigr\\\}\\;f\(\\bar\{x\}\)\\;\\bigl\\\{\\ \\mathit\{Post\}\\ \\bigr\\\}\}The premise assumes the contract holds for recursive calls and verifies the body under that assumption\. Rule \([4](https://arxiv.org/html/2607.01504#S4.E4)\) is sound for partial correctness unconditionally, and for total correctness provided the recursion terminates under a well\-founded measure\.*Kani does not currently verify termination for recursive functions*; termination remains the user’s responsibility\. Mutual recursion \(f→g→ff\\to g\\to f\) is not supported; Kani emits a compile\-time error when it detects a contracted function involved in a mutually recursive cycle\.

##### Soundness and panic semantics\.

Kani interprets Hoare triples under*partial correctness with panic safety*:\{P\}​S​\{Q\}\\\{P\\\}\\;S\\;\\\{Q\\\}means that ifPPholds andSSterminates normally \(without panicking\), thenQQholds\. Panics \(fromassert\!,unwrap\(\), arithmetic overflow, or out\-of\-bounds access\) are translated into assertion violations and are therefore checked as part of the verification\. A successful Kani run guarantees both the absence of panics and the postcondition, for all inputs satisfying the precondition, up to the following assumptions: harness coverage of reachable inputs, aliasing closure of𝑀𝑜𝑑\\mathit\{Mod\}forunsafecode, user\-guaranteed termination, sequential execution \(no threads orasync\), no Stacked Borrows\(Junget al\.,[2019](https://arxiv.org/html/2607.01504#bib.bib33)\)/ Tree Borrows\(Villaniet al\.,[2025](https://arxiv.org/html/2607.01504#bib.bib41)\)pointer\-aliasing modeling \(the primary class of UB inunsafeRust\), and FFI calls executing outside CBMC’s memory model unless stubbed \(§[4\.6](https://arxiv.org/html/2607.01504#S4.SS6)\)\. The last two are the most significant in practice\. Miri\(Junget al\.,[2026](https://arxiv.org/html/2607.01504#bib.bib59)\)checks aliasing violations dynamically, making it a natural complement\.

### 4\.4\.Loop Contracts

For programs where a completeness threshold exists but is too costly to reach, such as the 64\-bit GCD loop, loop contracts provide an alternative path to unbounded verification\. They replace exhaustive loop unrolling with an application of the Floyd–HoareWhilerule\.

A loop contract consists of three clauses:

- •loop\_invariant\(II\),
- •loop\_modifies\(WW\), and
- •loop\_decreases\(dd\)\.

For a loopwhileGG\{B\}\\\{B\\\}with post\-loop continuationCC, the proof obligation is:

\(5\)\{I∧G\}​B​\{I\}𝑤𝑟𝑖𝑡𝑒𝑠​\(B\)⊆W\{I\}​while​G​\{B\}​\{I∧¬G∧𝑓𝑟𝑎𝑚𝑒​\(σ,σ′,W\)\}\\frac\{\\displaystyle\\bigl\\\{\\ I\\wedge G\\ \\bigr\\\}\\;B\\;\\bigl\\\{\\ I\\ \\bigr\\\}\\qquad\\mathit\{writes\}\(B\)\\subseteq W\}\{\\displaystyle\\bigl\\\{\\ I\\ \\bigr\\\}\\;\\texttt\{while\}\\ G\\;\\\{B\\\}\\;\\bigl\\\{\\ I\\wedge\\neg G\\wedge\\mathit\{frame\}\(\\sigma,\\sigma^\{\\prime\},W\)\\ \\bigr\\\}\}Kani verifies rule \([5](https://arxiv.org/html/2607.01504#S4.E5)\) through a two\-level transformation that produces a single BMC query covering all three proof obligations\.

At the MIR level, Kani restructures the loop CFG \(desugaringforloops and hoisting variables for nesting\)\. At the GOTO level, CBMC’s DFCC pass rewrites the loop into four blocks executed in a single BMC run: Prehead \(snapshots and initialization\), Head \(guard evaluation and body execution\), Step \(base\-case assertion, havocWW, assumeII\), and Exit \(frame assumption\)\. The control flow is Prehead→\\toHead \(base case\)→\\toStep→\\toHead \(inductive step\)→\\tocut\. The loop body executes exactly twice, making verification time independent of the iteration count\.

Two aspects of this transformation are non\-obvious\. First, the Step block sits*between*the two passes through Head: if the loop guard is false on entry, Step is never reached and the havoc never fires, correctly preserving the program state for zero\-iteration loops\. Second, the inductive step routes through the actual compiled guard in Head rather than synthetically assuming it, so the body executes underI∧GI\\wedge Gwith all safety checks on the guard expression intact\.

Once an inner loop’s contract is verified, its abstraction \(i\.e\., havocW𝑖𝑛W\_\{\\mathit\{in\}\}, assumeI𝑖𝑛∧¬G𝑖𝑛I\_\{\\mathit\{in\}\}\\wedge\\neg G\_\{\\mathit\{in\}\}\) over\-approximates its concrete behavior\. The outer loop’s inductive step therefore remains sound against the abstracted inner body, providedW𝑖𝑛⊆W𝑜𝑢𝑡W\_\{\\mathit\{in\}\}\\subseteq W\_\{\\mathit\{out\}\}\. Function\-level composition follows the same argument: all loop abstractions are applied before checking the function’s postcondition\.

In our running example, the GCD loop invariant asserts thata\>0a\>0and that the set of common divisors of\(x,y\)\(x,y\)equals the set of common divisors of\(a,b\)\(a,b\)at every iteration\. The base case holds trivially \(\(a,b\)=\(x,y\)\(a,b\)=\(x,y\)on entry\); the inductive step follows because Euclid’s step preserves the set of common divisors; and the abstraction delivers¬G≡\(b=0\)\\neg G\\equiv\(b=0\), from which the postconditiona\>0a\>0follows directly from the invariant’s first conjunct\. The invariant also impliesa​∣x∧a∣​ya\\mid x\\wedge a\\mid yat this point, but verifying that implication automatically requires quantifier instantiation that current SMT solvers cannot perform; see Section[2](https://arxiv.org/html/2607.01504#S2)\.

Rust’sforloops desugar into iterator protocol calls with opaque internal state that CBMC cannot inspect\. Kani rewrites annotatedforloops intowhileloops over a simplifiedKaniIntoIterabstraction that exposes only the current index and the iteration bounds\. This allows invariants to be stated over the loop index rather than private iterator fields\. The rewrite is exact for range\-basedforloops; for custom iterators, the user must provide loop\-level contracts that reason about the iterator’s abstraction\.

##### Termination\.

Withoutloop\_decreases, rule \([5](https://arxiv.org/html/2607.01504#S4.E5)\) establishes only partial correctness: the invariant is checked at entry and preserved by each iteration, but non\-termination is not ruled out\. Kani emits a warning whenloop\_decreasesis absent\. Aloop\_decreases\(dd\)clause adds the termination proof obligation:

\{I∧G∧d=d0∧d0≥0\}​B​\{0≤d<d0\},\\bigl\\\{\\ I\\wedge G\\wedge d=d\_\{0\}\\wedge d\_\{0\}\\geq 0\\ \\bigr\\\}\\;\\;B\\;\\;\\bigl\\\{\\ 0\\leq d<d\_\{0\}\\ \\bigr\\\},upgrading the result to total correctness\. The measureddis restricted to non\-negative integer expressions; more general well\-founded orders \(e\.g\., lexicographic tuples\) are not yet supported\. In our example,loop\_decreases\(b\)is discharged because each iteration replacesbbwithamodb<ba\\bmod b<b, andb≥0b\\geq 0is preserved\. Currently, the underlying CBMC engine supports only simple integer expressions indecreasesclauses; struct field projections and tuple\-based lexicographic measures are not yet supported\.

### 4\.5\.Quantifiers

Kani provides first\-order quantifiers as procedural macros:

kani::forall\!\(\|x:Tin\(lo,hi\)\|P\(x\)\)

kani::exists\!\(\|x:Tin\(lo,hi\)\|P\(x\)\)

These compile to CBMC\-level quantified expressions\. With SAT solvers \(the default\), CBMC eagerly expands quantifiers over the specified range, so bounds must be compile\-time constants; Kani emits a warning when the range exceeds 1000 values\. With SMT backends \(\-\-solver z3,cvc5, orbitwuzla\), quantifiers are passed directly to the solver as first\-order formulas, supporting runtime\-valued bounds\.

### 4\.6\.Function Stubbing

Function stubbing replaces a function’s implementation with a handwritten mock for the duration of a specific harness, specified via the\#\[kani::stub\(ff,gg\)\]attribute\. The replacement is a MIR\-to\-MIR transformation: when the compiler requests the MIR forff, Kani returns the MIR forgginstead\. Kani validates signature compatibility \(matching parameter types, return type, and generic arity\) at compile time; without this check, a stub could silently operate on differently typed values, producing spurious proofs\.

Stubbing serves three purposes: \(1\) replacing functions with features unsupported by the verification backend \(inline assembly, FFI\); \(2\) replacing expensive implementations with lightweight nondeterministic abstractions; and \(3\) environmental modeling, where system interactions such as clock reads or random number generation are replaced with unconstrained nondeterministic values\.

##### Stubs versus verified contracts\.

Plain stubs are*not*checked against the original implementation: the user asserts thatggis a sound model offf, and Kani trusts this claim\. A verification result that relies on unverified stubs is therefore*conditional*: it is sound only if every stub faithfully over\-approximates the behavior of the function it replaces\. Verified contracts \(Section[4\.3](https://arxiv.org/html/2607.01504#S4.SS3)\), by contrast, machine\-check the contract against the implementation before admitting the abstraction; subsequent uses ofstub\_verifiedare then provably sound by rule \([3](https://arxiv.org/html/2607.01504#S4.E3)\)\. The two mechanisms are complementary: contracts for formally established behavioral abstractions, stubs for environmental modeling where no implementation exists to verify against\. In theTokenBucketexample of Section[2](https://arxiv.org/html/2607.01504#S2), thegcdfunction uses a verified contract, whileInstant::now, a system call whose semantics Kani cannot model, uses a plain stub that returns a nondeterministicInstant\. Together, they reduce the verification ofTokenBucket::newfrom an intractable loop\-unrolling problem to a bounded check with an unbounded correctness guarantee\.

## 5\.Evaluation

We evaluate Kani through three research questions grounded in the concerns of industrial practitioners:

RQ\-I:Does Kani find real bugs that testing and fuzzing miss?

RQ\-II:Do function and loop contracts extend bounded verification to stronger, unbounded guarantees in practice?

RQ\-III:Is Kani sustainable in continuous integration across diverse projects over time?

Table 1\.Subset of open\-source projects using Kani\.Table[1](https://arxiv.org/html/2607.01504#S5.T1)lists representative open\-source projects across multiple domains that use Kani in CI\. Our evaluation focuses on a subset of these: Firecracker, the virtual\-machine monitor behind AWS Lambda444[https://aws\.amazon\.com/lambda/](https://aws.amazon.com/lambda/)and AWS Fargate555[https://aws\.amazon\.com/fargate/](https://aws.amazon.com/fargate/); s2n\-quic, Amazon’s implementation of the IETF QUIC transport protocol\(Langleyet al\.,[2017](https://arxiv.org/html/2607.01504#bib.bib79)\); Cedar\(Cutleret al\.,[2024](https://arxiv.org/html/2607.01504#bib.bib78)\), an open\-source authorization policy language and engine \(which does not use Kani in its regular CI\); Hifitime, a high\-precision time management library used in the Moon landing mission Blue Ghost Mission 1666[https://fireflyspace\.com/missions/blue\-ghost\-mission\-1/](https://fireflyspace.com/missions/blue-ghost-mission-1/); and the Rust standard library verification campaign\(Cooket al\.,[2026](https://arxiv.org/html/2607.01504#bib.bib66)\)\.

### 5\.1\.Bug\-Finding Effectiveness

We highlight three cases that illuminate qualitatively different failure modes\.

Table 2\.Bugs found by Kani that testing and fuzzing missed\.##### s2n\-quic: finding bugs at encoding boundaries\.

Amazon’s QUIC implementation, s2n\-quic, uses Kani alongside the Bolero777[https://github\.com/camshaft/bolero](https://github.com/camshaft/bolero)property\-testing framework, allowing each harness to run as both a fuzz test and a Kani proof with a single attribute\. The most striking result involves thetry\_fitfunction, which determines how many bytes of data to fit into a QUICStreamframe given a packet’s remaining capacity, a subtle calculation because the variable\-length integer encoding of the frame length increases at capacity boundaries\. A differential Bolero harness compared the implementation against a reference model\. Running thelibfuzzerengine for over ten minutes \(16,777,216 executions\) found no failure\. Kani found a failing assertion in 20 seconds\. The failure lived near the boundary between one\-byte and two\-byte integer encodings, a sparse region of the input space that coverage\-guided fuzzing has no gradient toward; Kani’s symbolic execution reached it directly\.

A second s2n\-quic case illustrates complementarity: a bug indecode\_packet\_numberwas found by Kani in 2\.8 seconds and independently by fuzzing in under a minute\. When both methods find the same bug, the Kani result is more actionable: the failing check identifies a specific named property rather than an unexplained crash, and Kani generates a concrete counterexample \(via its*concrete playback*888[https://model\-checking\.github\.io/kani/reference/experimental/concrete\-playback\.html](https://model-checking.github.io/kani/reference/experimental/concrete-playback.html)feature\) that the developer can replay as a standard Rust test\.

##### Firecracker: verifying properties invisible to testing\.

The Firecracker virtual machine monitor applies Kani to two security\-critical components\. For the I/O rate limiter, which uses a token\-bucket algorithm where tokens accumulate over time and each I/O operation consumes tokens, the property of interest is that a microVM cannot exceed its configured I/O bandwidth in any one\-second interval\. This is inherently time\-dependent: the number of tokens replenished depends on whenauto\_replenishis called relative to the system clock, making it impossible to test exhaustively\. Kani resolves this by stubbinglibc::clock\_gettimewith a nondeterministic stub that returns monotonically non\-decreasingInstantvalues, turning the temporal dimension into a symbolic variable\. The resulting harnesses found several bugs in the rate\-limiter implementation, the most significant being a rounding error that allowed a guest to exceed its I/O budget by up to 0\.01% in adversarially timed invocations\. The error depends on the exact sub\-millisecond timing of replenishment calls relative to the system clock, a condition that testing cannot control deterministically and that fuzzing cannot target without an explicit time model\.

Firecracker also implements the VirtIO device emulation protocol\(OASIS,[2019](https://arxiv.org/html/2607.01504#bib.bib77)\), where shared memory between host and guest creates an adversarial attack surface: an untrusted guest can write arbitrary values into the shared descriptor and ring buffers\. Kani verified conformance to Section 2\.6\.7\.2 of the VirtIO specification using nondeterministic guest memory to represent this adversarial scenario\. Kani found an additional bug: a guest could cause Firecracker to panic on boot by placing a VirtIO queue component’s starting address in the MMIO gap\.

##### Cedar: a logic bug in policy evaluation\.

Cedar is an open\-source authorization policy language and engine\. A Kani experiment on Cedar’s evaluator found a bug in thecontains\_at\_least\_twofunction, which checks whether a string contains at least two occurrences of a substring\. When called with a multibyte character as the search query, the function could slice a&stracross a non\-character boundary, resulting in a runtime panic\. The bug was silent under all existing tests\. Kani’s symbolic execution over all possible collection inputs produced a counterexample that violated the function’s intended invariant; the fix was merged999More information available at[https://github\.com/cedar\-policy/cedar/pull/1037](https://github.com/cedar-policy/cedar/pull/1037)\.\. This case is notable because Cedar already uses differential testing against a formal reference model, yet the bug survived into production code\.

Answer to RQ\-I:Kani found eleven bugs across four production Rust codebases that testing and fuzzing missed, including bugs that survived millions of fuzz iterations \(s2n\-quic\), bugs in time\-dependent code invisible to testing without a time oracle \(Firecracker\), and differential testing against a formal reference model \(Cedar\)\. Beyond bug\-finding, the harnesses that detected these bugs also serve as machine\-checked specifications that persist in CI, foreshadowing the stronger correctness guarantees explored in RQ\-II\.

### 5\.2\.Contract\-Based Unbounded Verification in Practice

We present a detailed case study of Kani’s specification language applied to Hifitime, a high\-precision time\-management library used in aerospace and astrodynamics applications\. Hifitime stores durations as a pair\(𝑐𝑒𝑛𝑡𝑢𝑟𝑖𝑒𝑠:i16,𝑛𝑎𝑛𝑜𝑠:u64\)\(\\mathit\{centuries\}\{:\}\\,\\texttt\{i16\},\\,\\mathit\{nanos\}\{:\}\\,\\texttt\{u64\}\)where the nanosecond field must satisfy the normalization invariant𝑛𝑎𝑛𝑜𝑠<𝑁𝑃𝐶\\mathit\{nanos\}<\\mathit\{NPC\}\(i\.e\., the number of nanoseconds in one century\) except at the saturation extremesDuration::MINandDuration::MAX\. All arithmetic operations callnormalize\(\)to re\-establish this invariant, making it the library’s central safety\-critical function\.

#### 5\.2\.1\.Phase I: Panic\-Freedom Harnesses

Hifitime’s original Kani integration, developed by the library’s author in 2022–2023 with no \(substantial\) prior formal verification experience, consisted of 11 harnesses checking only*panic\-freedom*: that operations do not trigger arithmetic overflows, null dereferences, or out\-of\-bounds accesses\. Despite the absence of postconditions, this baseline found 8 bug categories in a single pull request101010More information available at[https://github\.com/nyx\-space/hifitime/pull/192](https://github.com/nyx-space/hifitime/pull/192)\., including overflow at boundary values ofnormalize\(\), sign errors inneg\(\), and overflow inPartialEqand arithmetic operations nearDuration::MINandDuration::MAX, all of which survived 78 existing tests\.

By 2024 the harness count had grown to 168 through a combination of manual and automated harness generation\. This expansion revealed a fundamental scalability limit: of 158 automatically generated harnesses, 57 timed out at the 60\-second CI budget\. The root cause was that bounded model checking re\-verified thenormalize\(\)loop inside every caller, with the loop’s nanosecond adjustment requiring many unrolling iterations in the worst case\.

#### 5\.2\.2\.Phase II: Contract\-Based Functional Verification

To address both the scalability problem and the expressive gap, we upgraded the Hifitime verification using Kani’s function and loop contracts\. This phase was conducted using an AI coding assistant, providing a concrete data point on AI\-assisted formal specification\.

The central idea is compositional verification via contracts\. We expressed the normalization invariant \(𝑛𝑎𝑛𝑜𝑠<𝑁𝑃𝐶\\mathit\{nanos\}<\\mathit\{NPC\}\) as a postcondition onnormalize\(\), enabling callers to usestub\_verified\(Equation[3](https://arxiv.org/html/2607.01504#S4.E3)\) to replace the implementation with its contract abstraction i\.e\. eliminating the need to re\-unroll the internal loop at each call site\. Building on this, we annotated 84 functions withensurespostconditions and 41 withrequirespreconditions, converted 12 of the existing 168 panic\-freedom harnesses intoproof\_for\_contractharnesses that verify functional properties, and added 61 newproof\_for\_contractharnesses and 80 standalone proofs with explicit functional assertions\. This compositional approach enabled us to go beyond panic\-freedom and prove six new classes of functional properties, from normalization invariants and algebraic laws to encode–decode identities and specification consistency \(see Table[3](https://arxiv.org/html/2607.01504#S5.T3)\)\.

Table 3\.Classes of functional properties proved with contracts in Hifitime \(Phase II\)\.For loops that require unbounded reasoning, Kani’s loop contracts \(§[4\.4](https://arxiv.org/html/2607.01504#S4.SS4)\) establish guarantees independent of iteration count\. As an example, theDuration::Mul<f64\>precision loop iteratively scales a multipliernew\_val\(computed asq \* 10ˆp\) to find the required decimal precision\. We annotated it with a loop invariant and a decreases clause:

letmutp:i32=0;

letmutnew\_val:f64=q;

\.\.\.

\#\[kani::loop\_invariant\(p\>=0&&p<=19\)\]

\#\[kani::loop\_decreases\(19i32\.wrapping\_sub\(p\)\)\]

whilenew\_val\.is\_finite\(\)

&&\(new\_val\.floor\(\)\-new\_val\)\.abs\(\)\>=f64::EPSILON

&&p<19

\{

p\+=1;

new\_val=q\*ten\.powi\(p\);

\}

The invariant is inductive and the decreases clause proves termination, together establishing*total correctness*: the loop terminates withp∈\\in\[0, 19\]for allf64inputs, with no assumptions onq\. In isolation, Kani verifies the loop contract in 0\.2 s; without it, CBMC unrolls 19 iterations and takes 91\.8 s\. In the full crate context, verification ofMul<f64\>completes in under 70 s with the contract, compared to intractable without it\.

The result is 153 active harnesses \(up from 168 in Phase I\), of which all prove functional correctness properties beyond panic\-freedom\. The most consequential change from Phase I is in the*class of guarantee*: Phase I proves that operations do not crash; Phase II proves that they compute correctly\. The timeout problem that surfaced in 2024 \(57 harnesses exceeding the CI budget\) is addressed by contracts, which allow callers to reason aboutnormalize\(\)via its specification rather than re\-verifying its internal loop\.

Bugs found by contracts\.As a side effect of establishing these functional properties, Kani uncovered six previously unknown bugs, properties that the original panic\-freedom harnesses could not express\.

\(i\) total\_nanoseconds\(\)sign error\.The implementation used subtraction instead of addition for durations spanning more than one century in the negative direction, producing incorrect values for anyDurationwithcenturies<−1<\-1\. The encode–decode identity \(from\_total\_nanoseconds\(d\.total\_nanoseconds\(\)\) == d\) condition immediately falsified the postcondition, providing a concrete counterexample\. The fix is a one\-character source change\. Notably, one existing integration test was*asserting the buggy behavior*and had to be corrected alongside the implementation\. The postcondition was derived from theDurationtype’s encoding invariant \(documented in the struct definition\), providing an independent specification against which both the implementation and the test were checked\. The test oracle, having been written against the implementation’s output, encoded the same error\.

\(ii\)i64::MIN\.abs\(\)arithmetic panic\.Unit::Mul<i64\>called\.abs\(\)oni64::MIN, which panics because the result does not fit ini64\. The normalization contract found this; the fix uses\.unsigned\_abs\(\)\.

\(iii\) NaN in float multiply\.Whennew\_valoverflows to infinity in theMul<f64\>precision loop, the loop invariant \(§[5\.2](https://arxiv.org/html/2607.01504#S5.SS2)\) falsified on the overflow iteration\. Two source\-level guards were added\.

\(iv\) Epoch::PartialEqandOrdinconsistency\.The methodDuration::PartialEqdeliberately treats opposite\-sign values as equal \(representing the same interval length regardless of direction\), butEpoch::PartialEqdelegated to this implementation\. Meanwhile,Epoch::Ordused a lexicographic comparison that is sign\-aware\. The Rust standard library requires thatPartialEqandOrdagree:a == bmust implya\.cmp\(b\) == Ordering::Equal\. This invariant was violated for any pair of epochs differing in sign\.

\(v\) Duration::PartialEqandOrdinconsistency \(zero\-crossing\)\.Duration::PartialEqhas a custom zero\-crossing special case that treats opposite\-sign durations as equal, butDuration::Ordis derived \(lexicographic on fields\) and does not\. Two durations can therefore satisfya == banda < bsimultaneously, violating Rust’sEq/Ordcontract\. This bug was discovered during the investigation of Bug 4: tracing theEpochinconsistency to its root cause inDuration\.

\(vi\)is\_gregorian\_validoverflow\.The Gregorian calendar validity check overflows atyear == i32::MAXdue to an unchecked addition in the leap\-year computation\. The contract on the calendar validation function detected this boundary case\.111111[https://github\.com/nyx\-space/hifitime/issues/475](https://github.com/nyx-space/hifitime/issues/475)

Bugs \(iv\) and \(v\) are the most semantically significant findings because they violate a requirement of the Rust standard library itself, not merely a domain\-specific invariant\. Bug \(iv\) was invisible to all existing tests because no test compared an epoch to its sign\-negation, a conceptually unusual operation for a “point in time\.” Kani’s symbolic execution generated this input automatically by exploring all possibleEpochpairs\. Thecontract\_epoch\_eq\_symmetricharness expressed the consistency requirement as a postcondition and immediately produced a counterexample\. The fix rewrites bothEpoch::PartialEqandEpoch::Ordto usetotal\_nanoseconds\(\)for a sign\-aware scalar comparison\. This case illustrates why exhaustive symbolic analysis over all inputs matters: the failing input lies in a region of the state space that no human tester would explore, yet it represents a real semantic violation\.

AI\-assisted formal specifications\.The Phase II specifications were developed using an AI coding assistant with shell access to the codebase\. Because Kani’s specification language is an extension of Rust itself \(i\.e\., contracts are Rust boolean expressions; harnesses are Rust functions\), the assistant could leverage its existing Rust knowledge to produce specifications without learning a separate formal language\. The workflow was a tight loop: the assistant proposed contract annotations, wrote them into the source files, rancargo kani, observed the result \(i\.e\., success, failure, timeout, or compile error\), and refined the specification in response\. The human researcher directed which functions to target, provided domain context, and reviewed the proposed contracts for correctness\.

Crucially, the specifications do not need to be trusted: Kani verifies every contract against the implementation\. This was demonstrated concretely when three AI\-generated contracts failed verification, and Kani caught all three: \(1\) an intractable postcondition that called the function under verification in its ownensuresclause, doubling the SAT formula and causing a solver timeout \(the assistant simplified it to a direct arithmetic expression\); \(2\) an overly broad symbolic input \(kani::any::<Epoch\>\(\)\) that included theTimeScale::ETvariant, pullingsin\(\)into the SAT formula and causing a timeout \(the assistant restricted the harness toTimeScale::TAI\); and \(3\) aconst fnincompatibility where Kani’s macro expansion generated non\-const code, producing a compile error \(the assistant switched to a standalone proof harness\)\. These errors classify as one specification design error, one harness design error, and one Kani limitation\. In all three cases, the assistant diagnosed the failure from Kani’s output and proposed a fix within the same session\.

Answer to RQ\-II:Contracts extend bounded panic\-freedom guarantees to stronger functional properties with unbounded coverage\. In Hifitime, 153 functional proofs covered six new classes of functional properties\. Contracts enabled compositional reasoning and uncovered six bugs that panic\-freedom checks could not express, including two violations of Rust’s ownEq/Ordcontract\.

### 5\.3\.Continuous Integration Sustainability

All projects listed in Table[1](https://arxiv.org/html/2607.01504#S5.T1)run Kani in CI, and several have done so for years: Firecracker integrated Kani in 2022\(Chonget al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib18)\), and s2n\-quic and Hifitime followed shortly after\. This sustained adoption builds on the code\-level model checking methodology established by Chong et al\.\(Chonget al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib18),[2021](https://arxiv.org/html/2607.01504#bib.bib19)\)for C codebases at AWS, which Kani extends to Rust\. The practical CI feasibility of Kani has been demonstrated at scale: the Rust standard library verification campaign runs 16,748 Autoharness\-generated harnesses via parallelization and incremental caching, achieving a 3\.97×\\timesspeedup over a naïve sequential pipeline\(Cooket al\.,[2026](https://arxiv.org/html/2607.01504#bib.bib66)\)\. Across the projects in Table[1](https://arxiv.org/html/2607.01504#S5.T1), CI runtimes range from under one minute \(x86\_64\) to approximately 69 minutes \(verify\-rust\-std\), with most completing in under 25 minutes, which are practical budgets for pull\-request workflows\.

A key enabler of CI adoption is Kani’scargo kaniinterface, which integrates identically withcargo test\. In s2n\-quic, the Bolero framework allows the same harness to run as both a fuzz test and a Kani proof via a single\#\[cfg\_attr\(kani, kani::proof\)\]attribute, adding Kani’s exhaustive analysis to existing fuzz infrastructure at zero additional annotation cost\. The breadth of adoption across domains \(from VMMs and network protocols to aerospace, microkernels, and OS infrastructure\) is evidence that Kani’s cargo\-native workflow lowers the barrier to verification across a wide range of industrial Rust contexts\.

Answer to RQ\-III:Kani is sustainable in CI across diverse projects and domains\. All projects in Table[1](https://arxiv.org/html/2607.01504#S5.T1)run Kani on every code change, with CI runtimes ranging from under one minute to 69 minutes\. The Rust standard library campaign verifies over 16,000 harnesses per code change\. Thecargo kaniinterface and proof\-harness\-as\-code model enable verification to evolve alongside the codebase\.

Threats to validity\.Our case studies are not a random sample: the evaluated projects self\-selected into Kani adoption, potentially over\-representing favorable cases; the Cedar experiment partially mitigates this as a deliberate evaluation on a project not previously using Kani\. Specifications can be wrong: three AI\-generated contracts required correction \(all caught by Kani, not human review\)\. Harnesses without loop contracts provide bounded guarantees only; we report unbounded claims only where contracts or passing unwinding assertions justify them\. The specification language does not address generics \(contracts are verified per monomorphization\), dynamic trait dispatch, or concurrent execution\.

## 6\.Related Work

Rust verification is an active area spanning dynamic analysis, deductive verification, and model checking\. On the dynamic side, Miri\(Junget al\.,[2026](https://arxiv.org/html/2607.01504#bib.bib59)\)detects undefined behavior at runtime, including Stacked Borrows\(Junget al\.,[2019](https://arxiv.org/html/2607.01504#bib.bib33)\)and Tree Borrows\(Villaniet al\.,[2025](https://arxiv.org/html/2607.01504#bib.bib41)\)aliasing violations \(the primary class of UB that Kani does not model; §[4\.3](https://arxiv.org/html/2607.01504#S4.SS3)\)\. Rudra\(Baeet al\.,[2021](https://arxiv.org/html/2607.01504#bib.bib60)\)scales to the full crates\.io ecosystem via over\-approximation, finding 264 bugs \(76 CVEs\)\. On the foundational side, RustBelt\(Junget al\.,[2017](https://arxiv.org/html/2607.01504#bib.bib3)\)and RefinedRust\(Gäheret al\.,[2024](https://arxiv.org/html/2607.01504#bib.bib37)\)provide machine\-checked soundness proofs in Rocq at the cost of substantial expertise\. Kani’s proof\-harness approach builds on code\-level model checking for C\(Chudnovet al\.,[2018](https://arxiv.org/html/2607.01504#bib.bib61); Chonget al\.,[2020](https://arxiv.org/html/2607.01504#bib.bib18),[2021](https://arxiv.org/html/2607.01504#bib.bib19)\), extending it to Rust with type\-aware nondeterminism and contract\-based unbounded verification\.

Verus\(Lattuadaet al\.,[2023](https://arxiv.org/html/2607.01504#bib.bib67)\)is the closest tool to Kani in ambition\. It embeds specifications and proofs directly in Rust syntax, using linear ghost types for ownership reasoning and targeting Z3\. The key difference is the verification paradigm: Verus requires proof code \(lemma functions, triggers, ghost state\), while Kani requires only contracts and harnesses\. Verus’s SOSP 2024 case studies report approximately 5 lines of proof per line of implementation \(6\.1K impl\., 31K proof\); Kani’s Hifitime case study adds 125 contract annotations to 153 harnesses covering a 9\.5K\-line library\. Kani is easier to adopt incrementally \(zero annotations yield panic\-freedom checks\) but is limited to properties expressible within BMC or inductive contracts; Verus can express richer properties \(e\.g\., complex data\-structure invariants with ghost state\) at higher annotation cost\.

Other Rust verifiers include Prusti\(Astrauskaset al\.,[2022](https://arxiv.org/html/2607.01504#bib.bib34)\), a deductive verifier for safe Rust built on the Viper infrastructure; Creusot\(Deniset al\.,[2022](https://arxiv.org/html/2607.01504#bib.bib21)\), which translates MIR into Why3’s WhyML with prophecy variables for mutable borrows; Flux\(Lehmannet al\.,[2023](https://arxiv.org/html/2607.01504#bib.bib15)\), which brings liquid types to Rust with low annotation overhead; Aeneas\(Ho and Protzenko,[2022](https://arxiv.org/html/2607.01504#bib.bib42)\)and hax\(Bhargavanet al\.,[2025a](https://arxiv.org/html/2607.01504#bib.bib36)\), which extract Rust into theorem provers \(F\*, Lean, Rocq\) for foundational or security\-critical verification; and VeriFast\(Jacobset al\.,[2011](https://arxiv.org/html/2607.01504#bib.bib64)\), a separation\-logic verifier for unsafe Rust that handles the most pointer\-intensive modules in the Rust standard library campaign\(Cooket al\.,[2026](https://arxiv.org/html/2607.01504#bib.bib66)\)\. Kani differs from these tools by operating on MIR, providingcargo\-integrated workflows, and supporting unbounded verification through function and loop contracts\.

## 7\.Conclusion

We presented Kani, an open\-source model checker for Rust that provides both bounded and unbounded verification through a specification language of function contracts, loop contracts, quantifiers, and function stubbing\. Our evaluation demonstrates that Kani finds bugs that testing and fuzzing miss \(eleven bugs across four production codebases\), that contracts upgrade bounded panic\-freedom checks to unbounded functional correctness proofs \(153 functional proofs in Hifitime\), and that verification integrates sustainably into CI across diverse projects \(over 16,000 harnesses in the Rust standard library campaign\)\. Model checking requires minimal proof expertise, yet provides exhaustive guarantees that testing cannot\. Kani makes this capability accessible to any Rust developer throughcargo kani\.

Data Availability\.Kani and all evaluated projects are available as open source; bug fixes are referenced by pull request number in the text\.

Acknowledgements\.We thank all open\-source contributors\.

## References

- A\. Agache, M\. Brooker, A\. Iordache, A\. Liguori, R\. Neugebauer, P\. Piwonka, and D\. Popa \(2020\)Firecracker: lightweight virtualization for serverless applications\.In17th USENIX Symposium on Networked Systems Design and Implementation \(NSDI\),Santa Clara, CA, USA,pp\. 419–434\.Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p1.1),[§1](https://arxiv.org/html/2607.01504#S1.p4.1),[§2](https://arxiv.org/html/2607.01504#S2.p1.1),[Table 1](https://arxiv.org/html/2607.01504#S5.T1.1.3.1.1)\.
- Amazon Web Services \(2024\)S2n\-quic: an implementation of the IETF QUIC protocol\.Note:[https://github\.com/aws/s2n\-quic](https://github.com/aws/s2n-quic)Cited by:[Table 1](https://arxiv.org/html/2607.01504#S5.T1.1.4.2.1)\.
- K\. R\. Apt, F\. S\. de Boer, and E\. Olderog \(2009\)Verification of sequential and concurrent programs\.3rd edition,Springer,Berlin, Heidelberg\.External Links:[Document](https://dx.doi.org/10.1007/978-1-84882-745-5)Cited by:[§4\.3](https://arxiv.org/html/2607.01504#S4.SS3.SSS0.Px5.p1.2)\.
- V\. Astrauskas, A\. Bílý, J\. Fiala, Z\. Grannan, C\. Matheja, P\. Müller, F\. Poli, and A\. J\. Summers \(2022\)The prusti project: formal verification for rust\.InNASA Formal Methods: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings,Berlin, Heidelberg,pp\. 88–108\.External Links:ISBN 978\-3\-031\-06772\-3,[Document](https://dx.doi.org/10.1007/978-3-031-06773-0%5F5)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p2.1),[§6](https://arxiv.org/html/2607.01504#S6.p3.1)\.
- V\. Astrauskas, C\. Matheja, F\. Poli, P\. Müller, and A\. J\. Summers \(2020\)How do programmers use unsafe Rust?\.Proc\. ACM Program\. Lang\.4\(OOPSLA\)\.External Links:[Document](https://dx.doi.org/10.1145/3428204)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p1.1)\.
- Y\. Bae, Y\. Kim, A\. Askar, J\. Lim, and T\. Kim \(2021\)Rudra: finding memory safety bugs in Rust at the ecosystem scale\.InProc\. ACM SIGOPS 28th Symposium on Operating Systems Principles \(SOSP\),New York, NY, USA,pp\. 84–99\.External Links:[Document](https://dx.doi.org/10.1145/3477132.3483570)Cited by:[§6](https://arxiv.org/html/2607.01504#S6.p1.1)\.
- H\. Barbosa, C\. Barrett, M\. Brain, G\. Kremer, H\. Lachnitt, M\. Mann, A\. Mohamed, M\. Mohamed, A\. Niemetz, A\. Nötzli, A\. Ozdemir, M\. Preiner, A\. Reynolds, Y\. Sheng, C\. Tinelli, and Y\. Zohar \(2022\)cvc5: a versatile and industrial\-strength SMT solver\.InTools and Algorithms for the Construction and Analysis of Systems \(TACAS\),LNCS, Vol\.13243,Cham,pp\. 415–442\.External Links:[Document](https://dx.doi.org/10.1007/978-3-030-99524-9%5F24)Cited by:[§3](https://arxiv.org/html/2607.01504#S3.SS0.SSS0.Px3.p1.1)\.
- K\. Bhargavan, M\. Buyse, L\. Franceschino, L\. L\. Hansen, F\. Kiefer, J\. Schneider\-Bensch, and B\. Spitters \(2025a\)Hax: verifying security\-critical Rust software using multiple provers\.InVerified Software\. Theories, Tools and Experiments \(VSTTE\),Cham,pp\. 96–119\.External Links:[Document](https://dx.doi.org/10.1007/978-3-031-86695-1%5F7)Cited by:[§6](https://arxiv.org/html/2607.01504#S6.p3.1)\.
- K\. Bhargavan, L\. L\. Hansen, F\. Kiefer, J\. Schneider\-Bensch, and B\. Spitters \(2025b\)Formal security and functional verification of cryptographic protocol implementations in rust\.InProceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security,CCS ’25,New York, NY, USA,pp\. 2729–2743\.External Links:ISBN 9798400715259,[Document](https://dx.doi.org/10.1145/3719027.3765213)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p1.1)\.
- A\. Biere, A\. Cimatti, E\. Clarke, and Y\. Zhu \(1999\)Symbolic model checking without BDDs\.InTools and Algorithms for the Construction and Analysis of Systems \(TACAS\),Lecture Notes in Computer Science, Vol\.1579,Berlin, Heidelberg,pp\. 193–207\.External Links:[Document](https://dx.doi.org/10.1007/3-540-49059-0%5F14)Cited by:[§4\.1](https://arxiv.org/html/2607.01504#S4.SS1.p1.9)\.
- A\. Biere, K\. Fazekas, M\. Fleury, and M\. Heisinger \(2020\)CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020\.InProc\. of SAT Competition 2020 – Solver and Benchmark Descriptions,T\. Balyo, N\. Froleyks, M\. Heule, M\. Iser, M\. Järvisalo, and M\. Suda \(Eds\.\),Department of Computer Science Report Series B, Vol\.B\-2020\-1,Helsinki, Finland,pp\. 51–53\.Cited by:[§3](https://arxiv.org/html/2607.01504#S3.SS0.SSS0.Px3.p1.1)\.
- K\. Boos, N\. Liyanage, R\. Ijaz, and L\. Zhong \(2020\)Theseus: an experiment in operating system structure and state management\.InProceedings of the 14th USENIX Conference on Operating Systems Design and Implementation,OSDI’20,USA\.External Links:ISBN 978\-1\-939133\-19\-9Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p1.1)\.
- N\. Chong, B\. Cook, J\. Eidelman, K\. Kallas, K\. Khazem, F\. R\. Monteiro, D\. Schwartz\-Narbonne, S\. Tasiran, M\. Tautschnig, and M\. R\. Tuttle \(2021\)Code\-level model checking in the software development workflow at amazon web services\.Software: Practice and Experience51\(4\),pp\. 772–797\.External Links:[Document](https://dx.doi.org/https%3A//doi.org/10.1002/spe.2949),https://onlinelibrary\.wiley\.com/doi/pdf/10\.1002/spe\.2949Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p4.1),[§4\.1](https://arxiv.org/html/2607.01504#S4.SS1.p1.9),[§5\.3](https://arxiv.org/html/2607.01504#S5.SS3.p1.1),[§6](https://arxiv.org/html/2607.01504#S6.p1.1)\.
- N\. Chong, B\. Cook, K\. Kallas, K\. Khazem, F\. R\. Monteiro, D\. Schwartz\-Narbonne, S\. Tasiran, M\. Tautschnig, and M\. R\. Tuttle \(2020\)Code\-level model checking in the software development workflow\.InProceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice,ICSE\-SEIP ’20,New York, NY, USA,pp\. 11–20\.External Links:ISBN 9781450371230,[Document](https://dx.doi.org/10.1145/3377813.3381347)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p4.1),[§5\.3](https://arxiv.org/html/2607.01504#S5.SS3.p1.1),[§6](https://arxiv.org/html/2607.01504#S6.p1.1)\.
- A\. Chudnov, N\. Collins, B\. Cook, J\. Dodds, B\. Huffman, C\. MacCárthaigh, S\. Magill, E\. Mertens, E\. Mullen, S\. Tasiran, A\. Tomb, and E\. Westbrook \(2018\)Continuous formal verification of Amazon s2n\.InComputer Aided Verification \(CAV\),Lecture Notes in Computer Science, Vol\.10982,Cham,pp\. 430–446\.External Links:[Document](https://dx.doi.org/10.1007/978-3-319-96142-2%5F26)Cited by:[§6](https://arxiv.org/html/2607.01504#S6.p1.1)\.
- E\. Clarke, D\. Kroening, and F\. Lerda \(2004\)A tool for checking ANSI\-C programs\.InTools and Algorithms for the Construction and Analysis of Systems \(TACAS\),LNCS, Vol\.2988,Berlin, Heidelberg,pp\. 168–176\.External Links:[Document](https://dx.doi.org/10.1007/978-3-540-24730-2%5F15)Cited by:[§4\.1](https://arxiv.org/html/2607.01504#S4.SS1.p1.9)\.
- B\. Cook, R\. Delmas, Z\. Hassan, B\. Jacobs, R\. Jhala, R\. Kumar, F\. R\. Monteiro, T\. Nguyen, R\. Rumbul, M\. Tautschnig, C\. Val, and C\. Zech \(2026\)Verifying the Rust standard library\.InNASA Formal Methods \(NFM\),Cham,pp\. 1–20\.Note:To appearCited by:[§1](https://arxiv.org/html/2607.01504#S1.p4.1),[§5\.3](https://arxiv.org/html/2607.01504#S5.SS3.p1.1),[Table 1](https://arxiv.org/html/2607.01504#S5.T1.1.6.4.1),[§5](https://arxiv.org/html/2607.01504#S5.p3.1),[§6](https://arxiv.org/html/2607.01504#S6.p3.1)\.
- M\. Cui, S\. Sun, H\. Xu, and Y\. Zhou \(2024\)Is unsafe an Achilles’ heel? A comprehensive study of safety requirements in unsafe Rust programming\.InProc\. IEEE/ACM 46th International Conference on Software Engineering \(ICSE\),New York, NY, USA\.External Links:[Document](https://dx.doi.org/10.1145/3597503.3639136)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p1.1)\.
- J\. W\. Cutler, C\. Disselkoen, A\. Eline, S\. He, K\. Headley, M\. Hicks, K\. Hietala, E\. Ioannidis, J\. Kastner, A\. Mamat, D\. McAdams, M\. McCutchen, N\. Rungta, E\. Torlak, and A\. M\. Wells \(2024\)Cedar: a new language for expressive, fast, safe, and analyzable authorization\.Proc\. ACM Program\. Lang\.8\(OOPSLA1\)\.External Links:[Document](https://dx.doi.org/10.1145/3649835)Cited by:[§5](https://arxiv.org/html/2607.01504#S5.p3.1)\.
- Datadog \(2024\)Lading: a load\-testing framework\.Note:[https://github\.com/DataDog/lading](https://github.com/DataDog/lading)Cited by:[Table 1](https://arxiv.org/html/2607.01504#S5.T1.1.8.6.1)\.
- L\. de Moura and N\. Bjørner \(2008\)Z3: an efficient SMT solver\.InTools and Algorithms for the Construction and Analysis of Systems \(TACAS\),LNCS, Vol\.4963,Berlin, Heidelberg,pp\. 337–340\.External Links:[Document](https://dx.doi.org/10.1007/978-3-540-78800-3%5F24)Cited by:[§3](https://arxiv.org/html/2607.01504#S3.SS0.SSS0.Px3.p1.1)\.
- X\. Denis, J\. Jourdan, and C\. Marché \(2022\)Creusot: a foundry for the deductive verification of Rust programs\.InFormal Methods and Software Engineering \(ICFEM\),LNCS, Vol\.13478,Cham,pp\. 90–105\.External Links:[Document](https://dx.doi.org/10.1007/978-3-031-17244-1%5F6)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p2.1),[§6](https://arxiv.org/html/2607.01504#S6.p3.1)\.
- N\. Eén and N\. Sörensson \(2003\)An extensible SAT\-solver\.InTheory and Applications of Satisfiability Testing \(SAT\),LNCS, Vol\.2919,Berlin, Heidelberg,pp\. 502–518\.External Links:[Document](https://dx.doi.org/10.1007/978-3-540-24605-3%5F37)Cited by:[§3](https://arxiv.org/html/2607.01504#S3.SS0.SSS0.Px3.p1.1)\.
- L\. Gäher, M\. Sammler, R\. Jung, R\. Krebbers, and D\. Dreyer \(2024\)RefinedRust: a type system for high\-assurance verification of Rust programs\.Proc\. ACM Program\. Lang\.8\(PLDI\)\.External Links:[Document](https://dx.doi.org/10.1145/3656422)Cited by:[§6](https://arxiv.org/html/2607.01504#S6.p1.1)\.
- S\. Ho and J\. Protzenko \(2022\)Aeneas: Rust verification by functional translation\.Proc\. ACM Program\. Lang\.6\(ICFP\),pp\. 711–741\.External Links:[Document](https://dx.doi.org/10.1145/3547647)Cited by:[§6](https://arxiv.org/html/2607.01504#S6.p3.1)\.
- L\. Huang, S\. Ebersold, A\. Kogtenkov, B\. Meyer, and Y\. Liu \(2026\)Lessons from formally verified deployed software systems\.ACM Comput\. Surv\.58\(8\)\.External Links:ISSN 0360\-0300,[Document](https://dx.doi.org/10.1145/3785652)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p2.1)\.
- B\. Jacobs, J\. Smans, P\. Philippaerts, F\. Vogels, W\. Penninckx, and F\. Piessens \(2011\)VeriFast: a powerful, sound, predictable, fast verifier for C and Java\.InNASA Formal Methods \(NFM\),Lecture Notes in Computer Science, Vol\.6617,Berlin, Heidelberg,pp\. 41–55\.External Links:[Document](https://dx.doi.org/10.1007/978-3-642-20398-5%5F4)Cited by:[§6](https://arxiv.org/html/2607.01504#S6.p3.1)\.
- R\. Jung, H\. Dang, J\. Kang, and D\. Dreyer \(2019\)Stacked borrows: an aliasing model for rust\.Proc\. ACM Program\. Lang\.4\(POPL\)\.External Links:[Document](https://dx.doi.org/10.1145/3371109)Cited by:[§4\.3](https://arxiv.org/html/2607.01504#S4.SS3.SSS0.Px6.p1.5),[§6](https://arxiv.org/html/2607.01504#S6.p1.1)\.
- R\. Jung, J\. Jourdan, R\. Krebbers, and D\. Dreyer \(2017\)RustBelt: securing the foundations of the rust programming language\.Proc\. ACM Program\. Lang\.2\(POPL\)\.External Links:[Document](https://dx.doi.org/10.1145/3158154)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p1.1),[§6](https://arxiv.org/html/2607.01504#S6.p1.1)\.
- R\. Jung, B\. Kimock, C\. Poveda, E\. Sánchez Muñoz, O\. Scherer, and Q\. Wang \(2026\)Miri: practical undefined behavior detection for Rust\.Proc\. ACM Program\. Lang\.10\(POPL\)\.External Links:[Document](https://dx.doi.org/10.1145/3776690)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p2.1),[§4\.3](https://arxiv.org/html/2607.01504#S4.SS3.SSS0.Px6.p1.5),[§6](https://arxiv.org/html/2607.01504#S6.p1.1)\.
- D\. Kroening, P\. Schrammel, and M\. Tautschnig \(2023\)CBMC: the C bounded model checker\.Note:arXiv:2302\.02384Cited by:[§3](https://arxiv.org/html/2607.01504#S3.p1.1),[§4\.1](https://arxiv.org/html/2607.01504#S4.SS1.p1.9)\.
- D\. Kroening and M\. Tautschnig \(2014\)CBMC – c bounded model checker\.InTools and Algorithms for the Construction and Analysis of Systems,E\. Ábrahám and K\. Havelund \(Eds\.\),Berlin, Heidelberg,pp\. 389–391\.External Links:[Link](https://doi.org/10.1007/978-3-642-54862-8_26),ISBN 978\-3\-642\-54862\-8Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p4.1),[§4\.1](https://arxiv.org/html/2607.01504#S4.SS1.p1.9)\.
- A\. Langley, A\. Riddoch, A\. Wilk, A\. Vicente, C\. Krasic, D\. Zhang, F\. Yang, F\. Kouranov, I\. Swett, J\. Iyengar, J\. Bailey, J\. Dorfman, J\. Roskind, J\. Kulik, P\. Westin, R\. Tenneti, R\. Shade, R\. Hamilton, V\. Vasiliev, W\. Chang, and Z\. Shi \(2017\)The QUIC transport protocol: design and internet\-scale deployment\.InProceedings of the Conference of the ACM Special Interest Group on Data Communication,SIGCOMM ’17,New York, NY, USA,pp\. 183–196\.External Links:[Document](https://dx.doi.org/10.1145/3098822.3098842)Cited by:[§5](https://arxiv.org/html/2607.01504#S5.p3.1)\.
- A\. Lattuada, T\. Hance, C\. Cho, M\. Brun, I\. Subasinghe, Y\. Zhou, J\. Howell, B\. Parno, and C\. Hawblitzel \(2023\)Verus: verifying Rust programs using linear ghost types\.Proc\. ACM Program\. Lang\.7\(OOPSLA2\)\.External Links:[Document](https://dx.doi.org/10.1145/3586037)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p2.1),[§6](https://arxiv.org/html/2607.01504#S6.p2.1)\.
- N\. Lehmann, A\. T\. Geller, N\. Vazou, and R\. Jhala \(2023\)Flux: liquid types for rust\.Proc\. ACM Program\. Lang\.7\(PLDI\)\.External Links:[Document](https://dx.doi.org/10.1145/3591283)Cited by:[§6](https://arxiv.org/html/2607.01504#S6.p3.1)\.
- A\. Levy, B\. Campbell, B\. Ghena, D\. B\. Giffin, P\. Pannuto, P\. Dutta, and P\. Levis \(2017\)Multiprogramming a 64kb computer safely and efficiently\.InProceedings of the 26th Symposium on Operating Systems Principles,SOSP ’17,New York, NY, USA,pp\. 234–251\.External Links:ISBN 9781450350853,[Document](https://dx.doi.org/10.1145/3132747.3132786)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p1.1)\.
- J\. Liebow\-Feeser and J\. Wrenn \(2024\)Zerocopy: zero\-cost memory manipulation\.Note:[https://github\.com/google/zerocopy](https://github.com/google/zerocopy)Cited by:[Table 1](https://arxiv.org/html/2607.01504#S5.T1.1.7.5.1)\.
- A\. Niemetz and M\. Preiner \(2023\)Bitwuzla\.InComputer Aided Verification \(CAV\),LNCS, Vol\.13965,Cham,pp\. 3–17\.External Links:[Document](https://dx.doi.org/10.1007/978-3-031-37703-7%5F1)Cited by:[§3](https://arxiv.org/html/2607.01504#S3.SS0.SSS0.Px3.p1.1)\.
- OASIS \(2019\)Virtual I/O device \(VIRTIO\) version 1\.1\.Note:[https://docs\.oasis\-open\.org/virtio/virtio/v1\.1/virtio\-v1\.1\.html](https://docs.oasis-open.org/virtio/virtio/v1.1/virtio-v1.1.html)Cited by:[§5\.1](https://arxiv.org/html/2607.01504#S5.SS1.SSS0.Px2.p2.1)\.
- C\. Rabotin \(2024\)Hifitime: a high\-fidelity time management library\.Note:[https://nyxspace\.com/hifitime/](https://nyxspace.com/hifitime/)Cited by:[§1](https://arxiv.org/html/2607.01504#S1.p4.1),[Table 1](https://arxiv.org/html/2607.01504#S5.T1.1.5.3.1)\.
- rust\-osdev contributors \(2024\)X86\_64: library for x86\_64 specific functionality\.Note:[https://github\.com/rust\-osdev/x86\_64](https://github.com/rust-osdev/x86_64)Cited by:[Table 1](https://arxiv.org/html/2607.01504#S5.T1.1.1.2)\.
- seL4 Foundation \(2024\)Rust\-sel4: Rust bindings for the seL4 microkernel\.Note:[https://github\.com/seL4/rust\-sel4](https://github.com/seL4/rust-sel4)Cited by:[Table 1](https://arxiv.org/html/2607.01504#S5.T1.1.9.7.1)\.
- A\. VanHattum, D\. Schwartz\-Narbonne, N\. Chong, and A\. Sampson \(2022\)Verifying dynamic trait objects in Rust\.InProceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice,ICSE\-SEIP ’22,New York, NY, USA,pp\. 321–330\.External Links:[Document](https://dx.doi.org/10.1145/3510457.3513031)Cited by:[§3](https://arxiv.org/html/2607.01504#S3.p1.1)\.
- N\. Villani, J\. Hostert, D\. Dreyer, and R\. Jung \(2025\)Tree borrows\.Proc\. ACM Program\. Lang\.9\(PLDI\)\.External Links:[Document](https://dx.doi.org/10.1145/3735592)Cited by:[§4\.3](https://arxiv.org/html/2607.01504#S4.SS3.SSS0.Px6.p1.5),[§6](https://arxiv.org/html/2607.01504#S6.p1.1)\.