"Q. How did you find this bug?
A. This bug was discovered by Masashi Kikuchi of Lepidum. He found this bug while studying safe TLS implementations using a proof assistant system Coq."
So they are starting to find actual bugs with Coq? I'm impressed, and would love to know if anybody has more details (lepidum's blog seems down at the moment).