Model Checking

Using the Kani Rust Verifier on a Firecracker Example

Kani is AWS's Rust model checker — a formal verification tool that proves correctness properties of Rust code by exhaustively exploring execution paths. This post shows it applied to Firecracker, AWS's microVM hypervisor, demonstrating industrial-scale use of formal methods.