Empirically, we can look at something like CompCert, which formally verified a substantial section of a C compiler. Subsequent high volume random testing with

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.