Testing tells you that your code works for the cases you tested. Formal verification tells you that your code works for every possible case. In a domain where a single edge case can drain millions, that distinction matters.
As we noted in The State of Web3 Security in 2026, formal verification is moving from academic exercise to mainstream practice. Here's what you need to know.
What Is Formal Verification?
Testing vs Formal Verification
Testing
Run the code with specific inputs and check the outputs. Covers the cases you thought of. "I tested 1,000 scenarios and none of them broke." Does NOT guarantee the 1,001st scenario is safe.
Formal Verification
Define mathematical properties that must always be true (invariants). Prove that no possible input or state can violate these properties. "No possible execution path can break this property." Provides mathematical certainty for the properties you specify.
ℹ️The Key Limitation
Formal verification proves that code matches its specification. It does NOT verify that the specification is correct. If your spec says "users can withdraw funds" but doesn't specify "only their own funds," formal verification will happily prove the insecure code correct. The specification is where human expertise remains essential.
The Tools
Tool
- •Certora Prover
- •Halmos
- •HEVM
- •Solidity SMTChecker
Best For
- •Custom invariant verification, most widely used in DeFi
- •Symbolic testing in Foundry — lower barrier to entry
- •Symbolic execution for Solidity with ds-test integration
- •Built into the compiler — lightweight but limited
What to Verify
Not everything needs formal verification. Focus on the properties where a violation means financial loss:
Invariants
Properties that must ALWAYS be true: total supply equals sum of balances, user can't withdraw more than deposited, health factor never below 1
State Transitions
Valid sequences: only specific functions can change specific state variables, state machine transitions are valid
Arithmetic
No overflow in unchecked blocks, division never by zero, precision loss within acceptable bounds
Access Control
Only authorized roles can call privileged functions, no privilege escalation paths exist
Key Invariants for DeFi
Critical Invariants by Protocol Type
Lending protocols
Total borrows never exceed total deposits plus reserves. Health factor is always checked before allowing new borrows. Liquidation always improves protocol solvency. Interest accrual is monotonically increasing.
AMMs / DEXs
Constant product invariant (x * y = k) holds after every swap. LP share value is monotonically non-decreasing (excluding impermanent loss). Fees are correctly accrued and never exceed the swap amount.
Vaults / Staking
Total shares represent total assets accurately. Deposit and withdrawal preserve the share-to-asset ratio. No single operation can dilute or inflate share value beyond a threshold.
The Practical Approach
Level 1: Property-Based Testing (Fuzzing)
The lowest barrier to entry. Use Foundry's fuzzing to test invariants with random inputs:
💡Start Here
If you've never done formal verification, start with Foundry invariant testing. Write functions that assert your critical invariants, and let the fuzzer try to break them. This catches most of what full formal verification catches, with 10% of the effort.
Level 2: Symbolic Testing (Halmos)
Halmos executes your Foundry tests symbolically — instead of testing with random values, it tests with symbolic values that represent ALL possible inputs. If a test passes symbolically, it passes for every possible input.
Level 3: Full Formal Verification (Certora)
Certora's CVL (Certora Verification Language) lets you write formal specifications that are checked against your Solidity code. It handles complex properties across multiple functions and state transitions.
When You Need Formal Verification
Fuzzing Is Sufficient
- •Simple token contracts
- •Low TVL protocols (under $1M)
- •Standard OpenZeppelin-based contracts
- •Non-financial NFT contracts
Formal Verification Recommended
- •Lending and borrowing protocols
- •Protocols with complex financial math
- •Bridge contracts holding locked assets
- •Any contract managing over $10M in TVL
Common Pitfalls
Verifying the wrong properties
Your invariants cover arithmetic correctness but miss access control. The code is mathematically perfect but anyone can call the admin functions.
Incomplete specifications
You verify that withdrawals work correctly but don't specify behavior during reentrancy. The formal verification passes, but the contract is still vulnerable.
Environment assumptions
Your specification assumes msg.sender is always an EOA. But contract wallets and flash loan callbacks mean msg.sender can execute arbitrary code during the call.
Verification of outdated code
You formally verify version 1.0, then make changes for version 1.1 without re-verifying. The proof no longer applies to the deployed code.
Formal Verification in the Audit Process
At RedVolt, we integrate formal verification into our audit workflow:
- AI static analysis identifies potential invariant violations and suggests properties to verify
- Fuzzing tests invariants with randomized inputs to catch obvious violations quickly
- Formal verification proves critical properties for high-value contracts
- Human review validates that the specifications are correct and complete — as we discussed in How RedVolt Combines AI with Human Expertise, human judgment in defining what to verify is irreplaceable
As outlined in our Solidity Security Patterns handbook and smart contract checklist, formal verification is one layer in a comprehensive security strategy — not a replacement for manual audit.
Want formal verification as part of your smart contract audit? Our Smart Contract Auditor includes property-based testing, and our expert review offers full formal verification for high-value protocols. Discuss your needs.