Comment by pfdietz

Empirically, we can look at something like CompCert, which formally verified a substantial section of a C compiler.

Subsequent high volume random testing with Csmith found no bugs in the formally verified section (unlike in every other C compiler tested with Csmith).

It should be noted that the verification performed was specifically about whether the compiler would produce incorrect code; cases where it would crash or error and not produce code would not be considered errors of verification. This would enable (for example) a coloring register allocator to be adjoined with some code that checked whether the coloring was correct and abort if not.