[mansr]

There are two fundamental problems with CompCert: 1) there is no formal, machine-readable specification of the C language, and 2) there is no formal, machine-readable specification of the target architectures. CompCert may be formally verified, but it's not necessarily a C compiler (even ignoring that it implements only a subset of C), nor does it necessarily compile for the advertised architecture.

[qznc]

Addressing number 1) https://code.google.com/p/c-semantics/

Not perfect, but pretty good.