first tool for precisely specifying and reasoning about

trace properties, which employs inter-procedural symbolic

analysis and concrete validator for exhibiting real

exploits. Our analysis of nearly one million contracts

flags 34,200 (2,365 distinct) contracts vulnerable, in 10

seconds per contract. On a subset of 3,759 contracts

which we sampled for concrete validation and manual

analysis, we reproduce real exploits at a true positive rate

of 89%, yielding exploits for 3,686 contracts. Our tool

finds exploits for the infamous Parity bug that indirectly

locked 200 million dollars worth in Ether, which previous

analyses failed to capture.