I don't understand why this is even a problem. If current models can formally verify vast amounts of software, couldn’t you use it to build a sandbox with formally verified guarantees against leaks?