What Is Compile-Time Verification for Smart Contracts?

Compile-time verification proves that a smart contract satisfies its declared properties during compilation, before the contract is deployed or any transaction is executed. The compiler analyzes each state transition, extracts proof obligations from the declared invariants, and discharges them through algebraic reasoning. Once an invariant is proven, its annotation is erased from the output binary. The resulting WASM contains only the transition logic with zero runtime verification overhead. This is categorically stronger than runtime checks, which detect violations only after they occur and cost gas on every transaction regardless of whether a violation is possible.

Three Stages of Verification

Smart contract properties can be verified at three different stages. Each stage offers different tradeoffs between when bugs are caught, what guarantees are provided, and what runtime cost is incurred.

Compile-time verification catches bugs before the contract is deployed. The proof covers all possible inputs, all possible states, and all possible sequences of transactions. If the contract compiles, the invariant holds universally. There is no gas cost because the proven property is erased from the output.

Runtime verification catches violations during transaction execution. In Solidity, this takes the form of require statements, assert statements, and modifier checks. Each check executes on every transaction that reaches it, consuming gas. If the check fails, the transaction reverts. The user pays gas for the failed computation, and the contract is left in its pre-transaction state. Runtime checks are necessary for conditions that depend on external inputs (such as whether the caller has sufficient balance), but they are redundant for properties that can be proven statically.

Post-deployment verification monitors the deployed contract for anomalous behavior. Tools like Forta, Tenderly, and OpenZeppelin Defender watch transactions and emit alerts when suspicious patterns are detected. This is useful for catching issues that neither compile-time nor runtime verification can address, such as oracle manipulation, MEV attacks, or governance anomalies. However, by the time a post-deployment monitor fires, the damage may already be done.

Why Catching Bugs at Compile Time Is Categorically Better

The difference between compile-time and runtime verification is not just earlier detection. It is a difference in kind.

A runtime check says: "if this property is violated, revert." A compile-time proof says: "this property cannot be violated." The runtime check implies the violation is possible and provides a recovery mechanism. The compile-time proof eliminates the violation from the space of possible behaviors. There is nothing to recover from because the bad state cannot be reached.

This matters because smart contracts are immutable once deployed. A runtime check that reverts prevents damage in the specific transaction, but the vulnerability remains in the contract code. An attacker can keep trying different inputs and sequences until they find one that bypasses the check or exploits a different path. A compile-time proof closes the entire class of vulnerability permanently.

Invariant Erasure: Zero Runtime Cost

When the Formagine compiler proves that an invariant holds across all transitions, it erases the invariant annotation from the intermediate representation before generating WASM. The final binary contains no assertion instructions, no conditional branches for invariant checks, and no error handling code for invariant violations.

This is sound because the compiler has already demonstrated that no execution path can violate the invariant. Checking it at runtime would be redundant. Erasing it produces a smaller binary that executes faster and consumes less gas per transaction.

-- Source Form (what you write)
form Token {
  state { balance : Nat per Address; supply : Nat }
  invariant conservation : sum(balance) == supply

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

-- Compiled WASM (what deploys)
-- Only the transition logic remains.
-- The invariant has been proven and erased.
-- No runtime check for sum(balance) == supply.
-- The require clause remains: it guards a precondition,
-- not a proven invariant.

Note the distinction between require clauses and invariants. A require clause is a precondition that depends on the caller's input (does the sender have enough balance?). It must remain in the runtime because the answer depends on the specific transaction. An invariant is a global property of the state space that the compiler can prove universally. Only the invariant is erased. The require clause stays.