Formal verification uses mathematical reasoning to prove that code satisfies specified requirements across every scenario covered by a defined model, under stated assumptions. For a business relying on that code, those requirements can represent essential commitments, such as maintaining accurate balances or restricting who can move money.

Solana's SPL Stake Pool has been running for almost five years. Users deposit SOL, the protocol delegates it to validators to earn rewards, and users redeem their share of the pool whenever they want out. A significant portion of all staked SOL on the network passes through it, and it had been audited several times before Certora verified it in 2025.

At the center of the protocol sits a reserve account, the operating account where deposits arrive and withdrawals are paid from. The account needs to retain a minimum balance to remain operational. The code has a rule intended to protect it.  Before releasing money from the reserve, confirm that the reserve still holds enough to stay open. That safeguard was present, and a comment written beside it shows the developers had considered this exact concern.

The safeguard read the reserve's balance before the withdrawal was subtracted. It never asked what the balance would be once the money left. A withdrawal large enough to take everything therefore passed the check, and the reserve could be drained to nothing. 

What formal verification proves

Formal verification starts by stating precisely what the software must do. That statement is called a property. In the Stake Pool example, the concern was whether withdrawals could undermine the reserve’s intended protection.

A proof here is a demonstration that a property cannot fail, within the model of the system being analyzed and under the assumptions made about it.

The model is the description the analysis works from: a mathematical representation of the code’s relevant behavior, together with whatever the analysis has been told about the world around it. Assumptions are conditions the analysis takes as given, such as an external service supplying accurate prices. Both of those qualifiers matter, and this article returns to them.

Properties can describe requirements such as a lending market’s assets covering its obligations under specified market conditions, a user’s balance never going negative, or the supply of a token changing only when tokens are minted or burned, meaning created or destroyed. Together, the requirements being checked form the specification: the standard against which the code is proved. That standard needs to reflect intended behavior; merely describing what the existing code does could preserve its mistakes.

Checking a property can produce a proof, meaning the condition holds everywhere the model reaches. It can also produce a counterexample, a specific scenario in which the condition fails. A counterexample may expose a genuine bug, or it may reveal that the model allowed something the real system never would, in which case the model is what needs correcting. 

Formal verification vs. testing and auditing

Formal verification, testing, and human audit are complementary practices, and the boundaries between them are not clean. A thorough audit often includes writing tests, and increasingly includes formal verification as well. The useful question is what each practice is positioned to find.

Testing checks concrete values one at a time. An engineer picks inputs, runs the code, and compares the result against what should have happened, so coverage reflects what that engineer thought to try. Fuzz testing removes part of that limit by generating large volumes of inputs automatically, many of them strange, and reporting any that cause a failure. It reaches cases nobody would have written by hand, but it remains sampling: a fuzzer left running for a week tries a large number of inputs rather than all of them.

Formal verification reasons about a property across the entire range of values and states its model covers, and settles the question for all of them at once. As an example, balances in these systems are commonly stored as 64-bit unsigned integers, a type with more than eighteen quintillion possible values. A test suite might try a few hundred of them. A fuzzer might try a few billion. Formal verification on the other hand covers the entire range of values at once via translation to logical formulas.

Human review contributes something neither of the other methods can. A reviewer brings context and judgment, and can ask whether the protocol's design serves the purpose the team intended, or whether a mechanism that works correctly is nevertheless a bad idea. Those questions resist translation into checkable properties, which is why people are needed to ask them.

The Stake Pool example shows the value of checking whether an intended protection actually holds. The failure required one specific situation: a withdrawal that emptied the reserve completely, at a moment when the protocol had no other funds to draw from first. Tests explore amounts an engineer thinks to try and fuzzers explore amounts automatically, but the dangerous amount was the exact remaining balance under one particular condition, a narrow target in an enormous space. Either approach could have exposed the flaw if it exercised that combination.

The same flaw could also be easy to miss in review. The safeguard was present and addressed the right concern, so a reviewer would see that someone had already thought about the reserve running low. The flaw was one of timing. Consider a shop assistant told to check the register has enough cash before handing out a refund. An assistant who checks, then hands over everything in the till, has followed the instruction and still emptied it. A safeguard that measures the wrong moment can still look reassuring at a glance.

What a formal verification engagement involves

A verification engagement has several parts. The first is deciding which properties matter for this particular system. Every property has to be stated precisely, and precision costs effort, so the ones chosen should be those whose failure the protocol cannot survive. For a lending market, that might be that the system never becomes insolvent. For a token, that total supply changes only through minting and burning. What the team gains here arrives before any checking starts: an unambiguous written statement of what their protocol must never do. For many teams this is the first time those commitments have been recorded anywhere outside the heads of the engineers who built the system.

A business objective such as "protect customer funds" is too broad to check directly. It needs to become specific claims: users cannot withdraw more than they own; only authorized parties can change withdrawal permissions; issued claims remain backed by assets. Leaders help identify the obligations that matter, while engineers make them precise enough to verify.

Something less obvious follows. Proving a headline property almost always requires establishing a chain of smaller facts underneath it, and those supporting facts are where the surprises live. A team sets out to prove that a pool can always cover its obligations. Getting there requires proving that a particular account always holds a minimum balance, which nobody listed as a requirement because nobody thought of it as one. The proof forces the question.

The second part is checking the code against those properties, and the third is interpreting what comes back. A proof is the clean case. A counterexample is considerably more useful than an abstract warning, because it is a concrete sequence of steps that produces the failure, which an engineer can reproduce and reason about directly. 

