Creusot helps you prove your Rust code is correct

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)

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

Fantastic work