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.