John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.