Rust is a systems programming language notable for its type system enforcing an ownership discipline (the borrow checker), preventing a large class of memory unsafety errors while keeping programmers in control of the memory layout of their data structures. This makes Rust an especially attractive programming language for developing low-level systems software. As Rust finds usage in key systems like Firefox and the Linux kernel, it becomes important to move beyond the safety guarantees of the language.

Creusot is a tool for formally verifying Rust programs, which improves upon the memory safety guarantees of Rust in two ways: it enables reasoning further about the functional behavior of programs, and it also enables the verification of pointer-manipulating unsafe code whose safety conditions cannot be tracked by Rust’s borrow checker.

Creusot allows users to specify their functions using contracts (pre- and post-conditions). Creusot then translates contracts into logical formulae to be dispatched to automated solvers. It has, for example, been used to develop a verified SAT solver.

The first session of this tutorial will present how Creusot works and its main features to help write specifications: using prophecies to represent mutable borrows, ghost resources to reason about pointers, etc. The second session (bring your own laptop!) will propose hands-on practical exercises to try Creusot in action.

Recommended prerequisites: familiarity with Hoare logic and program verification, and some awareness of ownership or separation logic. Only minimal knowledge of Rust syntax will be needed as exercises will consist in annotating preexisting code with specifications.