Disclaimer

This note is created for personal reference and is not endorsed by the official creator.

What is creusot?

Creusot is a tool for deductive verification for Rust code, which allows one to annotate the code with specifications, invariants and assertions and then verify them formally and automatically, proving, mathematically, that the code satisfies the specifications. To be precise, this is a tool for converting Rust code to formally verifiable code that can be feed to prover like Z3, CVC, etc. The target language is WhyML, the verification and specification language of Why3. Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions!

Prerequisites and Usage

1. Install creusot as a cargo plugin. Clone the repo and build it from source.
2. Set up Why3. This can be done via opam, a package manager for OCaml language.
3. Set up the project that the user wishes to verify:

# In Cargo.toml
[dependencies]
creusot-contracts = { path = "/path/to/creusot-contracts" }

[features]
contracts = ["creusot-contracts/contracts"]

// In some Rust source file.
extern crate creusot_contracts;
use creusot_contracts::*;

1. Copy necessary files to the root directory of the crate. These include ide script and /prelude directory in the creusot repository.

$ cp /path/to/creusot/ide /path/to/project;
$ cp -r /path/to/creusot/prelude /path/to/project;

1. Generate the target file .mlcfg by invoking the command:

$ cargo creusot -- --features creusot-contracts/contracts;
# You could find the [crate_name].mlcfg in /target/debug directory.

Note that the Rust toolchain version needs to be consistent with that of creusot; otherwise, cargo will report missing symbols because the libraries it tries to link against do not exist at all.

1. Send the target file to Why3 and verify it by some backend solver.

$ ./ide ./target/debug/[crate_name].mlcfg;

Contract Documentations