Creusot 0.14.0 - Contracts for Rust, formally proved

I am pleased to announce the release of Creusot version 0.14.0.

Creusot is a tool for formally verifying Rust code. Creusot extends Rust with a language of specifications, or contracts, and provides a toolchain for proving them (semi-)automatically with the help of SMT solvers.

The latest post on Creusot's devlog describes a few of the most recent features. For the rest, see the changelog.