Also check out the PolarSSL Verification Kit[1], a FRAMA-C verified version of PolarSSL.
You can see some screenshots at http://blog.frama-c.com/ but unfortunately their frama-c annotations for polarssl are not open source. It would help a lot if such annotations could be used for similar crypto APIs also.
There are many more such symbolic verifiers and bugfinders out there (using solvers), but Frama-C was one the first and is still one of the best.
Another possibility is that the person who found the memory corruption was not using PolarSSL in the same configuration as the one described in the verification kit. PolarSSL allows to select sub-components at compile-time, and to select between implementation options within these components. Finally, there is always the possibility that a bug remains for compilation parameters other than the ones the verification was configured for. If I did not do too bad a job, this comment should make it clear what kind of differences could explain a bug remaining: https://news.ycombinator.com/item?id=7573483
There is always the possibility of a bug in Frama-C having for consequence a bug in PolarSSL not being found. This is far less likely than the previous commenter referring to a version that was not verified.
Yes, Privacy Enhanced Mail is not part of the verified PolarSSL configuration. And the bug at https://github.com/polarssl/polarssl/issues/83 is definitely the sort of bug Frama-C would “not shut up” about, as Regehr puts it. The warning will only occur where the buffer overflow eventually happens, and it may be more or less pleasant to go back from the site of the buffer overflow to the bug in the fashion of http://blog.frama-c.com/index.php?post/2014/02/23/CVE-2013-5... , but Frama-C's value analysis is designed to reliably find this bug and not shut up about it.
It is more a choice of version, choice of compilation platform (some bugs only occur with 64-bit pointers or unsigned chars —the verification in question has been done with 32-bit pointers and signed chars, no guarantee is given for other parameters) and description of a library configuration.
The PolarSSL Verification Kit takes the form of a 8-page description of the above parameters and a 100-page technical annex with all the formal specifications and justifications. You only need to read the second part if you don't trust the kit's authors. Like similar documents are, the technical annex is intended to be audited by picking a piece at random and checking the reasoning locally and how it relates to the other pieces.