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.