seL4 kernel is formally verified

[Gernot Heiser]

Hi,

For those out there who missed the publicity (incl ./): NICTA
announced last week that the formal verification of our seL4 kernel
has been completed. This makes seL4 the first ever general-purpose OS
kernel with a formal proof that the implementation is consistent with
the specification.

A paper on the project will appear in this year's SOSP.

Details at http://ertos.nicta.com.au/news/home.pml#verified

Gernot