Creusot 0.11.0: VerifyThis winner

# Creusot 0.11.0: VerifyThis winner Source: [https://devlog.creusot.rs/2026-04-20/](https://devlog.creusot.rs/2026-04-20/) 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\ 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](https://verifythis.github.io/onsite/)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](https://hal.science/hal-05396946v1)\) and originally in Verus \([OOPSLA 2023](https://arxiv.org/abs/2303.05491)\)\. 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](https://github.com/creusot-rs/creusot-examples?tab=readme-ov-file#verifythis-2026)\. ## RustVerify 2026 The[RustVerify workshop](https://sites.google.com/view/rustverify2026/home)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](https://github.com/Lysxia/creusot-rust-std)\. 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](https://github.com/creusot-rs/creusot/blob/master/CHANGELOG.md#0110---2026-04-20)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<T> Iterator for Seq<T> { type Item = T; fn next(&mut self) -> Option<T> { /* ghost code */ } } // Blanket impl from std impl<I: Iterator> IntoIterator for I { type IntoIter = Self; fn into_iter(self) -> Self::IntoIter { self } } impl<T> IntoIterator for &Seq<T> { type IntoIter = Seq<&T>; fn into_iter(self) -> Self::IntoIter { /* ghost code */ } } impl<T> IntoIterator for &mut Seq<T> { 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](https://doc.rust-lang.org/std/iter/trait.IntoIterator.html#impl-IntoIterator-for-I): ``` impl<I: Iterator> IntoIterator for I ``` Indeed, since`Seq<T\>: Iterator`, we also have`&mut Seq<T\>: Iterator`via[this impl](https://doc.rust-lang.org/std/iter/trait.Iterator.html#impl-Iterator-for-%26mut+I): ``` 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](https://github.com/creusot-rs/creusot/pull/1964/changes#diff-5c9d108ce643f2321e13267ebb68245b32a136bd14dc968d2d7c8612f21967deL541)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\.