Critical bugs are periodically found in Coq, and I assume in other proof assistants as well. We are still happy to mostly trust the proof assistants, partly because these critical bugs are relatively rare, but also because most of the time the bugs are obvious in the sense that it's hard to rely on them without noticing something is off. Or is it? Have there been "proofs" that were later discredited due to such critical bugs?
Related: this question about type-in-type, which does list some examples of the phenomenon I'm pointing at, although in that case people were knowingly working in an inconsistent setting.