So whilst we haven't seen the proof, nor the code, will do have a good idea of what they've done and how they've done it.
Formal verification has been much researched, and its nice to see actual real systems starting to be checked by them. Just the other day I was reading about people doing TLS implementation verification using Coq.
They have published details of their formal verification on ACM http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A...
They use Isabelle.
So whilst we haven't seen the proof, nor the code, will do have a good idea of what they've done and how they've done it.
Formal verification has been much researched, and its nice to see actual real systems starting to be checked by them. Just the other day I was reading about people doing TLS implementation verification using Coq.