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 WhyML, the verification and specification language of Why3. Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions!

See ARCHITECTURE.md for technical details.

Help and Discussions

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 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

1. Install rustup, to get the suitable Rust toolchain
2. Get opam, the package manager for OCaml
3. Clone the creusot repository, then move into the creusot directory.

   $ git clone https://github.com/creusot-rs/creusot
   $ cd creusot
   

4. Install Creusot:

   $ ./INSTALL
   

   A regular installation consists of:
   • the cargo-creusot executable in ~/.cargo/bin/;
   • the creusot-rustc executable in {DATA_DIR}/toolchains/$TOOLCHAIN/bin;
   • the why3 and why3find executables in {SWITCH}/bin;
   • the Creusot prelude in {SWITCH}/lib/why3find/packages/creusot;
   • SMT solvers (Alt-Ergo, CVC4, CVC5, Z3) in {DATA_DIR}/bin;
   • configuration files in {CONFIG_DIR}.

where the directories depend on the OS:

Installation options can be set in a text file INSTALL.opts. They are just space-separated command-line arguments. Type ./INSTALL --help for a list of available options. For example:

echo "--external z3" > INSTALL.opts
./INSTALL

Upgrading Creusot

1. Enter the cloned Creusot git repository used previously to install Creusot
2. Update Creusot's sources:

   $ git pull
   

3. Update opam's package listing:

   opam update
   

4. Reinstall Creusot:

   $ ./INSTALL
   

Verifying with Creusot and Why3

• To learn how to write code with creusot: guide
• To see the API of creusot_contracts (creusot's "standard library"): creusot_contracts API

Hacking on Creusot

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

lib.rs:

The "standard library" of Creusot.

To start using Creusot, you should always import that crate. The recommended way is to have a glob import:

use creusot_contracts::*;

Writing specifications

To start writing specification, use the requires and ensures macros:

use creusot_contracts::*;

#[requires(x < i32::MAX)]
#[ensures(result@ == x@ + 1)]
fn add_one(x: i32) -> i32 {
    x + 1
}

For a more detailed explanation, see the guide.