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. I will explain how the Certora Prover successfully verifies programs with 10,000 lines of Solidity code.
