Formal verification of protocols like TLS is essentially the research thesis behind this group at INRIA, which was also responsible for Logjam (as well as the paper you linked to).
Oh yeah, they're kicking ass on every front of this sub-field. Then, Leroy et al are doing that for compilers and language analysis at INRIA as well. Then Astree is leading it for static analysis of C.
France, esp INRIA, seems to be in the lead on verified software with a real-world focus. It will be great when more elsewhere follow suit.
Oh yeah, Galois is another one of the greats in the field. They just keep cranking out one practical thing after another. At a higher pace than most it seems. Here are a few good things on their end.
