Most (all?) proof assistants have soundness bugs fixed on occasion. However, from those I've seen these bugs are usually difficult to come across unintentionally, and results proved before the bug is fixed generally hold up after the fix.
Three questions, in order of strength:
- Has such a soundness bug fix ever caused a major proof to fail, without modifying the proof?
- If (1) is true, were major modifications ever required to fix the proof?
- If (2) is true, has anyone proved a wrong major theorem due to a soundness bug?
I'll leave the definition of "major" up to others.