(okay, so only a portion of the compiler is proven correct, and they didn't find any bugs in that portion).
Note also that a compiler with a proof isn't necessarily correct - it just means that you've pushed all your bugs into your description of the rules of C and of the target architecture. Since neither C nor any common CPU architecture have a formal semantics, someone has to read the (english) description and convert it to a description in their theorem proving software, and there's no reason to believe this will be easy.
One thing I missed the first time reading the paper is that those were the only bugs they could find in the compiler. After reporting them and getting fixes, several CPU-years more of random programs haven turned up another failure.
All the other compilers pick up tens of failing cases a night, which they skim off and report as their previously reported tests are fixed (the LLVM and GCC teams are quite responsive, others less so).
This kind of differential testing also provides some evidence that the formalization isn't too far off - each "passing" case means that almost all the compilers produced exactly the same results for the program.
Both projects are awesome, especially if you like reliable compilers.
(okay, so only a portion of the compiler is proven correct, and they didn't find any bugs in that portion).
Note also that a compiler with a proof isn't necessarily correct - it just means that you've pushed all your bugs into your description of the rules of C and of the target architecture. Since neither C nor any common CPU architecture have a formal semantics, someone has to read the (english) description and convert it to a description in their theorem proving software, and there's no reason to believe this will be easy.