I think in most cases the compilers already warn, if they detect a definitive signed overflow, instead of just silently creating a nonsensical program. And in the cases, where overflows can sometimes happen, you have wrong, but (kind of) defined behavior (with modulo/wrap-around, etc.). Perhaps the tooling has to go into a direction to automatically suggest function pre-conditions and/or tests to make sure that signed overflow does not happen. With contracts pre-conditions (and perhaps at some time class invariants) can be specified in a language a machine can parse and often deduce further correctness of functions.