Comment by Smaug123
16 hours ago
Not necessarily. For example, perhaps my ZFC first-order-logic theorem checker implicitly accidentally contains the continuum hypothesis as an axiom. This isn't inconsistent but it is a correctness bug.
(For that matter, another correctness bug is "the checker rejects all proofs". You can't prove false if you can't prove anything.)
good point, I didn't think about these cases.