It is well known that proof assistants can be wrong. Fortunately, the theories underlying formal methods are usually simple enough that it is feasible to write verifiers for these proofs.

The UB goes all the way down!