As it happens, the Python verifier mmverify.py has an even simpler soundness bug [0], and so far I've reviewed two independent AI-written verifiers that have replicated that bug, since they apparently really like to copy the strategy from mmverify.py. A sound verifier isn't too difficult to write in terms of architecture (I just wrote one myself for differential testing [1]), but it requires some close attention to the details.

That is to say, the Swiss-cheese approach definitely lends authority, but individual implementations are unfortunately not as foolproof as they're made out to be.

[0] https://github.com/david-a-wheeler/mmverify.py/issues/30

[1] https://github.com/LegionMammal978/mm-verifier-tests/blob/ma...