Skip to content
Quantix Security Labs

Formal Verification

Formal verification expresses critical requirements as mathematical properties and uses tooling to check them against the implementation for all reachable states within a defined model. It complements manual review: it does not replace it. The value lies in writing the right properties, stating the assumptions explicitly, and reporting exactly what was and was not proved.

Machine-checked reasoning about properties that must always hold.

Request an AssessmentWhat a proof does not tell you
Illustration of a timelock state machine on a specification plate, its transitions inside an invariant boundary, discharging into rows of proof obligations that converge on a verified result.

Service overview

A proof is only as good as the sentence it starts from.

Formal verification turns requirements your team already holds into statements a machine can check against the code, for every input and every reachable state within a stated model.

Testing checks the paths you thought of. Verification asks a stronger question: is there any sequence of calls, by anyone, with any inputs, that breaks this property? When the answer is yes, the tool returns a concrete counterexample. When it is no, the property holds for the code in scope under the stated assumptions.

Most of the value is created before any tool runs. Writing a property precisely forces ambiguity in the requirement into the open: what exactly must hold for share accounting, liquidation, or a timelock queue. Properties are written twice, in plain language your team can agree with and in a formal notation a tool can check.

Verification complements manual review; it does not replace it. Every result is reported with the assumptions it depends on and the properties that were not proved.

Best suited to
Accounting cores, vaults, liquidation, timelocks, bridges
Result types
Proved, violated (with counterexample), inconclusive
Handover
Specifications and harnesses you keep in CI

Applies to

  • Core accounting and solvency logic
  • Token and vault share mechanics
  • Lending and liquidation engines
  • Governance and timelock state machines
  • Bridge message validation
  • Protocol upgrades with invariant-preserving requirements
Formal specificationsSMT-based provingBounded model checkingCounterexample analysis
Formal verification workflowA plain-language requirement is written as a formal property, checked against a model of the code that states its assumptions, and the prover returns one of three results: proved within the model, a concrete counterexample, or inconclusive.Requirement“Users can alwaysredeem their share”Formal propertyassets ≥ convert( totalSupply)Model of the codecontracts in scope+ stated assumptionsProver / checkerall reachable stateswithin the modelassumptions are part of the resultProvedholds within the modelCounterexampleconcrete trace → findingInconclusivetimeout → refine or bound

Threats addressed

Failures that only appear on paths nobody tested.

Verification is aimed at the classes of failure where one violated property is catastrophic and the state space is too large to sample.
  • Precision and rounding

    Conservation violations

    Value created or destroyed by rounding, fee accrual or share conversion on some sequence of deposits and withdrawals.

  • First-depositor attack

    Share-price manipulation

    States where the ratio of assets to shares can be pushed far enough that later deposits mint nothing.

  • Business logic

    Insolvency paths

    Sequences of borrows, price moves and liquidations that leave debt uncovered by collateral.

  • Governance manipulation

    Early or repeated execution

    A queued action executed before its delay, executed twice, or executed after cancellation.

  • Access control

    State changed by the wrong role

    Any path, including through a callback or delegatecall, by which an unprivileged caller changes privileged state.

  • Bridge message validation

    Replay and double processing

    A message accepted twice, out of order, or for a destination or nonce it was not signed for.

Technical capabilities

Six kinds of statement that catch most critical bugs.

Properties are written about your protocol, not copied from a template. The notation is shorthand; each property is also stated in plain language.

  • State invariants

    Relationships that must hold between storage variables in every reachable state.

    • totalSupply == Σ balanceOf(a)

  • Conservation

    Value is neither created nor destroyed except by the functions designed to do so.

    • assets_in − assets_out == Δ totalAssets

  • Safety properties

    Something bad never happens, whatever sequence of calls an attacker chooses.

    • executed(id) ⇒ now ≥ eta(id)

  • Access control

    Only the intended roles can change a given piece of state, on every path.

    • Δ fee ⇒ msg.sender == governor

  • Monotonicity and ordering

    Values that may only grow, nonces that never repeat, states that cannot be revisited.

    • nonce' > nonce

  • Equivalence

    A refactored or optimised implementation behaves exactly like the version it replaces.

    • ∀ s, x: v1.f(s, x) == v2.f(s, x)

A governance timelock, simplified. Tests confirm that a queued proposal executes after its delay. A safety property asks whether any sequence of calls, by anyone, executes a proposal early.

