[rurban]

This should be the major argument against GnuTSL and OpenSSL. PolarSSL is symbolically verified!

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.