[lmm]

Maybe. But when carefully investigated, the overwhelming majority of C code does in fact use undefined behaviour, and there is no practical way to verify that any given code doesn't.

[uecker]

It is easy to create code where this can be verified. It is difficult to verify for arbitrary code.