So, if I understand correctly, this appears to be a 'man in the middle' vulnerability where you need to actually have control of a node somewhere between the user and the server.
Not nearly as easy to take advantage of as the Heartbleed vulnerability, but serious never the less the less.
It's interesting that the bug was found using the Coq proof assistant. Hopefully this vulnerability brings attention to the usefulness of theorem-provers like Coq for finding these sorts of bugs.