Where can one locate a formally verified ERC20/ERC721 solidity code/template that adheres to security design patterns such as check effects interaction patterns?


Here is the relevant code in the 0xcert reference implementation:

 * @dev Actually perform the safeTransferFrom.
 * @param _from The current owner of the NFT.
 * @param _to The new owner.
 * @param _tokenId The NFT to transfer.
 * @param _data Additional data with no specified format, sent in call to `_to`.
function _safeTransferFrom(
  address _from,
  address _to,
  uint256 _tokenId,
  bytes _data
  address tokenOwner = idToOwner[_tokenId];
  require(tokenOwner == _from);
  require(_to != address(0));
    _transfer(_to, _tokenId);
    if (_to.isContract()) {
    bytes4 retval = ERC721TokenReceiver(_to).onERC721Received(msg.sender, _from, _tokenId, _data);
    require(retval == MAGIC_ON_ERC721_RECEIVED);

Source: https://github.com/0xcert/ethereum-erc721/blob/master/contracts/tokens/NFToken.sol#L310-L337

This is not formally verified, to a rigorous definition of the word. Actually very few things are formally verified, please see the Vyper project if you are interested in that -- people interested in formality are using that language.

But informally, you can see that onERC721Received, the recursion step is applied at the tail of this function. That is the important part.

Here is the standard text -- https://eips.ethereum.org/EIPS/eip-721 -- and it states:

When transfer is complete, this function checks if _to is a smart contract (code size > 0). If so, it calls onERC721Received on _to ...

Therefore this is a tail-end recursion, which follows the check effects interaction pattern.


Main problem with formally verifying ERC-20 implementations is that ERC-20 standard is informal by itself. Different developers treat it very differently, and even mainstream interpretation changes over time, especially after infamous hacks.

For example, standard states, that Approval event

MUST trigger on any successful call to approve(address _spender, uint256 _value)

however some popular implementations also log this even on calls to transferFrom and other functions that may change allowance, such as burnFrom.

Another example is Transfer event that, according to standard:

MUST trigger when tokens are transferred, including zero value transfers.

The note about zero value transfer was added to the standard quite recently, so many old token contracts do not log this event on zero value transfers.

Also it is unclear whether Transfer event should be logged on non-zero value transfers from address to itself.

And there are many other ambiguous things in the standard.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.