The Csmith paper notes two types of errors found in CompCert: front-end errors and a misunderstanding of PPC semantics.

The former type of bug was apparently due to a part of the compiler that wasn't verified at the time. According to the Csmith paper, " This bug and five others like it were in CompCert’s unverified front-end code. Partly in response to these bug reports, the main CompCert developer expanded the verified portion of CompCert to include C’s integer promotions and other tricky implicit casts."

Additionally, the CompCert team produced a validated parser which they discussed in their ESOP 2012 paper, "Validating LR(1) Parsers"

The second type of bug (misunderstanding the semantics of the target architecture) is, as far as I know, impossible to avoid. Any verification project can end up with a true proof of the wrong theorem!