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.