Challenges Encountered In the Formal Verification of ERC-20 Contracts

This article explains CertiK’s methods and limitations for tool-assisted formal verification of ERC-20 token contracts: how standard property checks can be mismatched by contract extensions (such as timelocks), how false positives and inconclusive results arise from undecidability and resource limits, and how manual review and custom verification complement automated analysis to assess security and non-standard behaviors.