17 Aug
2009
17 Aug
'09
3:26 a.m.
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