Actually, if you take a look at the semantic preservation theorems that CompCert actually proves, you can see that it allows for compilation to fail, even in optimization and code generation:<p><a href="http:&#x2F;&#x2F;compcert.inria.fr&#x2F;doc&#x2F;html&#x2F;Compiler.html" rel="nofollow">http:&#x2F;&#x2F;compcert.inria.fr&#x2F;doc&#x2F;html&#x2F;Compiler.html</a><p>As one particular example, register allocation is performed by an untrusted oracle that may not even terminate, and then verified a posteriori:<p><a href="http:&#x2F;&#x2F;compcert.inria.fr&#x2F;doc&#x2F;html&#x2F;Allocation.html" rel="nofollow">http:&#x2F;&#x2F;compcert.inria.fr&#x2F;doc&#x2F;html&#x2F;Allocation.html</a><p>They proved a traditional register allocator correct in a paper (<a href="https:&#x2F;&#x2F;www.cs.princeton.edu&#x2F;~appel&#x2F;papers&#x2F;regalloc.pdf" rel="nofollow">https:&#x2F;&#x2F;www.cs.princeton.edu&#x2F;~appel&#x2F;papers&#x2F;regalloc.pdf</a>), but I guess there are practical reasons why they are not using it in CompCert by default.