seL4 kernel is formally verified

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