My guess is https://en.wikipedia.org/wiki/Model_checking . C Bounded Model Checker [0] is a relatively well-known instance in the niche.
replyNo, he used verus, a rust tool.
And shuffle and ffs. See his docs
replySure. I didn't mean to say that the author used CBMC, only that it's an example of model checking.
replyIncidentally, the docs don't seem to say what model checker was used. I don't think any of verus, shuffle, or ffs are technically model checkers (or at the very least they don't describe themselves as such)