Creusot Wins VerifyThis: What Rust's Borrow Checker Means for Formal Proof

Formal verification of real programs is still rare enough that a tool winning a major competition is worth examining closely. Creusot released version 0.11.0 alongside winning VerifyThis 2026, the annual competition where teams solve structured verification challenges live, in front of judges, using whatever tools they prefer. That result is interesting not just as a milestone for the project but as evidence about where Rust’s type system and the state of deductive verification intersect.

What Creusot Actually Does

Creusot is a deductive verifier for Rust. You annotate your code with pre- and post-conditions, loop invariants, and logical functions, and Creusot translates your annotated program into Why3, a platform for deductive program verification maintained at Inria/LRI. Why3 then dispatches the resulting proof obligations to SMT solvers, typically Alt-Ergo, Z3, and CVC5, which attempt to discharge them automatically. If all obligations are discharged, you have a machine-checked proof that your program satisfies its specification.

The specification language Creusot uses is called Pearlite. It looks like Rust, uses Rust syntax, and is embedded via procedural macros:

#[requires(n >= 0)]
#[ensures(result >= 0)]
#[ensures(result * result <= n)]
#[ensures((result + 1) * (result + 1) > n)]
fn integer_sqrt(n: u64) -> u64 {
    let mut r = 0u64;
    #[invariant(r * r <= n)]
    while (r + 1) * (r + 1) <= n {
        r += 1;
    }
    r
}

The #[requires] and #[ensures] attributes express the function’s contract. The #[invariant] attribute annotates the loop. None of this is evaluated at runtime; it all lives in the verification layer. You can also write #[logic] functions that exist purely for specification purposes, and #[predicate] for boolean-valued logical functions. These are how you express auxiliary lemmas and helper definitions that the SMT solvers can use.

The Prophecy Variable Problem

The genuinely hard part of verifying Rust is mutable borrows. In most languages with formal verification support, heap mutation is handled by tracking what a pointer points to before and after a function call. Rust’s borrow checker eliminates aliasing, but it does so by introducing a concept that has no direct analog in classical program logic: a mutable reference &mut T is a temporary, exclusive loan. The value will eventually be returned to its owner, possibly in a modified state, and the original owner resumes control at that point.

Creusot handles this with prophecy variables, a technique adapted from the work of Matsushita, Tsukada, and Kobayashi. When you take a mutable reference to a value, Creusot introduces a logical variable that stands for the final value the reference will hold when it is dropped. Specifications can mention both the current value and this prophetic final value. A function that takes &mut Vec<i32> can say in its post-condition that the output vector is a permutation of the input vector, even though the function mutated the vector in place, because the prophecy variable lets you relate the before and after states across the loan boundary.

This is what makes Creusot’s approach qualitatively different from tools like Kani, AWS’s Rust model checker. Kani is a bounded model checker based on CBMC. It unrolls loops to a fixed depth and checks all reachable states within that bound, which is excellent for finding bugs but does not produce proofs. Creusot is after mathematical certainty, not bounded exploration. The prophecy variable mechanism is what allows that certainty to survive contact with Rust’s ownership model.

Comparison with the Rust Verification Landscape

Prusti is the other major deductive verifier for Rust. It was developed at ETH Zurich and uses Viper as its intermediate verification language rather than Why3. Both tools aim at the same goal, but they have different strengths. Prusti has historically had better integration with Rust’s trait system and was one of the first tools to demonstrate that separation logic-style reasoning could be automated in the Rust setting. Creusot’s prophecy-based approach handles mutable borrows without requiring explicit framing conditions in many common cases, which makes specifications more concise.

Verus, developed at CMU and Microsoft Research, takes yet another approach: it embeds a rich specification language directly in Rust syntax and compiles specifications to Z3 queries without going through an intermediate verification language. Verus has been applied to verified systems code, including verified components of operating system kernels, and has a more active development community around verified OS and hypervisor work.

All three tools are trying to solve the same fundamental problem from different angles. VerifyThis is one of the few venues where they would be measured against each other on the same problems, which is part of why Creusot’s result matters.

What VerifyThis Actually Tests

VerifyThis is a competition held annually at ETAPS, the European Joint Conferences on Theory and Practice of Software. Teams receive algorithmic problems during the competition and have a fixed time to produce verified implementations. Past problems have included variants of sorting algorithms, tree rotations, concurrent data structures, and mathematical algorithms with non-obvious invariants.

The competition favors tools that can handle complex loop invariants and data structure invariants under time pressure. This is where SMT automation matters. If a tool requires manual proof steps for every heap operation, it will not finish in time. Winning VerifyThis means Creusot’s automation is strong enough to close goals that less automated tools would require hand-written lemmas to handle.

It also means the specification language is expressive enough to capture the invariants the problems require. A verifier is only as useful as what you can say in it. Pearlite’s ability to express quantified properties over sequences and its integration with Rust’s iterator and closure machinery are what make complex algorithm specifications writeable at all.

The 0.11.0 Release

Version 0.11.0 accompanies the competition result. Creusot’s development has been steady since its initial publication, with incremental improvements to the standard library of verified specifications, the handling of Rust features like closures and iterators, and the quality of the Why3 output that makes it easier for SMT solvers to find proofs. Each release represents more of the Rust standard library covered by specifications that can be used in downstream proofs, which is important because a verifier that cannot reason about Vec or iterator combinators is severely limited in practice.

The broader trajectory of Creusot reflects a maturing recognition in the Rust community that the borrow checker is not just a safety mechanism but a formal structure that can be exploited for verification. Languages without ownership have to encode aliasing information in their specifications explicitly, using separation logic or region annotations. Rust’s type system does that work for free, and tools like Creusot convert that structural information into logical constraints that SMT solvers can handle.

The combination of a strong ownership model, a maturing ecosystem of verifiers, and competition results demonstrating that automated proof works on non-trivial problems is a reasonable picture of where Rust’s formal verification story stands in 2026. It is not yet at the point where you would verify a production codebase without significant annotation effort, but the gap between what is theoretically possible and what is practically achievable is closing at a visible rate.