Creusot helps you prove your Rust code is correct

Creusot is a deductive verifier for Rust code that automatically proves programs are safe from panics, overflows, and assertion failures, with the ability to verify broader correctness properties through annotations. The tool translates Rust code into an intermediate verification language called Coma within the Why3 Platform to discharge verification conditions semi-automatically. Notable projects using Creusot include CreuSAT, a verified SAT solver written entirely in Rust.