Machine code is insecure, we should all run interpreted code in a formally verified interpreter.
Alternatively, only allow for the execution of cryptographly signed static linked binaries, this naturally includes the interpreter above.
If we are sprinkling formal verification on things, we can sprinkle it on a JIT.
If we are sprinkling formal verification on things, we can sprinkle it on a JIT.