The work you have been doing on polarssl is pretty inspiring. I use it as a success story for formal methods and PL technology when I do &quot;science of security&quot; classes or briefings.<p>Someday, I would love to do a research project on using tools like yours to prove higher level properties of programs, much like what the Ironclad&#x2F;Dafny teams have done. Their approach is good when you have a formal spec and can write from scratch, your approach is good when you already have the code and can create a spec post-hoc, I think. Have you followed their work?