How would you make machine defined the behaviour of, say, use after free, or data races?

Also compilers normally do not prove that programs hit UB, quite the contrary. Doing that statically is, in general, impossible.