I gave an introductory talk to Red Hat about proving C code with Frama-C, which touched on CompCert. (Coq, Frama-C, CompCert and OCaml are all written by an overlapping set of the same people.) Note I'm very much a beginner here myself.

http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4