I think the issue with such formal analysis tools is that in order to make the analysis succeed you often end up writing code that doesn't look like normal C an

I think the issue with such formal analysis tools is that in order to make the analysis succeed you often end up writing code that doesn't look like normal C anymore and arguably at that point you're not writing C anymore. --- As an aside, does CBMC check temporal memory safety and thread safety? It seems it checks for out-of-bound accesses, null pointer access and double-free, but I could not find a mention of use-after-free and data races.