Note that fuzzing CompCert has still found bugs in it - because the entire compiler actually isn't verified. They've extended the proof over time.
(Note that "formally verified" still does not mean "bug free", it just means it's a refinement of a proof that is also a program which can have bugs in it. And "formally" sounds like a weasel word.)
Yeah, there were some bugs in the frontend and I think one in the backend. But there were zero bugs in the optimization pipeline, which is where typically the most subtle bucks lurk.
(Note that "formally verified" still does not mean "bug free", it just means it's a refinement of a proof that is also a program which can have bugs in it. And "formally" sounds like a weasel word.)