Formal Verification Smart Contracts: What to Fund and What a Proof Leaves Out

What a proof proves

Formal verification checks a precise property of a program against a mathematical model and stated assumptions.

For readers comparing formal verification smart contracts services with a conventional audit, the first question is which property matters to the release decision. A proof of an irrelevant property can be correct while leaving the dangerous behavior unexamined.

The Ethereum developer guide distinguishes specifications from the verification techniques used to check them.

A specification says what must hold. The technique determines how the claim is investigated. Neither the tool name nor the presence of a proof file tells a buyer whether the desired property was expressed correctly.

Program

The exact source or bytecode revision to which the result applies.

Property

A statement about permitted states or behavior, expressed precisely enough to check.

Assumptions

Conditions the proof accepts rather than establishes.

Result

The outcome for the stated property under those conditions, including any unresolved analysis.

Consider an accounting rule that a user's withdrawal must not exceed the balance they are entitled to redeem.

The specification must define entitlement, the state before withdrawal and the effect of other calls. If it excludes a state reachable through liquidation, the result may say little about that omitted path. The equation needs a model of the application, not just a plausible name.

A counterexample gives inputs or a path that violates the encoded property.

It may reveal a contract defect, a mistaken specification or an unrealistic environment model. Investigate which interpretation applies before assigning severity. A failing proof is useful evidence, but it is not automatically a confirmed exploit.

A successful result also needs a status explanation.

Ask whether the tool established the requested property, exhausted a bounded search or stopped with unresolved obligations. Timeouts and unsupported operations belong in the report. Silence about them makes the result harder to interpret.

Our Halmos census: the example configuration is part of the evidence

We inspected all 21 example test files in the measured Halmos revision and counted 42 check_ declarations plus 6 invariant_ declarations. Local Halmos options occur in 18 files. The census shows where a reader must look for execution settings. It does not report whether any property passed.

Method

Source

a16z/halmos at the measured revision

Retrieved

September 5, 2026

Population and selection

All examples/**/*.t.sol blobs. Count check_ and invariant_ function declarations after removing comments. Count local @custom:halmos annotation occurrences separately in raw source. No proofs executed. Annotations are not global bounds and inherited tests are not resolved.

All repository files

219

Non example test files

198

Included test files

21

Revision

079bb4241d1b460baf986257d56ea86977d73451

Results

Limits

• We counted static source and did not run a solver. Proof status remains unknown for every file.
• An absent local annotation does not imply absent bounds. Configuration files, inherited tests and tool defaults can still affect execution.
• Function counts do not deduplicate semantic properties or measure their strength. A single declaration may exercise complex behavior, while several may overlap.
• This is one tool's example directory, not a benchmark against Certora or Kontrol and not a sample of production verification engagements.

The reproducible script is seo/research/formal-example-survey.py. The fixed evidence is seo/research/formal-example-survey-2026-09-05.json.

Both are kept in the repository and are not published as downloads. The output retains request statuses and raw evidence so a later review can distinguish a source change from a counting error.

Specification errors and out-of-scope invariants

An assumption can remove the very behavior a reviewer intended to examine. Suppose a specification assumes only authorized callers without proving how authorization is enforced. It may establish accounting behavior for authorized calls while missing the access-control defect that admits an unauthorized caller. The proof is conditional on a premise the deployment does not guarantee.

Review assumptions as carefully as assertions. A useful specification review asks where each premise comes from, whether production enforces it and what evidence shows the excluded states cannot occur. If the premise is a business expectation rather than a contract guarantee, make that dependency visible in the release decision.

Vacuous success is another concern: the property may hold because its preconditions admit no relevant execution. Include sanity checks showing that intended ordinary states remain reachable in the model. Review a representative successful operation and a deliberately invalid one so the harness demonstrates that it can distinguish them.

For economic properties, name the environment. A contract can preserve an internal arithmetic relationship while consuming an incorrect oracle value. Proving the relationship does not prove the price reflects a market. Our oracle manipulation guide explains the separate evidence needed for price and timing assumptions.

Do not turn every audit recommendation into a theorem. Some questions are about key custody or a human response process. These may influence the assumptions of a verification task without becoming properties of the contract. Keep the operational review linked to the proof boundary.

Release artifact

Identify the program revision that the proof concerns.

Property model

Write the desired property and the assumptions accepted by the model.

Execution scope

Preserve bounds and configuration governing the analysis.

Interpreted result

State what was established and which obligations remain unresolved.

Cost bands from published engagements

A published engagement proposal is a scope-specific observation, not a current market price. The Aave continuous formal verification proposal, posted on November 20, 2021, includes ongoing work and support. Its figures help show what a substantial program can contain, but they do not price a standalone token proof today.

These are proposal terms as published, not evidence here of execution or a paid invoice. The source describes activities beyond running a solver, including rule development and a community program. Comparing its total with the price of a short manual audit would conceal those differences. No present-day price band is established by this historical example alone.

Build a quote around work packages instead. Ask separately about specification development, modeling dependencies and resolving proof failures. Include review of assumptions and the maintenance needed when code changes. A license price without the engineering effort can understate the cost of obtaining a result the team can use.

Specification work

