Proof assistants are not magically bug-free. As others have said, an exhaustive model checker failing to find a counterexample is a proof. That you trust proof

Proof assistants are not magically bug-free. As others have said, an exhaustive model checker failing to find a counterexample is a proof. That you trust proofs more because you haven't yet seen a bug in a proof assistant speaks only to your personal experience, not to any logical truism. (That said, most models are not finite, and thus cannot be exhaustively checked. This is where proof systems do have a leg up. But that has nothing to do with bugs or representation of the system under test.)