That's both funny and true, but note that the same CompCert semantics is also the basis of a verified static analysis tool that can be used to prove the absence of such errors in C programs: http://compcert.inria.fr/verasco/

If you have a program that runs successfully through both the analyzer and the compiler, you can have quite a bit of confidence in the result.

It's just one part of the tooling, and doesn't solve program-correctness on its own. A formally verified toolchain is only really useful for projects which have pervasive mitigations against these kinds of errors. In other words, if you have a code base which has been verified to a high standard, you would also want a toolchain verified to a high standard.

In an ideal world you'd have a formally verified toolchain for a language without as many deficiencies as C, but here we are.

And that specified manner is 'Undefined'. Exactly to spec!

I know you're being facetious, but even if your compiler is verifying that your overflows are happening correctly, it is not a stretch to see that it can report that such overflows are occurring at all and what assumptions are causing them.