Illustrative timelock state machine with a safety propertyA proposal moves from Proposed to Queued, becomes Executable once the timelock delay has passed, and can then be Executed; it can be cancelled while Proposed or Queued. The safety property states that execution is only possible after the delay, which rules out a direct transition from Queued to Executed.S1 safetyexecuted(id) ⇒ block.timestamp ≥ eta(id)I1 invariantdelay ≥ MIN_DELAY in every reachable stateunreachable if S1 holdsqueue()time ≥ etaexecute()cancel()cancel()ProposedQueuedExecutableExecutedCancelled

Assessment methodology

From requirement to machine-checked result.

Every engagement starts with a specification workshop and ends with results you can rerun. Failed properties become findings only after they are reproduced as tests.
The seven-stage Quantix workflow
  1. 01

    Specification workshop

    Agree which properties matter, the contracts and assumptions in scope, and which results would change your launch decision.

  2. 02

    Formal specification

    Requirements written in plain language and in formal notation; ambiguity resolved with your engineers.

  3. 03

    Mathematical reasoning

    Properties decomposed into lemmas about individual functions and transitions, so failures point to a specific step.

  4. 04

    Model checking

    Bounded exploration of call sequences up to a stated depth, returning a concrete trace for any violation.

  5. 05

    Proof-oriented verification

    Inductive proofs that each transition preserves the property, for any number of calls.

  6. 06

    Counterexample analysis and report

    Each violation reproduced as a test, classified as bug or specification error, and reported with assumptions.

What a proof does not tell you.

A verified property is a precise, conditional statement. These are the conditions, and every report states them for the properties it covers.

It proves what was specified, not what was intended
A missing or wrongly stated property is not checked. Reviewing the specification with your engineers is part of every engagement for this reason.
It holds within a model
External contracts, tokens and oracles are modelled with assumptions, for example that a token transfers exactly the amount requested. If reality differs, the result may not carry over.
It covers the code in scope
Contracts added later, configuration set at deployment and the behaviour of integrations outside the model are not covered.
Bounds and timeouts matter
Bounded model checking explores sequences up to a stated depth. Some properties end inconclusive; we report them as such rather than as proved.
It says little about economics
A protocol can satisfy every invariant and still be exploitable through prices, incentives or governance. Those require adversarial and economic review.
The toolchain is part of the trust base
Compiler behaviour, prover soundness and the translation from source to model are assumptions too. We state which tools and versions were used.

Tools & techniques

Tools chosen per property, results you can reproduce.

Fuzzers give fast feedback, provers give unbounded guarantees, model checkers explore call sequences. The report names every tool and version used.
Tools and techniques used for Formal Verification
Tool or techniqueCategoryWhat it is used for
Foundry invariant testsProperty fuzzingFast, stateful exploration of invariants before they are stated for a prover.
Echidna / MedusaProperty fuzzingCoverage-guided long sequences against the same properties, with shrinking to minimal traces.
HalmosSymbolic testingSymbolic execution of Foundry-style tests to check properties for all inputs within bounds.
SMT-based provers (CVL-style rules)Deductive verificationUnbounded rules and invariants over contract state, proved inductively over every function.
hevm / bounded model checkingModel checkingExhaustive exploration of bounded call sequences with concrete counterexamples.
Move ProverMove specificationsPre- and post-conditions, aborts and global invariants for Aptos and Sui modules.
Equivalence checkingUpgrade safetyShows a new implementation behaves identically to the previous one on shared functions.

Properties are code you keep.

Invariants usually start life in a fuzzer, where they fail fast and cheaply. The ones that matter most are then stated as rules for a prover. Specifications and harnesses are handed over with the report so they keep running in your CI. See also Writing invariants that find bugs.

specs/VaultSolvency (illustrative)solidity
// Illustrative: a solvency invariant for an ERC-4626 vault,// first exercised by a fuzzer, then stated as a rule for a prover. function invariant_solvency() public view {    uint256 owed = vault.convertToAssets(vault.totalSupply());    assertLe(owed, vault.totalAssets());} rule withdrawNeverMintsShares(env e, uint256 assets, address receiver, address owner) {    uint256 sharesBefore = totalSupply();    withdraw(e, assets, receiver, owner);    assert totalSupply() <= sharesBefore;}
Illustrative example in Solidity and a CVL-style rule syntax. Real specifications are written against your contracts and toolchain.

Ecosystem coverage

Technical depth per execution environment.

Verification depends on the language and its tooling. EVM chains share most of the toolchain; Move modules are specified with the Move Prover.

Ethereum

