My guess is https://en.wikipedia.org/wiki/Model_checking . C Bounded Model Checker [0] is a relatively well-known instance in the niche.
My guess is https://en.wikipedia.org/wiki/Model_checking . C Bounded Model Checker [0] is a relatively well-known instance in the niche.
No, he used verus, a rust tool. And shuffle and ffs. See his docs