How to Formally Verify a Smart Contract

Verifying a Token Form Step by Step

The following walkthrough demonstrates algebraic verification applied to a Token form. The goal is to prove that the conservation invariant sum(balance) == supply holds across every transition.

Step 1: Define the Form

form Token {
  state {
    balance : Nat per Address
    supply  : Nat
    owner   : Address
  }

  invariant conservation :
    sum(balance) == supply
}

The Form declares three state fields and one invariant. The balance field is a mapping from addresses to natural numbers. The supply field is a scalar. The invariant states that the sum across all entries in the balance mapping must equal supply at all times.

Step 2: Define Transitions

transition transfer(from, to, amount) {
  require balance[from] >= amount
  balance[from] -= amount
  balance[to]   += amount
}

transition mint(to, amount) {
  require msg.sender == owner
  balance[to] += amount
  supply      += amount
}

transition burn(from, amount) {
  require balance[from] >= amount
  balance[from] -= amount
  supply        -= amount
}

Each transition modifies state variables. The compiler must prove that conservation holds after each one.

Step 3: Compiler Extracts Proof Obligations

For each transition, the compiler computes the post-state of every variable referenced in the invariant and substitutes into the invariant expression.

Transfer: sum(balance') = sum(balance) - amount + amount = sum(balance) = supply = supply'. The net change to the sum is zero. Supply is unchanged. The obligation sum(balance') == supply' holds by arithmetic cancellation.

Mint: sum(balance') = sum(balance) + amount and supply' = supply + amount. Both sides increase by the same delta. The obligation holds because sum(balance) + amount == supply + amount follows from the pre-state invariant sum(balance) == supply.

Burn: sum(balance') = sum(balance) - amount and supply' = supply - amount. Both sides decrease by the same delta. The same reasoning as mint applies in reverse.

Step 4: Proof Obligations Discharged

All three transitions preserve the conservation invariant. The compiler has proven that for any initial state satisfying sum(balance) == supply, and for any sequence of valid transitions, the invariant continues to hold. This proof covers all possible addresses, all possible balance values, and all possible orderings of transactions.

Step 5: Invariant Erasure and WASM Emission

Because the invariant is proven to hold universally, there is no need to check it at runtime. The compiler erases the invariant annotation from the output, producing WASM that contains only the transition logic. The result is a smaller, faster binary with zero runtime verification overhead.

Choosing the Right Approach

Model checking is best for protocols with finite state and complex temporal properties (liveness, fairness). Theorem proving is best when you need to verify arbitrary specifications and have the expertise and time to write proofs. Abstract interpretation is best for rapid, automated detection of common vulnerability classes in existing codebases. Algebraic verification is best when your critical properties are algebraic (conservation, access control, bounds) and you want the verification to be fully automated, integrated into the build process, and imposing zero runtime cost.

These approaches are not mutually exclusive. A project might use abstract interpretation for rapid screening, algebraic verification for core invariants, and theorem proving for a particularly subtle protocol property. The key is matching the verification technique to the property being verified.

Frequently Asked Questions

What is the difference between formal verification and auditing?

Auditing is a human review process that depends on the auditor's skill and time. Formal verification uses mathematical proof to demonstrate that specific properties hold for all possible executions. An audit might miss a subtle edge case. A verified property is proven to hold regardless of inputs or state. However, formal verification only covers properties you specify, while an auditor may spot issues you did not think to check. Read more about alternatives to smart contract audits.

How long does it take to formally verify a smart contract?

It depends on the approach. Theorem proving can take weeks to months. Model checking requires building a model and can take days. Abstract interpretation tools run in seconds but check a narrower set of properties. Algebraic verification through Formagine runs at compile time, typically completing in seconds, because proof obligations reduce to arithmetic identities.

Can I verify an existing Solidity contract with Formagine?

Formagine verifies Forms, not Solidity contracts. The verification is integrated into the language and compiler. To use Formagine, you define your contract as a Form with explicit state, invariants, and transitions. Existing Solidity logic would be rewritten as a Form definition, making invariants explicit so the compiler can prove them.

What properties can formal verification prove about smart contracts?

Safety properties (something bad never happens), liveness properties (something good eventually happens), and functional correctness (outputs match the specification). Specific examples include conservation of funds, access control enforcement, absence of integer overflow, state machine correctness, and reentrancy safety. The scope depends on the approach chosen.

Related Topics

Resources