seL4 kernel is formally verified

John van V. john.van.v at
Mon Aug 17 04:34:27 CEST 2009

It would be really nice to create some plain-langauge text for the
general public so that it knows the significance of this L4 milestone.


On Sun, Aug 16, 2009 at 9:26 PM, Gernot Heiser<gernot at> wrote:
> 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
> Gernot
> _______________________________________________
> l4-hackers mailing list
> l4-hackers at




More information about the l4-hackers mailing list