Creusot Devlog

Creusot 0.10.0: February update

· 5min

What's new in Creusot?

This February's release brings a couple of QOL improvements. For the rest, see the Changelog.

Assume (trusted asserts)

The proof_assert! macro now supports the #[trusted] attribute.

#[trusted]
proof_assert! { answer == 42 };

It removes the proof obligation that would come from the assertion, so it effectively becomes an assumption available to the rest of the program after it.

We could have called it assume! or proof_assume!, but reusing #[trusted] makes it convenient to grep for all assumptions in a project.

This is useful as a placeholder à la todo!(), letting you stub out parts of a proof while you're focusing on other aspects of it.

Wildcard patterns on integers

In match expressions with integer patterns, the wildcard branch now remembers the values that the integer does not equal.

match n {
    42 => proof_assert! { n == 42 },
    _ => proof_assert! { n != 42 }, // FIXED
}

Thanks to Eric Jackson for the contribution!

Multi-package workspaces

We added options to select packages in workspaces.

The command line option -p (or --package) selects a package to build with cargo creusot and to run provers on with cargo creusot prove. This is basically the same option as in cargo build, but to call why3find and run provers, we must additionally find the output Coma files corresponding to these packages.

As the Creusot compiler is basically a modified rustc, the unit of compilation is a crate. A package defines multiple crates, and cargo does not build all of them by default: only libraries and binaries, excluding tests, examples, and benches. Creusot only supports that default target selection for now (that is libraries and binaries), until the need for others arises.

You can also choose a default set of packages to build with cargo creusot, using the default-member field in the [workspace.metadata.creusot] section of your workspace Cargo.toml:

[workspace.metadata.creusot]
default-members = ["PKG1", "PKG2"]

This falls back to the existing default-member field in [workspace] for regular cargo build. Having a separate field for Creusot lets you designate packages specifically as targets for formal verification, next to other buildable but unverified packages.

Story of a toolchain update

Creusot depends on a nightly Rust toolchain. With this release, we upgraded our toolchain from nightly-2025-11-13 to nightly-2026-01-29.

We do toolchain upgrades regularly to keep up with the fast-moving rustc API. Ideally we do this at the beginning of each release cycle to give time to potentially subtle issues to surface by the next release.

This time, there was one change that required a bit of thinking to deal with: the orphan check now panics when it encounters an unnameable type (typically, a function type).

The orphan check and unnameable types

The orphan check is what enforces "trait coherence" in Rust: that there is at most one implementation of a trait for any given type. The orphan check basically answers the question "might another crate implement this trait Tr for this type Ty?"

In rustc, this check is performed whenever you implement a trait. Since you must spell out the type for the impl block, there is normally no way to encounter an unnameable type there (unnameable types are types of functions, closures, and coroutines). However rustc did have an experimental feature "typeof" which could cause the orphan check to encounter unnameable types, allegedly (I'm not familiar with the details). That feature was removed in late November, and the now unreachable code in the orphan check that dealt with unnameable types was replaced with panics.

In Creusot, we use the orphan check in the implementation of type invariants. This feature lets you specify a property that should be satisfied by all values of a type. For example, you can define a type of integers bounded by 42 as a struct with an Invariant impl:

struct Bounded42(usize);

impl Invariant for Bounded42 {
    #[logic]
    fn invariant(self) -> bool {
        pearlite! { self.0 <= 42usize } 
    }
}

All functions that take a Bounded42 argument can assume the type invariant, and all functions that return a Bounded42 must prove the type invariant.

Any type Ty has a type invariant, which we determine as follows:

  • if there is an instance Ty: Invariant, that is a user-provided type invariant;
  • if there is definitely no such instance, then we fall back to a structural type invariant derived from the type definition (it basically says that all fields satisfy their type invariant);
  • if there is no instance Ty: Invariant in this context, but we cannot rule it out definitely (an instance may appear after instantiating some type variables, possibly using implementations provided by an unknown crate), then the type invariant is an undefined predicate.

The orphan check is what distinguishes between the last two cases. Furthermore, because type invariants apply to all types, this also concerns unnameable types: for example if you pass a closure as an argument to a function, then Creusot will look for its type invariant, involving an orphan check.

The update to the orphan check caused it to panic in this case.

The fix is simple in hindsight: we replace unnameable types (function types) with the unit type () before invoking the orphan check. Indeed, these types should behave the same as far as the orphan check is concerned: both the unit type and function types from the current crate or its dependencies are "external types" from the point of view of a sibling or descendant crate.

It is also possible to fix the orphan check in rustc itself to not panic in those cases even though they don't happen within rustc. But our workaround works and we just don't have an incentive to tinker with it further, at least until that becomes a bigger issue.