GitHub - creusot-rs/creusot: Creusot helps you prove your Rust code is correct.

Le marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889

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 To get an idea of what verifying a program with Creusot looks like, we encourage you to take a look at some of our test suite:

Zeroing out a vector Binary search on Vectors Sorting a vector IterMut Normalizing If-Then-Else Expressions

More examples are found in examples and tests/should_succeed. Projects built with Creusot

CreuSAT is a verified SAT solver written in Rust and verified with Creusot. It really pushes the tool to its limits and gives an idea of what 'use in anger' looks like. Another big project is in the works :)

Installing Creusot as a user

Install rustup, to get the suitable Rust toolchain Get opam, the package manager for OCaml Clone the creusot repository, then move into the creusot directory. git clone https://github.com/creusot-rs/creusot cd creusot

Install Creusot: ./INSTALL

Check that the installation succeeded: cargo creusot --help

See the Creusot guide: Installation for more details.

Upgrading Creusot

Enter the cloned Creusot git repository used previously to install Creusot Update Creusot's sources: git pull

Update opam's package listing: opam update

Reinstall Creusot: ./INSTALL

Hacking on Creusot See CONTRIBUTING.md for information on the developer workflow for hacking on the Creusot codebase.