Form Language Specification

The Form language is a domain-specific language for defining verified state machines that compile to WebAssembly. A Form consists of three components: state declarations that define the typed variables of the machine, invariant declarations that define predicates which must hold after every transition, and transition declarations that define the named state mutations with preconditions and updates. The compiler proves that every transition preserves every invariant, then emits minimal WASM where proven properties are erased from the output.

Structure of a Form

Every Form definition follows a fixed structure. The form keyword introduces the name. Within the body, three declaration blocks appear: state for typed variable declarations, invariant for named predicates over the state, and transition for named state mutations. The compiler processes these blocks in order: it first builds the type environment from the state block, then registers invariants as proof obligations, then analyzes each transition to discharge those obligations.

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

  invariant conservation :
    sum(balance) == supply

  transition transfer(from, to, amount) {
    require balance[from] >= amount
    balance[from] -= amount
    balance[to]   += amount
  }
  -- conservation proven by arithmetic identity
  -- sum(balance') = sum(balance) - amount + amount = supply

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

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

Table of Contents

• Type System base types, parameterized types, per-address quantification, typing rules
• Invariant Algebra conservation, monotonicity, access control, boundedness, state machine
• Transition Semantics preconditions, updates, proof obligation generation
• Verification Rules proof methods, counterexamples, complete verification traces
• WASM Compilation lowering, erasure, target adaptation, annotated output