> Constructing a ZKP of the same is certainly more cost intensive. That is certainly true for the compilation phase (i.e. constructing the ZKP). But for the ve

> Constructing a ZKP of the same is certainly more cost intensive. That is certainly true for the compilation phase (i.e. constructing the ZKP). But for the verifier, that isn't so obviously true: - Firstly, the verifier might not even have access to the formal proof that the program meets the memory correctness guarantees. It might have access to a binary code, plus a proof that the binary code compiled from a completely memory safe language. The verifier would need zero knowledge of the code (which might be proprietary). - Secondly, proofs aren't necessarily that big (especially for Groth16 circuits), and can be applied recursively (you prove that you had a proof that something was true), and aren't that expensive to verify. If verifying a program once when you download it means it can be flagged as being safe to run without expensive bounds and MMU checks, it could open up new types of more performant CPUs, and potentially save far more than it costs to verify.