Re: seL4 kernel is formally verified

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