Disclaimer

This tool is offered "as is" with no guarantees of any kind. It represents a symbolic formal verifier of standard ERC20 functions. The user is expected to have basic knowledge of symbolic execution.

This is what the tool does:
  • It tests standard ERC20 functions approve, transfer, transferFrom over symbolic input values which represent all possible inputs.
  • For tested functions, it tests that balances/allowances change for provided arguments, and don't change for any other argument.
What the tool does not test:
  • Functions may implement any kind of additional checks through require. No outcomes are tested for execution paths that result in revert.
  • If the contract has additional functions besides ERC20 standard, they are ignored.
  • The firing of log events is not tested, although we may implement this in the future. Only the checks described in the paragraph above are performed.
Limitations:
  • The verifier currently only supports straightforward ERC20 implementations.
  • It does not support for example external function calls, for loops.
  • The storage model for allowances and balances must be standard Solidity mappings. Any other implementations are not supported.
  • Any ERC20 contract that transfers tokens for more than one account during transfer calls (because it uses fees), is not supported.
  • The above list is not exhaustive.

When will results be available? After submitting the bytecode for testing we will send you the report by email in 1-2 days.

At the moment we are in a very early experimental stage. Execution of the tests is triggered manually by our engineers, but report generation is otherwise automatic.