"The L4.verified project A Formally Correct Operating System Kernel L4.verified The University of New South Wales Function calls in the seL4 kernel [What's this?] In current software practice it is widely accepted that software will always have problems and that we will just have to live with the fact that it may crash at the worst possible moment: You might be on a deadline. Or, much scarier, you might be on a plane and there's a problem with the board computer. Now think what we constantly want from software: more features, better performance, cheaper prices. And we want it everywhere: in mobile phones, cars, planes, critical infrastructure, defense systems. What do we get? Mobile phones that can be hacked by SMS. Cars that have more software problems than mechanical ones. Planes where computer problems have lead to serious incidents. Computer viruses spreading through critical infrastructure control systems and defense systems. And we think "See, it happens to everybody." " Full text in url below http://ertos.org/research/l4.verified/ One of their papers from wilipedia's citations http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf Now, can all these above mentioned problems disappear with seL4 microkernel? Thanks.