Would you rather run a formally verified application on top of a conventional kernel/compiler toolchain, or a conventional application on verified kernel/compiler toolchain? Why?