The Certora prover simplifies the process of verifying a smart contract in a professional manner. Firstly, the prover compiles the Solidity smart contract to obtain EVM bytecodes. These bytecodes are then decompiled into a simplified intermediary three address code (TAC) language using static analysis, which removes irrelevant variables for the property being analyzed. The specification is used to generate verification conditions for the simplified code, which are translated into logical formulas in the SMT-LIB format. These formulas are fed into various solvers, each with different capabilities, to find values for variables. The negation of the intended property is checked to determine if a solution is found, which represents a counterexample, or if the property is proved. The use of bytecode and the simplification performed by the static analyzer are the two main advantages of the Certora prover over other verification tools, making it more scalable and capable of analyzing real-world smart contracts. Figure~\ref{fig:TheCertoraProver} illustrates the architecture of the Certora prover.
This paragraph is mostly accurate. However, the two main advantages of the Prover over other formal verification tools are its ease of use and speed.
- Ease of use: Certora’s specifications are written in CVL, an expressive language that resembles Solidity
- Speed: the static analyzer is a big player here, but so are clever formula generation/splitting and solver configurations.
The verification of EVM bytecode over high-level Solidity code follows our design principle “Verify What You Execute”. Indeed, we have found several compiler bugs using the Certora Prover.