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?
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?
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]
[1] https://www.learntla.com/
[2] https://quint.sh/
[3] https://apalache-mc.org/
[4] https://docs.rs/quint-connect/latest/quint_connect/