Creusot: A Deductive Verifier for the Rust Programming Language

Creusot is a deductive verifier for the Rust programming language. It ensures that your code is free from errors such as panics, overflows, and undefined behaviors by proving compliance with formal specifications. This verification method provides high confidence in program correctness, establishing mathematically rigorous connections between code and specifications.