I'm confused. The title made me think "list of compilers I can trust", but the website provides no such thing. It looks to me like they've written their own compiler.
The main guy behind CompCert is Xavier Leroy (already known for OCaml).
I still had a jaw-drop moment the first time I heard about this; Coq is not a pleasant language, and proving this thing must have been a nightmare.
A C compiler doesn't have to promise much of anything about the behavior of the code produced for a program with undefined behavior.
This statement could be vacuous for a program p with undefined behavior if (Cstrategy.exec_program p beh) isn't true for any behavior beh, or only true for a behavior which makes (not_wrong beh) false.
If they don't always, then they actually give you a guarantee for some bad programs as well. Nothing in the spec says running a bad program has to make demons fly out your nose.
http://cristal.inria.fr/~xleroy/