Layer 1, proof of stake EVM

Programming languages
SolidityVyperYul
Assessment methodologies
  • Line-by-line manual review
  • Invariant fuzzing (Foundry, Echidna)
  • Symbolic execution and formal verification
  • Economic attack modelling
Typical vulnerabilities
  • Reentrancy, including read-only reentrancy
  • Oracle and spot-price manipulation
  • Access control on privileged functions
  • Proxy storage collisions and initializer misuse
  • Signature replay across chains and contracts
  • Front-running and MEV exposure
Monitoring capabilities
  • Proxy admin and implementation changes
  • Governance proposals and timelock queues
  • Large transfers and treasury outflows
  • Oracle deviation against reference feeds
Supported standards
ERC-20ERC-721ERC-1155ERC-4626EIP-2612EIP-712ERC-1967ERC-4337

Ecosystems indicate technical specialisation only, not partnerships or endorsements.

Deliverables

A precise record of what was proved, and under which assumptions.

Results are reported per property. Nothing is summarised as "verified" without the conditions attached.

  • Written specification

    Every property in plain language and formal notation, agreed with your engineers.

  • Harnesses and rules

    Verification code delivered as a repository your team owns and runs in CI.

  • Per-property results

    Proved, violated or inconclusive, with tool, version, bounds and run configuration.

  • Counterexamples as tests

    Every violation reproduced as a failing test with the minimal call sequence.

  • Assumptions and scope

    Modelling assumptions about tokens, oracles and external calls, and what was not proved.

  • Technical report

    Formal verification results inside a Quantix Technical Security Assessment.

Property results from a research assessment

Fenwick Lending, Quantix research assessment: 10 proved, 1 inconclusive, 1 not in scope.

Open the assessment
Verified properties and results
IDPropertyResult
P-01cash + totalBorrows − totalReserves = Σ supplierAssetsProved
P-02¬badDebtEvent ⇒ exchangeRate′ ≥ exchangeRateViolated on the original commit (FL-02); re-proved after the fix.Proved
P-03borrowIndex′ ≥ borrowIndexProved
P-04health(a) ≥ 1 ⇒ liquidate(a) revertsProved
P-05debt(a) > 0 ∧ collateral(a) = 0 ⇒ isBadDebt(a)Violated on the original commit (FL-01); re-proved after the fix.Proved
P-06transferIn(repay) ≤ debt(a)Violated on the original commit (FL-03); re-proved after the fix.Proved
P-07u₁ ≤ u₂ ⇒ rate(u₁) ≤ rate(u₂), within one unit at the kinkProved with a documented one-unit tolerance (FL-04).Proved
P-08withdrawReserves ⇒ msg.sender = reserveAdminProved
P-09withdraw(a, x) ⇒ x ≤ redeemable(a)Proved
P-10accrue(t₀→t₂) ≈ accrue(t₀→t₁→t₂) within 1 wei per stepHolds for sequences up to 8 accruals; the prover timed out for unbounded sequences.Inconclusive
P-11paused ⇒ supply, borrow and withdraw revertProved
P-12price > 0 ∧ now − updatedAt ≤ heartbeat ∧ sequencerUpAssumption about OracleRouter, not proved (FL-05).Not in scope

Relevant research

Read the work behind the service.

How properties are written, where verification pays off, and the research assessments where it was applied.
Research hub

Publications

Case studies

All case studies

Research assessments

Security assessments library
Compare all services

FAQ

Questions teams ask before an engagement

Not always. It is worth the investment where a single violated property would be catastrophic and the logic is compact enough to specify precisely: accounting cores, vault share mechanics, liquidation engines, bridge message validation. We will tell you if an audit and strong testing are the better use of budget.

We choose tools per engagement: invariant fuzzers for fast feedback, SMT-based provers for unbounded properties, and bounded model checkers where sequences of calls matter. The report lists every tool and version so results can be reproduced.

The tool produces a counterexample: a concrete sequence of calls and inputs. We reproduce it as a test, decide whether it reveals a bug or a mistake in the specification, and report it as a finding when it is a bug.

Yes. Specifications and harnesses are delivered as code you own, so you can run them in CI on every change.

No. It means the stated property holds for the code in scope under the stated assumptions. The report lists those assumptions and what was not proved, so you can judge the residual risk yourself.

Decide which properties must never fail.

Tell us about the system and the outcome you are most worried about. We will propose the properties worth proving and say plainly where testing is enough.

Request an AssessmentSmart contract auditing