Creusot: A Deductive Verifier for Proving Rust Code Correctness

Creusot is a deductive verifier tool for Rust code that helps developers prove their code is correct. It verifies safety from panics, overflows, and assertion failures, and with annotations can verify that code behaves correctly. The tool works by translating Rust code to Coma, a