Ah, I see what you mean. The fork would break the execution model/reality equivalence and thus (possibly) invalidate the verified properties. It could also modi

Ah, I see what you mean. The fork would break the execution model/reality equivalence and thus (possibly) invalidate the verified properties. It could also modify the Solidity code itself, as in the DAO fork. Formal verification still provides benefit here: the proposed changes are easy to check for backwards-compatibility breakage prior to the fork, providing a valuable political tool to either oppose the change or require a rider contract code fix in the fork. I do think your requirement of universal correctness is unfair. We can rightfully criticize the naivete or misleading marketing of Ethereum, but the system isn't valueless despite its limitations, and formal verification enables us to capture more of that value.