My understanding is that sanitizers are generally not designed to be deployed in production software, they're written with catching problems in testing in mind

My understanding is that sanitizers are generally not designed to be deployed in production software, they're written with catching problems in testing in mind (i.e. calling them an implementation of C seems dubious to me), and have problems resulting from that[0]. That said, I'd guess this is changing given how tempting it is to use these tools as a hardening mechanism. Also, unless you're talking specifically about CompCert's interpreter, I don't think CompCert does what you think it does. The compiler is a verified implementation of the standard, but that, by definition, doesn't say anything about how it handles undefined behaviour. [0]: http://seclists.org/oss-sec/2016/q1/363 http://seclists.org/oss-sec/2016/q1/363