No, he used verus, a rust tool.
And shuffle and ffs. See his docs
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)