The yellowpaper specifies the EVM, albeit in a fashion that favors formalism over readability:

enter image description here

But there's no indication if this is up to date with the current state of the Ethereum ecosystem or not, and I haven't been able to find a formal VM specification anywhere else. Is there one?

2 Answers 2


The yellow paper is up-to-date and the only technical specification I know of. Below the headline, it says Homestead Draft which refers to the most recent homestead release on March 14, 2016.

homestead draft

I just checked some formulas today and noticed they moved up in numbering, so you can consider this specification is always updated with the latest design changes.

You can track the progress on github by the way.

  • Thanks. That answers the "is it up to date" question (though not in a particularly discoverable way), but not the "is there a separate spec" one. Having read the appendix concerned with the VM, it's really not a very helpful format for anyone who wants to actually implement the VM; the author seems to love formalisms over readability. Commented Mar 29, 2016 at 16:29
  • Have you looked at the open-source implementations of the VM? For example pyetherem or ethereumjs-vm? Studying that code should provide more than enough information to implement your own VM
    – dbryson
    Commented Mar 29, 2016 at 16:44
  • @dbryson Yes - and again, it helps, but it's not a specification. Commented Mar 29, 2016 at 17:59
  • Yellowpaper is the only spec afaik.
    – q9f
    Commented Mar 30, 2016 at 5:49
  • 1
    @eth Unfortunately, I don't think a more readable style is possible without rewriting the whole paper. IMO, the issue is a reliance on mathematical notation (single letter greek variables, etc), when an RFC-style spec would be far more useful to implementers. Commented Mar 31, 2016 at 18:27

This is an old thread, but probably worth mentioning that there is a formal and executable semantics of the EVM written using the verification-friendly language Dafny.

The public GitHub repo is here. And there is a companion conference paper:

[1] Cassez, F., Fuller, J., Ghale, M.K., Pearce, D.J., Quiles, H.M.A. (2023). Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In: Chechik, M., Katoen, JP., Leucker, M. (eds) Formal Methods. FM 2023. Lecture Notes in Computer Science, vol 14000. Springer, Cham. DOI

also available on ArXiv

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.