An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.