Invariant Algebra

An invariant is a predicate over the state that must hold after every transition. The compiler classifies each invariant by its algebraic structure and applies the corresponding proof method. There are five invariant classes: conservation, monotonicity, access control, boundedness, and state machine. Each class reduces to a specific algebraic verification technique, which is why the compiler can discharge proof obligations mechanically without requiring user-supplied proofs.

Invariant Declaration Syntax

Invariants are declared with the invariant keyword, followed by a name, a colon, and a predicate expression. The predicate is a boolean expression over state variables, aggregation functions, and logical connectives.

invariant conservation :
  sum(balance) == supply

invariant time_lock :
  withdraw => block.time >= lock_until[msg.sender]

invariant no_overflow :
  supply <= MAX_SUPPLY

invariant monotonic_counter :
  nonce' >= nonce

invariant phase_ordering :
  phase only advances

The compiler examines the structure of the predicate to classify the invariant. Classification is unambiguous: a predicate involving sum() equality is conservation, a predicate with '>= previous is monotonicity, and so on. If a predicate does not match any recognized class, the compiler rejects it with a diagnostic indicating the unsupported pattern.

Class 1: Conservation

Form

invariant name : sum(x) == y -- where x : T per Address (or Map(K, T)) -- and y : T (a scalar of the same numeric type)

A conservation invariant asserts that the aggregate of a mapped variable equals a scalar variable. The canonical example is sum(balance) == supply in a token form. Conservation is the most common invariant class in financial contracts, where it ensures that value is neither created nor destroyed except through designated paths.

Proof Strategy

For each transition, the compiler computes the net change to sum(x) and to y, then checks that the two deltas are equal. The computation works as follows.

Let a transition modify entries x[a1], x[a2], ..., x[ak] by deltas d1, d2, ..., dk and modify y by delta dy. The compiler derives:

