So, any experience reports? I can recommend https://www.imperialviolet.org/2014/09/07/provers.html https://www.imperialviolet.org/2014/09/07/provers.html. Per

So, any experience reports? I can recommend https://www.imperialviolet.org/2014/09/07/provers.html https://www.imperialviolet.org/2014/09/07/provers.html. Personally, I tried to prove that a fairly simple program I had written a few years prior was free of undefined behavior. Frama-C was tantalizingly capable - it was easy to tell Frama-C what I wanted to prove, and it managed to propagate possible values and control flow through the program pretty accurately, even with minimal assistance. Although I disliked the absence of a usable text-mode integration (vim?), the GUI presented the results clearly. The Frama-C manuals were extensive, mostly up-to-date, and managed to explain even complicated concepts in a pretty clear way. (Fair warning: although I have zero background in formal methods, I have quite a lot of mathematical training and like language lawyering.) Unfortunately, Frama-C did not grok malloc() at the time. My program consisted of I/O into malloc()'ed buffers plus some processing. Teaching Frama-C about malloc() was clearly beyond my skill. Worse, I really wanted to prove that my program output was some suitably processed form of its input data, and I didn't look forward to trying to model read()/write() - so I stopped the experiment, and planned to revisit Frama-C in a couple years. Actual experts can apparently get much better results: Frama-C was used to prove that chunks of PolarSSL were free of certain undefined behavior (http://blog.regehr.org/archives/1261 http://blog.regehr.org/archives/1261, or the actual report at http://trust-in-soft.com/polarSSL_demo.pdf http://trust-in-soft.com/polarSSL_demo.pdf). This is a limited result: huge chunks of code are out-of-bounds. Also, "PolarSSL is memory-safe" is very far from "PolarSSL is a secure SSL library". Still, I'm impressed. I did not see a good way to integrate Frama-C in our development process. From reading and talking to some people, I am left with the distinct impression that keeping proofs up-to-date in living software is not a solved problem. Frama-C does allow you to annotate code with assertions (which, I expect, can act as hints to the provers). However, the workflow still seems to be oriented around Frama-C's interactive mode, which is very powerful but doesn't yield artifacts that can easily be reused. Also, mastering Frama-C is hard - it's not something that you can just expect a software developer to pick up. (In contrast, the Coverity static analysis tool uses unsound analysis and can't guarantee anything. However, colleagues report that it does a decent job at finding some bugs with a low false-positive rate, especially after you add a few annotations. Coverity offers ongoing scans to open-source projects; unfortunately, Coverity's scan servers appear to be backlogged at the moment. "Not a need-to-have, but something we could consider buying.")