Ethereum is a distributed blockchain platform, serving as an ecosystem for smart contracts: full-fledged inter-communicating programs that govern crypto-economic systems. MadMax is a framework for detecting a broad family of vulnerabilities in these smart contract related to out-of-gas behavior. Vulnerabilities of this nature are extremely hard to detect with anything other than static program analysis, as they only manifest themselves after several distinct runs. MadMax is highly efficient and effective: it analyzes the whole Ethereum blockchain in 10 hours, and reports numerous vulnerable contracts holding a total value exceeding $2B, with high precision, as determined from a random sample.

The toolchains surrounding MadMax today (namely Ethane and Gigahorse) are all declaratively specified, which has yielding great benefits. This includes a decompiler (Gigahorse), with fully declaratively specified decompilation phases and strategies, and a general framework (Ethane) for program analysis of smart contracts at multiple levels of abstractions.