API Reference

POST /api/verify
Content-Type: application/json

{
  "form": {
    "name": "Token",
    "state": {
      "balance": { "type": "Nat", "indexed_by": "Address" },
      "supply": { "type": "Nat" }
    },
    "invariants": [
      { "name": "conservation", "expr": "sum(balance) == supply" }
    ],
    "transitions": [
      {
        "name": "transfer",
        "params": ["from", "to", "amount"],
        "body": [
          { "require": "balance[from] >= amount" },
          { "assign": "balance[from]", "op": "-=", "value": "amount" },
          { "assign": "balance[to]", "op": "+=", "value": "amount" }
        ]
      }
    ]
  }
}

{
  "status": "verified",
  "form": "Token",
  "invariants": [
    {
      "name": "conservation",
      "status": "proven",
      "method": "arithmetic_identity"
    }
  ],
  "transitions_checked": 1
}

{
  "status": "rejected",
  "form": "Token",
  "invariants": [
    {
      "name": "conservation",
      "status": "violated",
      "counterexample": {
        "transition": "mint",
        "initial_state": { "supply": 100, "balance": { "alice": 100 } },
        "final_state": { "supply": 100, "balance": { "alice": 100, "bob": 50 } },
        "violation": "sum(balance) = 150 != supply = 100"
      }
    }
  ]
}

POST /api/build
Content-Type: application/json
Authorization: Bearer fmg_live_abc123...

{
  "form": {
    "name": "Token",
    "state": {
      "balance": { "type": "Nat", "indexed_by": "Address" },
      "supply": { "type": "Nat" }
    },
    "invariants": [
      { "name": "conservation", "expr": "sum(balance) == supply" }
    ],
    "transitions": [
      {
        "name": "transfer",
        "params": ["from", "to", "amount"],
        "body": [
          { "require": "balance[from] >= amount" },
          { "assign": "balance[from]", "op": "-=", "value": "amount" },
          { "assign": "balance[to]", "op": "+=", "value": "amount" }
        ]
      }
    ]
  },
  "target": "cosmwasm",
  "optimize": true
}

{
  "status": "compiled",
  "form": "Token",
  "target": "cosmwasm",
  "artifact": {
    "url": "https://formagine.com/api/artifacts/fmg_tok_a1b2c3.wasm",
    "sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855",
    "size_bytes": 14832,
    "expires": "2026-04-12T00:00:00Z"
  },
  "verification": {
    "invariants_proven": 1,
    "invariants_erased": 1
  }
}

{
  "forms": [
    {
      "name": "Token",
      "description": "Fungible token with supply conservation",
      "invariants": ["sum(balance) == supply"],
      "transitions": ["transfer", "mint", "burn"],
      "url": "/forms/token"
    },
    {
      "name": "Escrow",
      "description": "Two-party escrow with deadline and refund",
      "invariants": ["locked + released == deposited"],
      "transitions": ["deposit", "release", "refund"],
      "url": "/forms/escrow"
    },
    {
      "name": "Vesting",
      "description": "Linear vesting schedule with cliff",
      "invariants": ["claimed <= vested(now)", "vested(now) <= total"],
      "transitions": ["claim"],
      "url": "/forms/vesting"
    },
    {
      "name": "Multisig",
      "description": "M-of-N multisignature with threshold invariant",
      "invariants": ["approvals >= threshold => executable"],
      "transitions": ["propose", "approve", "execute"],
      "url": "/forms/multisig"
    }
  ]
}

{
  "chains": [
    {
      "id": "cosmwasm",
      "name": "CosmWasm",
      "vm": "wasm32",
      "networks": ["osmosis", "neutron", "terra", "injective"]
    },
    {
      "id": "near",
      "name": "Near Protocol",
      "vm": "wasm32",
      "networks": ["mainnet", "testnet"]
    },
    {
      "id": "stylus",
      "name": "Arbitrum Stylus",
      "vm": "wasm32",
      "networks": ["arbitrum-one", "arbitrum-sepolia"]
    },
    {
      "id": "polkadot",
      "name": "Polkadot",
      "vm": "wasm32",
      "networks": ["astar", "aleph-zero", "phala"]
    }
  ]
}

POST /api/explain
Content-Type: application/json

{
  "form": {
    "name": "Token",
    "state": {
      "balance": { "type": "Nat", "indexed_by": "Address" },
      "supply": { "type": "Nat" }
    },
    "invariants": [
      { "name": "conservation", "expr": "sum(balance) == supply" }
    ],
    "transitions": [
      {
        "name": "transfer",
        "params": ["from", "to", "amount"],
        "body": [
          { "require": "balance[from] >= amount" },
          { "assign": "balance[from]", "op": "-=", "value": "amount" },
          { "assign": "balance[to]", "op": "+=", "value": "amount" }
        ]
      }
    ]
  }
}

{
  "form": "Token",
  "explanation": {
    "summary": "A fungible token where each address holds a non-negative balance, and a global supply counter tracks the total tokens in existence.",
    "invariants": [
      {
        "name": "conservation",
        "plain": "The sum of all individual balances always equals the total supply. Tokens cannot be created or destroyed except through explicitly defined transitions."
      }
    ],
    "transitions": [
      {
        "name": "transfer",
        "plain": "Moves tokens from one address to another. The sender must have sufficient balance. The total supply is unchanged because the amount subtracted from the sender equals the amount added to the receiver."
      }
    ],
    "guarantees": "After verification, it is mathematically proven that no sequence of transfers can create or destroy tokens. The conservation invariant holds for every possible execution path."
  }
}