Skip to content

Creusot helps you prove your code is correct in an automated fashion.

License

Notifications You must be signed in to change notification settings

p-sawicki2/creusot

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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:

More examples are found in creusot/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 for the rest of the setup.
    $ git clone https://github.com/creusot-rs/creusot
    $ cd creusot
    
  4. Set up Why3 and Alt-Ergo. Create a local opam switch with why3 and alt-ergo:
    $ opam switch create -y . ocaml.4.14.1
    $ eval $(opam env)
    
    This will build why3, alt-ergo and their ocaml dependencies in a local _opam directory.
  5. Build Creusot:
    $ cargo install --path creusot-rustc
    $ cargo install --path cargo-creusot
    
    this will build the cargo-creusot and creusot-rustc executables and place them in ~/.cargo/bin.
  6. Set up Creusot:
    $ cargo creusot setup install
    
    this will download additional solvers (Z3, CVC4, CVC5) and configure Why3 to use them.

Upgrading Creusot

  1. Enter the cloned Creusot git repository used previously to install Creusot
  2. Update Creusot's sources:
    $ git pull
    
  3. Upgrade Why3 and Alt-Ergo if needed:
    $ eval $(opam env)
    $ opam update
    $ opam install .
    
  4. Rebuild and reinstall Creusot:
    $ cargo install --path creusot-rustc
    $ cargo install --path cargo-creusot
    
  5. Re-run Creusot's setup:
    $ cargo creusot setup install
    

Verifying with Creusot and Why3

See the guide.

Hacking on Creusot

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

About

Creusot helps you prove your code is correct in an automated fashion.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Rust 99.7%
  • Other 0.3%