Devcon VI

Bad Proofs in Formal Verification
10-12, 16:00–16:30 (America/Bogota), Talk 3

Formal verification can be a huge boon to smart contract security as it checks all possible execution paths. Unfortunately, even verified code can be faulty if the formal specification contains mistakes. "Bad" proofs can lead to false confidence in the code and premature deployment. This talk will discuss different types of "bad" proofs and how to avoid them.

Uri is a Developer Advocate and Software Developer at Certora. Uri fell in love with blockchain in 2018 after doing a research project as an undergraduate student at the Technion. He joined Certora right after graduation.