[skew]

Do you mean "seL4 is great"? I agree it won't do much for application-level security without adding some formally verified code on top (perhaps as simple as setting up isolation between VMs), but it looks great if you do want to use formal methods. For the simplest thing, just starting out with a formal semantics of the OS and reason to trust that semantics would save a lot of work (of course, a lot may remain).

[tptacek]

Honestly, I don't much care about the formal verification of L4; it's the L4 design and implementation strategy that I find compelling.