Creusot 0.14.0 introduces support for partial orders in its formal verification of Rust traits, relaxing the previous total-order-only restriction on PartialOrd. It also adds logic verification condition generation for snapshots, with automated provers handling the changes seamlessly.
Background
Creusot is an open-source formal verification tool for Rust that translates Rust code into verified logic specifications using Why3 and other theorem provers.
- Source
- Lobsters
- Published
- Oct 13, 2026 at 03:57 PM
- Score
- 6.0 / 10