CompCert is a verified compiler – as in the compiler itself won't silently miscompile your code. It has nothing to do with verifying your C code. For that, othe

CompCert is a verified compiler – as in the compiler itself won't silently miscompile your code. It has nothing to do with verifying your C code. For that, other tools can be used (e.g. Frama-C Wp). One verified TLS implementation is miTLS, written in F*.