Soma, a language for programs written by coding agents

Soma is an open-source programming language (MIT) for services whose correctness is a lifecycle and a few hard limits: approvals, quotas, escrow, agent workflows. One .cell file holds the data, the state machine, the handlers, the tests and the HTTP routes. soma check answers every mistake with the form to write instead; soma verify proves the lifecycle and the limits it can, and says which ones it only checks at runtime.

curl -fsSL https://soma-lang.dev/install.sh | sh

The current release is Soma 3.2.4 (release notes). It runs on Linux and macOS. Soma is experimental: status says what that means.

One rule, and the proof that it holds

A quota of 100 units per user. The limit is written once, next to the data, as an invariant; the handler states its own preconditions with require.

quota.cell

cell Quota {
    memory {
        used: Map<String, Int> [persistent]
        invariant used >= 0 && used <= 100
    }

    on consume(user: String, n: Int) {
        require n > 0 else BadAmount
        let before = used.get(user) ?? 0
        require before + n <= 100 else QuotaExceeded
        used.set(user, before + n)
        return 100 - (before + n)
    }
}

The verifier proves the invariant for every input, then the program runs. These outputs were printed by the soma binary when this page was built:

$ soma verify quota.cell
Verifying quota.cell...

Quota/invariants:

  ✓ invariant used >= 0 && used <= 100 — writer 'consume' proven by induction (writes before + n)

1 passed, 0 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK

$ soma run quota.cell consume ana 60
40

$ soma run quota.cell consume ana 60
error: require failed: QuotaExceeded: constraint violated
  --> quota.cell:10:9
   |
10 |         require before + n <= 100 else QuotaExceeded
   |         ^

$ soma run quota.cell consume ana -5
error: require failed: BadAmount: constraint violated
  --> quota.cell:8:9
  |
8 |         require n > 0 else BadAmount
  |         ^

$ soma run quota.cell consume ana 40
0

The second call fails and leaves the slot unchanged: a handler that fails leaves no write behind. Remove the QuotaExceeded line and soma verify no longer proves the bound; it reports it as checked at runtime and names the line that would make it provable. Lesson 3 shows it.

Every error names its fix

Models write habits of other languages. Soma refuses them before anything runs, and the message says what to write:

cart.cell

cell Cart {
    memory { items: Map<String, Int> [persistent] }

    on add(sku: String) {
        let current = items.get(sku)
        if current == null {
            items.set(sku, 1)
        }
    }
}

$ soma check cart.cell
error: 'null' does not exist in Soma — Soma's null is `()`: `if x == () { … }`, `x ?? default`
  --> cart.cell:6:23
  |
6 |         if current == null {
  |                       ^
  = code: E0091
✗ 1 error(s), 0 warning(s).

Each of the 150 diagnostic codes has a page with a program that triggers it, the real output, and the fix: Diagnostics.

Large programs, skeleton first

No model holds a 10,000-line program in context. In Soma the structure is written first, as a skeleton: memory, invariants, state machines, and for each signal a frame saying what its body may read, write, call, and which edges it may take. Bodies come later, in flesh blocks, one at a time, each from a one-screen brief (soma skeleton app.cell Cell.signal), and soma check refuses a body that leaves its frame. soma verify proves the lifecycle before any body exists.

loans.cell

skeleton Loans {
    memory { holder: Map<String, String> [persistent] }   // loan id -> member

    state loan {
        initial: requested
        requested -> out
        requested -> refused
        out -> returned
    }

    face {
        // Lends a book to `member` under loan `id`.
        signal lend(id: String, member: String) -> String
            writes holder
            moves requested -> out, requested -> refused

        // Closes loan `id`.
        signal close(id: String) -> String
            writes holder
            moves out -> returned
    }
}

$ soma verify loans.cell
Verifying loans.cell...

State machine 'loan': 4 states, initial 'requested'
  States: [out, refused, requested, returned]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'requested'
  ✓ terminal states: [refused, returned]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  · think-isolated: judged when the 2 holes of the program have a body
  · termination: 2 holes — judged when they have a body
  · refinement: `lend` is a hole — its frame allows {requested → out, requested → refused}
  · refinement: `close` is a hole — its frame allows {out → returned}

5 passed, 0 warnings, 0 failures

  Temporal properties for 'loan':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
○ 2 holes — signals of a skeleton with no body yet: Loans.lend, Loans.close  (`soma holes loans.cell`)
VERIFY OK (skeleton — the holes above are open obligations)

$ soma holes loans.cell
2 holes of 2 signals in loans.cell — numbered in the order to fill them (a hole comes after the holes it calls):

Loans (2)
    1. lend    writes holder  moves requested -> out, requested -> refused
    2. close   writes holder  moves out -> returned

the brief for one: soma skeleton loans.cell Loans.lend

The guide: Large programs, skeleton first. Step by step: lesson 6. At scale: Orbite, a 67,000-line space traffic coordination system written by twenty agents in parallel, with 97 rules between state machines proven.

Reference and builtins

Every construct, and every builtin with its exact signature.

327 verified programs

Payments, interlocks, medical devices, games, agents: source and the toolchain's real output.

Diagnostics and pitfalls

What the compiler says when a program is wrong, and how to fix it.

For AI agents

What to fetch, the loop to run, and when not to pick Soma.

What is proven, what is not

Proven for every input	Checked at runtime	Not covered
Every declared state machine: reachability, deadlocks, liveness, temporal properties, and that handlers take only declared edges. An invariant whose every write is bounded. Termination and declared cost bounds.	Every invariant on every write, including one between two slots of a cell. Transitions, guards, typed parameters, token budgets.	Rules between two cells that `soma.toml` does not state; business rules nobody wrote; effects outside the program (HTTP, files, LLM answers); cluster behaviour.

The full table: guarantees. The limits of the implementation: status.

The command line

soma check app.cell      # static checks; every error names its fix (--json for agents)
soma verify app.cell     # proves state machines, invariants, termination, cost bounds
soma test app.cell       # runs `cell test` assertions
soma run app.cell handler arg1 arg2
soma serve app.cell -p 8080
soma skeleton app.cell   # the program's structure, without bodies
soma explain E0028       # what a diagnostic means
soma docs agent          # the language guide, offline

Every command: command line. Source code: github.com/soma-dev-lang/soma. The paper: Scale as a type.