Formal Verification
Ensuring smart contracts do as intended
TLDR:
Audits check the code for cases humans think to test, formal verification mathematically proves that specific properties hold for every possible input.
The biggest protocols already use it: Aave used it on their V3/V4 contracts, Uniswapâs used it, and even Ethereum used it for the merge code in â22.
Formal verification is not a silver bullet as it proves the code matches the specification, not that the specification itself is complete with all possible threats.
Formal Verification is growing as ZK proofs can make it continuous and bring it onchain, and AI can automate the hardest part of writing the specifications itself.
Iâve kept to a pretty consistent theme of privacy and security recently, well today will be no different as we discuss a concept that lives deep in the security realm called âFormal Verificationâ.
Formal Verification is a way of ensuring that a smart contract, or in fact any piece of code, does what it is intended to and therefore an important concept when dealing with securing financial assets onchain, read on below to learn more.
If this post resonates with you and you enjoy the content then please share it with a friend and get rewarded for doing so!
This blog goes out weekly to over 20,000 subscribers. Please message me if youâre interested in sponsorships or partnerships.
Formal Verification
Most people in DeFi have learned to look for the word âauditedâ before using a protocol. Itâs become a basic hygiene check, and for good reason. But as we continue to see hacks onchain, many of them on protocols that had been audited, itâs worth asking how can we secure our code further!
The answer that many of the smartest teams in the space are increasingly pointing to is formal verification. Itâs not a replacement for audits, itâs an additional set of safeguards.
When a security firm audits a smart contract, theyâre doing two things: reading the code carefully for anything that looks suspicious, and running a large number of tests against specific scenarios they think might reveal a bug.
Both approaches rely on humans imagining what could go wrong. And humans, however skilled, have a limited imagination when it comes to edge cases.
Formal verification takes a different approach entirely. Instead of testing a large number of scenarios, you write a âspecificationâ, which is a precise mathematical description of how the contract must behave. Things like:
The total supply of this token can never increase except through the mint function.
A userâs balance after withdrawal must equal their balance before, minus the amount withdrawn.
A liquidation can only happen if a position is genuinely under-collateralised.
These are called âinvariantsâ, they are properties that must always hold no matter what.
A tool then tries to prove mathematically that the code satisfies every invariant, for every possible input and every possible state.
This is not just a large number of inputs as with tests, weâre talking about literally the space of all possible inputs, checked rigorously through mathematical proofs. This is the key difference between testing and proving!
How it works
The core piece of the puzzle is something called an âSMT solverâ (Satisfiability Modulo Theories solver). This is an automated theorem prover, a piece of software that can determine whether a mathematical statement is true or false.
Once youâve written your specification and your code, both get compiled into a mathematical formula, and the SMT solver tries to find any scenario where an invariant is violated. If it finds one then you have a bug. If it canât find one after an exhaustive search then the property is proved.
The process is more iterative than it sounds. The solver sometimes gets stuck on particularly complex logic and needs a human expert to provide hints to move forward. This is partly why formal verification is expensive, as you still need skilled people working alongside the tool.
One detail worth knowing is that the best tools work at the bytecode level, the compiled machine code the EVM actually runs, rather than the human-readable Solidity code developers write.
This matters because it means the verification catches bugs that might be introduced by the compiler itself, and edge cases in how the EVM handles gas limits and integer overflow that Solidity level code can hide.
![[SE] Software Testing : SMT Solver, Concolic Testing Algorithm](https://substackcdn.com/image/fetch/$s_!3EbL!,f_auto,q_auto:good,fl_progressive:steep/https%3A%2F%2Fsubstack-post-media.s3.amazonaws.com%2Fpublic%2Fimages%2F07b48cf0-f37b-40ae-a0cb-09bfdc5bcb4d_676x204.png "[SE] Software Testing : SMT Solver, Concolic Testing Algorithm")
A good illustration of what this catches in practice:
Runtime Verification, one of the leading firms in this space, once caught a bug in a contract that used a mathematical âpowerâ function. The bug would only trigger if a very small number was raised to a very large power, producing a result so tiny it rounded to zero, and then that zero was used in a division elsewhere.
The result is that a transaction that should have processed 3,000 ETH processed nothing instead. Testing would almost certainly have missed this. The formal verifier found it because it explored states no human tester would think to check.
Whoâs using it
Formal verification has moved well beyond academic research. Some of the biggest protocols in DeFi like Uniswap and Aave use it on their most critical code.
Aave used Certoraâs Prover on their V3 contracts. Then for V4 they went even further, as rather than working through a third-party tool, they used Microsoftâs Z3 SMT-solver directly to formally verify core properties, shifting from using an external team to doing formal verification in-house.
Before the Ethereum merge back in 2022, the auditing company Runtime Verification formally verified the Ethereum deposit contract, the contract that accepts staked ETH from validators.
The logic being that this contract would hold billions of dollars and could not be upgraded, so you needed to get it right the first time.
The main tools in use today are Certora, Halmos, the K Framework, and Z3. Certora remains the most widely used commercial tool in this space. Teams write specifications in their âCVLâ language, and the Prover checks them against the contract.
Halmos, built by a16z, is a newer and more accessible option aimed at developers who want formal verification integrated into their existing workflow. The K Framework, used by Runtime Verification, is more powerful but also more complex to work with.
Then there's Z3, Microsoft's SMT solver, which is the underlying engine that tools like Certora are built on top of. Most teams access it indirectly through one of these tools, but experienced teams like Aave can use it directly to cut out the intermediary.
Formal verification is costly, an engagement is comparable in price to a top-tier security audit, sometimes more. This is why most protocols formally verify their most critical components rather than their entire code, systems such as the core accounting logic and liquidation engine, and larger teams like Aave try to bring it in-house.
The honest limitations
Formal verification is not a guarantee of safety, crucially because: it proves the code matches the specification, it does not prove the specification is correct.
If your invariants donât account for a threat then the prover wonât catch it. The April 2026 bridge hacks are a useful example here.
Formally verifying the bridge contract logic wouldnât have caught a vulnerability that depended on external actors feeding incorrect data. To catch that, your specification would need to include a property like âwhat if the verifier lies?â And that requires knowing external manipulation was a threat vector in the first place.
Writing good specifications is genuinely hard. A bad or incomplete spec can create false confidence where the prover says everything is fine, but the bug lives in what you forgot to check.
The other honest limit is scope. Even well-resourced protocols canât afford to formally verify everything as complex systems have hundreds of components. Prioritising which invariants matter most is itself a skill, and getting it wrong leaves gaps.
Where itâs heading
The most interesting development at the frontier is the convergence of formal verification with ZK proofs.
As we covered in last weekâs post, ZK proofs let you prove off-chain that a computation ran correctly and verify that proof cheaply on-chain. Formal verification defines precisely what âcorrectlyâ means.
The emerging idea is to combine them: run a formal verification check off-chain, generate a ZK proof that the check passed, and have contracts reject any transaction that canât produce a valid proof.
Projects building âzkVMsâ, ZK-provable virtual machines like RISC Zero and SP1, are making this increasingly practical. The potential end state changes from âwe audited this before it went liveâ, to âevery execution is provably correct by construction, and the proof lives on-chain.â This will be a massive improvement for onchain security.
The other shift happening in parallel is AI. The most expensive bottleneck in formal verification has always been writing the specifications as it requires people who understand both the code and which properties actually matter, and that expertise is rare and costly.
AI models are now good enough at reading smart contracts to suggest invariants a developer might not have thought to specify!
Certora has been building AI-assisted tooling that generates CVL specifications from code and interprets counterexamples in plain language rather than raw math. The idea is that a developer describes what their contract should do, the AI drafts the formal spec, and the developer reviews and refines it.
This doesnât eliminate the need for human judgement. A bad spec still produces a bad proof. But it meaningfully lowers the barrier. What previously required a specialist can now be reduced to a developer who understands their own code and can evaluate suggestions.
Putting these two things together: (1) ZK proofs making verification continuous, and (2) AI making specification writing accessible to teams who couldnât previously afford it, and we could see a far more secure onchain future!
Formal verification started as an academic discipline for aerospace and chip design. It became a practical tool for the most security-conscious teams in DeFi. The next step is making it standard practice across the ecosystem to improve security in the space.
Whenever youâre ready, these are the main ways I can help you:
Want high crypto returns? Earn up to 14% APY with your own Yieldseeker agent!
Love Web3 & AI? Follow @afoxinweb3 on X for insights!
Entrepreneur using AI? Join our AI community to accelerate your results!