FWIW, formal verification requires a complete and exact spec - the TZ kernel is very complex and interacts with nearly all the peripherals on the SoC, it doesn't just manage QSEE applications. I think creating a spec for something like that would be really hard.
The whole point of using seL4 is that you can use it to provide guaranteed isolation. If you were to use seL4 it would be so that you could write those drivers in user mode and so that a bug in one would not let you extract crypto keys in another.
