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.<p>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.<p>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: <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><p>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.