First machine-checked OS kernel

[Mattias Holm]

Kagamin wrote:
> NICTA announced the completion of the world’s first formal machine-checked proof of a general-purpose operating system kernel, promising safety-critical software of unprecedented levels of reliability.

Yes, sort of what they proved was that the implementation was inline 
with the specification. The spec may still have bugs though. Also, they 
proved this for a very limited microkernel (not a general purpose OS), 
so they now know only that the message passing, task handling and some 
other minor parts work as specified, they still have no idea about the 
disk drivers or anything outside the micro kernel.

For the amount of work they put into it, you would have been able to 
write tests for everything and conducted code reviews to reach a 99.9% 
confidence in the system for a small fraction of the cost. I still find 
that their work is incredibly impressive, and will be very appreciated 
with many software communities, especially the defense community.

/Matt