I used to work for a large defence company. They paid for "certified" ADA compilers for PPC architecture. They had as many (if not more) bugs. Not only that, they built their stuff on FPGAs which had even buggier compilers than the compilers for the software.
Certified compilers are protected only by maintenance agreements.
When a piece of software is verified with an Agda proof, that is generally a real proof. The proof may not cover all aspects, but in those aspects you really do not have bugs.
Perhaps you mean non-proven certification? Or a weak certification of too few aspects?
I think it was probably a weak certification in this case. They paid for core concerns to be covered, not necessarily the entire toolchain (which TBH is where the problems were - X working with Y properly). In fact I think it was that linker that fluffed stuff. I should modify my comment really.
Historically, compiler certification is a bad joke. It amounts to concerted testing at best, and wishful thinking in most cases. Few (remotely useful) compilers have been verified in any mathematical sense, and even then there is generally a wide gulf between what is proved and what we would intuitively expect a truly correct compiler to do.
Certified compilers are protected only by maintenance agreements.