seL4 kernel is formally verified

[Roman Beslik]

Hi.
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 
performance.

Gernot Heiser wrote:
> For an outsiders' view see this article:
>
> http://www.computerworld.com.au/article/314817/nicta_wins_race_secure_l4