GoKawiilLe marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889 Creusot
About
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, an intermediate verification language of the Why3 Platform. Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions!
See ARCHITECTURE.md for technical details.
Help and Discussion
If you need help using Creusot or would like to discuss, you can post on the discussions forum or join our Zulip chat!
Citing Creusot
If you would like to cite Creusot in academic contexts, we encourage you to use our ICFEM'22 publication.
Examples of Verification
... continue reading