3 ms·
A decent amount of mission-critical software undergoes formal verification, like spacecraft flight software (my area of expertise). SparkADA lives on because of
by mbonnet 4mo 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 4mo agoInteresting, 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 4mo agoMake 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] [1] https://www.learntla.com/ https://www.learntla.com/ [2] https://quint.sh/ https://quint.sh/ [3] https://apalache-mc.org/ https://apalache-mc.org/ [4] https://docs.rs/quint-connect/latest/quint_connect/ https://docs.rs/quint-connect/latest/quint_connect/
- mbonnet 4mo agoit's generally another layer on top of things like unit testing, MC/DC coverage, etc. not all programs use formal verification though.