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.