How CertiK's Formal Verification Engine Could Have Detected ICX's EnableTokenTransfer Issue

On Jun 16th 2018 a logic bug was reported in ICON's ICX token contract: a require statement used 'msg.sender != walletAddress' instead of 'msg.sender == walletAddress', which allowed anyone other than the owner to enable or disable token transfers. Attackers exploited this to disable ICX transfers and halt thousands of transactions; while tokens were not stolen, the incident disrupted functionality and prompted mitigation and public statements from the ICON team and offers of formal verification from CertiK.