[sanxiyn]

Yes, but large part of Coq is designed to be untrusted. Roughly, Coq searches proof and checks found proof. Search part is larger, it can be incorrect, can have bugs, etc. without affecting the proof. Check part is trusted, and is available as a separate binary (coqchk), which consumes proof found by search (coqc).

For CompCert, the more worrying is the correctness of "extraction". This is somewhat technical, you should be able to search if you are curious. CakeML solves extraction problem.

For HOL, Proof Technologies Ltd developed HOL Zero, which is solely dedicated to trustworthiness without bells and whistles. Bells and whistles are absolutely necessary for proof development. The idea is to use HOL Zero at the end, after proof is finished. It's like coqchk idea on steroid. http://proof-technologies.com/holzero/

Summary: CompCert trusts coqchk and extraction. CakeML trusts HOL, hopefully something like HOL Zero can be used in the future.