It's interesting that Frama-C was mentioned. I have been playing with it the last few months and would love to hear exactly how it was used. I've read through a lot of the documentation but haven't found many examples of it being used
Note that this is the initial stage of using Frama-C. The next step would probably include writing some specifications for functional behavior (in ACSL), and then using the WP plug-in (based on weakest precondition calculus) to prove those specifications, providing much stronger guarantees.
A few Frama-C case studies are on Github (https://github.com/Frama-C/open-source-case-studies), including an old release of Monocypher, but they constitute mostly a initial parametrization of the EVA plug-in. Most advanced users of Frama-C apply it on industrial code that is not available, but academic users regularly publish papers with case studies (searching "frama-c" on Google Scholar gives good results).
