erc20-steps.md

Typing the specification and checking it

Inspecting a complete spec

1. Read EIP-20 and try to figure how it is working.

2. Read the description of the attack scenario on EIP-20

3. Open ERC20.tla and MC_ERC20.tla.

4. Check the trace invariant NoTransferAboveApproved:

   $ apalache-mc check --inv=NoTransferAboveApproved MC_ERC20.tla

5. The tool reports an invariant violation.

6. Open the counterexample and see, whether it matches the above attack scenario.