[pirapira]

Using my definition of EVM, I think it's already possible to create a small verified compiler.

My priority is on keeping the formal definition in sync with the Yellow Paper and the implementations.

[Jabanga]

It's a surprise to see you here! :) Thanks for the explanation. Good luck with your work!