A formal verification tool for Ethereum VM bytecode
In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K framework's reachability logic theorem prover to generate a correct by construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts.
ESEC/SIGSOFT FSE