Jan 2023 Online Event: Scaling Formal Verification to Find Bugs in Complex Smart Contract Systems.

Mon, Oct 2, 2023, 12:00 AM

Formal verification is a technique for detecting bugs and mathematically proving their absence. By comparing the existing behavior of the program to its desired behavior, code security is drastically increased. However, most tools do not scale to handle realistic programs. Mooly will explain how the Certora Prover successfully verifies programs with 10,000 lines of Solidity code. Mooly Sagiv is a computer scientist known for his work on static program analysis. He is currently Chair of Software Systems in the School of Computer Science at Tel Aviv University, and CEO of Certora, a startup company providing formal verification of smart contracts. Certora offers a unique SaaS product called the Certora Prover for Web3 code security. The Certora Prover compares the smart contract code to a formal specification – a way to express fundamental properties of the code. The tool automatically locates bugs before deployment or mathematically proves their absence even after code updates.