As the Ethereum ecosystem prepares for the Fusaka release, there has been debate about the merits of shipping the Ethereum Object Format (EOF) proposal. For the unfamiliar, EOF is a reimagining of smart contract deployment and execution; among other things, it separates code from data, introduces new transaction types, changes how external calls are made, and more. It is no exaggeration to say this change, if adopted, would be quite radical. Given the scope of the proposed changes, there has been perfectly justified scrutiny of the proposal. Unsurprisingly, there is a portion of the Ethereum community that opposes this change. One particularly outspoken critic is pcaversaccio, who wrote, with others, a long post outlining the argument against EOF.

It is important to stress first that the author and Certora do not take issue with many of the arguments raised by pcaversaccio and their co-authors, nor do we take any particular stance on the adoption of EOF. However, in discussing one of the changes in EOF, the removal of dynamic jumps, the post states:

"Furthermore, the value of statically analysable code to the EVM is questionable in and of itself. While it might simplify some off-chain tooling implementation, it doesn't enable new use cases. As mentioned previously, the impact of lacking statically resolvable jumps on off-chain tools is potential timeouts off-chain — infinitely preferable to deploying consensus bugs."

We strongly disagree with this claim. First, the value of statically analysable code has been repeatedly demonstrated. Certora’s Prover, which is itself a very sophisticated static analysis tool, has found and prevented countless bugs prior to deployment, the descriptions of which you can find on this blog and our published reports. The benefits of static analysis do not begin and end with Certora however; Trail of Bits has used their tool Slither to identify multiple issues in their security review process. Bytecode based tools, which include the Certora Prover, have to contend with the complexity and the sharp edges of EVM bytecode, one of which is the existence of dynamic jumps. Removing them, which the EOF proposal achieves, makes these tools more robust, easier to maintain, and easier to use.

Further, the claim that “it doesn’t enable new use cases” deserves scrutiny. The complexity of dealing with the full generality of EVM bytecode raises significant barriers to entry for the development of new static analysis tools. You can find the implementation of the Prover’s decompiler, which handles the dynamic jumps, here; at the time of writing, the file is close to 2 thousand lines long. While other static analyzers targeting bytecode may not need all of the features in our implementation, this demonstrates that constructing a static control-flow graph, one of the basic building blocks of any static analysis tool, is harder than it needs to be for the EVM tooling. Simpler control-flow mechanisms mean simpler decompilers, which makes it easier to develop the next generation of static analysis tools that prevent hacks before they are deployed.

Finally, it is important to remember that while the risk of consensus bugs should be treated with due gravity, it does not mean we should dismiss the “off-chain” benefits of the EOF proposals and others like it. Static analyses have a proven track record in preventing losses of millions of dollars; they deserve a seat at the table when considering these proposals and the future of the EVM.