How Formal Verification Could Help to Prevent Gridlock Bug

Yet another smart contract bug

Recently, a hidden DoS bug (called Gridlock) was revealed in Edgeware's Lockdrop smart contract that has locked hundreds of millions of dollars worth of Ether. Because of this bug, Edgeware had to newly deploy the fixed version of the contract, and as a result, two Lockdrop contracts (old version and new version) currently live in parallel on mainnet. (This means that you can send a transaction to either of these contracts to lock your Ether, until the old one is attacked and becomes incapable.)

In this article, we will review the Gridlock bug and discuss how formal verification can help to prevent this type of bugs.

Continue reading

Formal Verification of Ethereum 2.0 Deposit Contract (Part I)

Ethereum 2.0 is coming. And rest assured, it will be formally specified and verified!

Ethereum 2.0 is a new sharded PoS protocol that, at its early stage (called Phase 0), lives in parallel with the existing PoW chain (called Eth1 chain). While the Eth1 chain is powered by miners, the new PoS chain (called Beacon chain) will be driven by validators.

Continue reading

ERC777-K: Formal Executable Specification of ERC777

Denis Bogdanas and Daejun Park


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.

Continue reading