As @VitalikButerin says, we need formal verification of security properties.

But scaling formal verification for Ethereum smart contracts has always been a challenge due to how the EVM handles memory—one big, monolithic array with no explicit allocation. This poses difficulties for SMT solvers because it requires the solvers to infer complex invariants about memory.

So, how did Certora overcome this? Let’s break it down 🧵👇