Breakthrough software testing technology hailed by a Cambridge University expert as a tool able to deliver "currently unimaginable standards of reliability" to software has been unveiled by NICTA chief executive officer Dr David Skellern. [...] researchers last week completed the world's first formal machine-checked proof of a general purpose operating system. In short the technology is a way for developers to test that the software they have designed works the way it is expected to, before it is put into production. According to Dr Skellern, NICTA's formal verification research team has completed the world's first mathematical proof of a general purpose operating system kernel. The Secure Embedded L4 (seL4) microkernel is being initially targeted at applications in defence and safety-critical sectors.
Is it finally time to switch our desktops to microkernels in order to get bug-free OSs?"