-- Conservation proof obligation: sum(x') = sum(x) + d1 + d2 + ... + dk y' = y + dy -- Prove: d1 + d2 + ... + dk == dy -- Example: transfer(from, to, amount) -- x[from] -= amount => d1 = -amount -- x[to] += amount => d2 = +amount -- supply unchanged => dy = 0 -- Check: -amount + amount == 0 => 0 == 0 QED -- Example: mint(to, amount) -- x[to] += amount => d1 = +amount -- supply += amount => dy = +amount -- Check: +amount == +amount QED

The proof reduces to an arithmetic identity over the deltas. No runtime evaluation is needed. The compiler performs symbolic cancellation on the delta expressions and checks that the result is the identity element (zero). If it is, the invariant is proven for that transition and no code is emitted for it.

When Conservation Fails

If a transition modifies x[a] without a corresponding change to y, the delta check fails. The compiler reports the transition name, the computed deltas, and the non-zero residual. For example, if a transition increments balance[to] without incrementing supply, the compiler reports: "transition 'free_mint' changes sum(balance) by +amount but changes supply by 0; conservation violated with residual +amount."

Class 2: Monotonicity

Form

invariant name : x' >= x -- where x : Nat or Int -- x' denotes the post-transition value of x

A monotonicity invariant asserts that a state variable never decreases. The canonical examples are nonces (which must strictly increase to prevent replay), counters, and accumulated totals. Monotonicity is also important for governance contracts where vote counts must never be decremented.

Proof Strategy

For each transition, the compiler examines every assignment to x. If the transition does not modify x, the invariant holds trivially (x' = x >= x). If the transition modifies x, the compiler checks that the update is of the form x += delta where delta >= 0, or x = expr where the compiler can prove expr >= x from the transition's preconditions.

-- Monotonicity proof obligation: -- For each transition that modifies x: -- Prove: x' >= x -- Case 1: x += delta where delta : Nat -- x' = x + delta >= x (since delta >= 0) QED -- Case 2: x = x + 1 -- x' = x + 1 > x >= x QED -- Case 3: x -= delta => FAILS monotonicity -- x' = x - delta < x when delta > 0

The proof reduces to showing that every assignment to the variable is non-decreasing. If any transition contains a decrement, the monotonicity invariant is rejected for that variable.

Class 3: Access Control

Form

invariant name : transition_name => msg.sender == authorized_address -- Equivalently expressed as a require in the transition body: transition admin_action() { require msg.sender == owner -- ... state updates ... }

An access control invariant restricts which addresses may invoke a transition. The invariant is expressed either as a top-level implication (the transition implies a caller identity check) or equivalently as a require clause within the transition body. The compiler treats both forms identically.

Proof Strategy

The compiler verifies that every execution path reaching the state mutations of the guarded transition passes through a require msg.sender == authorized_address check. This is a structural property of the transition's control flow, not an arithmetic proof. The compiler constructs the set of preconditions that dominate the mutation block and checks that the identity comparison is in the dominator set.

-- Access control proof obligation: -- For transition t guarded by msg.sender == addr: -- Prove: all paths to state mutations in t pass through -- the require msg.sender == addr check. -- Example: mint(to, amount) with require msg.sender == owner -- The require is the first statement in the transition. -- All subsequent statements are dominated by the require. -- Therefore all mutations are reachable only when -- msg.sender == owner holds. QED

Because msg.sender is a runtime context value, the require clause is never erased. It compiles to a WASM instruction that checks the caller address and aborts the transaction if the check fails. The invariant is proven in the sense that the compiler guarantees the check is structurally present; the actual enforcement happens at runtime.

Class 4: Boundedness

Form

invariant name : x <= MAX -- where x : Nat and MAX is a constant -- Also: x >= MIN, x < LIMIT, MIN <= x <= MAX

A boundedness invariant asserts that a state variable remains within a constant range. The canonical example is a fee rate cap (fee_rate <= 1000) in a marketplace contract. Boundedness invariants prevent overflow, enforce economic constraints, and provide guarantees about derived quantities.

Proof Strategy

The compiler proves boundedness by induction over transitions. The proof has two parts: a base case showing the initial state satisfies the bound, and an inductive step showing that each transition preserves the bound.

-- Boundedness proof obligation: -- Base case: -- The initial value of x (its type default or explicit -- initializer) satisfies x <= MAX. -- Nat default is 0. 0 <= MAX for any non-negative MAX. QED -- Inductive step for each transition that modifies x: -- Given: x <= MAX (inductive hypothesis) -- Prove: x' <= MAX -- Case: x = constant where constant <= MAX => QED -- Case: x += delta with require x + delta <= MAX => QED -- Case: x = expr where expr <= MAX provable from -- inductive hypothesis + requires => QED

For transitions that do not modify x, the bound is preserved trivially. For transitions that modify x, the compiler checks that either the new value is a constant within bounds, or a require clause explicitly bounds the new value, or the update expression can be proven to stay within bounds using the inductive hypothesis and the transition's preconditions.

Class 5: State Machine

Form

invariant name : phase only advances -- where phase is a state variable with a defined ordering -- The ordering may be implicit (Nat: 0 < 1 < 2 < ...) -- or explicit (enum: Created < Active < Resolved < Closed)

A state machine invariant constrains a phase or status variable to advance monotonically through a defined ordering. This prevents contracts from reverting to previous states and ensures that lifecycle progressions are irreversible. The invariant is a specialized form of monotonicity applied to discrete phases rather than numeric values.

Proof Strategy

The compiler verifies that every transition which modifies the phase variable sets it to a value that is strictly greater than or equal to the current value in the defined ordering. The ordering is either the natural ordering on Nat or a user-defined enum ordering.

-- State machine proof obligation: -- For each transition that modifies phase: -- Prove: phase' >= phase in the defined ordering -- Example: Escrow with released : Bool -- Ordering: false < true -- release() sets released = true => true >= false QED -- refund() sets released = true => true >= false QED -- No transition sets released = false after it is true, -- because require !released guards both transitions. -- Example: Governance with phase : Nat -- 0 = Proposed, 1 = Active, 2 = Executed -- activate() sets phase = 1 when phase == 0 => 1 > 0 QED -- execute() sets phase = 2 when phase == 1 => 2 > 1 QED

The compiler also checks that every transition which reads the phase variable but does not modify it is consistent with the current phase. If a transition's preconditions require phase == k, then only states at phase k can reach that transition, and the post-state must have phase >= k.

Invariant Composition

A Form may declare multiple invariants of different classes. The compiler verifies each invariant independently against each transition. The proof obligations are the Cartesian product of transitions and invariants: if a Form has n transitions and m invariants, the compiler generates n * m proof obligations.

Invariants do not interact during verification. The conservation proof for a token transfer does not depend on the access control proof for minting. This independence is a consequence of the algebraic classification: each class has a self-contained proof method that does not reference other invariant classes.

-- Vault form: two invariants of different classes

invariant conservation :         -- Class 1: conservation
  sum(deposited) == total

invariant time_lock :             -- Class 3: access control (temporal)
  withdraw => block.time >= lock_until[msg.sender]

-- Proof obligations: 2 transitions x 2 invariants = 4 checks
-- deposit  x conservation  => co-variance check       QED
-- deposit  x time_lock     => deposit does not withdraw QED
-- withdraw x conservation  => co-variance check       QED
-- withdraw x time_lock     => require guard present    QED

Algebraic Reduction Summary

Every invariant class reduces to one of three algebraic verification techniques. This is the fundamental reason that Form verification is decidable and efficient.

-- Reduction table: -- -- Conservation => Arithmetic identity (delta cancellation) -- Monotonicity => Ordering proof (non-negative deltas) -- Access Control => Set membership (precondition dominance) -- Boundedness => Arithmetic identity + induction -- State Machine => Ordering proof (phase advancement) -- -- All five classes reduce to combinations of: -- 1. Arithmetic identity checking -- 2. Ordering relation verification -- 3. Set membership / precondition analysis

Arithmetic identity checking handles conservation and the arithmetic component of boundedness. Ordering relation verification handles monotonicity, state machine invariants, and the non-negativity constraints in Nat subtraction. Set membership and precondition analysis handles access control and temporal guards. These three techniques are all decidable for the restricted expression language of Forms, which is why the compiler can always either prove or refute a well-formed invariant.

Specification

Overview Type System Transition Semantics Verification Rules WASM Compilation

Form Templates

Token Vault Escrow Governor Marketplace

Resources

Formagine home API documentation Membership