erc_20_formal_verification

Formal verification using KEVM of high-profile ERC20 tokens: https://etherscan.io/tokens

• Tronix (TRX)
  • totalSupply - proved without change
  • balanceOf - proved without change
  • allowance - proved without change
  • approve - changes from ds-token:
    • validAddress modifier
    • require(_value == 0 || allowance[msg.sender][_spender] == 0)
  • transfer - changes from ds-token
    • validAddress modifier
  • transferFrom - changes from ds-token
    • validAddress modifier
• BNB (BNB)
  • had problems at compilation, skipped for the moment
• VeChain (VEN)
  • claimBonus function at transfer and transferFrom functions
  • bonusOffered - checked in balanceOf
• OmiseGO (OMG)
  • it does not really implement the ERC20 interface, ( transfer, transferFrom and allowance don't return anything )
• ZRXToken (ZRX)
  • it contains small deviation from the StandardToken ( Older version of OpenZeppelin StandardToken )
• ICON (ICX)
  • it contains small deviation from the ds-token -> next to be updated