You could go further. There are a lot of bugs in provers like Coq themselves for which developers create their own proofs of correctness [1]. More precisely: th

You could go further. There are a lot of bugs in provers like Coq themselves for which developers create their own proofs of correctness [1]. More precisely: the paper which is linked implements a type checker for the core language of Coq which is proven correct in Coq. https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf https://www.irif.fr/~sozeau/research/publications/drafts/Coq...