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.