hub / github.com/creusot-rs/creusot

github.com/creusot-rs/creusot @v0.12.0

repository ↗ · DeepWiki ↗ · release v0.12.0 ↗ · + Follow

5,095 symbols 12,852 edges 692 files 457 documented · 9% ● updated 4d agov0.12.0 · 2026-06-12★ 1,78895 open issues

What it actually does AI analysis from the code graph — generated when you open this

loading…

README

Le marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889

Creusot

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 Coma, an intermediate verification language of the Why3 Platform. Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions!

See ARCHITECTURE.md for technical details.

Help and Discussion

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 examples and 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

Install rustup, to get the suitable Rust toolchain
Get opam, the package manager for OCaml
Clone the creusot repository, then move into the creusot directory. sh git clone https://github.com/creusot-rs/creusot cd creusot
Install Creusot: sh ./INSTALL
Check that the installation succeeded: sh cargo creusot --help

See the Creusot guide: Installation for more details.

Upgrading Creusot

Enter the cloned Creusot git repository used previously to install Creusot
Update Creusot's sources: sh git pull
Update opam's package listing: sh opam update
Reinstall Creusot: sh ./INSTALL

Hacking on Creusot

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

Extension points exported contracts — how you extend this code

VeryStableHash (Interface)

HashStable is not stable enough for our purposes of hashing ImplSubject to identify Rust impls in the output Coma: HashS [12 …

creusot/src/very_stable_hash.rs

Resolve (Interface)

The trait `Resolve` makes it possible to expose to clients a custom resolve assertion for opaque types. For example, if [36 …

creusot-std/src/resolve.rs

Invariant (Interface)

Check that we can still see the bodies of default implementations which are marked as final though. [21 implementers]

tests/should_fail/bug/222.rs

Print (Interface)

(no doc) [30 implementers]

why3/src/printer.rs

Iterator (Interface)

(no doc) [22 implementers]

examples/iterators/common.rs

Hash (Interface)

(no doc) [4 implementers]

examples/bdd.rs

Hash (Interface)

A slightly simplified version of the Rust hashing mechanisms, this sufficiently captures the behavior though [1 implementers]

tests/should_succeed/hashmap_list.rs

Tokens (Interface)

(no doc) [2 implementers]

pearlite-syn/tests/macros.rs

Core symbols most depended-on inside this repo

new

called by 788

cargo-creusot/src/new.rs

iter

called by 472

creusot-std/src/std/iter/rev.rs

unwrap

called by 413

tests/should_succeed/result/own.rs

map

called by 383

creusot-std/src/logic/seq.rs

clone

called by 284

creusot-std/src/ghost.rs

len

called by 139

creusot-std/src/std/ptr.rs

into_iter

called by 138

creusot-std/src/logic/seq.rs

peek

called by 137

creusot-std/src/logic/fset.rs

Shape

Method 2,466

Function 1,749

Class 518

Enum 185

Interface 177

Languages

Rust98%

TypeScript2%

Modules by API surface

creusot/src/validate/erasure.rs107 symbols

guide/theme/highlight.js93 symbols

creusot-std/src/logic/seq.rs74 symbols

why3/src/exp.rs72 symbols

creusot/src/translation/pearlite.rs69 symbols

creusot/src/ctx.rs67 symbols

creusot/src/translation/fmir.rs62 symbols

creusot-std/src/std/ptr.rs51 symbols

creusot-std/src/logic/fmap.rs50 symbols

creusot/src/backend/clone_map.rs48 symbols

creusot-std/src/logic/int.rs47 symbols

examples/red_black_tree.rs46 symbols

For agents

$ claude mcp add creusot \
  -- python -m otcore.mcp_server <graph>

⬇ download graph artifact