"The proof assumptions mean that there may be faults remaining in the kernel that could be classified as implementation faults below the level of C. They will n

"The proof assumptions mean that there may be faults remaining in the kernel that could be classified as implementation faults below the level of C. They will not be faults that are properly visible on the level of the C programming language (which is our main claim of correctness), but they could still be serious faults that make the seL4 kernel misbehave." -- http://ertos.nicta.com.au/research/l4.verified/proof.pml http://ertos.nicta.com.au/research/l4.verified/proof.pml This just seems to be a case of someone running their mouth a bit too liberally and Hindustan Time jumping the gun. The actual project, which unfortunately is quite proprietary, has a much better overview of the whole ordeal. I would however like to se how their 1:1 strict C/haskell conversion actually looks (and why they decided against just modifying the something like the ghc :P). You were right in not trusting the paper.