seL4 kernel is formally verified

Nicholas Mc Guire mcguire at
Mon Aug 17 11:43:40 CEST 2009

On Mon, 17 Aug 2009, Gernot Heiser 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

This linke might help:

for some general comments (including this project) on complex software
and safety related verification - I would like to point you to from Peter Bernard Ladkin as he raises
some interesting questions related to this work.

What did supprise me a bit is that: 

 7500 LoC yield 200k Lines of formal proof
 7500 LoC yield "more than 10k intermediate theorems

I wonder how scalable such an approach is... And of course raising (from a 
safety perspective) the question if the complexity and potential failures of
7.5k of Code were not replaced by a even higher complexity (of course its
a diverse representation - which takes out a lot of this imediately) - the
main concern I would have is that while this initial core might be very
reliable (see concerns raised at it
is a question of how changes to such a system can be handled and how the
interaction of the application/drivers can be handled in such a system. The
isolation of the core (microkernel) is not the issue (provided the full range
of the interface is covered in the formal proof) - but how far does that
actually help with respect to the actual safety related code, which is in
a user-space task/driver ? 

Neve the less this is a really impressive stunt - and I do hope more will be made available on the verification of this project !


More information about the l4-hackers mailing list