ERC20-K: Formal Executable Specification of ERC20

ERC20
The ERC20 standard is one of the most important standards for the implementation of tokens within Ethereum smart contracts. ERC20 provides basic functionality to transfer tokens and to be approved so they can be spent by another on-chain third party. Unfortunately, ERC20 leaves several corner cases unspecified, which makes it less than ideal to use in the formal verification of token implementations. Indeed, we at RV, Inc., have been asked to verify smart contracts for ERC20 compliance. However, we found that it is unclear what ERC20 compliance means, because the existing presentations of ERC20 are far from serving as mathematical models of the standard token. Consequently, we decided to create ERC20-K, a mathematically rigorous formalization of ERC20, making sure that all corner cases are thought through, explicitly covered, and thoroughly tested. From here on, when we claim that we prove implementations of ERC20 tokens correct, we mean that they provably satisfy the 13 rules of ERC20-K.

Continue reading