creusot-rs/creusot

A deductive verifier for Rust that proves absence of panics, overflows, and assertion failures by translating code to the Why3 verification platform