So, any experience reports?<p>I can recommend <a href="https:&#x2F;&#x2F;www.imperialviolet.org&#x2F;2014&#x2F;09&#x2F;07&#x2F;provers.html" rel="nofollow">https:&#x2F;&#x2F;www.imperialviolet.org&#x2F;2014&#x2F;09&#x2F;07&#x2F;provers.html</a>.<p>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.)<p>Unfortunately, Frama-C did not grok malloc() at the time. My program consisted of I&#x2F;O into malloc()&#x27;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&#x27;t look forward to trying to model read()&#x2F;write() - so I stopped the experiment, and planned to revisit Frama-C in a couple years.<p>Actual experts can apparently get much better results: Frama-C was used to prove that chunks of PolarSSL were free of certain undefined behavior (<a href="http:&#x2F;&#x2F;blog.regehr.org&#x2F;archives&#x2F;1261" rel="nofollow">http:&#x2F;&#x2F;blog.regehr.org&#x2F;archives&#x2F;1261</a>, or the actual report at <a href="http:&#x2F;&#x2F;trust-in-soft.com&#x2F;polarSSL_demo.pdf" rel="nofollow">http:&#x2F;&#x2F;trust-in-soft.com&#x2F;polarSSL_demo.pdf</a>). This is a limited result: huge chunks of code are out-of-bounds. Also, &quot;PolarSSL is memory-safe&quot; is <i>very</i> far from &quot;PolarSSL is a secure SSL library&quot;. Still, I&#x27;m impressed.<p>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&#x27;s interactive mode, which is very powerful but doesn&#x27;t yield artifacts that can easily be reused. Also, mastering Frama-C is <i>hard</i> - it&#x27;s not something that you can just expect a software developer to pick up.<p>(In contrast, the Coverity static analysis tool uses unsound analysis and can&#x27;t guarantee anything. However, colleagues report that it does a decent job at finding <i>some</i> bugs with a low false-positive rate, especially after you add a few annotations. Coverity offers ongoing scans to open-source projects; unfortunately, Coverity&#x27;s scan servers appear to be backlogged at the moment. &quot;Not a need-to-have, but something we could consider buying.&quot;)