Yes. CompCert is a project of the French research institute in computer science and automation (INRIA). The goal is to have a certified compiler for the C programming language. I believe they're writing a C compiler in Coq (a proof assistant also developped mainly at INRIA).

The main guy behind CompCert is Xavier Leroy (already known for OCaml).

There's a list of papers published on his page:

  http://cristal.inria.fr/~xleroy/

I keep this link in a feel-good folder, next to Bellard's page. Sometimes I need a feel-good break after reading US-centric news.

Yeah, the big thing here is that almost all of this thing is proven, meaning that the compiler's behavior is well-defined and correct, all the time, on all inputs.

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.

What does it do about the undefined behaviour parts of the spec?

You can see the statement here: http://compcert.inria.fr/doc/html/Compiler.html#transf_c_pro...

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.

The frontend is not verified. This part parses, checks and lowers C code to a Clight. There is no formal specification of C itself and that would be the first step to verify the frontend.

It is a list of formally verified C compilers. At the moment, there's one.