Formagine Forms vs Solidity Contracts

How Forms Work

A Form is a declarative state machine definition. It declares state fields with types, invariants as first-class language elements, and transitions as the only operations that can modify state. The compiler extracts proof obligations from every (transition, invariant) pair and discharges them algebraically before producing WASM output.

Invariants in the Form language are not runtime assertions. They are compile-time proof obligations. The compiler proves that every transition preserves every invariant for all possible inputs and all reachable states. Proven invariants are then erased from the output binary, producing contracts with zero verification overhead at runtime.

The Form language is intentionally constrained. It does not support arbitrary computation, inheritance, libraries, or inline assembly. These constraints make algebraic verification tractable. The trade-off is that some contracts cannot be expressed in the Form language at all.

Code Comparison: Token Contract

The same fungible token with supply conservation, expressed in Solidity and in the Form language.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

contract Token {
  mapping(address => uint256)
    public balance;
  uint256 public supply;
  address public owner;

  // No compile-time proof.
  // Conservation is an
  // assumption, not a
  // guarantee.

  function transfer(
    address from,
    address to,
    uint256 amount
  ) external {
    require(
      balance[from] >= amount
    );
    balance[from] -= amount;
    balance[to]   += amount;
    // Runtime check only:
    // assert(sum == supply)
    // would cost O(n) gas
  }

  function mint(
    address to,
    uint256 amount
  ) external {
    require(
      msg.sender == owner
    );
    balance[to] += amount;
    supply      += amount;
  }

  function burn(
    address from,
    uint256 amount
  ) external {
    require(
      balance[from] >= amount
    );
    balance[from] -= amount;
    supply        -= amount;
  }
}

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

  invariant conservation :
    sum(balance) == supply
  -- Proven at compile time.
  -- Erased from output.
  -- Zero runtime cost.

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

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

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

The Solidity version is structurally similar but lacks a mechanism to prove conservation at compile time. A runtime assert(sum(balance) == supply) would require iterating over all holders, costing O(n) gas per transaction and making it impractical. Conservation is an assumption that the developer hopes the code preserves, but no tool in the Solidity compilation pipeline guarantees it.

The Form version declares conservation as a first-class invariant. The compiler proves it holds for all three transitions by algebraic identity. The proof is erased from the WASM output. There is no runtime cost and no possibility of violation.

Key Differences

Where Solidity Wins

Ecosystem depth. Solidity has OpenZeppelin's audited contract library, Hardhat and Foundry for development and testing, Etherscan for verification and exploration, and the largest community of smart contract developers. Building on Solidity means building on a decade of accumulated infrastructure.

Expressiveness. Solidity can express any computation the EVM supports. Proxy patterns, delegate calls, complex inheritance hierarchies, inline assembly optimizations, and arbitrary inter-contract composition are all possible. The Form language deliberately excludes these features.

Liquidity access. Solidity contracts deploy to Ethereum mainnet and EVM-compatible chains with the deepest on-chain liquidity. DeFi composability with existing protocols (Uniswap, Aave, Compound) requires EVM deployment, which requires Solidity or Vyper.

Where Forms Win

Correctness guarantees. Declared invariants are mathematically proven at compile time. There is no possibility that a compiled form violates its invariants, regardless of inputs or state. Solidity has no equivalent mechanism in the compiler itself.

Zero verification overhead. Proven invariants are erased from the output binary. There are no runtime checks consuming gas for properties that have already been proven. In Solidity, runtime assertions consume gas on every transaction and still only check one specific execution, not all possible executions.

Spec-implementation unity. The form definition is simultaneously the specification and the implementation. There is no gap between what is specified and what runs on-chain. In Solidity with Certora, the specification (CVL) and implementation (Solidity) are separate documents that must be shown to correspond.

Multi-chain output. A single form definition compiles to WASM for four chain ecosystems. Solidity targets the EVM only. Reaching CosmWasm, Near, or Polkadot from Solidity requires rewriting the contract in Rust or another WASM-targeting language.

When to Use Each

Use Solidity when you need EVM-native deployment, composability with existing DeFi protocols, complex inheritance patterns, proxy upgradability, or access to the Ethereum mainnet liquidity pool. Also use Solidity when your contract requires arbitrary computation that the Form language cannot express.

Use Forms when correctness guarantees are your primary concern, your contract logic can be expressed as a state machine with algebraic invariants, and your deployment targets include WASM-compatible chains. Forms are particularly well-suited for token contracts, vaults, escrow systems, governance mechanisms, and any contract where invariant violations would be catastrophic.

Consider both in a multi-chain strategy. Use Forms for core financial primitives where correctness is critical and deploy them to WASM chains. Use Solidity for composability and liquidity access on EVM chains. On Arbitrum Stylus, Form-compiled WASM contracts can interoperate directly with Solidity contracts, enabling a hybrid approach.

Frequently Asked Questions

Can Formagine Forms do everything Solidity can?

No. Solidity is a general-purpose language that supports arbitrary computation, inheritance, inline assembly, delegate calls, and proxy patterns. The Form language is a domain-specific language for verified state machines, intentionally constrained to make algebraic verification tractable. Contracts requiring unrestricted computation are better served by Solidity.

Can I migrate an existing Solidity contract to a Form?

For contracts whose core logic is a state machine with expressible invariants, yes. Token contracts, vaults, escrow systems, and governance mechanisms translate naturally. Contracts relying heavily on Solidity-specific features (inheritance, libraries, inline assembly, proxy patterns) require significant restructuring. The Form language is not a drop-in replacement.

Does the Form language target the EVM?

No. The Form language compiles to WASM, targeting CosmWasm, Near Protocol, Arbitrum Stylus, and Polkadot. Through Stylus, Form contracts can interoperate with EVM contracts on Ethereum L2, but the Form compiler does not produce EVM bytecode directly.

How does verification in Solidity compare to verification in Form?

In Solidity, verification is applied through external tools (Certora, Slither, Mythril) that require separate specification files and analysis passes. In Form, verification is compilation. Invariants are proof obligations discharged by the compiler before producing output. There is no separate tool, no separate specification, and no gap between what is specified and what is compiled.

Related Comparisons

Form Templates

Resources