Bad Proofs in Formal Verification
Duration: 00:28:48
Speaker: Uri Kirstein
Type: Talk
Expertise: Intermediate
Event: Devcon
Date: Oct 2022
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.