Translate the intended behavior into properties and review them for omissions.

Harness and models

Represent deployment state and external interactions in the tool's environment.

Proof investigation

Resolve counterexamples and distinguish tool limitations from program defects.

Maintenance

Update specifications and rerun checks when relevant code or assumptions change.

For a constrained budget, propose a narrow pilot on a high-consequence property with a clear acceptance artifact. Ask what the pilot excludes and which conditions would justify expansion. A quoted property count is not comparable unless the properties have similar scope and complexity.

The smart contract audit RFP guide gives a structure for comparable proposals. Formal verification should have its own deliverables in that scope statement, including result status and assumptions. Avoid accepting formal verification included as an undefined line item.

Tools: Certora, Halmos, Kontrol and KEVM

Choose a tool by the property and model it can express, then assess the evidence it produces. The Halmos repository describes a symbolic testing tool for EVM contracts using a Solidity and Foundry frontend. Its getting-started guide demonstrates symbolic inputs and assertions. Familiar test syntax can help a team reuse knowledge, but the specification still needs review.

Kontrol's documentation describes verification of EVM contracts through Foundry-style tests and compositional symbolic execution. It identifies KEVM as its formal bytecode semantics and discusses support for lemmas and loop invariants. These capabilities describe the tool. They do not establish a successful result for a particular protocol.

The Ethereum guide describes Certora's use of CVL for specifications. Treat this as a different specification workflow from writing a Solidity test, not as a ranking. A fair comparison would use the same property and environment and report unresolved cases. This article did not run such a benchmark.

Halmos' FAQ explains that solver timeouts can affect observed runs. Record exact options and tool versions with results. A result that changes after a timeout adjustment needs investigation. It should not be described as the program changing when the source and configuration stayed the same.

The example census above makes this reporting need concrete: local options are common within the measured example set. It does not establish that other files run without bounds, because repository configuration or defaults may apply. Preserve configuration files alongside the local annotations rather than choosing whichever setting makes a summary look strongest.

Which member firms offer relevant work

Use the directory to build a shortlist, then require direct evidence of the proposed verification work. A firm may list formal verification alongside manual auditing without committing to specification development for your architecture. An offered service and a completed proof are different evidence types.

The Certora company analysis is a starting point for examining a provider associated with formal verification. The provider's own public reports let a buyer look for relevant prior scope. Read the specific report and its assumptions before concluding that experience with one protocol transfers to another.

Cyberscope's retrieved service navigation also lists formal verification, while Trail of Bits describes software assurance work and publishes its assessment archive. Those observations establish publicly described offerings and artifacts, not the personnel or method available for a new engagement. Ask each candidate to name the work it will actually perform and show a relevant example.

The security firm directory can help locate additional candidates. Keep availability and pricing as open questions until the bidder confirms them. A report delivered by a firm in the past is not a promise that the same team or commercial arrangement is available now.

Specify ownership and access to the artifacts. The protocol team needs enough information to understand the result after the engagement ends. If a proprietary environment is involved, ask what can be rerun independently and what requires continued access to the provider's service.

A decision rule for funding verification

Fund verification when a consequential security question can be written precisely and the team can supply a credible model. A repeated accounting operation, a permission boundary or a high-value state transition may be a suitable candidate. The decision should explain why the property matters and how the result changes release confidence.

Start elsewhere when the design is still undefined. If the team cannot explain intended behavior, a proof engineer must first help create the specification. That work may be valuable, but it should be named and budgeted as such. Formal notation cannot repair an unresolved product rule by itself.

1. Identify a failure whose consequences justify focused investigation. Write the user or asset impact in ordinary language.
2. Translate that concern into a candidate property and list the environment assumptions it needs.
3. Have another reviewer challenge the property for omitted paths and vacuous success before extensive proof work.
4. Run a bounded pilot with an agreed artifact: specification, configuration and interpreted result tied to a revision.
5. Decide whether to expand based on unresolved risk and the work required, then define a maintenance trigger for future changes.

Combine the result with a manual audit and appropriate testing. Our smart contract fuzzing guide discusses another way to investigate properties through generated executions. These methods can inform each other: an audit finding can become a property, and a counterexample can become a regression test.

Keep the final claim narrow enough to be checked. State the property, revision and assumptions, followed by the result and remaining limitations. A team that can explain that sentence has evidence it can maintain. A badge saying formally verified without those details leaves the buyer guessing.

Define a response to each possible pilot outcome before the work begins. A counterexample should lead to investigation of code and specification. An unresolved obligation should lead to a stated limitation or a separately priced next step. A successful result should be attached to its exact property and assumptions, then considered alongside the other evidence for release. This prevents the procurement process from treating every non-failing output as success.

Ask the team to demonstrate that the property detects a deliberately introduced violation in an isolated copy of the program. Such a check is not a proof of the specification's completeness, but it can reveal an ineffective assertion or a harness that never reaches the relevant operation. Keep the altered fixture clearly separate from the release artifact.

A maintenance plan should identify changes to assumptions as well as changes to code. An oracle dependency, governance route or deployment parameter can alter the relevance of an earlier model without editing the verified function. Have an owner review those changes and state whether the existing result still supports the intended claim.