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.
transferFromover symbolic input values which represent all possible inputs.
require. No outcomes are tested for execution paths that result in
transfercalls (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.