Kani: Bounded model checker for Rust
====================================

Kani is AWS's bounded model checker for Rust. It proves absence of panics, undefined behaviour and violated assertions within loop bounds, with no specification language to learn, and is used across AWS's Rust libraries and the Rust standard library verification challenge.

Maintainer: AWS
Website: https://github.com/model-checking/kani
Category: Verified implementations
Targets: Rust, Rust standard library verification challenge, AWS Rust libraries
Approach: Bounded model checking (CBMC backend) for panics, memory safety and user assertions
Access: Open source (Apache-2.0 / MIT)
Status: Active
Strengths: Low effort, high value on unsafe and arithmetic code. | Concrete counterexamples. | AWS-backed, well maintained.
Limits: Bounded: no guarantee beyond the unwinding depth. | No functional correctness against a cryptographic spec. | Struggles with large state spaces.
Firms using it: none listed
Sources: https://github.com/model-checking/kani

Source page: https://sorryfree.com/frameworks/kani/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13