Creusot helps you prove your Rust code is correct

giltho

Fantastic work

rendaw

I'm super interested in this sort of stuff, but I have a hard time figuring out where to get started. Like, could this help in a typical CRUD application? What sorts of problems is it super useful for? What's a good way to get started integrating it into existing software, or is it better to design software ground-up to be verified? Are there limitations, or certain standard library features that are/aren't supported? (Not specifically for Creusot)

Trung0246

How does this differ from https://github.com/verus-lang/verus

Loic

I like the name[0][1]. [0]: https://www.britannica.com/place/Le-Creusot [1]: https://en.wikipedia.org/wiki/Le_Creusot