5/28/2026 at 4:19:59 PM
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)
by rendaw
5/28/2026 at 4:58:05 PM
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.by mbonnet
5/28/2026 at 6:14:12 PM
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?by crackalamoo
5/28/2026 at 7:10:52 PM
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]
by phillc73