Formal Verification of ERC-20 Tokens

This article explains the ERC-20 token standard, highlights common implementation pitfalls (such as arithmetic overflows/underflows and refactoring mistakes that omit allowance updates), and describes CertiK's methodology for formally verifying ERC-20 contracts using mathematical models, linear temporal logic, and symbolic model checking with SMT solvers to prove or disprove 38 contract-specific properties.