Formal methods have no place in this, they are too hard or expensive!

Phil has without permission quoted Gernot but I think its good one, apologies to Gernot:

"You go first. Part of the argument is that once seL4 is verified, there’s no more cost, it’s open-source. And for higher layers you need less effort because you can leverage seL4’s proved isolation. -- Gernot

"Phils quote will follow, lets await it" -- Phil