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.
approve
,
transfer
,
transferFrom
over
symbolic input values which represent all possible inputs.
require
. No outcomes are
tested for execution paths that result in
revert
.
transfer
calls (because
it uses fees), is not supported.
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.