Creusot Devlog

Creusot 0.9.0

· 6min

Begin Devlog

Welcome to the Creusot Devlog, where we blog about the development of Creusot project, a deductive verifier for Rust.

The plan is to have posts accompany our monthly releases, highlighting key features and writing about happenings in and around Creusot.

Creusot at POPL

Last week, the Creusot Team went to POPL 2026, a major academic PL conference.

  • We presented a tutorial on Creusot. More details below.

  • Arnaud Golfouse gave a talk at the CPP workshop (Certified Programs and Proofs):

Upcoming events

One more Creusot paper will appear in JFLA 2026, a French-speaking academic conference taking place next week. This paper is about verifying an implementation of a tricky tree traversal algorithm (see also Threaded binary tree on Wikipedia) using Creusot:

Also next week, Li-yao Xia will give another presentation of Creusot at the RFMIG meeting (Rust Formal Methods Interest Group), online, on Monday, January 26 at 18:00 GMT (19:00 in France). It will focus on a work-in-progress case study: verifying slice methods in Rust's core library.

What's new in Creusot?

Creusot 0.9.0 was released earlier this month, right before the start of POPL.

Creusot Tutorial

The Creusot tutorial walks you through the process of verifying a Rust program with Creusot. The tutorial is available in the creusot-rs/tutorial repository. You don't even need to install anything: you can try Creusot online in your browser! See the README for more details.

This uses a DevContainer, made possible by recently added support for installing Creusot with Nix.

Contents of the tutorial

Infer trivial loop invariants

This is a convenience enhancement for type invariants.

A type invariant is a property that all values of a type should satisfy. This is a natural way to encode well-formedness conditions of many data structures.

For example, below is a type of "ordered pairs", OPair, with the type invariant that its fields are indeed ordered.

// Ordered pairs
pub struct OPair(pub u64, pub u64);

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

By equipping a type with a type invariant, every function whose interface involves that type will implicitly assert its type invariant in the function's preconditions and postconditions.

    #[requires(self.0 < self.1)]
    // Implicit:
    // #[requires(inv(*self))]
    // #[ensures(inv(^self))]
    pub fn bump(&mut self) {
        self.0 += 1;
    }

The problem arises when we use such a type in a loop. For example:

    pub fn bump_loop(&mut self) {
        while self.0 < self.1 {
            self.bump()
        }
    }

In that loop, we call self.bump, which requires self to satisfy its type invariant.

Previously, we had to explicitly state the loop invariant, that the type invariant is preserved by each iteration of the loop body:

    pub fn bump_loop(&mut self) {
        #[invariant(inv(*self))]
        while self.0 < self.1 {
            self.bump()
        }
    }

This kind of condition easy to forget for newcomers, and becomes quite cumbersome as more type invariants are involved.

Now this invariant is automatically inserted by Creusot.

That's not all. It may still be desirable to write loops that don't preserve the type invariant—for example, in the initialization of a complex data structure.

Although one might imagine a flag to toggle this behavior, we propose an automatic but conservative solution that guesses right in most cases: a type invariant is inserted in a loop invariant only if the last write to a given variable before (re)entering the loop comes from a function boundary.

For the example above, self is written to by the caller of the function first, and then by the bump method in the loop, both of which involve a type invariant assertion, so we can safely insert that type invariant as a loop invariant.

For a counterexample, below we replaced the bump call with a direct assignment to a field of self. Such assignments are not required to preserve the type invariant of self in general (even though in this case it does). Indeed, we expect field assignments to occur as part of the implementation of a data structure, temporarily breaking type invariants. Consequently, Creusot does not insert the type invariant implicitly in this case. The user can still provide it if necessary.

    pub fn bump_loop_raw(&mut self) {
        #[invariant(inv(*self))] // Must be explicit
        while self.0 < self.1 {
            self.0 += 1;
        }
    }

Creusot decides whether to insert such type invariants by performing a little static analysis, a standard exercise in compiler writing.

This analysis also detects mutable variables that are not actually written to, so that Creusot can also insert invariants that say "this value hasn't changed since the beginning of the loop".

Renamed creusot_std

Creusot's standard library has been renamed from creusot_contracts to creusot_std.

This library provides macros to enable writing contracts (requires, etc.), and it also contains contracts for the Rust standard library, hence the old name creusot_contracts. The new name creusot_std better conveys the idea that it's a fundamental library to be imported by all Creusot users.

Compatibility with no_std

The creusot_std library now features a flag std which can be disabled for no_std projects. This is part of ongoing work to support the verification of low-level embedded code.

Disabling std reduces the dependencies of creusot_std to core and alloc. This removes contracts for a few data structures such as hashmaps. In the future, it may be possible to avoid the dependency on alloc as well, but it seems that most no_std projects also depend on alloc anyway.

Concurrency: atomic invariants

Creusot takes its first step in the formal verification of concurrent programs. Our first working example is parallel_add (for comparison, here is the equivalent Rust code without ghost annotations).

This builds on top of the aforementioned work on ghost ownership presented at CPP 2026. For concurrency, this release makes two key additions to the creusot_std library: the AtomicI32 type—a ghost-aware wrapper around std::sync::atomic::AtomicI32—and a notion of AtomicInvariant inspired by Iris, a separation logic framework in Rocq. For now, this only supports sequential consistency. There is ongoing work to also provide support for relaxed memory models.

Stay tuned for future updates on Creusot!