seL4 kernel is formally verified

Roman Beslik rabforum at
Mon Aug 17 13:48:45 CEST 2009

Are there any indications which properties of seL4 are verified?

Heiser said one of the primary research objectives was to come up with a 
kernel that would not only be verified but whose performance would be 
suitable for use in real-life systems.

“My briefing was that we must not *lose more than 10 per cent 
performance through the verification process*. Right from the start, 
this was not just an academic exercise but something that was for 
real-world use.”

I just can't understand how a verification process can undermine 

Gernot Heiser wrote:
> For an outsiders' view see this article:

More information about the l4-hackers mailing list