Preventing billion dollar coding errors with scalable formal verification


Dec 3, 2022


Spoken At

ETHIndia 2022

Featured Speakers


Mooly Sagiv

Formal verification is a technique for detecting bugs and mathematically proving their absence. The main idea is to compare the existing behavior of the program to the desired behavior of the program. Formal verification drastically increases code security. I will describe the Certora Prover to verify programs with 10,000 lines of Solidity code formally. It automatically analyzes the low-level bytecode program.