seL4 kernel is formally verified

Gernot Heiser gernot at
Mon Aug 17 03:26:07 CEST 2009


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


More information about the l4-hackers mailing list