Comment by aw1621107

Sure. I didn't mean to say that the author used CBMC, only that it's an example of model checking.

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)