JelloPaper: Human Readable Semantics of EVM in K

The Jello Paper is an attempt at defining the EVM semantics using the KEVM project. Unlike the Yellow Paper, the Jello Paper is an executable semantics, and can provide a full EVM interpreter usable for testing contracts, analyzing gas usage, verifying contracts correct, and a wide range of other tasks as specified in the technical report on KEVM.

The KEVM semantics described by the Jello Paper is the first machine-executable, mathematically formal, human readable, and complete semantics of the EVM. KEVM is capable of passing the full EVM VMTests and GeneralStateTests testing suites, and can also be used in smart contract formal verification, debugging, and more. The Jello Paper (this document) is automatically generated from the K definition of the KEVM semantics.

Start by choosing any section below or in the sidebar.

Indices and tables