Creusot is a deductive verifier for the Rust programming language.
Creusot helps you verify that your code is free of errors—panics, overflows, undefined behaviors, etc.—by proving that it conforms to a formal specification.
Deductive verification provides high confidence in the correctness of your programs by connecting code to specifications with mathematically rigorous proofs.
With Creusot, you will find the true meaning of "if it compiles, it works."
Prophecies are the logical model that powers Creusot's first-class support for mutable borrows.
// Choose an integer depending on a boolean
//
// This specification says that the `result` is indeed `x` or `y`,
// but also that the other value is unchanged:
// the prophecy (final value) `^y` equals the initial value `*y`.
#[ensures(
if b { result == x && ^y == *y }
else { result == y && ^x == *x }
)]
pub fn choose<'a, T>(
b: bool,
x: &'a mut T,
y: &'a mut T,
) -> &'a mut T {
if b { x } else { y }
}
Pearlite is the language of contracts in Creusot for specifying Rust functions. You can define new Pearlite functions and predicates, and even declare Pearlite functions in traits!
// Pearlite predicate that a sequence `s` is sorted
#[logic(open)]
pub fn is_sorted(s: Seq<u64>) -> bool
{
pearlite! {
// A sequence `s` is sorted if `i < j` implies `s[i] <= s[j]`
forall<i: Int, j: Int>
0 <= i && i < j && j < s.len()
==> s[i] <= s[j]
}
}
// Contract for sorting: the final slice `^s` is sorted
// and is a permutation of the initial slice `*s`
#[ensures(is_sorted((^s)@))]
#[ensures((^s)@.permutation_of((*s)@))]
pub fn sort(s: &mut [u64])
{
// ...
}
Prove that your programs terminate using variants and well-founded relations.
// Sum of integers from 1 to n
//
// Terminates
// Requires: the sum must not overflow
// Ensures: the result is the `n`-th triangular number
#[check(terminates)]
#[requires(n@ * (n@ + 1) / 2 <= u32::MAX@)]
#[ensures(result@ == n@ * (n@ + 1) / 2)]
pub fn sum_first_n(n: u32) -> u32 {
let mut sum = 0;
let mut i = 0;
// The variant is a quantity that decreases at every iteration,
// ensuring that the loop eventually stops.
#[variant(n@ - i@)]
#[invariant(sum@ == i@ * (i@ + 1) / 2)]
#[invariant(i@ <= n@)]
while i < n {
i += 1;
sum += i;
}
sum
}
A technique for verifying code featuring interior mutability, raw pointers, or atomics.
// Linked list: pointers to the first and last links,
// and a ghost sequence of pointer permissions (`Perm`)
pub struct List<T> {
// actual data
first: *const Link<T>,
last: *const Link<T>,
// ghost
seq: Ghost<Seq<Box<Perm<*const Link<T>>>>>,
}
// Link of a linked list: value and pointer to the next link
struct Link<T> {
value: T,
next: *const Link<T>,
}
// ...
// Insert an element in a linked list
#[check(terminates)]
#[ensures((^self)@ == (*self)@.push_front(value))]
pub fn push_front(&mut self, value: T) {
// Allocate a new `Link` and get the pointer and the permission to that allocation
let (link_ptr, link_own) = Perm::new(Link { value, next: self.first });
// Update the end pointers of the linked list
self.first = link_ptr;
if self.last.is_null() {
self.last = link_ptr;
}
// Push the permission into the list
ghost! { self.seq.push_front_ghost(link_own.into_inner()) };
}
Full example: linked_list.rs
Creusot calls off-the-shelf SMT solvers to prove verification conditions. Multiple solvers can be used to leverage their respective strengths. Not everything can be automated, of course. To make this method work, you still have to annotate functions with contracts and loops with loop invariants. Automation takes care of proving simple goals immediately, letting you focus on the proof obligations that matter.
From our gallery of examples:
Verified sort implementations
Left pad (from Hillel Wayne's Great theorem prover showdown)
Creusot compiles Rust programs to Coma, an intermediate verification language, then leverages the Why3 Platform to generate verification conditions to be dispatched to SMT solvers. See our papers for more details.