AI Formal Verification for Smart Contracts: Costs and Use Cases
How AI formal verification works for smart contracts, what it costs, where it falls short, and how AutoProver performed on Aave V4.
Author:
Certora AI formal verification for smart contracts harnesses artificial intelligence to make formally verifying smart contracts more accessible, scalable, and cost-effective. Formal verification uses mathematical techniques to prove a smart contract satisfies specific requirements, known as properties, under the assumptions of a formal model. A formal specification combines different properties and describes correct behavior for a contract in mathematical language; proving a smart contract satisfies a formal specification proves that certain properties hold, though it cannot establish the contract as a whole is correct.
Writing formal specifications and proving smart contract properties demands specialist expertise and involves considerable time and effort. This puts traditional formal verification out of reach for many development teams. AI can reduce formal verification cost and effort by automating parts of the process that historically required expensive specialist labor. For example, AI agents can generate candidate specifications and verification rules, run provers, and triage proof failures. AI formal verification doesn’t replace human expertise, however, and should ideally be combined with traditional formal verification.
Before adopting AI formal verification, it is important to understand what the technology can realistically accomplish. Business leaders, including CEOs, CTOs, and CSOs, will want to know what guarantees automated formal verification provides, how much it costs, when to use it, and where human oversight and expertise remain necessary. This article provides information to help development teams effectively adopt and use AI-assisted formal verification alongside other software security techniques. For a general introduction to formal verification of smart contracts, see What Is Formal Verification?
What is AI formal verification for smart contracts?
In AI formal verification, AI agents identify candidate properties and invariants, write the formal specification, generate verification rules, and use a prover to verify that a formal model of a smart contract satisfies the specified properties. A property is a formally stated requirement or rule that the execution of a smart contract must satisfy for the contract to behave correctly from the developer’s perspective. An invariant is a property that must hold for all reachable states in a smart contract. AI agents read smart contract code and documentation to infer candidate properties and invariants, which they translate into a specification.
Suppose a developer wants to formally verify a token contract and provides the codebase and, optionally, a design document that describes intended behavior, security assumptions, and threat model. A specialized agent can infer, from reading the code and design document, that the contract must satisfy certain requirements, such as “only authorized users can transfer tokens from an account” and “total circulating supply must equal the sum of user balances”. The first is an authorization property that applies to all token transfers. The second is an invariant that requires the stated relationship between token supply and user balances to hold as the contract’s state changes. The AI agent combines these properties into the formal specification and passes it to the prover.
The prover takes the specification as input and checks whether the modeled contract satisfies the specified properties and invariants. If it finds a violation, it can generate a counterexample showing the input or state under which the contract fails to satisfy a requirement. If verification completes successfully, the prover establishes that the property holds within the assumptions of the formal model and the verification scope.
Failing to find a counterexample is not the same as successfully proving a property. A prover may fail to find a counterexample because it runs out of time or exhausts computational resources, meaning it cannot rule out the possibility that a counterexample exists. Properties may be hard to prove because they are too complex, poorly specified, or have inadequate verification rules. AI agents can help resolve inconclusive verification runs by refining the formal specification, rewriting verification rules, or breaking difficult properties into smaller properties that are easier to prove. These tasks normally require formal methods expertise and involve significant manual effort but can be implemented using AI, though formal verification engineers may be better at executing them.
While AI formal verification is useful for reducing the cost of formal verification, it has limitations that must be acknowledged. AI-generated specifications may omit important requirements or reflect inaccurate assumptions about a smart contract. If a property is missing from the specification, the prover cannot guarantee the contract satisfies that requirement.
How is AI formal verification different from AI code review?
AI code review and AI formal verification can both identify potential security issues in a smart contract. AI code review analyzes smart contract code for potential vulnerabilities and flags identified security issues for review. AI-powered formal verification uses a formal prover to mathematically determine whether a smart contract satisfies specific requirements, such as restrictions on contract operations and permissible contract states. The difference lies in the evidence produced: code review can identify potential logic bugs or design issues, while a completed formal proof establishes that a specific property holds within the verification model and scope.
We can illustrate the distinction using the earlier example of a token contract. The contract allows authorized users to transfer tokens and requires total token supply to equal the sum of user balances. Burning tokens should reduce the total supply, but regular token transfers should leave the total circulating supply unchanged since the tokens still exist. An AI code review can evaluate the transfer function and identify potentially flawed accounting logic that might cause a transfer to increase or decrease the total token supply. But the agent’s assessment doesn’t prove that every possible transfer preserves the total supply. Moreover, if the bug identified by the code review agent is fixed, the developer still has no guarantee that a transfer never creates or destroys tokens.
AI formal verification approaches the problem differently. An AI agent can express the requirement that a successful token transfer must never change the total token supply as a property. The prover evaluates all possible states to determine if this property is ever violated. If a violation is detected, the prover can produce a counterexample to show the sequence of inputs that cause the token supply to change unexpectedly after a transfer.
Same property, two kinds of evidence
If verification completes, the property holds for the modeled transfers, and the strength of that guarantee depends on the verification assumptions (for example, that the onchain code matches the code the prover evaluated) and on the verification scope.
Code review can identify issues that may produce incorrect behavior, even if developers haven’t formally specified the underlying requirement as part of a specification. AI formal verification can provide stronger guarantees that contract logic satisfies specific properties provided that the AI-written formal specification includes those requirements. Neither approach establishes that the entire contract is free from security vulnerabilities, however. Code review and automated formal verification are best used together as part of a smart contract security toolbox that includes other approaches for assessing software correctness such as fuzz testing, unit tests, and audits.
What can AI automate in formal verification, and what still needs experts?
AI agents can automate several tasks in formal verification, such as inferring candidate requirements from code and documentation, generating formal specifications and verification rules, executing property verification, investigating verification failures, and preparing reports for human review. By reducing the manual labor required to complete formal verification, AI agents can make the process cheaper and easier to scale. Development teams may be able to adopt formal verification without immediately hiring specialized engineers or commissioning an expert-led engagement.
However, AI-generated specifications may omit important requirements, misrepresent developer intent, or rely on assumptions that do not reflect the contract’s deployment environment. Human experts can assess whether the specification captures the relevant requirements and whether the verification results provide sufficient evidence for the intended use.
Specialists with formal methods expertise can review codebases to identify the most important properties, assess assumptions and threat models, debug failed or inconclusive verification runs (when AI agents cannot resolve them independently), and perform additional proof engineering for complex properties that cannot be conclusively verified without human intervention. They can also identify and address issues that may undermine formal verification, as discussed in How Formally Verified Code Goes Wrong and How to Catch It.
AI formal verification can complement human-driven formal verification by generating candidate properties, providing formal specifications that engineers can build on, and detecting potential property violations. Developers can use the counterexamples produced by a prover during automated formal verification to understand and patch vulnerabilities before re-running verification to assess correctness. This reduces the work that formal verification engineers have to do and can speed up the engagement. More importantly, AI formal verification can provide a set of verified properties, which allows engineers to focus on more complex requirements that verification agents miss or cannot prove on their own.
When should a smart contract team use AI formal verification?
AI formal verification is useful when a development team wants to assess specific components or interactions in a smart contract for correctness without initiating a full specialist engagement. Development teams can use agentic formal verification in combination with code reviews, unit tests, and fuzz tests conducted in-house, or even treat it as a starting point in a protocol’s security audit process. AI-assisted formal verification can be used to check for regressions after code changes and generate reusable specifications and verification rules that developers can use to continually evaluate correctness as the codebase evolves.
Some examples:
- Before an audit: Automated checks can identify straightforward property violations before external auditors begin their review. Teams can also share existing specifications, verification rules, and results with auditors, giving them a starting point for identifying missing requirements and investigating more complex vulnerabilities.
- During development: Developers can integrate automated formal verification into continuous integration (CI) workflows to verify whether smart contract code still satisfies requirements after bug fixes or code changes. For example, if a token contract’s function is modified, the development team can re-run verification to confirm that it satisfies authorization properties and token-supply invariants.
AI-assisted formal verification can help teams check specific properties, identify violations, and maintain verification rules as their code changes. For systems managing significant liquidity or providing critical infrastructure, expert review is particularly important to assess whether the right properties have been specified and whether the verification results are conclusive.
How much does formal verification cost?
The cost of formal verification varies for each project and depends on the complexity of the codebase, the amount of specialist effort required, and the length of the engagement. A token contract may be cheaper to formally verify than a lending protocol, for example, especially if the former has fewer lines of code (LOC) and straightforward requirements that are easy to translate to properties and formally prove. A team that requires formal verification engineers to maintain specifications and re-run verification as the codebase changes will pay more for ongoing specialist support compared to a one-time engagement. The scope of a formal verification engagement, i.e., components of a smart contract system covered by the audit, also influences formal verification costs, with broadly scoped engagements costing more than engagements with limited scopes.
When evaluating costs, development teams should consider which formal verification tasks should be performed by human experts and those that can be safely automated. For example, it might be easy to use an AI formal verification tool to prove that only authorized administrators can change configuration parameters. In contrast, proving that the lending protocol correctly enforces collateralization and liquidation rules is more difficult and requires formal methods expertise. Given that proper collateralization and liquidation matter for solvency, it makes sense to have formal verification engineers verify that property. Automated tools can reduce the amount of manual work required, but they may generate incomplete specifications or fail to prove a property. The resulting specifications and verification results should be reviewed before they are relied on, particularly for properties that affect protocol solvency.
Development teams looking to work with dedicated formal verification engineers are encouraged to obtain a project-specific quote based on their requirements. They can also evaluate public DAO proposals submitted by security companies to get a sense of how much a formal verification engagement (of a certain scope and duration) costs. An October 2025 proposal submitted to Aave DAO quoted $2.39 million for 12 months of continuous security work to support the Aave V4 deployment. The proposed engagement covers formal verification, manual audits, and fuzz testing, so the quoted figure should not be treated as the cost of formal verification alone. The proposal illustrates the cost of a broad, year-long security engagement but does not provide a separate price for formal verification.
What does AI formal verification look like in practice? AutoProver on Aave V4
Certora tested AutoProver against the Aave V4 Hub, a key component of Aave V4’s lending infrastructure that manages shared liquidity and accounting operations. AutoProver independently generated 104 verification rules covering basic contract behavior and important accounting requirements. It also wrote properties that made the same assertions as P-04 and P-05 (properties from Certora's formal verification audit of Aave V4), enforcing critical invariants such as bounds on accounting and configuration values and consistency between the Hub’s aggregate asset totals and the Spokes’ recorded amounts. Crucially, AutoProver was able to perform these tasks without access to original specifications written by Certora engineers.
To understand what AutoProver achieved, consider how Aave V4 tracks deposits with shares. Suppose five users each deposit 1 ETH into a lending pool and collectively receive five shares, with one share initially representing a claim on 1 ETH. The amounts backing those shares can increase as loans accrue interest. For example, if the amount owed to depositors grows from 5 ETH to 6 ETH, each of the five shares now represents a claim on 1.2 ETH instead of 1 ETH. Note that this is a simplified illustration of share accounting, not a precise description of the Hub’s share-minting mechanism.
The Hub has two important accounting-related requirements:
- The value backing a share added to the Hub must never fall below one unit of the underlying asset.
- The value of each share must never decrease because of routine contract operations such as deposits, withdrawals, and transfers.
These requirements look similar but are different in practice. Suppose interest accrued by the lending pool increases the value of each share from 1 ETH to 1.2 ETH, but an accounting error subsequently reduces the value per share to 1.1 ETH. The Hub would still satisfy the first requirement because each share would be worth more than 1 ETH. But the change in value per share, from 1.2 ETH to 1.1 ETH, would violate the second requirement, which prohibits unexpected decreases in share price during routine contract operations.
A minimum share value doesn’t guarantee it never decreases
In Certora’s experiment, AutoProver formalized the first requirement as a property and successfully proved it: the property corresponded to one half of the P-06 property that Certora engineers specified and manually proved. It also developed supporting verification rules and divided the property into smaller parts to resolve verification failures that emerged while trying to prove the original property. However, AutoProver could not conclusively prove the second property, which corresponds to the other half of P-06, within the available compute budget. It did generate a verification rule that would have helped prove the property if the run hadn’t ended prematurely, though.
The second property requires the value of shares to increase monotonically, i.e., a share can increase in value, or remain constant, but it never decreases during relevant contract operations. AutoProver proved that “V ≥ 1 ETH” always holds, but couldn’t prove that “V(after) ≥ V(before)” always holds, where V represents the value of a share. This means AutoProver established that shares retain a minimum value without equally establishing that shares never unexpectedly lose value. The difference matters because a decrease in per-share value, for example, from 1.2 ETH to 1.1 ETH, would reduce each depositor’s claim by 0.1 ETH without violating the minimum-value requirement.
Formal verification engineers from Certora had identified two accounting issues that could induce property violations (M-01 and M-02). The property AutoProver proved would have caught the same vulnerability specified in M-02, which would have caused the share price to fall below the minimum. However, M-01 could reduce the per-share value without necessarily pushing it below the required threshold. AutoProver would need to prove the monotonicity property to detect the vulnerability in M-01, but it couldn’t complete the proof within the allotted time.
The Aave V4 experiment shows that AutoProver can generate verification rules for important properties and complete some of the proof engineering involved in formal verification. It also shows the limits of automation: AutoProver did not conclusively prove the share-value monotonicity property within the available compute budget. The results therefore need to be assessed alongside the requirements being checked and any properties that remain unproven.
How much does Certora’s AutoProver cost?
AutoProver combines subscription plans with usage-based pricing for automated formal verification runs. The Free plan supports a single user and doesn't have a subscription fee, though runs are paid for separately. The Pro subscription supports more users and offers discounts on verification runs. The Enterprise plan supports unlimited seats per organization and provides custom discounts and committed credits.
Here's a breakdown based on AutoProver’s pricing page:
Subscription plus usage-based runs
API access and CI integration are also available for users, with the option to run verification through the AutoProver API depending on the plan. Some other things to know about pricing and costs:
- Annual billing saves 17% on eligible subscriptions.
- Users pay for runs with credits from an organization’s balance.
- The estimated cost of a run is shown in the UI before agents start working.
- The final amount billed depends on work performed during a run.
- If the final charge is lower than the estimated cost, unused credits are added to the balance.
AutoProver’s pricing model makes it easy to try out AI formal verification without making a huge upfront commitment. A Free plan may be useful for testing AI-assisted verification on small contract modules to understand how the system works and what it can do. A Pro subscription becomes useful when a team is comfortable with agent-driven formal verification and wants to scale up security reviews. An Enterprise plan might make sense for protocol teams with more resources and significantly more funds at stake: beyond getting priority support, they can run automated formal verification more frequently, take advantage of bespoke pricing, and access expert support as needed.
How to get started with Certora’s AutoProver
To get started, create an account at app.certora.com and select the GitHub repository that contains the smart contract you want to formally verify. You can provide existing documentation, or a plain-language design document that describes intended code behavior. This is entirely optional, as AutoProver can automatically infer intent and write properties that correlate with intended behavior. After selecting a contract and reviewing the estimated cost, you can launch a verification run.
For each verification run, AutoProver generates a report that says which properties were verified and which it could not. You can see which requirements were included in the formal specification along with the verification rules the Certora Prover used to establish that a contract’s code satisfies those requirements. AutoProver currently supports verification of Solidity contracts, with support for contracts written in Rust, C, C++, Go, and Java in development.
Formal verification isn’t the only thing you can do on the AutoProver platform. The app offers an AI auditor for agentic code reviews and AutoFuzzer for running property-based fuzz tests. Teams can select the All in one option to combine formal verification, fuzzing, and code review in a single run, thereby adopting a robust and multi-layered approach to assessing software correctness. See the AutoProver user manual for more detailed instructions.
Get started with AutoProver’s Free plan and follow Certora on X/Twitter and LinkedIn for product updates.
Frequently asked questions
What is AI formal verification for smart contracts?
AI formal verification uses AI agents to infer a smart contract’s requirements from its code and documentation, write the formal specification and verification rules, and run a prover that checks whether the contract satisfies them. Each property the prover proves holds within the assumptions and scope of the formal model.
How is AI formal verification different from AI code review?
AI code review flags potential vulnerabilities for a person to assess. AI formal verification uses a prover to determine mathematically whether a contract satisfies a specific property, and it produces a counterexample when the property fails. A completed proof establishes that the property holds within the verification model and scope. Neither approach shows that an entire contract is free of vulnerabilities.
Can AI replace formal verification engineers?
No. AI agents can infer candidate requirements, generate specifications and verification rules, run the prover, and investigate failures. AI-generated specifications can still omit requirements or rely on wrong assumptions, and some properties cannot be proven without human proof engineering. Experts check whether the specification captures the right requirements and whether the results are conclusive.
How much does AutoProver cost?
AutoProver combines subscriptions with usage-based pricing for verification runs. The Free plan costs $0/month for 1 seat, with runs billed at standard rates. Pro costs $120/month for up to 5 seats and takes 10% off runs. Enterprise starts at $3,000/month with unlimited seats, custom discounts and committed credits. Annual billing saves 17% on eligible subscriptions, and the estimated cost of each run is shown before agents start. [Pricing as of November 2026.]
When should a smart contract team use AI formal verification?
Use it to check specific components or interactions without a full specialist engagement. Before an audit, it can catch straightforward property violations and give auditors existing specifications to build on. During development, it can run in continuous integration to confirm that code changes still satisfy requirements. For systems that manage significant liquidity or provide critical infrastructure, expert review is particularly important.
