seL4 kernel is formally verified
rabforum at ukr.net
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
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