The other day I saw a link to Verus on here and it’s made me somewhat interested in the topic how Rust and formal verification can work together.
It’s quite insightful to see how the borrow checker both required and ended up facilitating the ability to do more extensive formal verification on Rust code.
Something like Verus (I haven’t looked into most of the other tools in this space yet, there seem to be many!) does appear poised to make verification quite approachable in low-level, self-contained Rust code already, and I’m curious to see how things evolve from there.
It would be exceedingly cool if one day there’s a subset of libraries on crates.io that are fully verified (similar to how today there’s a subset that supports no-std
development) and which are then usable to build upon in your own formally verified code.