The Coq compiler is unverified, it is written in OCaml.

It's not possible for Coq's consistency to be verified in itself, thanks to Gödel's second incompleteness theorem. However there are still various other aspects of the compiler that could be verified in principle. The CertiCoq project is actively going in that direction.

I love this comment, because there is this pie in the sky mathematical idea, with direct consequences for practical coding.