Rust 130 🦀 Formal Verification and Theorem Proving in Rust (Kani / Prusti)
Testing shows the presence of bugs, never their absence. Fuzzing finds panics and crashes, but it cannot prove that a function returns the correct value for every possible input. Formal verification is the discipline of mathematically proving that a program satisfies a specification. For Rust, two tools occupy opposite ends of the verification spectrum. Kani…