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)
mbonnet 22 hours ago [-]
A decent amount of mission-critical software undergoes formal verification, like spacecraft flight software (my area of expertise). SparkADA lives on because of not just its safety, but formal verifiability.
crackalamoo 21 hours ago [-]
Interesting, how common is this vs just unit testing? How do you avoid formally verifying something against a spec that could subtly fail in production?
phillc73 20 hours ago [-]
Make sure the specifications can’t fail by verifying them for correctness.
Something like TLA+[1] and Quint[2] specifications can be verified for correctness using Apalache[3]. Then test the Rust code against the specifications using quint_connect.[4]
(Not specifically for Creusot)
Something like TLA+[1] and Quint[2] specifications can be verified for correctness using Apalache[3]. Then test the Rust code against the specifications using quint_connect.[4]
[1] https://www.learntla.com/
[2] https://quint.sh/
[3] https://apalache-mc.org/
[4] https://docs.rs/quint-connect/latest/quint_connect/
Verus encodes directly to SMT.
Creusot may gain some more automation perhaps from this approach.
[0]: https://www.britannica.com/place/Le-Creusot
[1]: https://en.wikipedia.org/wiki/Le_Creusot