Formal verification is a way of proving, mathematically, that a piece of code keeps a rule you wrote down, for every input and every sequence of calls it could ever receive. A test shows the code behaved on the cases you tried. A proof shows there is no case left to try.
Nobody has measured every triangle to confirm the angles add up to 180 degrees. Nobody needs to, because it has been proved. The proof also carries a condition in the small print: it holds on a flat surface. Draw the triangle on a globe and the angles add up to more. Formal verification works the same way. It gives you certainty, and the certainty covers exactly the rule you stated and the assumptions you made. That second half is where most of this page is spent.
Quick Answer
Formal verification uses a solver or a prover to show that a smart contract satisfies a written property (for example “total shares always equal the sum of every balance”) under all possible inputs and states. It is stronger than testing or fuzzing, which only sample behaviour. It proves nothing about properties nobody wrote, and it is only as good as the specification.
Last updated September 2026.
For the founder’s version, with the analogy and none of the maths, read Formal analysis in Web3: what founders need to know. This page is the reference layer underneath it.
On this page
- How formal verification works
- A proof and a counterexample in one small contract
- How it compares with testing, fuzzing, static analysis and an audit
- What a proof does not tell you
- The tools
- Where it fits in a security process
- Frequently asked questions
How formal verification works
Every formal verification run has three inputs, and a result is only meaningful if you know all three.
- The code: usually the Solidity source or the compiled bytecode. Some tools reason about the bytecode on purpose, so that a compiler quirk cannot hide between the source you read and the code that runs.
- The property: a precise statement of what must always be true. “A user can never withdraw more than they deposited.” “Only the owner can change the fee.” “Total supply only changes on mint and burn.” This is the specification, and writing it is most of the work.
- The prover: a solver that turns the code and the property into logic and either finds an input that breaks the property, or shows no such input exists.
There are two broad ways the prover does its job. Model checking explores the states the contract can reach and checks the property in each one. Deductive verification builds a logical argument that the property is preserved by every function, often with a human guiding the prover through the hard steps. The ethereum.org overview of formal verification describes both, and it is the best neutral starting point.
Either way, a run ends in one of three places. The property is proved. The prover returns a counterexample, which is a concrete input that breaks it. Or the prover times out and tells you nothing, which is common on complex properties.
A proof and a counterexample in one small contract
The quickest way to see this is with the model checker built into the Solidity compiler. The SMTChecker documentation describes the contract it makes with you: it treats require statements as assumptions and “tries to prove that the conditions inside assert statements are always true”.
Here is a fee split with two properties written as assertions.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;
// Illustrative only. Splits a payment between two parties at a rate in basis points.
contract Split {
function split(uint256 amount, uint256 bps) public pure returns (uint256 a, uint256 b) {
require(amount <= type(uint128).max);
require(bps <= 10_000);
a = (amount * bps) / 10_000;
b = (amount * (10_000 - bps)) / 10_000;
// Property 1: the split never pays out more than came in.
assert(a + b <= amount);
// Property 2: the split pays out everything that came in.
assert(a + b == amount);
}
}
Run it through the checker (solc --model-checker-engine chc --model-checker-targets assert) and the compiler answers both questions without a single test being written.
Info: CHC: Assertion violation check is safe!
--> Split.sol:13:9:
|
13 | assert(a + b <= amount);
Warning: CHC: Assertion violation happens here.
--> Split.sol:15:9:
|
15 | assert(a + b == amount);
Property 1 is proved for every amount up to the uint128 limit and every rate. Property 2 is false, and the bounded engine (--model-checker-engine bmc) names an input that breaks it: amount = 1, bps = 9978. Both halves round down to zero and one unit of the payment vanishes.
A unit test with round numbers would pass Property 2 all day. A fuzzer might find the rounding loss, if it happened to try small amounts. The prover found it by reasoning about every input at once. Notice also what it did not do: it did not tell you whether losing one unit of dust matters. You decide that, and you decide it when you write the property.
How formal verification compares with testing, fuzzing, static analysis and an audit
These five get bundled together as “security testing”. They answer different questions, and a clean result from each one means something different.
| Technique | The question it answers | What a clean result means | What it misses |
|---|---|---|---|
| Unit testing | Does the code do what I expect on these inputs? | The cases you wrote pass | Every case you did not write |
| Fuzzing and invariant testing | Can random inputs break a property I stated? | Nothing broke in the runs that were made | Paths the fuzzer never reached |
| Static analysis | Does the code contain a known bad pattern? | No known pattern was found | Logic errors with no pattern to match |
| Manual audit | What is wrong here, including in the design? | Reviewers found no further issue in this version | Anything the reviewers missed, and every later version |
| Formal verification | Can this property ever be broken, by any input? | The property holds in all executions, under the stated assumptions | Properties nobody wrote, and anything outside the model |
The last row is the only one where “clean” means “impossible” rather than “not found”. That is the whole appeal. The last column is the reason it does not replace the other four. For the tool-by-tool version of the same distinction, including which popular “static analysers” are really fuzzers or provers, see Solidity static analysis tools: what they catch, and what they miss.
There is a reason the property matters more than the pattern. A 2024 ICSE study by Chaliasos and colleagues ran five automated security tools against 127 real attacks worth $2.3 billion in losses. The tools could have prevented 8% of them, $149 million, and every preventable attack was reentrancy. The practitioners surveyed named logic bugs and protocol-level flaws as the threats the tools do not address. A logic bug has no signature to match. It can only be caught by a rule that says what the logic was supposed to do.
What a proof does not tell you
A proof is a strong claim with a narrow scope. Five limits are worth knowing before anyone quotes one to you.
It only covers the properties that were written
If nobody wrote “the oracle price cannot be moved inside one transaction”, nothing was proved about it. Ethereum.org puts it plainly: if specifications are poorly written, violations “cannot be detected by the formal verification audit”, and “a developer might erroneously assume that the contract is bug-free”.
The specification can be wrong
A property can be true and still not be the property you needed. The triangle proof is correct; it is also useless on a globe.
The model has edges
External calls, oracles, other protocols, governance actions and the chain itself are usually modelled as assumptions. The proof holds if the assumptions hold. Bridges are the obvious case: most of the risk lives in what the contract trusts, which is why chain bridges keep appearing at the top of loss tables.
Some properties will not resolve
Solvers time out, loops and unbounded state explode the search, and some questions are undecidable in principle. A run that ends in “unknown” is not a pass.
It expires when the code changes
A proof is about one version of the code, exactly like an audit. Upgrade the implementation and the proof describes a contract that no longer exists. We made this argument for audits in when a smart contract audit actually expires, and it applies to proofs unchanged.
The tools teams actually use
The ecosystem has settled into a handful of tools. They differ mainly in where the property is written and how much the developer has to learn.
| Tool | What it is | Where the property lives | Source |
|---|---|---|---|
| SMTChecker | The model checker built into solc | require and assert in the contract itself | Solidity docs |
| Certora Prover | A prover with its own specification language, CVL, plus separate provers for Solana, Sui and Soroban | A separate spec file | Certora docs |
| Halmos | “A symbolic testing tool for EVM smart contracts”, from a16z | Existing Foundry-style tests, run symbolically | GitHub |
| Kontrol | Runtime Verification’s tool combining the KEVM semantics with Foundry | Foundry tests, executed symbolically against a formal model of the EVM | GitHub |
The trend across the last two is worth noticing. Both let a team reuse tests it already has, which moves formal methods from a specialist’s job towards a developer’s, without removing the hard part. Someone still has to decide what must always be true.
Where formal verification fits in a security process
Our own post makes the case briefly: formal analysis matters most when a protocol holds significant value, is immutable, or has complex logic such as DeFi, bridges, governance or vaults. If yours matches, read the founder’s version before you budget for it.
In practice the techniques stack in a fairly fixed order.
- Write the invariants down: What must always be true about balances, shares, fees, roles and upgrades. This list is the input to everything that follows.
- Test and fuzz against them: Cheap, fast, and good at finding the obvious breaks before anything expensive runs.
- Get the design and the list reviewed by people: A manual audit is where a wrong or missing property gets caught, because a reviewer asks what the code was meant to do rather than what it does.
- Prove the properties that hold the money: Start with the functions where a failure is unrecoverable.
- Keep checking after launch: Code changes, proofs and audits expire, and the check has to run again.
Step 1 is the one teams skip, and it is the one every later step depends on. In our Adrena audit, one stage of the review traced every path that moves value through a Solana perps DEX, from liquidity deposits to borrow and exit fees, and turned it into a set of conservation invariants. Those invariants became the assertions the fuzzers checked afterwards. The same list is what a prover would need.
A manual audit at Fidesium starts at $5,000, covers logic and economic risk line by line, and includes two rounds of fix verification. Our published reports are in the audit portfolio, and every audit is minted as an on-chain record so the result can be checked rather than claimed. After launch, deterministic static analysis runs on every commit from $399 a month.
A proof is only as good as the property list it was given. Talk to the audit team if you want that list written and challenged before anyone relies on it.
Frequently asked questions
What is formal verification in simple terms?
Formal verification is a mathematical check that a program always keeps a rule you wrote down. Instead of running the code on sample inputs, a solver reasons about every possible input and state at once. It either proves the rule can never be broken, or it returns a specific input that breaks it.
What is the difference between formal verification and fuzzing?
Fuzzing runs the code on large numbers of random inputs and reports any that break a property, so a clean fuzzing run means nothing broke in the runs that were made. Formal verification reasons about all inputs at once, so a clean result means the property cannot be broken under the stated assumptions. Both need the same written property, and many teams fuzz first and prove the most important properties afterwards.
Does formal verification replace a smart contract audit?
No. Formal verification proves that written properties hold, and an audit asks whether those properties are the right ones and what else could go wrong in the design, the economics and the permissions. A proof of the wrong property is still a proof. The two work best together, with the audit shaping the property list the prover checks.
Can a formally verified smart contract still be hacked?
Yes. The proof covers only the properties that were written and only under the assumptions in the model, such as how oracles, external contracts and governance behave. An attack that breaks an assumption, targets a property nobody specified, or hits a later version of the code is outside what the proof says.
What tools are used for formal verification of smart contracts?
The most common are the SMTChecker built into the Solidity compiler, the Certora Prover with its CVL specification language, Halmos from a16z, and Kontrol from Runtime Verification, which builds on the KEVM formal model of the EVM. Certora also offers provers for Solana, Sui and Soroban. Halmos and Kontrol let teams run their existing Foundry-style tests symbolically.
Which protocols need formal verification?
Protocols that hold significant value, cannot be changed after deployment, or have complex logic such as lending, perpetuals, vaults, bridges and governance get the most from it. A simple token with standard, well-tested code gets little extra from a proof. The deciding question is whether a single failure would be unrecoverable.
Is formal verification expensive?
It costs more than testing because writing a correct specification takes skill and time, and guiding a prover through hard properties is manual work. Ethereum.org lists that labour first among the drawbacks. Teams keep the cost down by proving only the properties that protect funds, and by using tools that reuse the tests they already have.
