My guess is https://en.wikipedia.org/wiki/Model_checking . C Bounded Model Checker [0] is a relatively well-known instance in the niche.
Incidentally, 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)