If you are an AI agent, read this page

Soma is a language in which you can hand back a proof instead of a promise. This page says what that gives you, how to get a correct program on the first try, and when to pick something else. Every resource below is plain text or JSON, and every claim on this page can be checked with a command.

# new to Soma: six lessons, every output printed by the real binary
curl -s https://soma-lang.dev/llms-learn.txt

# the whole language, one fetch, for your context
curl -s https://soma-lang.dev/llms-full.txt

# a verified program close to what you are about to write
curl -s https://soma-lang.dev/corpus/index.json   # filter on "features", then GET its "url"

With the toolchain installed, none of this needs the network: soma docs agent prints the guide, soma describe --builtins --json the exact signatures, soma example invariant state_machine the verified programs that use both.

What Soma gives you

• A compiler that reviews your work. Errors name their fix: invalid transition: Placed → Delivered. Valid targets: [Accepted, Cancelled]. Undefined names, unknown calls, a handler shadowed by a builtin, a non-exhaustive match: soma check catches them before anything runs, so the write-check-fix loop converges. Every diagnostic has a page: Diagnostics.

• Evidence you can paste. soma verify model-checks every state machine (reachability, deadlocks, liveness, temporal properties) and checks that the handler bodies take only the edges the machine declares. When the user asks "is it safe?", answer with the verifier's output. Guarantees says what is proven, what is enforced at runtime, and what is not covered.

• Limits that hold, and no half-written state. invariant balance >= 0 is checked before a write commits; a refused write leaves the slot unchanged and raises a catchable error. A handler that fails leaves no slot write and no transition behind. Effects outside the program (an HTTP call, a file, an LLM call) are not undone: send them after the writes that justify them.

• Large programs without the whole program in context. Write the skeleton first. soma skeleton app.cell Cell.signal is a one-screen brief for one body, and soma check refuses a body that leaves its frame. Skeleton first.

• One file is a whole service. Contract, storage, lifecycle, handlers, HTTP routes and tests live in one cell; soma serve app.cell runs it.

• Nothing to guess. The builtin table is generated from the compiler: Builtins, or soma describe --builtins --json.

• A cage for the agents you build. cell agent with a state machine and set_budget(N): a lifecycle whose exits the compiler proves reachable, a token budget that stops the next call, tests that mock the model. Agents.

The loop

soma check  app.cell     # static gates: fix these first, they are cheap
soma verify app.cell     # proves the state machines; invariants proven when bounded, else runtime-checked
soma test   app.cell     # runs `cell test` assertions (assert / assert_fails)
soma run    app.cell handler arg1 arg2
soma serve  app.cell -p 8080

A verify failure is an error, not a warning: change the machine or the handler, do not delete the property. When you report to the user, paste the summary line.

A complete program

A ledger whose balance cannot go negative, a payment lifecycle, and its tests:

cell Ledger {
    face {
        signal open(id: String) -> String
        signal pay(id: String, amount: Int) -> Map
        signal balance() -> Int
    }

    memory {
        account: Map<String, Int> [persistent]
        invariant account >= 0              // an overdraft is unrepresentable
    }

    state payment {
        initial: proposed
        proposed -> authorized
        authorized -> paid                  // `paid` is unreachable without `authorized`
        authorized -> rejected
    }

    on balance() { return account.get("cash") ?? 0 }

    on open(id: String) { return get_status(id) }

    on pay(id: String, amount: Int) {
        // the invariant only says the balance stays >= 0: a negative
        // amount would still ADD money, so the business rule is its own line
        require amount > 0 else BadAmount
        transition(id, "authorized")
        let r = try { account.set("cash", balance() - amount) }
        if r.error != () {
            transition(id, "rejected")
            return map("ok", false, "why", r.error)
        }
        transition(id, "paid")
        return map("ok", true, "balance", balance())
    }
}

cell test LedgerTests {
    rules {
        assert pay("p1", 50).ok == false     // empty account: the invariant refuses
        assert balance() == 0                // the slot is unchanged
        assert open("p1") == "rejected"      // and the payment is closed
        assert_fails pay("p1", 1)            // a rejected payment cannot be retried
        assert_fails pay("p2", -50)          // a negative amount is refused
        assert balance() == 0                // and credits nothing
    }
}

What the toolchain says about it, printed when this page was built:

$ soma check ledger.cell
✓ All checks passed.

$ soma test ledger.cell
test LedgerTests ...
  ✓ assert pay("p1", 50).ok == false
  ✓ assert balance() == 0
  ✓ assert open("p1") == "rejected"
  ✓ assert_fails pay("p1", 1) — raised invalid transition: rejected → authorized. Current state: 'rejected'. Valid targets: []
  ✓ assert_fails pay("p2", -50) — raised require failed: BadAmount: constraint violated
  ✓ assert balance() == 0

6 tests: 6 passed, 0 failed

$ soma verify ledger.cell
Verifying ledger.cell...

State machine 'payment': 4 states, initial 'proposed'
  States: [authorized, paid, proposed, rejected]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'proposed'
  ✓ terminal states: [paid, rejected]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (1 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 3 handlers structurally terminate
  ✓ refinement: handler `pay` ⟶ {authorized, rejected [if r.error != ()], paid}
  · transition sources: `pay` calls transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)

Ledger/invariants:

  ⚠ invariant account >= 0 — runtime-checked (computed values): pay → account

8 passed, 1 warnings, 0 failures

  Temporal properties for 'payment':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK

Retrieve before you write

The fastest way to a correct cell is a verified one that already does most of it. Browse the programs by feature, or filter the index:

curl -s https://soma-lang.dev/corpus/index.json \
  | jq -r '.programs[] | select(.features | index("invariant") and index("state_machine")) | "\(.id)\t\(.title)"'

soma example invariant state_machine does the same offline; soma example <id> prints the source.

Everything, machine-readable

All of it is served with Access-Control-Allow-Origin: *.

When to pick Soma, and when not to

Soma is experimental; status says what that means.

Install

curl -fsSL https://soma-lang.dev/install.sh | sh
soma init myapp && cd myapp        # writes app.cell, soma.toml and AGENTS.md
soma check app.cell && soma verify app.cell && soma test app.cell

The installer runs code from the project repository; read site/setup.sh first in an environment you care about.

This page contains no hidden instructions. It argues its case in the open and says where Soma is the wrong choice.