The ERC777 standard is a new token standard, designed to be an alternative to the ERC20 standard, improving usability by giving account holders more control over token transactions, while keeping backward compatibility with ERC20. It defines an "operator" who can be thought of as a (trusted) third party to whom an infinite amount of "allowances" is approved to spend on behalf of the token owner. It also introduces the concept of a "hook", a callback function that is triggered when an operator performs a token transfer. The hook can either accept or reject the token transfer, allowing the token holders to have a finer-grained control of delegating the token transfer to operators. This hook can be also used to notify the token holders that they have received tokens, which is an important feature missed in ERC20.
Foreseeing the massive adoption of this new token standard by the community in the near future, we at Runtime Verification have specified ERC777-K, a mathematically rigorous formalization of ERC777, to facilitate formal verification of potential ERC777 token implementations. Specifically, it is a formal executable semantics of ERC777, being parameterized by the implementation-dependent behaviors to admit all standard-conforming implementations. In the process of the formalization, we made sure that all corner cases are thought through, explicitly covered, and thoroughly tested. We also discovered a number of ambiguities in the standard which we documented and delivered to the authors of ERC777. From here on, when we claim that we prove implementations of ERC777 tokens correct, we mean that they provably satisfy the rules of ERC777-K.