Smart contracts form the backbone of many modern blockchain protocols. They implement critical functions such as token management, deposits, and credit positions. That is why contract correctness is crucial: code bugs can lead to financial losses and reputational damage for blockchain projects.

Because the cost of mistakes is so high, smart-contract security is ensured through several methods at once — primarily manual audits and automated tests. Formal verification, which this article focuses on, is one of those methods. It is used to check contract properties and uncover vulnerabilities.

Below we look at Certora Prover, one of the formal-verification tools used to check the correctness of Solidity smart contracts, and then move on to the principles behind its workflow and practical use.

The main feature of this tool is process automation, so the user does not need to derive mathematical proofs manually. Instead, the user provides the smart-contract source code and a specification describing the properties the code must satisfy. The specification is written in CVL (Certora Verification Language).

As a result of verification, Certora Prover produces a report stating whether the target properties were proven for all possible scenarios or whether a counterexample was found — a sequence of actions under which those properties are violated.

To understand how Certora Prover performs such checks, we first need to review its general workflow.

As mentioned earlier, the verification process begins with two inputs — the code and the specification. At the first stage, Solidity code is compiled into Ethereum Virtual Machine bytecode. Next, the bytecode is decompiled into Three-Address Code (TAC), which is a simplified but more verbose representation of the program logic. TAC breaks computation into smaller steps, which is important for further analysis.

At the static-analysis stage, TAC is optimized. For example, some parts of the program that do not affect the property being checked can be removed. The optimized code is then combined with the CVL specification to build logical formulas. Those formulas are passed to a constraint solver such as Z3 or CVC5, which either proves the property or finds a counterexample.

Next, let us review the formal foundations behind the Prover architecture. They help explain which properties are checked and how they are formalized.

Certora Prover relies on classical formal-verification concepts — induction and the Hoare triple. Induction is used to verify properties over all possible contract states, including the base state after constructor execution and any arbitrary state. This simplifies reasoning: instead of simulating long sequences of calls, verification may start from an arbitrary state. To avoid unrealistic counterexamples, the specification adds constraints on the initial state of the checked properties.

The tool also uses the Hoare triple, written as {P} C {Q}, where P is the precondition, C is the command, and Q is the postcondition. The precondition describes the system state before the command is called, and the postcondition describes the expected state afterward. If the first holds, then a correct implementation of the command must guarantee the second.

In CVL, these ideas are expressed through rules and invariants. Rules describe specific call scenarios: they define a sequence of actions and verify that the required property still holds afterward. Invariants describe properties that must always remain true at every stage of the system lifecycle.

The verification of both rules and invariants is based on induction: the system must preserve the target property and satisfy the postcondition. The difference between them is not the use of induction itself, but the scope of application. Any invariant can be implemented as a rule, while not every rule can be expressed as an invariant. In addition, invariants are checked from the state that exists after constructor execution, whereas rules are not intended to verify properties immediately after the constructor.

The examples below illustrate the difference between rules and invariants.

This example shows a rule that verifies the behavior of a specific function. According to it, after any contract function is called, the value of contractOwner must remain unchanged.

rule contractOwnerNeverChange(env e) {
address owner = contractOwner();
method f;
calldataarg args;
f(e, args);
assert owner == contractOwner();
}

The next example is an invariant describing a contract-state property. It states that totalSupply must always equal the sum of all user balances.

invariant totalSupplyIsSumOfBalances() {
totalSupply() == sumOfBalances;
}

However, contractOwnerNeverChange cannot be expressed as an invariant because in Certora Prover invariants cannot capture variable values from before the function call.

In practice, however, verification can run into limitations that need to be handled separately.

It is important to note that not every verification ends with either a proof or a counterexample. In some cases — for example, when the property is computationally expensive — the run may hit a timeout because of internal limits.

To address timeouts, several techniques are used. One of them is approximation. It replaces some code fragments with simpler models that do not affect the property being verified. Over-approximation replaces a function with a simpler one that returns values from a wider range. Under-approximation, on the other hand, narrows the set of values and must be used far more carefully because it reduces coverage.

Besides approximation, teams also adjust specifications and tune the Prover configuration, including the choice of constraint solver and analysis parameters.

Certora Prover can be used at different stages of the project lifecycle. For example, it can be applied during audits, after bug fixes to confirm that an issue has truly been removed, and in public audits or bug-bounty programs where companies reward external researchers for vulnerabilities they discover.

Formal verification is also useful at earlier stages — especially during architecture design and development. Understanding which properties will be checked helps surface architectural inconsistencies earlier and reduce the number of errors before the code is written. At the same time, it is important to remember that Prover is just one of the security tools and works best when combined with others.

Finally, let us look at how Certora Prover appears in a concrete example.

Take a basic ERC20 contract — one of the most common building blocks in blockchain systems. For ERC20, teams typically verify properties related to correct balance updates, the equality between totalSupply and the sum of all user balances, and the correctness of transfers and approvals. Once verification starts, Prover builds a report listing all checked properties and their outcomes. When a property is violated, the report includes the call stack and variable values needed to analyze the failing scenario.

This screenshot shows an invariant asserting that totalSupply equals the sum of all user balances, as well as the helper functions used to check that property.

This screenshot shows a counterexample found by Certora Prover, pointing to a rule violation in the permit implementation.

In that sense, Certora Prover helps verify smart-contract correctness against explicitly stated properties and uncover bugs missed by audits and tests. In practice, it is used as one security instrument among others and is most effective as part of a broader security stack.