I have followed the Dafny language from a distance since the beginning. The Ironclad project I am just discovering, but it is everything I would expect from Mic

I have followed the Dafny language from a distance since the beginning. The Ironclad project I am just discovering, but it is everything I would expect from Microsoft: a willingness to give formal methods a chance at real use and to get valuable feedback. The sad truth of from-scratch formal methods is that only Microsoft-like companies can afford to give them a try. And so far, of the Microsoft-like companies, only Microsoft is doing so. Regarding the verification of PolarSSL, you may find it useful to see what the entire report looks like concretely, even if it is for a now obsolete version of PolarSSL, so here: http://trust-in-soft.com/polarSSL_demo.pdf http://trust-in-soft.com/polarSSL_demo.pdf We have improved the methodology somewhat since that report was made, but it does give a prospective customer an idea of what they can expect for a recent branch of PolarSSL and for a usage of the library that we have agreed on before elaborating the report. TrustInSoft is going to announce the availability of this demo report this week; consider this a sneak preview.