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.
Source: I have worked at NICTA, with the seL4 team, on the seL4 project, I've seen the seL4 source code and am (was?) a primary author of the user manual.
These claims have been peer reviewed in top formal methods and operating systems journals/conferences and have won some very awards doing so.
In short some very smart, and very qualified people can vouch for them.
It will be interesting to see once it becomes open source.
My favorite story relating to that is john regher compiler testing effort found a bunch of bugs in a research compiler that was proved to be correct.
[Edit]
Not strictly true. As John noted in comment below:
John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.
actually that story is the opposite of true. John Regher and CSmith fuzzed CompCert and they found no bugs. from the csmith PLDI paper:
"The striking thing about our CompCert results is that the middleend bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task."
John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.
From the paper "Comprehensive formal verification of an OS microkernel":
"We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware"
To be fair. Every operating system assumes these things. At least the seL4 team has made this explicit. Secondly, there is a tiny amount of this code amounting to a few hundred lines of assembly and there are numerous verified hardware projects underway. Furthermore, as time has gone by, many of the original assumptions have been whittled away. This is by far the most robust operating system ever written.
Sure, I agree. There is indeed some work being done in making some of those parts more trustworthy. That being said, it will probably be sometime before that technology is usable by the average person. I'm really interested in seeing what they release.
Has any smart person looked at their claims enough to vouch for them?