You can prove Rust code correct without writing a single proof. The tool that does it is called a model checker, and for Rust the most practical one right now is Kani, built by AWS. You write normal Rust assertions. Kani turns them into mathematical claims and checks them for every possible input. No theorem provers. No proof assistants. No six-month detour into Coq.
The catch is that “every possible input” only works when the input space is small enough to exhaust. If your function takes a Vec<u8> with a million elements, Kani will not check every permutation. It will check up to a bound you specify, or run until your laptop runs out of RAM. The proof is real, but it is bounded.
What “proof without proofs” actually means
Formal verification usually means writing your program in a proof assistant like Coq, defining invariants by hand, and guiding the solver through tactical steps. A verified compiler like CompCert took years. Most teams do not have years.
Model checking is different. You write normal Rust. You add a test function annotated with #[kani::proof]. Inside, you create symbolic values with kani::any(), call your code, and assert properties. Kani compiles your code to a logical formula and hands it to an SMT solver. The solver either confirms the property holds for all inputs within the bound, or it produces a concrete counterexample.
You did not write a proof. You wrote a test with a universal quantifier. The tool wrote the proof.
How Kani turns Rust into logic
Kani is a bounded model checker. It unrolls your code into a logical formula and asks an SMT solver whether any execution path can violate an assertion. The solver treats variables as symbolic. A normal test gives x the value 5. A Kani proof gives x a symbol that represents every possible u32.
Here is a trivial example. We have a function that should never overflow, and we want to prove it.
// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
x.saturating_mul(2)
}
#[cfg(kani)]
mod proofs {
use super::*;
#[kani::proof]
fn check_saturating_double_never_overflows() {
let x: u32 = kani::any();
let result = saturating_double(x);
if x > u32::MAX / 2 {
assert_eq!(result, u32::MAX);
} else {
assert_eq!(result, x * 2);
}
}
}Run cargo kani and Kani verifies this in seconds. It checks all 4,294,967,296 possible values of x without running them one by one. The SMT solver reasons about the symbolic representation and concludes no counterexample exists.
The #[cfg(kani)] guard means this code compiles only under Kani. It does not bloat your release build.
A real example: proving a parser is crash-free
Overflows are easy. The interesting cases are data-dependent. Let’s say we have a function that parses a small protocol header. We want to prove it never panics, no matter what bytes we feed it.
// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
TooShort,
InvalidVersion,
}
pub struct Header {
pub version: u8,
pub length: u16,
}
/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
if buf.len() < 4 {
return Err(ParseError::TooShort);
}
let version = buf[0];
if version != 1 {
return Err(ParseError::InvalidVersion);
}
let length = u16::from_be_bytes([buf[2], buf[3]]);
Ok(Header { version, length })
}
#[cfg(kani)]
mod proofs {
use super::*;
#[kani::proof]
#[kani::unwind(5)]
fn check_parse_header_no_panic() {
let len: usize = kani::any();
kani::assume(len <= 8);
let buf: [u8; 8] = kani::any();
let _ = parse_header(&buf[..len]);
}
}Kani verifies that parse_header never panics for any input buffer of length 0 through 8. It checks the bounds test, the version check, and the array indexing. If we had written buf[1] instead of checking length first, Kani would find a counterexample: a 1-byte buffer where buf[1] is out of bounds.
The #[kani::unwind(5)] annotation tells Kani how many times to unroll loops. Since our function has no loops, this is conservative.
The bounding problem: where model checking hits the wall
Model checking is exhaustive within its bounds. Outside those bounds, it says nothing. This is the fundamental trade-off.
Loops are the first wall. Kani must unroll every loop a fixed number of times. If your function iterates over a Vec and you set the unwind bound to 10, Kani proves correctness for vectors of length 0 through 10. It says nothing about length 11. Each increment multiplies the state space. An unwind of 50 might finish in minutes. An unwind of 500 might not finish at all.
Recursion is similar. Each call expands the formula. Deep recursion explodes memory usage.
Data size is the second wall. Kani handles fixed-size arrays well. It struggles with dynamically allocated collections unless you bound their size explicitly.
The standard library is the third wall. Kani models much of it, but not all of it. If you call something Kani doesn’t understand, the proof fails with a missing function definition.
What Kani can prove and where it falls short
Kani is good at finding panics, integer overflows, and assertion violations in bounded code. It is excellent for cryptographic primitives, protocol parsers, and small state machines. These are places where a single bad input causes catastrophe, and the code is naturally bounded.
Kani is not good at proving liveness properties, like “every request eventually gets a response.” That requires reasoning about infinite executions, which bounded model checking explicitly does not do. For liveness, you want a temporal model checker like TLA+.
Kani is also not a replacement for tests. A passing proof tells you no counterexample exists within the bound. A test tells you the code behaves correctly for a specific input you care about. Kani catches the edge cases you didn’t think to test. Tests catch the integration problems Kani cannot see.
Running Kani in CI without melting your runners
A single Kani proof on a small function takes seconds. A suite on a real crate takes minutes. A proof with high unwind bounds can take hours. You do not want your CI pipeline waiting on a two-hour SMT solve.
Keep Kani proofs small and fast. Prove the safety-critical functions, the ones where a bug is an incident. Do not try to prove your entire web framework. Set a timeout, maybe five minutes per proof, and treat a timeout as a failure to prove, not a proof of failure.
Here is a Makefile pattern that works:
# Makefile
kani:
cargo kani --only-codegen --output-format=terse
cargo kani --timeout 300 --all-functions --enable-unstable
kani-fast:
cargo kani --only-codegen --output-format=terse
cargo kani --timeout 60 --all-functions --enable-unstablekani-fast runs in CI on every pull request. kani runs nightly. If a proof regresses, you find out within a day, not after shipping.
If you expose a public API, write one Kani proof per public function that calls it with fully symbolic inputs. This is the closest thing to a formal contract test. It does not prove the implementation is correct, but it proves the implementation does not crash on arbitrary valid inputs.
When to reach for a real proof assistant instead
If you need to prove properties about unbounded data structures, like “this linked list is always acyclic,” Kani will not help you. The unwind bound defeats the claim. For this, you need a tool like Creusot, which translates Rust to WhyML and uses a proof assistant. It is more work, but it handles unbounded structures.
If you need equivalence proofs or undefined behavior detection, tools like MIRI or KLEE sit at different points on the effort-versus-coverage spectrum. Kani is the sweet spot for “I have bounded code and I want to know if it panics.” Parsers, decoders, serializers, and configuration validators all fit. The Rust type system already eliminates entire classes of bugs. Kani eliminates the ones the type system can’t reach.
What to try first
If you have a Rust crate with a function that scares you, add Kani. The scary function is usually the one that parses untrusted input, does bit manipulation, or indexes into arrays. Write a proof harness that calls it with kani::any(). Run cargo kani. If it passes, you have a bounded proof of crash-freedom. If it fails, you have a concrete counterexample that would have been a bug report.
You do not need to learn a new language. You do not need to understand sequent calculus. You write Rust assertions, and a solver tells you if they hold. That is not a formal proof in the academic sense. It is a mechanical proof in the practical sense, and for most software, practical is exactly what you need.
Frequently Asked Questions
What is model checking in software verification?
Model checking is an automated technique that exhaustively explores all possible states of a system to verify whether specified properties hold. For Rust, tools like Kani use bounded model checking to prove assertions over all possible inputs within defined limits, without requiring manual proof construction.
How is Kani different from writing unit tests?
A unit test checks one specific input. A Kani proof checks every input within a bound. If a Kani proof passes, you know no counterexample exists within the bounded state space. The proof is stronger, but it is limited by the bounds you set.
Can Kani prove my entire Rust application is correct?
No. Kani works best on small, bounded functions. The state space grows exponentially with loop iterations, recursion depth, and data size. Use Kani for safety-critical components like parsers and protocol handlers, not for application-level logic.
What happens when Kani hits a loop with no fixed bound?
Kani requires an unwind bound for loops. If the loop might execute more times than the bound allows, Kani inserts an unwinding assertion that fails. You must either raise the bound or refactor the code to have a statically known iteration count. This is the main limitation of bounded model checking.