Welcome back to the devlog of Creusot, a tool for proving Rust programs correct.
New website
If you are curious to know what this project is about,
check out Creusot's new website! creusot.rs
It presents what Creusot is, its main features, and links to resources.
Also new is a list of publications related to Creusot.
Last week, the Creusot team went to the ETAPS conference in Turin. The main two events
we attended were the VerifyThis challenge and the RustVerify workshop.
This release was delayed to prepare for the RustVerify talk.
VerifyThis 2026
VerifyThis is a program verification competition.
It's similar to a programming competition but instead of passing test cases,
the goal is to prove that programs satisfy given specifications using
your favorite verification tool.
Solutions will be judged for correctness, completeness, and elegance.
Jacques-Henri Jourdan and Li-yao Xia participated to this year's VerifyThis
as a team (The Steelmakers) using Creusot.
We are happy to report that we got the Best Overall Team award!
It was a nice opportunity to see what it's like to use the tool we've been working on.
Our tooling didn't cause issues—except for one isolated bug in #[bitwise_mode]—so
we could quickly focus on the challenge. The concurrency problem (Challenge 2)
was the perfect use case for ghost permissions, a feature presented in Creusot
earlier this year (CPP 2026)
and originally in Verus (OOPSLA 2023).
VerifyThis challenges are designed to be especially difficult, and participants are
allowed to adapt the problem to fit tool limitations or time constraints—problem
statements may even explicitly suggest possible simplifications.
We are proud that Creusot enabled us to make a total of zero simplifications:
we (tried to) verify the programs as written in the problem statements,
for better or for worse.
Our solutions are available in the creusot-examples repository.
RustVerify 2026
The RustVerify workshop
included two talks directly connected to Creusot:
- Verifying the Rust standard library with Creusot, by Li-yao Xia et al., presented
our ongoing effort at verifying slice functions in the standard library.
It uses a new "proof modes" feature which is work-in-progress
and not part of the present release. - Supporting weak memory in Creusot and Verus, by Natalie Neamtu et al.,
presented new primitives for release-acquire and relaxed atomic accesses.
On Creusot's side, they are available in this release. A proper write-up
of how to reason about concurrency in Creusot is future work.
What's new in Creusot?
No major new features this release; see the Changelog for details.
But big things are already lining up for next month. Stay tuned!
Explicit binder for results
It is now possible to name the result variable in postconditions:
```
[ensures(result@ == 0)] // default name result (old, still supported)
[ensures(|my_result| my_result@ == 0)] // explicitly named my_result (new)
fn zero() -> usize {
0
}
```
You can also destructure the result using patterns:
```
[ensures(|(_, b)| b@ == 42)]
fn forty_two() -> (usize, usize) {
(0, 42)
}
```
Collections should not be iterators
A little something we learned about iterators in Rust.
A collection type, like Vec, typically comes with three iterators:
an "owning" iterator (often named IntoIter or Iter), a "shared" iterator
(Iter), and a "mutable" iterator (IterMut). Each of these iterator types
is associated with the collection type via an IntoIterator impl.
My "genius" idea was that Seq<T>, Creusot's type of sequences of T,
could play the role of all three iterators for itself.
I thought it would trivialize implementations of IntoIterator for Seq<T>.
This turned out to be a bad idea. Can you guess the problem in the following snippet?
```
/ A bad idea in the making /
impl Iterator for Seq {
type Item = T;
fn next(&mut self) -> Option {
/ ghost code /
}
}
// Blanket impl from std
impl IntoIterator for I {
type IntoIter = Self;
fn into_iter(self) -> Self::IntoIter {
self
}
}
impl IntoIterator for &Seq {
type IntoIter = Seq<&T>;
fn into_iter(self) -> Self::IntoIter {
/ ghost code /
}
}
impl IntoIterator for &mut Seq {
type IntoIter = Seq<&mut T>;
fn into_iter(self) -> Self::IntoIter {
/ ghost code /
}
}
```
If this were a regular type like Vec<T>, a simple reason against
making Vec<T> into its own iterator is that it would be extremely inefficient:
next would remove the first element then shift all of the remaining elements
over it in linear time. And the other "obvious" choice of defining next
as pop would yield iteration in reverse order. Moreover, for borrowing
iterators (Iter, IterMut), you don't want to allocate a whole Vec of borrows,
instead you want next to return borrows on the fly without allocating anything.
However, Seq<T> is a logic type: it is only present in ghost code to help verification
(a key feature is that the length of Seq<T> is finite but unbounded, unlike
Vec which cannot contain more than usize::MAX elements). Ghost code does not
actually exist at run time so performance is of no concern. So what else went wrong?
Simply put, the above code does not compile. The Rust compiler rejects the
IntoIterator for &mut Seq<T> because it overlaps
with the blanket implementation:
impl<I: Iterator> IntoIterator for I
Indeed, since Seq<T>: Iterator, we also have &mut Seq<T>: Iterator via this impl:
impl<I: Iterator> Iterator for &mut I
Furthermore, if you decided to stick with that blanket implementation, you would end up with
a very confusing behavior: if you write a for loop over &mut s, you would expect to
iterate over mutably borrowed elements &mut T, but instead you would be consuming s
to yield fully owned T!
let s: Seq<T> = ...;
for x in &mut s {
...
}
/* Here `s` would be empty! */
Since this error was caught by the compiler and such code is intended for formal proof anyway,
it wouldn't be so bad... if I hadn't already started doing exactly the same thing for FMap,
another of Creusot's logic types, in the previous release. I just happened to temporarily
omit the IntoIterator for &mut FMap<K, V> which would have revealed this issue. Oops.
I hurried to revert it
as soon as I realized the mistake.
Thus Seq<T> (and other "logic types") now has distinct iterator types (IntoIter, Iter, IterMut),
which are mere newtype wrappers around Seq<T>, Seq<&T>, Seq<&mut T>.
That was this month's (not so) hard-earned lesson: collections should not be iterators.