I think we're talking about two different things. Imagine you have a generic program A that you've formally verified. Now you ask me to execute it for you. I sa

I think we're talking about two different things. Imagine you have a generic program A that you've formally verified. Now you ask me to execute it for you. I say: "ok, the output of the program is X." Can you trust the output? No, you cannot trust the output even though you've formally verified the program. If you formally verify the smart contract, you can trust the output.