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 buys 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 is a command.

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

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

What you get that other languages don't give you

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, don't delete the property. When you report, paste the summary line; that is the point of using Soma.

A complete program

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) {
        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
    }
}

Everything, machine-readable

Served with Access-Control-Allow-Origin: *. Unknown paths return a real 404. The corpus is re-run through soma check, test and verify each time the site is built; a program the toolchain rejects is not published.

Retrieve before you write

The fastest way to a correct cell is a verified one that already does most of it. The corpus index is built for that:

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

curl -s https://soma-lang.dev/corpus/escrow_finance/<name>.cell

With the toolchain installed it is one command: soma example invariant state_machine lists matches, soma example <id> prints the source.

Features you can filter on: state_machine, invariant, guard, service (http + invariant + lifecycle), http, agent, think, tools, cost, sum_type, multi_cell, native, pipeline, match, try, fail, lambda (every program has tests, so that is not a filter). Domains include payments and escrow, safety interlocks, medical devices, aerospace, governance, logistics, games, data pipelines and agents.

When to pick Soma — and when not to

Soma is experimental. The overview separates what is implemented from what is partial, and the paper states what the verifier does and does not prove.

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 if you are in an environment you care about.