Creusot 0.14 adds another round of proved Rust contracts

Creusot 0.14.0 landed on 13 October 2026. It is a verifier for Rust, not a new compiler. You write ordinary Rust, then add a specification language of contracts, and Creusot tries to prove those contracts with SMT solvers.

That split matters. A test shows that one input behaved the way you hoped. A contract says what must be true for every input the specification covers, and the solver searches for a counterexample. When the proof goes through, you have a stronger claim than a green CI job. When it fails, the failure is a concrete reason the spec and the code disagree.

The 0.14 release notes point readers at the project changelog and a recent devlog for the newest features. The release itself is the news: the toolchain moved forward, and teams already using Creusot can pick it up without waiting on a language change in rustc.

Formal tools still ask for a different kind of work. Someone has to write the contracts, keep them honest as the code changes, and decide which properties are worth proving. Creusot does not remove that judgment. It shortens the path from “we think this function is safe” to a check a machine can rerun.

For a codebase that already lives in Rust, that is a practical place to start. The proofs sit next to the implementation, and the same people who change the function can change the spec. Juensy will keep an eye on which contracts the 0.14 line actually makes easier to discharge.