The fourth part is acting on what was found. Where verification exposed a genuine bug, the code gets fixed. Where a counterexample described behavior the protocol actually intends, the specification or the model gets refined to match the real design. The team must check that the refinement preserves the intended protection, then rerun the affected checks, often more than once. The specification that survives this process is reusable, so when the protocol changes later, the same properties can be checked against the new code. Changes to the design or dependencies may require revisiting those properties and their assumptions too. Once the specification is formalized and implemented, it also works as a protective layer against future code changes.

Why smart contracts are a strong fit for formal verification

Smart contracts are programs that run on a blockchain. They are an unusually good match for this kind of analysis, and the reason comes down to how expensive mistakes are and how little can be done about them afterward. A contract typically controls valuable assets from the moment it goes live. Conventional software can reach users gradually, through a staged rollout or a beta period that limits how many people a defect can affect. Smart contracts can also use staged rollouts and deposit limits, but a deployed contract holding real money can suffer losses before a fix arrives.

Mistakes are also difficult to undo. Many protocols can be upgraded, and teams should build that capability, but an upgrade only changes what the code does next. It does not return assets that already left. A defect found on a Tuesday and patched on a Wednesday still cost whatever it cost on the Tuesday. Transactions are final by design. Finally, reputational damage is an additional cost on top of concrete losses.

There is a second reason smart contracts can suit verification: their execution environments define how code runs and changes data. Ethereum's environment, the Ethereum Virtual Machine or EVM, is one example. Solana, Stellar, and Sui have different execution models that the analysis must account for. Reasonably scoped code and explicit rules can support rigorous analysis, although complex interactions can still make a proof difficult.

Those facts change where security effort pays off. For a contract holding user funds the first sign of a defect may be the loss itself. The Stake Pool bug is a case in point. Emptying the reserve could allow an attacker to revive and take control of the account through further actions within the same transaction.

The property that exposed the bug was that the pool must always be able to draw from its reserve, which requires the reserve account to remain usable by the pool. It emerged while proving solvency, the requirement that the pool's issued shares remain backed by assets it controls.

Had the code stayed in that state, an attacker could have emptied the reserve and taken ownership of the account the pool treats as its own. They could then deposit into that reserve, receive newly minted shares in return, and withdraw the deposited funds afterward. Shares obtained for nothing are a claim on assets that other users paid for. The gap was found during verification, reported to the Stake Pool team, and remediated.

When formal verification is worth considering

The strongest candidates combine serious consequences of failure with requirements that can be stated precisely. Core accounting and authorization logic, systems controlling substantial value, and infrastructure reused by many applications are natural places to consider it. The decision should reflect the harm a failure could cause and which important questions verification could resolve.

A team does not have to verify everything at once. It can begin with critical components and the properties that protect users most directly, while stating what remains outside scope. If a prototype's intended behavior is still unsettled, clarifying those requirements may be the immediate priority. That work can happen alongside verification, but frequent design changes will also require revisiting the analysis.

What are the limitations of formal verification?

Every guarantee produced by this work comes with a boundary. Knowing where that boundary sits is what makes the guarantee useful.

A proof covers what was modeled, and anything outside the model sits outside the guarantee. If a protocol reads prices from an external oracle, a service supplying outside data, a proof that assumes accurate prices does not establish safety when those prices are false. Verification can examine faulty prices if that behavior is included in the model; modeling the oracle does not itself guarantee that the real service follows the model.

The same holds for off-chain components, meaning software running outside the blockchain, for dependencies that were never verified, and for interactions between contracts that were analyzed separately. Two contracts can each be correct alone and still combine into a system that is not. Verification can cover their interactions when the relevant behavior is modeled together.

Assumptions work the same way, and good practice states them openly. In Certora’s recent verification of a replacement for Solana's token program, our proofs carried a small number of explicit assumptions. Each one corresponded to a behavioral difference the client had designed deliberately. Written into the proof, those assumptions became a formal record of design decisions, readable by anyone who wants to know exactly what was covered and what was not.

The other limit is practical. Serious verification takes specialized people and real time. How much depends on the size of the system, the complexity of its properties, and how much of the surrounding environment has to be modeled.

These limits argue for using all three practices together. Formal verification settles questions across a whole space of behaviors. Testing exercises the real system as built. Human review asks whether the design makes sense at all. Each covers ground the others do not.

Questions business leaders should ask about formal verification

"Formally verified" is meaningful only when it is clear which code was checked and against which properties. Business leaders can use three questions to understand the scope and significance of that work. Each should have a concrete answer, readable without opening a specification.

1. Which properties hold, and which risks do they cover? The output is a specific list, and a leader can read it to see whether the failure that would hurt most appears on it.
2. What was assumed about the world around the code? Oracles, off-chain components, and unverified dependencies sit outside the guarantee unless they were modeled, and the assumptions written into a proof mark exactly where it stops.
3. What has to be rechecked when the protocol changes? A specification stays valid across revisions, so the same properties can be run again against new code, which is how a guarantee survives the next release.

Formal verification, then, is the practice of stating what a protocol must never do and proving that the code cannot do it, within a model and assumptions that are written down and open to inspection. Its guarantees reach only as far as that model, which is why it belongs alongside testing and human review rather than in place of them. What it adds is coverage nothing else provides: a claim that holds for every value and every sequence the model admits. For code that holds other people's money and cannot be recalled once deployed, that is the difference between believing a system is correct and knowing which parts of it are.

This article has described what formal verification is and why it matters. Later pieces in this series go deeper on how it compares to testing and auditing, on how a prover actually works, and on what this looks like applied to a specific ecosystem such as Solana.