Quickstart

Installation

Install Creusot and why3 as described in the README.

Write specifications

Create a new project, and import creusot-contracts to start writing specifications:

# Cargo.toml
[package]
name = "add_one"
version = "0.1.0"
edition = "2021"

[dependencies]
creusot-contracts = { path = "/PATH/TO/CREUSOT/creusot-contracts" }

Remark This may only work if you're using the same rust toolchain that was used to build creusot: you can copy the rust-toolchain file into the root of your project to make sure the correct toolchain is selected.

Then you can start writing specifications:

#![allow(unused)]
fn main() {
// src/lib.rs
use creusot_contracts::*;

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

Prove with Why3

Finally, launch the why3 ide:

cargo creusot why3 ide

The documentation for the why3 ide can be found here.

We also recommend section 2.3 of this thesis for a brief overview of Why3 and Creusot proofs.

We plan to improve this part of the user experience, but that will have to wait until Creusot gets more stable and complete. If you'd like to help, a prototype VSCode plugin for Why3 is in development, it should make the experience much smoother when complete.

Prove with Why3find

Configure

$ cargo creusot config

The configuration is stored in why3find.json.

Prove

Run the Creusot translation.
```
$ cargo creusot
```
Run the Why3find prover.
```
$ cargo creusot prove
```
Run the Why3find prover on specific files:
```
$ cargo creusot prove verif/[COMA_FILES]
```
Launch Why3 IDE on unproved goals (this will only open one file even if there are many listed with unproved goals).
```
$ cargo creusot prove -i
$ cargo creusot prove -i verif/[COMA_FILES]
```

Creusot User Guide