What's actually happening is a bit more subtle: The compiler is allowed to assume that the programmer in fact made no mistake and there's a reason why the UB is never actually triggered at runtime. Reasoning backwards from that can open up large optimization opportunities elsewhere, like not loading a value from memory twice, or not actually checking a condition. A good article about this that was recently discussed on HN: https://news.ycombinator.com/item?id=18575383

What they do is not try to prove UB, but use it as a precondition for the proof that their optimizations don't change the program behavior - ie. they can assume that anything resulting in UB won't happen.

> Do compilers really try to prove UB so they can use it as an excuse to silently murder kittens?

Clang in particular is quite aggressive about this, and is prone to producing surprising results. GCC has started doing this too, but it is much more conservative,