We reviewed two preliminary versions of the code provided by Geoff Hayes on July 14 and July 26, 2018. A partial analysis was conducted on the July 14 version, followed by a more thorough analysis of the July 26 version. Our audit focused on three contracts: CarefulMath, Exponential, and PriceOracle. Logical specifications were written for methods in all three contracts, along with global invariants for the PriceOracle contract. These specifications, along with assertions in the original code, were rigorously checked using our verification tool.

The audit uncovered 7 issues and verified 5 global properties. One issue (Issue #1) was identified in the July 14 version and resolved in the July 26 version. All other identified issues remain in the July 26 version.