Thank you for bringing this to my attention. If I am following along correctly, it does not so much verify the deployed EVM as it provides a formal and executab

Thank you for bringing this to my attention. If I am following along correctly, it does not so much verify the deployed EVM as it provides a formal and executable semantics for an EVM that satisfies the test suite, and the authors demonstrate its use in finding some real-world problems, which is exactly the sort of thing that we want: "These properties make KEVM an ideal formal reference implementation against which other implementations can be evaluated. We proceed to argue for a semantics-first formal verification approach for EVM contracts, and demonstrate its practicality by using KEVM to verify practically important properties over the arithmetic operation of an example smart contract and the correct operation of a token transfer function in a second contract." From the paper, it seems that the latter example could have found a bug that caused problems in a deployed Ethereum contract.