Proof assistants based on type theory, such as Agda, Coq, Idris and Lean, are widely used to establish the correctness of programs. Conceptually, such proof assistants – where the logic and programming language coincide – should reduce the trusted code base. In practice, however, verified programs can – and do – go wrong. In this talk, I’ll try to sketch various ways in which verified programs can still fail and what we might do to prevent them from doing so.