Comment by markasoftware

A correctness bug in a proof checker by definition means that you can prove false.