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
