We are very happy to share a report from the recipients of our first grant, the Kestrel Institute; the grant of $3,000 was for “Ethereum Yellow Paper Improvements.” Kestrel is known for (among other projects) their work on formal specification and implementation of a full Ethereum client using the ACL2 theorem prover and APT toolkit. In the course of this client development and related work, they found a few ways in which the Ethereum Yellow Paper could be improved, which was the focus of our small grant to them. Alessandro Coglio and Eric McCarthy implemented the changes and also wrote the report below summarizing how the grant was used.

Ethereum Yellow Paper Improvements, Kestrel Institute
Final Report, 2019-05-31
by Alessandro Coglio and Eric McCarthy

What is the Yellow Paper, and how is it related to Decentralization?

The Yellow Paper (YP) is the primary specification for the Ethereum blockchain. Ethereum is the most widely used blockchain smart contract platform, and therefore it is the most widely used platform for decentralized applications. Improving the security of Ethereum is important for all applications running on the platform. Improving the precision and clarity of the YP can help implementors of Ethereum avoid bugs, so improvements to the YP are contributions to the security of Ethereum and therefore to the security of many decentralized applications.

Work done under this grant

Prior to this grant, we were working on formalizing Ethereum in the ACL2 theorem prover. The Yellow Paper (YP) is the primary specification for Ethereum, so it was our primary reference. As a specification, it should be precise and understandable by someone who recognizes notations used by mathematics and logic. Whenever we found issues with the YP, we recorded the issues and our proposed solutions.

On this grant, we worked though a large part of our list of problems with the YP. This included things that seemed wrong, inconsistent, underspecified, or unclear when we attempted to formalize the YP. We studied each issue and proposed suggested improvements. We reached consensus within Kestrel and then created pull requests and participated in subsequent community discussions on Github to reach consensus with the community, in some cases modifying the suggested changes accordingly. In some cases, we studied implementations. When community consensus was reached, we pushed our changes, thus improving the YP for all current and future users.

We made the following changes to the Yellow Paper (YP) under this grant. This list does not include pull requests done prior to the start of this grant. The changes vary in complexity and importance.

The most interesting change from a technical point of view is:

However, the cleanup tasks are also important, since they affect the general understandability (and sometimes the correctness) of the YP. Here are the other commits we did under this grant:

We also cleaned up some older, related issues and pull requests by adding explanatory comments, some of which were subsequently closed. From a technical point of view, these can be quite interesting:

We added this issue, which has not yet been resolved:

Note, we did a variety of adjunct work without charging to the grant, such as recording and discussing our proposed changes and discussions and meetings about maintainership.

Discussion

Our experience attempting to improve the Yellow Paper

When we started working on the Yellow Paper, we thought it would be reasonably straightforward to submit pull requests with our proposed improvements. However, after Yoichi Hirai departed, his role as an active maintainer of the YP was not specifically reassigned to anyone else at the Ethereum Foundation.

We would like to thank Nick Savers for stepping in to maintain the YP and to review and merge and approve many pull requests, Kenneth Ng for connecting us with Jamie Pitts, and Jamie Pitts for attempting to build a Yellow Paper community. Jamie started the Ethereum Specification mailing list (specification@ethereum.org). Jamie also set up a Doodle signup for an Ethereum Specification group call, but the only people who signed up were from Kestrel Institute: Alessandro Coglio and Eric McCarthy, and the call never happened. Then Jamie gave us push access to the Yellow Paper Github repo, so we are part of a small group of YP maintainers.

More Information about the Yellow Paper

There seem to be many people who find the YP valuable, and many who do not. There are people who want the YP to be “The Canonical Ethereum Specification”, those who want a machine-readable canonical specification (such as expanding the Jello (K-framework) specification to cover more than the EVM), and those who think it is fine not to designate any specification as “canonical” and who support a diversity of specifications. Rather than take any sides in these discussions, we mainly focused on improving what we find useful: the Yellow Paper.

Currently, the main forums for discussing the Yellow Paper are:

In Conclusion

On this grant we accomplished our goal to improve the YP in quite a few ways. Also, this project has been helpful for us to become better integrated contributors to the Ethereum Ecosystem. We have met others in the intersection of Ethereum and Formal Methods. We continue to see ways the Yellow Paper can be improved, and we hope to continue contributing to the YP in the future. We thank the Decentralization Foundation for helping us get to this point.