seL4 may give you a formally verified kernel. However, formal verification is a dark art with very few high priests that actually understand it on the planet. Unless it becomes commoditised, it's not going to be popular. There has been some work towards that but it's still high-priest land.
Unless a significant portion of the software that runs on top of that microkernel is also formally verified, there's always risk of many sorts.
Oh and don't forget the fact that the hardware itself is likely not formally verified so open to attack.
That's a very absolutist way of thinking and therefore not very practical I confess - but hey I was playing devil's advocate.
If the Sealed Rust initiative succeeds then we may have a general purpose formal provability story at the Rust-LLVM-IR boundary thanks to the RustBelt project. That, in theory, will open the door to provably correct kernels and full stacks which I think is the right way to attack the problem.