12

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?

tayvano
  • 15,961
  • 4
  • 45
  • 74
Nick Johnson
  • 8,144
  • 1
  • 28
  • 35

2 Answers2

10

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.

q9f
  • 32,913
  • 47
  • 156
  • 395
  • 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. – Nick Johnson Mar 29 '16 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 Mar 29 '16 at 16:44
  • @dbryson Yes - and again, it helps, but it's not a specification. – Nick Johnson Mar 29 '16 at 17:59
  • Yellowpaper is the only spec afaik. – q9f Mar 30 '16 at 05:49
  • @5chdn If you edit your answer to say as much, I'll gladly accept it (then gripe to myself about people who design systems but don't document them properly). – Nick Johnson Mar 30 '16 at 09:10
  • @NickJohnson The readability and level of formalism in a spec is somewhat subjective; since it's on github, feel free and anyone can submit pull requests to improve its readability :) – eth Mar 31 '16 at 06:28
  • 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. – Nick Johnson Mar 31 '16 at 18:27
1

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

Franck Cassez
  • 11
  • 2