There's a whole segment of CompSci dedicated to doing that. Softbound+CETS and SAFEbound are two of the better examples giving C memory safety. Data Flow Integr

There's a whole segment of CompSci dedicated to doing that. Softbound+CETS and SAFEbound are two of the better examples giving C memory safety. Data Flow Integrity is a newer one thst might be combined to bring security against data-oriented attacks. The big issue with such tools is that C's lack of design and low-level nature make the tools have to be extra careful in ways that add extra overhead vs languages designed for verification (eg Gypsy, SPARK Ada). So, the slowdowns can be huge. I still like them, though, given any approach that works turns the problem from "recode critical, legacy apps securely" to "buy a load balancer and some more servers." Huge improvement in feasibility. Far as proving absence, RVI's RV-Match can do that against a full (or nearly so) semantics of C in K Framework. Their semantics, KCC, is mocked up like a GCC compiler to make it easy to try with code. It also gets stuck (fail-safe) on undefined behavior.