Creusot: a deductive verifier that discharges Rust proofs through Why3

Rust in, verification conditions out through Coma

The pipeline is worth understanding precisely. Creusot takes Rust source, and what it produces is not a binary and not a lint report but verification conditions. Those conditions are written in Coma, an intermediate verification language belonging to the Why3 platform, and it is Why3's provers that discharge them.

That division of labour is the whole design. Creusot owns the front end: parsing Rust, understanding its semantics, and knowing what a slice index, an integer addition or a match on an uninitialised value actually means. Why3 is used to semi-automatically discharge the resulting verification conditions. The README describes the result as using the full power of Why3 to semi-automatically discharge the conditions, and the word semi-automatically is doing real work there.

What Creusot buys you without any annotation is memory and arithmetic safety: it verifies that code is free of panics, overflows and assertion failures. Adding annotations takes it further, to checking that the code does the correct thing rather than merely that it does not crash.

The repository structure reflects this layering. There are separate workspace members for the compiler driver (`creusot-rustc`), the standard library and its procedural macros (`creusot-std`, `creusot-std-proc`), the argument parsing and metadata crates, a `why3/` member for the prover interface, and a `coma/` directory holding the intermediate language implementation. `ARCHITECTURE.md` in the root is the documented place to look for the technical detail, and there is a `why3find.json` at the root that a Why3 installation can pick up.

Installation needs rustup, opam and a script

The user install path is short and it depends on an OCaml package manager, which surprises people who expect a Rust tool to install itself with Cargo.

You need `rustup` first, which supplies the appropriate Rust toolchain; the repository pins its own through a `rust-toolchain` file at the root. Then you need `opam`, the package manager for OCaml, which is how the Why3 side gets its dependencies. Clone and enter the repository:

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

Installation itself is a single script in the repository root:

./INSTALL

Then check it worked:

cargo creusot --help

That last command is the real acceptance test. The tool installs as a Cargo subcommand, so if `cargo creusot` responds at all, the driver is wired into your toolchain correctly.

The presence of an `INSTALL` script rather than documented `cargo install` instructions tells you the build is not a normal crate install. For teams with a reproducible Linux or Nix setup, the repository also ships `flake.nix`, a `flake.lock` and a `nix/` directory, so a Nix-based environment has a path that does not depend on your global opam switch.

The version numbers tell you where this sits. The workspace manifest declares `0.15.0-dev`, so the checked-out master is ahead of the last release, which was v0.14.0 on 2026-10-12.

Upgrading means reinstalling, not rebuilding

The upgrade procedure is worth reading because it tells you what kind of artefact this is. You go back into the cloned repository you installed from, pull the new sources, refresh opam's package listing, and run the install script again:

git pull
opam update
./INSTALL

There is no `cargo install --force` step in that sequence, because `cargo install` is not how Creusot got onto your machine in the first place. The compiler driver and the standard library both live in a workspace you keep a clone of, and the install script is what places them. That has a practical upside: your working copy is the source of truth, and `git log` in it tells you exactly which Creusot a given artifact came from. It has a downside too: you are maintaining a clone rather than consuming a published binary, so your install is only as reproducible as your opam switch and your toolchain pin.

Release cadence is steady. v0.12.0 landed on 2026-06-12, v0.13.0 on 2026-07-30 and v0.14.0 on 2026-10-12, and the last push was on 2026-10-15. The workspace uses a shared version across members, with the tag named from that shared version, so `creusot`, `creusot-std` and the rest move together rather than independently.

The licence is LGPL-2.1. The licence is LGPL-2.1; the obligations for a particular integration depend on how Creusot is used and distributed.

The examples directory is the actual onboarding material

Rather than a tutorial of prose, the project points you at its own test suite as the place to learn what verified Rust looks like. The examples named in the README are specific enough to be a syllabus.

For a first look, zeroing out a vector (`examples/all_zero.rs`) is the shortest path to a complete program. Binary search on vectors (`examples/binary_search.rs`) is the canonical case where arithmetic and bounds interact, which is exactly where Creusot earns its keep. Sorting a vector with gnome sort (`examples/gnome_sort.rs`) shows a loop with a non-obvious termination argument. The `IterMut` example at `examples/iterators/02_iter_mut.rs` deals with mutable iteration, and normalising if-then-else expressions at `examples/ite_normalize.rs` covers an expression-handling detail rather than an algorithm.

The layout tells you what a verified program looks like mechanically. Each `.rs` file has a sibling `.coma` file and a same-named directory, which is the emitted intermediate representation next to its source. Seeing those pairs side by side is the fastest way to understand what the front end is doing, because the translation is the product of the front end.

A wider set lives under `tests/should_succeed`, which is where the regression cases are. And there is an `exercises/` directory, which suggests the project has started treating verification as something you practise rather than only something you read.

For real-world evidence, the README names projects built with it: CreuSAT, a verified SAT solver in Rust that the description says pushes the tool to its limits and shows what use in anger looks like, and Krabka, a Kafka broker whose key safety algorithms are verified. A SAT solver is a much better sanity check on a verifier's usefulness than a vector example is.

The cost is in the annotations, and the limits are in the prover

Two things decide whether Creusot is usable for your project.

The first is specification effort. Verifying absence of panics and overflows needs no contracts from you. Verifying intended behavior may require additional annotations, after which Creusot can generate obligations that must be discharged. That loop is the daily cost of using this tool, and it is paid per function. On a large existing codebase it is not a tool you switch on; it is a tool you point at the functions where a bug would be expensive.

The second is prover coverage. Creusot emits conditions into Why3, and the automation available depends on which provers you have installed and what they can handle. Goals that fall outside their reach return unproven, and closing them means writing Why3 tactics yourself. The README's promise of semi-automatic discharge is honest about this, and it is the reason the upstream projects that use Creusot are the kind of thing where a human verification expert is already in the loop.

There is a third, smaller limit: the Rust that Creusot understands is Rust that its front end models. The `expand/` directory at the repository root suggests work on macro expansion, and the presence of `pearlite-syn` for parsing and a `prelude-generator` for generating the standard library prelude indicates that the front end does real syntax work. But language features that the model does not cover are the kind of thing you discover by trying them, not by reading the README, which does not enumerate unsupported constructs.

Help comes from two places the README names: a GitHub discussions forum and a Zulip stream hosted on the Why3 community's Zulip instance.

Editorial conclusion

Adopt Creusot if you are writing Rust where a panic, an overflow or a broken invariant has a real cost, and you can accept annotating functions with contracts and waiting on a prover queue. Do not adopt it for an entire codebase on the expectation that it runs like a linter, because it is deductive rather than exploratory, each function you want verified needs specification work first, and the difficulty of a goal depends on which Why3 prover answers it. Verify first that `./INSTALL` completes on your machine with rustup and opam present, that `cargo creusot --help` runs afterwards, and that the example you plan to start from, such as `examples/binary_search.rs`, verifies before you commit to annotating your own code.

Frequently asked questions

Official sources

1. creusot-rs/creusot on GitHub
2. License: LGPL-2.1
3. Project website
4. README
5. Releases