Rust Verification with Creusot

Creusot is a deductive verifier for Rust code. It verifies your code is safe from panics, overflows, and assertion failures. By adding annotations you can take it further and verify your code does the correct thing. Creusot works by translating Rust code to Coma.