It is not really a fork: all the necessary bugfixes to make the chosen PolarSSL version free of undefined behavior have been contributed back and either have been released or are pending release.
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.
Oh, that's great news! Unfortunately I'm on other projects now and likely won't have a chance to reevaluate in the short term, but I'd like to take a look at some point.
GnuTLS was not the most pleasant API to use, but it did hit some very impressive throughput numbers in our use cases, and seemed to deliver on the theoretical promised instructions/byte that Intel talks about in their whitepaper(s) about AES-GCM.
