Hi,
I work on hevm, a symbolic execution framework for EVM with over 5k commits. What I can say is that EOF will significantly lower the burden of doing formal verification of contracts. And there’s some really good reasons why that’s important. Hacks are an issue. But so are bugs (e.g. funds accidentally locked in). All serious crypto systems do formal verification of their code, be that AAVE, Uniswap, etc. These are not small players, and I’m pretty sure some people on this very thread trust these systems with some serious money. If you want these, and similar systems to thrive, you need to make sure they can be formally verified. EOF helps with that in a big way. I don’t think I need to go into details of what’s wrong with no separation of code and data, and basically impossible-to-disentangle control flow graphs. But I will anyway. It’s hard. Sometimes very hard, and sometimes impossible without human help (which can not only be costly, and delay verification work, but can introduce errors). Now, of course, if you are willing to spend a few million USD, Certora will disentangle that for you, no worries. But… innovation in the application space will suffer for it due to the delay, uncertainty, and monetary barrier it introduces. Furthermore, it unnecessarily raises the barrier of entry for tools that perform formal verification of contracts – and it’s already a pretty high bar.
I can’t comment on many of the things that are said here, and I don’t want to – they are outside the scope of my expertise. What I am an expert in is formal verification (wrote a SAT solver, and a model counter that are quite widely used), and I worked a lot in the IT security space (at one point having written code that broke >60% of all car anti-theft systems on the road). Based on these experiences, my opinion is that (1) we need formal verification or bugs will slip through and (2) without EOF, formal verification of contracts is gonna keep on being harder than it needs to be.
Just my 2 cents,
Mate
PS: I am also in favour of (1) mature and (2) well-thought-through proposals that (3) solve the CFG & data/code separation issues that (4) have a serious chance of being accepted and implemented. As they say: “Scientists are treacherous allies on committees, for they are apt to change their minds in response to arguments”.