Rust’s ownership model catches memory bugs at compile time. But it does not catch logic bugs. A function that swaps two pointers safely but incorrectly still compiles. Creusot, a verification tool for Rust, closes that gap.
The project, hosted on GitHub, compiles Rust code into SMT (Satisfiability Modulo Theories) logic. It then feeds that logic to an automated theorem prover, typically Z3, and asks: does this function satisfy its specification? The specification is written in Creusot’s own annotation language, a set of Rust-like contracts that describe preconditions, postconditions, and invariants.
What is surprising is how far Creusot has come. Earlier verification tools for Rust, such as Prusti, required the programmer to learn a separate specification language and often struggled with the standard library. Creusot reuses Rust’s own type system and trait machinery. It handles Vec, Box, and Option out of the box. It supports loops with invariants, recursion, and even some unsafe code patterns.
The tradeoff is real. Writing specifications is still manual work. A function like fn add(x: u32, y: u32) -> u32 requires an annotation that says ensures result == x + y. For a hundred-line function with mutable state and heap allocation, the specification can be longer than the code. Creusot does not automate correctness. It automates the verification of correctness once the specification exists.
This matters because the industry is running out of tolerance for subtle bugs. The CrowdStrike outage in 2024, the Heartbleed vulnerability, the Mars Climate Orbiter crash: all were logic errors that type systems could not catch. Formal verification has historically been confined to aerospace, cryptography, and compiler backends, where the cost of failure is high enough to justify the overhead. Creusot lowers that threshold.
The tool is not ready for production use on a million-line codebase. The SMT solver can time out on complex functions. The annotation language is still evolving. But the direction is clear. Rust already gives developers memory safety. Creusot gives them the option of correctness. For safety-critical systems, embedded firmware, and financial infrastructure, that option is beginning to look like a requirement.
The open question is whether the Rust community will adopt specification-as-code as a normal practice, or whether it will remain a niche for the most paranoid projects. Creusot makes the choice available. It does not make it easy. That is the honest state of the art.