Formal verification has a long history of working on languages purpose-built for it. Dafny has its own syntax. KeY targets Java. Frama-C works on C with heavy annotation overhead. The idea of taking a mainstream systems language and building a full deductive verifier on top of it has always seemed like the harder path. Creusot takes that path, and its 0.11.0 release, coming alongside a first-place finish at VerifyThis 2026, suggests the bet is paying off.
What Creusot Actually Does
Creusot is a deductive program verifier for Rust. You annotate your functions with contracts, preconditions and postconditions describing what the function is supposed to do, and the tool generates proof obligations that it discharges using automated theorem provers. The backend is Why3, a platform for deductive verification that can route proof obligations to multiple SMT solvers simultaneously: Alt-Ergo, Z3, CVC5. If any solver closes a goal, the goal is done.
A simple annotated function looks like this:
use creusot_contracts::*;
#[requires(x@ < i64::MAX@)]
#[ensures(result@ == x@ + 1)]
fn increment(x: i64) -> i64 {
x + 1
}The @ operator lifts Rust values into the logical model that the prover reasons about. Integers become mathematical integers, vectors become sequences, and so on. The #[requires] macro states what must hold before the call; #[ensures] states what the function guarantees on return. Loop invariants go inside loops with #[invariant].
This is straightforward for pure functions. Where things get interesting is mutable references.
Prophecy Variables and Mutable Borrows
Mutable references are the hardest part of verifying Rust. When you take a &mut T, you get exclusive access for the duration of the borrow, and the caller needs to know what value the reference will have after it comes back. In classical Hoare logic, you express this with framing conditions and pre/post pairs. In Rust, the borrow checker already enforces the exclusivity, but the verifier still needs a way to talk about the reference’s value at borrow end.
Creusot uses prophecy variables, a technique from concurrent program logic, adapted here for sequential Rust. A prophecy variable stands for the future value of a mutable reference — what it will contain when the borrow expires. In Creusot’s specification language, Pearlite, you write ^x to mean the final value of x at borrow end and *x to mean its current value.
#[ensures(*result == old(*x) + 1)]
#[ensures(^x == ^result)]
fn add_one_and_return(x: &mut u32) -> &mut u32 {
*x += 1;
x
}The second postcondition says: whatever happens to the returned reference after this function returns, the same thing happens to x. The prover can carry this constraint forward into whatever code uses the return value. It is a clean way to reason about pointer aliasing and deferred writes without needing a separation logic heap model.
This design choice reflects something deeper: Rust’s ownership rules map naturally onto the aliasing restrictions that deductive verifiers need. In C, you spend a lot of annotation budget establishing that two pointers do not alias. In Rust, the compiler already checked that. Creusot can rely on those guarantees and focus verification effort on the functional behavior.
VerifyThis and What the Competition Tests
VerifyThis runs annually as a satellite workshop of ETAPS, the European Joint Conferences on Theory and Practice of Software. Competing teams receive a small set of algorithmic challenges — typically three to five problems over a few hours — and must use their chosen verification tool to prove functional correctness, not just safety properties. Problems usually involve loops over arrays, sorting or searching algorithms, tree traversals, or concurrent data structures, all with precise mathematical specifications to prove.
The time pressure matters. Tools that require extensive interactive proof work, where you have to guide a theorem prover step by step through a proof, struggle when the clock is running. Automation is at a premium. Past winners have tended to favor tools with strong SMT integration and good support for quantified invariants over structures.
Winning this competition with a tool that operates on real Rust code, not a verification-specific language, is a meaningful result. It means Creusot’s automation is good enough to close non-trivial proof obligations quickly, and that its contract language is expressive enough to state what needs to be proven without requiring manual proof steps for every loop iteration.
Where Creusot Sits in the Rust Verification Ecosystem
Several tools target Rust verification, and they occupy different points on the spectrum between automation and expressiveness.
Prusti (ETH Zürich) is Creusot’s closest relative in philosophy. It also targets full functional correctness and uses Viper as its backend rather than Why3. Prusti uses a concept called pledges to handle mutable borrows, which serves a similar role to Creusot’s prophecy variables. The two tools have converged on similar ideas through different research lineages. Prusti has historically had better IDE tooling; Creusot has generally handled more of Rust’s trait system.
Verus takes a different approach: it asks you to write specifications in a Rust-like syntax with a more explicit proof style, closer to Dafny. It has produced impressive verified systems code, including components of an OS kernel, but the annotation overhead is higher and it requires more user-directed proof work.
Kani from AWS is a model checker rather than a deductive verifier. It unrolls loops to a bounded depth and uses SAT solving to find counterexamples. It is excellent at finding bugs quickly and requires minimal annotation, but it cannot prove full correctness for loops without explicit bounds, and it does not scale to the kind of proofs VerifyThis requires.
The tradeoff between these tools is fundamentally automation versus control. Kani maximizes automation at the cost of completeness. Verus maximizes expressiveness at the cost of annotation effort. Creusot and Prusti try to sit in the middle: enough SMT automation to handle common patterns without help, enough expressiveness to state and prove properties over complex data structures.
What 0.11.0 Adds to the Picture
Creusot’s development since its initial releases has progressively expanded its coverage of Rust’s type system. Early versions had significant gaps around closures, trait objects, and iterator combinators — the parts of Rust that feel most like a functional language. Verifying code that chains .map().filter().fold() required either rewriting it or providing manual axioms for the standard library functions involved.
Recent releases have improved closure handling and added specifications for more of the standard library. The 0.11.0 release continues this, with better support for the iterator protocol and improvements to how Pearlite specifications interact with trait bounds. The VerifyThis result is partly evidence that this work has reached a threshold: Creusot can now handle the kind of mixed imperative and functional Rust that shows up in realistic algorithmic code, not just pedagogically simple examples.
The broader significance of that threshold is that verification is no longer gated on avoiding idiomatic Rust. You do not have to write Rust-shaped C to get proofs to go through. That matters because the value of verification scales with how much of your actual code you can verify, not how much of a simplified model of it you can put into the tool.
The Larger Point
Formal verification has always faced a gap between what researchers can prove and what engineers actually write. Creusot’s strategy for closing that gap is to meet Rust where it is: real syntax, real ownership semantics, real SMT automation. The VerifyThis win is a signal that this strategy is working, at least for the class of algorithmic code that competitions test.
What remains open is the question of scale. Competition problems are self-contained; production codebases have hundreds of dependencies, complex trait hierarchies, and unsafe blocks that need manual axiomatization. Creusot’s current model requires you to either verify library code yourself or annotate it as trusted. That is tractable for a small dependency tree and becomes expensive as the tree grows.
Still, the direction is right. A deductive verifier that operates on idiomatic Rust, handles mutable references through principled logical machinery, and can close competition-level proof obligations in real time is qualitatively different from where the ecosystem was five years ago. The Creusot devlog covering this release is worth reading for the specifics of what changed in 0.11.0 and how the VerifyThis problems were approached.