Specification

Finding Bugs Automatically in Smart Contracts with Parameterized Invariants

A 2020 WIP paper from Certora describing a framework of reusable parameterized invariants for automatically finding bugs in smart contracts, with the Certora Prover discovering two real bugs in MakerDAO's Multi-Collateral Dai. The core insight is that the hardest problem in formal verification is specification, and smart contracts are unusually amenable to shared invariants — enabling a community network effect.