CompCert is a formally-verified C99 compiler.