If I understand correctly, CompCert doesn't promise to compile correct programs correctly. Rather, it promises that if the compile succeeds, it's correct. This means it suffices to have (for example) a proved-correct check that a coloring register allocator allocated correctly, but that's allowed to abort if the coloring is incorrect. The register allocator itself need not be proved correct.
In practice, this is probably fine, since you won't run into bugs where the compiler aborts very often (and if you do, you know that you did.)
In practice, this is probably fine, since you won't run into bugs where the compiler aborts very often (and if you do, you know that you did.)