mind that just because SeL4 micro-kernel is proven secure, there's no guarantee that all leyers on top of it are. There's a presentation (https://www.youtube.com/watch?v=LhUwwsVq5E4) that's pretty much about "so we gave sel4 to students, and NONE of them managed to build utilities on top safely - now we have to provide our own Core Platform implementation to be sure"

But most important of all, the highest level - human operators - are not provable secure anyway. Any castle gate can be opened from inside - so why have the gate anyway? Security by absence is absolute