# Soma Language — for AI Agents

> Soma is a declarative cell language where systems carry their proofs.
> One file holds a whole service: contract (`face`), storage with invariants
> (`memory`), a model-checked lifecycle (`state`), handlers, HTTP routes and
> tests. `soma verify` proves the state machines; memory invariants reject
> bad writes before they commit; LLM agents run inside lifecycles the
> compiler proves terminate, with token budgets. Every compiler error
> names its own fix, so the write → check → fix loop converges.

Everything below is current for the soma binary named in
https://soma-lang.dev/version.json and generated from the compiler or
verified against it. Unknown URLs on this site return 404, never a page.

## Machine-readable resources

- [llms-service.txt](https://soma-lang.dev/llms-service.txt): this file + [guarantees](https://soma-lang.dev/docs/guarantees.md) (proven / enforced / not covered) + [serving](https://soma-lang.dev/docs/serving.md) (routing, exposure, atomicity) + [operations](https://soma-lang.dev/docs/operations.md) (what kills the process, ports, exit codes, HTTP statuses, limits, Linux deploy) + every gotcha — what a service needs, ~100 KB
- [llms-full.txt](https://soma-lang.dev/llms-full.txt): this file + full reference + every gotcha + every builtin, one fetch (~130 KB)
- [docs/robotics.md](https://soma-lang.dev/docs/robotics.md): 100 robotics robustness scenarios, reproduction commands and limits; offline with `soma docs robotics`
- [agent.md](https://soma-lang.dev/agent.md): drop-in AGENTS.md / CLAUDE.md block for a project that uses Soma
- [skill/SKILL.md](https://soma-lang.dev/skill/SKILL.md): the same knowledge packaged as an agent skill
- [builtins.json](https://soma-lang.dev/builtins.json): every builtin with its exact signature (from `soma describe --builtins --json`) — never guess one
- [gotchas.json](https://soma-lang.dev/gotchas.json): the mistakes models make, each with the real diagnostic and the fix
- [corpus/domains.json](https://soma-lang.dev/corpus/domains.json): the domains (~3 KB) → one domain's index (~20 KB, summaries, each program's verify verdict and soma.toml)
- [corpus/index.json](https://soma-lang.dev/corpus/index.json): 300+ verified programs (id, title, features, url) — filter on `features`, then GET the `url` for the raw source. Per domain with summaries: `https://soma-lang.dev/corpus/<domain>/index.json`. Plain listing: [index.md](https://soma-lang.dev/corpus/index.md)
- [docs/reference.md](https://soma-lang.dev/docs/reference.md), [docs/builtins.md](https://soma-lang.dev/docs/builtins.md), [docs/gotchas.md](https://soma-lang.dev/docs/gotchas.md): raw markdown
- [repo/index.json](https://soma-lang.dev/repo/index.json): the package registry
- [status](https://soma-lang.dev/status): maturity, version, MIT license, known limits, security contact
- Source: https://github.com/soma-dev-lang/soma

## Pick Soma when / skip it when

Soma 2.8.10 corrects native code that diverged from the interpreter: an exact
Int quotient next to `%` stayed a Float, Int-only builtins given a Float were
truncated or failed in rustc (they are refused like the interpreter), a huge
literal times a small local overflowed instead of promoting to BigInt,
`to_string` of an exact quotient printed "2.0", `str_at` bounds and error
wording differed, `buffer(-3)` died on "capacity overflow". Storage: Int indices
past 64 bits acted on element 0 of a List slot, a Map key serde reserves broke
its round trip, `set_budget` accepted a negative BigInt; `rows[i] = v`,
`rows.delete(i)` and `m.len` on persistent slots no longer rewrite or scan the
whole table, joins and self-assigned `with`/`without` are linear. The
quadratic-concatenation lint ignores numeric accumulators, `(f)(x)` is refused
like `f(a)(b)`, `"{0x1F}"` interpolates, `check --json` keeps its keys on a load
failure, and a restarted cluster node no longer reports its own tables as
orphans. Sixteen new Rust regressions cover these changes; every program of the
repository keeps its `check`, `verify` and `test` verdicts.
Scope: native `/` is typed Float, so an exact-quotient division by zero answers
`inf`/`NaN` natively where the interpreter raises. Details:
https://soma-lang.dev/CHANGELOG.md.

Soma 2.8.9 distinguishes storage read failures from absent keys and empty
collections. A failed read aborts the invocation and rolls back earlier local
writes, including inside `try`. Legacy lists retain their values on append and
cannot resurrect deleted items or hang during replacement. The JSON backend
refuses malformed/unreadable files and preserves its old state on write failure.
The HTTP storage adapter validates responses, propagates failures and preserves
typed non-finite Floats. Both protocol demos are corrected. Thirty-six new Rust
regressions cover these changes (including three Python HTTP scenarios).
Scope: JSON storage has per-file replacement, not SQLite multi-slot transactions;
HTTP providers have no remote transaction or exactly-once guarantee, and this
release does not wire HTTP providers into `run`/`serve`.
Details: https://soma-lang.dev/CHANGELOG.md.

Soma 2.8.8 checks SQLite transaction boundaries and propagates refused writes
from `remember()`, `next_id()` and transitions. Failed commits withhold queued
events and replication; failed task boundaries stop execution. Auxiliary tables
open before the transaction. List writes handle failures atomically, indexed
reads handle gaps, and normal returns from scheduled ticks commit their writes.
`next_id()` rejects counter exhaustion/corruption and migrates only its own
cell's legacy counter. Twenty-nine new regression tests cover these paths.
Compatibility: a lost transaction aborts the invocation even inside `try`;
already committed task steps and external effects are not undone.
Details: https://soma-lang.dev/CHANGELOG.md.

Soma 2.8.7 fixes `if` expression scope, lambda capture inside interpolations
and error details, and collection evaluation when interpolations assign locals.
Static analyses now see calls containing quoted colons: recursion, invariant
writes and token costs cannot disappear from the proof. `recall()` stays within
its cell and preserves JSON-shaped Strings; `remember()` rejects functions and
excessive encoded nesting before writing. Twenty-four integration regressions
reproduce the defects on 2.8.6; a unit test covers legacy memory migration.
Compatibility: parse remembered JSON text explicitly with `from_json()`; keep
branch locals inside their branch. Details: https://soma-lang.dev/CHANGELOG.md.

Soma 2.8.6 corrects duplicate/skipped argument evaluation, self-append bindings,
piped map updates, ignored builtin mocks and inconsistent pipe dispatch.
Calls and pipes share local-lambda and cell-handler resolution. Constructors
coerce declared Float and nested record fields and reject incompatible shapes.
Twenty-four new integration regressions cover these fixes. Compatibility and
examples: https://soma-lang.dev/CHANGELOG.md.

Soma 2.8.5 fixes typed input and storage boundaries: implicit Int-to-Float
promotion rejects overflow, typed maps check underscore keys and variant
payloads, and declared sum/record returns validate their values. Persistent
writes reject functions hidden in variants and excessive encoded nesting.
Local nth index limits are consistent; sleep requires an Int. Eighteen new
integration regressions plus a date-count unit test cover these corrections.
See https://soma-lang.dev/CHANGELOG.md.

Soma 2.8.4 corrects finite means that overflowed, large or tiny standard
deviations, mixed Int/Float medians and clamps. Means round after averaging;
medians preserve the selected Int and propagate NaN. Clamp rejects nonnumeric
operands and NaN bounds, compares exactly, and preserves the selected operand's
type. Nine regressions plus 320 independent numeric reference vectors cover
these fixes. See https://soma-lang.dev/CHANGELOG.md.

Soma 2.8.3 adds 100 regression scenarios for robot-controller use: numeric
boundaries, mission transitions, rollback, native execution and persistence.
They do not establish hardware qualification, hard real-time behavior or
distributed safety. Matrix: https://soma-lang.dev/docs/robotics.md.

Soma 2.8.2 cluster corrections: typed Map updates after commit, qualified
slot identities, full-mesh reconnect, logical versions, persisted tombstones
and state resynchronization. Local reads; no consensus, physical sharding,
exactly-once signals or distributed proof. Unsupported strong/causal
configurations are refused. See https://soma-lang.dev/docs/cluster.md.

Soma 2.8.1 corrections (2026-09-20): integer while optimization
preserves outer operands, each assignment and raised errors. Int ratios
round once without inf/inf; variance retains nearby large-number differences.
chr rejects invalid Unicode; substring clamps negative ends; index_of uses
exact structural equality. Numeric builtins reject invalid operand types.
Huge bit counts cannot become zero; native random bounds cannot overflow.
Generated native temporaries avoid operand and loop-counter collisions.
The deprecated --jit flag is now a compatibility no-op; use [native].

Also included in Soma 2.8.1: Int/Float comparisons are
exact across interpretation, bytecode and native code; numeric sorting and
filtering do not round Ints through Float. NaN remains unordered. `distinct`
and `distinct_by` use structural equality, including nested collections.
`range(a, b, 0)` raises kind `range`; `top`/`bottom` need a nonnegative Int.
HTTP query `%2B` stays `+`, and `?flag` supplies an empty String. New replay
logs tag errors separately from returned values. These are source-build
fixes; consult CHANGELOG.md and version.json for build provenance.
Cost proofs reject arithmetic overflow and a shadowed `range` needs an
explicit loop bound. Invalid mock clocks fail tests; `days_in_month` needs
Int arguments. Native failures are recorded after the transaction completes;
replay refuses malformed logs and native compilation failures.

Pick it when the task has a lifecycle or a limit that must hold: payments,
approvals, interlocks, quotas, escrow, agent workflows with a budget — and
you want to hand back evidence (`soma verify` output) instead of "I believe
this is correct". Also for a small self-contained HTTP service: one file,
no framework, storage and tests included.
Skip it when you need a large ecosystem, a mature package set, or raw
interpreter speed outside numeric `[native]` handlers. Soma is
experimental: verification is per cell; cross-cell composition is linted,
not proven.

## The agent loop

```
soma check  app.cell     # static gates FIRST: contracts, undefined
                         # interpolation vars, unknown/ambiguous calls
soma verify app.cell     # prove state machines + memory invariants
soma test   app.cell     # run `cell test` assertions (assert/assert_fails)
soma run    app.cell sig arg1 arg2
soma serve  app.cell -p 8080
soma describe app.cell --faces       # contract summary of every cell
soma describe --builtins --json      # exact builtin signatures — never guess
soma fix    app.cell                 # auto-repair common check errors
soma docs agent                      # this file, offline, from the binary
soma docs guarantees|serving|operations   # proofs, HTTP rules, what goes wrong — offline too
soma example invariant state_machine # verified programs with those features;
soma example <id>                    #   …and the source of one
soma init myapp                      # app.cell + soma.toml + AGENTS.md
```
Work in that order. `check` is cheap and catches most mistakes before
anything runs; a `verify` failure is an error, not a warning.

## Cell anatomy

```soma
cell App {
    face {                                   // the contract
        signal add(a: Int, b: Int) -> Int    // return types live HERE
        promise all_persistent
    }
    memory {
        data: Map<String, Int> [persistent, consistent]
        invariant data >= 0                  // checked BEFORE every write;
        // between two slots of the cell (a rule no single slot can state):
        // reserved: Map<String, Int> [persistent]
        // invariant (reserved ?? 0) <= (data ?? 0)
        // — checked on every write to EITHER slot; the written slot is its new
        // value, the other is read AT THE SAME KEY (a key it lacks reads as
        // (): default both sides with `?? 0`). verify reports it
        // runtime-checked: a rule between slots is not proven by induction —
        // by design, so verify prints it as a `·` note and `--strict` passes.
        // A delete is a write here too (dropping the other side's entry takes
        // it to ()). `?? 0` means the absent side reads 0: write the
        // right-hand slot FIRST (or seed both in one handler), else the first
        // write to the other is refused. `other.size` is that slot's entry
        // count; `other.get(key)` is refused (it is the value BEFORE the
        // write, so it would not guard that slot).
        // Between two CELLS nothing is proven (verify is per cell): it lists
        // `note: cross-cell: …` for each handler that transitions its machine
        // while acting on another cell's — enforce those with a `require`.
        // To refuse AND keep what you wrote (an audit row), `return
        // refusal("conflict", "…")` instead of raising: same body and status
        // a raised error would give, without the rollback.
    }                                        // violating write rejected, slot unchanged
    state flow {                             // model-checked by `soma verify`
        initial: draft
        draft -> approved { guard { amount < 1000 } }   // guard: reads the CALLING handler's locals
        draft -> rejected                    // approved/rejected: terminal (no outgoing edge)
    }
    on add(a: Int, b: Int) { return a + b }  // NO return type on handlers
    on approve_request(id: String, amount: Int) { transition(id, "approved") }  // binds the guard's `amount`
    on reject(id: String) { transition(id, "rejected") }
    on request(method: String, path: String, body: String) {
        match map("method", method, "path", path) {
            {method: "GET", path: "/"} -> html("<h1>hi</h1>")
            {method: "POST", path: "/approve/" + id} -> approve_request(id, 500)   // ONE variable per pattern, at the end
            _ -> response(404, map("error", "not found"))
        }
    }
}
```

## Core syntax (current)

```soma
let x = 42                  x += 1            // no semicolons; newlines separate
let v = -1                                    // negative literals work
let s = "hello {name}"                        // interpolation; UNDEFINED vars are
                                              // check-time errors; an unescaped " inside {} ends the string
let xs = [1, 2, 3]          xs[0] = 99        // bracket index read AND write
let m = map("k", 1)         m["k"] = 2        // maps too; m.k and m["k"] both read
let g = Game { bet: 10 }    g.bet = 20        // records: literal + dot mutation
g.board[0] = 7              xs[i][j] = v      // nested lvalues
let y = m["nope"] ?? 0                        // null-coalescing; () is null
for i in range(0, 10) { }   range(9, -1, -1)  // stepped/descending ranges
sum(xs) avg(xs) min(xs) max(xs) product(xs)   // reductions over lists
contains(xs, x)  index_of(xs, x)  slice(xs, 1, -1)  keys(m) values(m) entries(m)   // membership, slices, map views
sort_by(rows, "field")   sort_by(rows, r => [0 - r.total, r.name])   // stable; list key = several keys
xs = push(xs, x)            concat(a, b)      // push/concat RETURN a new list; `+` on numeric
                                              // lists adds element-wise — it does not concatenate
xs.sort()  xs.reverse()  m2.det()             // UFCS: any builtin as method
match x { 1 -> "a"  n if n > 5 -> "big"  _ -> "other" }   // arms use ->
let f = p => p * 2          f(3)              // lambdas use =>; first-class
data |> filter(x => x.ok) |> sort_by("score", "desc") |> top(10)
let r = try { risky() }     if r.error != () { ... }      // error handling
```

## Vectorized (numpy/MATLAB style)

```soma
let M = [1, 0, 0, 1].reshape(2, 2)    // matrices = List<List<Float>>, first-class
A * B          // matmul        A + B / A - B   elementwise
A + 10  A / 2  // scalar broadcast (both orders)
v * v  v + v   // numeric vectors: + * / - elementwise
A > 2  v >= 1.0                       // comparison masks (0.0/1.0 Floats); Int vectors compare and + - * exactly, [6] / 3 is [2] (the `/` rule per element)
A.T    A.shape    det(A)    matrix("1 2; 3 4")
concat(a, b)   // EXPLICIT list concatenation (+ on non-numeric lists concats)
```

## Sum types (exhaustive — compiler refuses a missing arm)

```soma
cell type Pay { variants { Charged { tx: String }  Declined { reason: String }  Cash } }
match r {
    Charged { tx }      -> "paid {tx}"
    Declined { reason } -> "no: {reason}"
    Cash                -> "cash"
}
// typed state machines: state order: OrderState { initial: Placed ... }
// transition(id, Variant) is compile-checked against the type
// to_json(Charged { tx: "t1" }) == '{"_type":"Pay","_variant":"Charged","tx":"t1"}'
// (a tuple variant carries "_values"); from_json brings the variant back; HTTP
// answers a returned variant the same way. Slots store variants as variants.
// A variant with named fields reads them by name too: `c.tx`.
// RECORD type = a `cell type` with ONE variant with named fields:
//   cell type Line { variants { Line { sku: String, qty: Int } } }
//   on add(lines: List<Line>) { … }   // a JSON object / Map becomes a Line
// — from HTTP, a tool call or the CLI — field by field; a missing, extra or
// mistyped field is a `type` error naming it (400). Several variants: the
// client cannot pick one (`_type`/`_variant` are refused).
```

## Coming from Python / TypeScript

```soma
map("k", v)   map()                // no {k: v} literal;   record: Name { k: v }
m.k   m["size"]                    // a key; m.len / m.size / m.keys: the entry count / keys
                                   // when the map has no such key (a record: () ) — m["size"] is always the key;
                                   // a List / String has only .len / .size (.first / .last); any other field raises kind `type`
[1, 2, 3]     []                   // list literals
x == ()       x ?? 0               // null is (); no null / None / undefined; `??` only runs its right side on ()
5 == ""                            // raises kind `type` (Int vs String is a bug); nested values of different types are just unequal
substring(s, i, i + 1)             // s[i] as a String; str_at(s, i) is a BYTE (Int)
if c { a } else { b }              // is an expression; no ternary; && || !  (no and/or/not)
                                   // a condition (if, while, &&, ||, !, require, guards,
                                   // filter/any/all predicates, invariants) is a Bool — `()`
                                   // counts as false; a String/Int/List is a type error
x => x + 1                         // lambdas take ONE parameter
for x in xs { }   for k in keys(m) { m[k] }   for e in entries(m) { e.key  e.value }   // for over () runs 0 times, over a String its lines, over a number: type error
slice(xs, 1, 3)  slice(xs, -2)     // no xs[a:b]
xs = push(xs, x)                   // push / concat / sort / with RETURN new values
on f(n: Int) [native] { … }        // annotations go AFTER the parameter list; no @decorator
fail("bad_kind", "bad kind: {k}")  // throw new Error(msg); catch: let r = try { … }  r.detail == msg
parse_int(s) ?? parse_float(s)     // Number(s); to_float("5") prints 5.0; round(x) is an Int, round(x, 2) a Float
m["k"] = v   m.get("k")            // a LOCAL map has no .set — .set/.delete/.push are slot methods
f(opts: Map) … opts.x ?? 10        // keyword arguments / defaults: pass a map, read with ??
Name { k: v }   is_a(r, "Name")    // struct / dataclass / interface: a record literal (no class)
format("%5.2f|%-8s|%03d", x, s, n) // printf / f-string widths (%d %s %f %.Nf, - and 0 flags)
7 / 2 == 3.5   idiv(-7, 2) == -3   // `/` is exact; idiv truncates toward zero, % follows the dividend's sign
floor_div(-7, 2) == -4   mod(-7, 2) == 1   // Python's // and %
```
A `class` with private fields is a `cell` with `memory` slots: one instance,
no `new`, no `this` — `this.hits.get(u)` is `hits.get(u)`; `constructor(a, b)`
is a `configure(a, b)` handler writing a `config` slot; subclasses are the
variants of a `cell type`, overridden methods one exhaustive `match` each.
A script is `on main() { print(…) }` run with `soma run --fresh app.cell main`:
`soma run` prints the handler's returned value (return nothing from main),
and slots persist in `.soma_data/` between runs unless `--fresh` (one
database per DIRECTORY: when other programs' cells have data there,
`--fresh` resets only this program's tables); `soma test`
starts empty. `counts[k] += 1` on a missing key is `() + 1` — write
`(counts.get(k) ?? 0) + 1`; `for r in rows { r.v = 2 }` changes a copy
(check warns). Number literals: `1_000_000`, `0xFF`, `0b101`; strings:
`\n \t \r \" \\ \u{1F600}`. `soma check` names the Soma form for each of
these when you get it wrong.

## Tests

`every` / `after` blocks do not run under `soma test`: call the sweeper
directly (`assert _sweep(5) == ["o4"]`) with `mock now` for the clock.

```soma
cell test MyTests {                // a name and a `rules` block are required; it may also
                                    // hold its own helpers (`on _walk(n: Int) { … }`),
                                    // private to that test cell (shared ones go in a plain cell)
    rules {
        let orders = fixture()                   // shared by the rules below; a bare call
                                                 // is not a rule: bind it (let _ = f())
        assert total(orders) == 42               // == is structural on lists/maps
        assert_fails pay("x")                    // passes when the expression RAISES
        assert_fails pay("x") matching "invalid transition"   // …for the right reason
        mock think "billing"                     // next think() reply; or a list to queue
        mock think error "timeout"               // next think() fails
        mock approve false                       // next approve() answer (one per call)
        mock price_check 120                     // next call of the handler of that name (a tool, an
        mock Notifier.send error "down"          // http wrapper) — Cell.h: THAT cell's only — answers / raises instead;
                                                 // error "not_found: x" raises kind not_found
        mock now 1700000000                      // freeze now()/now_ms()/today() until the next mock now (1700000000.25 or `mock now_ms …` for sub-second)
        property "sum" forall n: Int in 0..100 ensures f(n) >= 0   // 0..100 = 0…99, every value (≤ 20k); ONE Int variable over a range; iterations share the test cell's slots (a writing body sees earlier iterations' writes)
    }
}
```
`soma test` isolates storage (fresh per run), runs `[native]` handlers natively,
and — with no LLM key configured — mocks `think()` (echo: reply = prompt).
A mock answers the NEXT matching call, even one in a later rule (a queue like
`mock think ["a", "b"]` spans rules); a mock still unused after a rule that
raised is discarded (with a note). A mock naming no handler, a test helper
named like a program handler or a builtin, and test cells that assert nothing
are errors. Each `cell test` starts with fresh slots,
machines, mocks and trace(). `soma test --json` gives one record per rule.
`approve()` never answers on its own: unscripted it raises `approval_required`
(also under serve; SOMA_APPROVE=always|never is the explicit unattended
policy; `soma run` at a terminal asks). `assert` needs a Bool. A test cell
calls the handlers of every cell unqualified, or as `Cell.handler(…)`; slot
methods (`m.get(k)`, `xs.len`) work there too. A failure prints the asserted
source, `file:line`, left/right, and the fields a value really has when
`x.field` came back `()`.

## Things you would otherwise guess

- A fresh id is implicitly in the initial state: `transition(id, "held")` on an
  id nobody created is legal; `has_state(id)` is true only once the id has
  TRANSITIONED — a record stored in a slot but never transitioned is "fresh"
  to it (test the slot for duplicates: `require m.get(id) == () else Dup`).
- `transition()`'s first argument is an INSTANCE id (an order, a ticket) — a
  String or an Int (`42` and `"42"` are one instance; `()` is refused), not
  the machine's name; one cell has one machine, any number of instances. A
  cell without a machine may call transition() / get_status() when the
  program has exactly one machine; that machine's guards then read the
  CALLING handler's locals (a check error if it does not bind them).
- A slot is a Map or a List (`n: Int` is a check error); a handler parameter
  may not take a slot's name (reads and writes would mix the two). Read a
  whole slot by its bare name (`history`, `counts`); write with
  `counts.set(k, v)` / `counts[k] = v` / `history.push(x)`; `history = …` is
  an error. An invariant on a Map slot applies to every value written (`value`
  / `key` name the value and key being written — only inside an invariant;
  `slot.get(key)` there is the value BEFORE the write: `invariant value >=
  (versions.get(key) ?? 0)` keeps versions monotone); it is
  a pure condition (on a List slot `key` is the element's Int index) — no
  handler call, think(), transition(), I/O or network,
  even inside a lambda or an interpolation (a check error).
- `r.kind` of a refused write is `"invariant"`; of a bad `transition()`,
  `"invalid_transition"`; of `require … else Tag`, `"Tag"`.
- Every parameter has a type (`x: Any` takes a value of any kind — check it
  with `type_of(x)`); element types too (`xs: List<Int>`).
- Declared parameter types are enforced at runtime: `add(points: Int)` given
  `2.5` raises kind `type` (400) before the body runs — no `is_int` check needed;
  a missing value `()` is refused for a List parameter (a Map parameter accepts
  `()`: an absent record, such as an empty tree).
- Values are copies: `let row = s[k]  row.count += 1` changes `row` only —
  write it back (`s[k] = row`); a map read from a slot is a copy too
  (`cards.set(id, c)` after editing `c`). Records keep their field order.
- In `cell test`, `request(...)` is an ordinary call: an error it does not
  catch RAISES (assert it with `assert_fails request(...) matching "not_found"`);
  the kind → HTTP status mapping is applied by `soma serve` only. Return
  `response(status, …)` yourself when a test must see the status.
- `"""…"""` is raw for escapes (`\t` stays two characters) but `{x}` IS
  interpolated; write `{{` for a literal brace.
- `[1, 2] + [10, 20]` is element-wise (`[11, 22]`; Floats when a value is
  one); `concat(a, b)` joins lists.
- Persistent data lives in `.soma_data/` beside the program (serve and run);
  `soma test` starts empty. A slot gives back exactly what it accepted (an Int
  beyond 64 bits stays an Int); a value that does not fit the slot's declared
  value type (`Map<String, Int>` given a String) is refused with kind `type`.
- On a List slot: `rows.push(x)`, `rows[i] = x`, `rows.delete(i)` (by index),
  `rows.get(i)`, `rows.len` — all invariant-checked. A Map slot's `.keys` /
  `.values` / `.entries` come SORTED by key (every backend); a LOCAL map
  (`keys(m)` on a `let`) and a record's own fields keep insertion order.
  `keys(record)` / `values(record)` on a record (`Line { … }`) are its
  declared fields, in order; `r.field = v`, `r.field += 1` and
  `xs[0].field = v` check the field's declared type.
- A bare call to a name two cells define (`pack(id)` with `Orders.pack` and
  `Warehouse.pack`) is a check error from a third cell: qualify it
  (`Warehouse.pack(id)`). Inside `Warehouse` the bare call runs Warehouse's
  own `pack` (check warns); write `Orders.pack(id)` for the other.
- `xs[i]` is the same everywhere (local list, List slot, string): negative
  from the end, kind `index` out of range, kind `type` for a non-Int;
  `nth(xs, i)` and `rows.get(i)` answer `()` out of range instead (a
  negative `i` still counts from the end: `nth(xs, -1)` is the last). A `let`
  named like a memory slot hides the slot (check warns).
- `emit ev(data)` inside one process is a synchronous, atomic fan-out to
  every cell with `on ev(data)`, the emitting cell included (a handler does not
  receive its OWN event: `on ping` emitting `ping` does not re-enter itself —
  recurse with a call): a listener that raises fails the emitter,
  and the emitter's rollback takes the listeners' writes with it. Only across
  processes (the `[peers]` bus) is an emitted event an effect that is not
  rolled back. `soma check` warns when nobody handles the event.
- A bound is proven only against LITERALS: repeat the number in the
  invariant and in the `require` (there are no constants; a handler returning
  it is not used by the prover).
- `invariant rows.size <= 500` (NOT `len(rows)`, which in an invariant
  measures the value being written; a bare `size <= 500` that names no slot
  bounds EVERY slot of the memory) is proven when the handler's ONE write that
  can add an entry (a `push`, or a `set` of a key not known to exist) comes
  after `require len(rows) < 500 else Full`, is not in a loop or a lambda, and no
  handler it calls (or event it emits) adds to the slot too; a `set` after
  `require rows.get(k) != () else Missing` (or in the `else` of `if rows.get(k) == ()`)
  cannot grow the slot.
- An invariant is checked AT each write: a `require` proves only the writes
  that come AFTER it. A `require` counts for the writes of its own block and the blocks nested
  in it — `if ok { require n < 3 else Full  m.set(k, n + 1) }` is proven; a require
  inside a loop body narrows that iteration's `let` locals only.
- A trailing `Map` parameter is optional: `on add(a: Int, opts: Map)` is
  callable as `add(1)` (`opts` is `map()`) — the keyword-argument idiom,
  read with `opts.step ?? 1`. HTTP headers reach `request` as a fifth
  `headers: Map` parameter (lower-case names).
- HTTP out: `http_get/post/put/patch/delete(url, body?, map("timeout", ms,
  "headers", map(...)))` never raise on the network (a timeout, a refused
  connection, a non-2xx answer come back as values); an invalid or unknown
  option raises kind `type` (a program bug); non-2xx is `{error, kind, status, body}`
  (kind `http_status` — redirects are followed up to 5 hops; a 3xx left unfollowed (a 307/308 answering a POST) is http_status too, a 6th hop is kind `network` (too many redirects) — | `timeout` —
  also a body that stalls — | `too_large` over `max_bytes` | `refused` |
  `network`); default timeout 30 s; invalid option values are refused;
  a String body is sent as text/plain unless it is JSON; `mock http_post …`
  in tests.
- `verify --strict` bounds a write only from numbers it can bound: literals,
  slots with an interval invariant, and values narrowed by `require`/`if`. A
  number read out of a record (`a.balance`) is unbounded until a `require`
  narrows it; the ⚠ line says why (`` `v` = a.balance — not bounded ``, or
  `` `v` is only known to lie in [0, ∞) — narrow it: `require v <= 100 else …` ``).
- `ensure cond` at the end of a handler raises kind `ensure` (422) when the
  postcondition is false — the whole handler is rolled back. In a `[task]`
  handler it undoes the CURRENT step only: writes made before the last
  think() are already committed (check warns).
- Dates: `parse_date("2026-03-01")` → map(year, month, day, weekday, epoch_day),
  `add_days`, `add_months`, `days_between`, `months_between`, `days_in_month`,
  `format_date(ts)` (a date argument may also be an Int Unix time in seconds,
  as now() returns — validate client input as a String); ISO strings compare with `<`. Dates are UTC and there
  are no time zones or time-of-day builtins: keep a fixed offset per place
  (`let local_min = floor_div(now_ms(), 60000) + offset_min` — now() is seconds) and parse "HH:MM"
  yourself (`split(t, ":")`); `every` / `after` run in any cell, `request` or not.
- Money: Ints in cents (any size, exact); `div_round(n, d)` is HALF_UP
  division (`div_round(cents * bps, 120000)` = BigDecimal interest at scale 2);
  `format("%10.2f", …)` only for display, `money = "{idiv(c, 100)}.{…}"` for exact text.
- Data: `read_csv(path)` → List<Map>: RFC 4180 (quoted `"a, b"`, `""`, multi-line
  cells); unquoted cells auto-typed (`1.00` → 1.0), quoted cells and `007` stay
  Strings; `read_csv(path, map("raw", true))` keeps all text (exact money);
  `map("delimiter", ";")` reads `;` files (other options are refused);
  `from_csv(text, opts?)` parses CSV text already in memory (an upload);
  `to_csv(rows)` is the text `write_csv` writes (a download).
  `write_csv` quotes what a reader would change (a String "12" stays a String;
  a List cell is its JSON text). One builtin call builds at most 100,000,000
  characters / matrix cells (`pad_left`, `format` widths, `zeros`…) and a List
  of at most 10,000,000 (`range`); an Int holds at most 2^24 bits (a product,
  shl, product(), parse_int / to_int of text past it is refused before it is
  built); matmul does at most 10^9 multiply-adds, pow_mod bits(exp) × bits(m)
  ≤ 2^30 — past any of these it raises kind `range`. Map slot keys are text
  (`m.set(1, …)` and `m.set("1", …)` are one entry).
  `use helper` imports helper.cell beside the program, `use lib::m`
  lib/m.cell (a `use` inside an imported file resolves beside THAT file);
  imported handlers are callable by name; an imported file's
  test cells run only under `soma test lib/m.cell`. `agg`, `sort_by`,
  `top`, `median`, `pstdev`; `stdev` / `variance` are SAMPLE (n − 1) like
  Python's statistics, `pstdev` / `pvariance` population. `|> map`, `|> filter`,
  `xs[i]`, `len(xs)`, `nth(xs, i)`, `xs.len` and a List slot's `rows[i]` /
  `rows.len` cost O(1) per call (20k rows in 0.1 s); passing a big list to a
  handler COPIES it (values are copies) — loop inside the handler, or pass
  an index.
- `think_json()` raises kind `json` when the model does not answer a JSON
  object (catch it with `try`); a ```json fence around the object is fine.
  A mocked `think` costs ~4 characters per token, so `set_budget` exhaustion
  (kind `budget`) is testable offline. Under `soma serve`, `trace()` keeps the
  last 1000 steps process-wide.

## Scheduled work

```soma
every 30s { expire_due() }      // under soma serve: runs at start-up, then every 30 s (units: ms s min h d — 500ms, 90min, 24h, 1d);
                                // a daily job at a time of day: `every 1h` + a "last run" slot compared with today()
after 10s { warm_cache() }      // once, 10 s after start-up
```
A tick is a handler invocation: atomic, serialized with requests (and with
other processes on the same `.soma_data`), rolled back and logged if it
raises; the next tick still runs. The interval counts from the end of the
previous tick. verify checks the `transition()` targets of these blocks too.

## Handlers are atomic

With SQLite or in-memory storage, a top-level handler invocation is
all-or-nothing: if it raises, its slot writes and transitions are rolled back. A failing `try { }`
block's slot writes, transitions and pushes are rolled back to where it started (plain locals it assigned keep their new value), and the handler continues. Under
`soma serve` handlers run one at a time (a [task] handler: each step between think()s), so read-modify-write is safe
(300 parallel payments of 10 against a balance of 1000 pay exactly 100).
`[immutable]` on a slot makes it append-only: a List slot only grows by
`push`, a Map slot only gains new keys; overwriting or deleting an entry
raises kind `invariant` (an audit log that cannot be truncated or rewritten).

With SQLite persistent slots the handler IS one SQLite transaction: a process killed
mid-handler (`kill -9`) leaves nothing of it on disk. `every` / `after` ticks
are handler invocations too (same rollback). You do not write compensation
code. Not rolled back: effects outside the process (http calls, think(),
emitted events). Storage read failures abort the invocation even inside `try`.
The legacy JSON backend only replaces individual files; it has no multi-slot
transaction or cross-process isolation. The HTTP provider adapter has no remote
transactions, and a failed write may have reached the remote service.

## Errors

```soma
fail("not_found", "reservation {id}")     // raise: a kind + a detail
require amount > 0 else InvalidAmount      // raise with kind InvalidAmount (a bare tag)
require open < 3 else LoanLimit "{member} holds {open} loans"   // kind + interpolated detail
let r = try { reserve(id) }                // r = {value, error, kind, detail}
if r.kind == "not_found" { return response(404, map("error", r.detail)) }
if r.error != () { fail(r) }               // re-raise unchanged
```
Kinds raised by the runtime: `invalid_transition`, `guard_failed`, `invariant`,
`ensure`, `division_by_zero`, `index`, `llm`, `budget`, `type`, `json` (a body
that is not JSON), `stack_overflow`, `approval_required` (`approve()` with
nobody to answer). Branch on `r.kind`, never on substrings of `r.error`; in
tests `assert_fails f() matching "not_found"` matches the kind or the message.

## HTTP

`response(status, body)` is a map `{_status, _body}` (assert `r._status == 404`);
`html(..)`, `redirect(..)` likewise. A handler may also return a plain map or
string (200). `soma run app.cell request GET /path ""` calls the router without
a server; `soma serve app.cell -p 8080` serves it. Static files: `static/`.
`soma serve` ALSO exposes every public handler of the request-owning cell at
`/<handler>/<arg>/<arg>` (that is how forms post to `/add`). A path that
`request` matches explicitly goes to `request`; prefix handlers that must not
be reachable over HTTP with `_` (`on _debit(…)`); `start`/`init` are never
endpoints. A handler that changes state (a slot write, a transition, an emit,
a call into another cell) answers GET/HEAD with 405 — POST to it. A request
body may not carry `_type`/`_variant`/`_values` anywhere in its JSON, even
for a `body: String` handler (a client cannot forge a record or a variant). Only a map built by `response()` / `html()` / `redirect()`
is an HTTP response: a returned map with `_status` keys from client data is
plain JSON. Response header values with CR/LF are dropped. A handler that
calls `from_json` on other client text (a ws message, a decoded field)
builds whatever declared variant it names — shape-checked (a missing or
mistyped field raises kind `type`), but validate WHICH variant. Realtime: `on ws(msg: String)` (port+1, same-origin browsers
only), `publish(stream, data)`, `sse(...)` routes — pushes (publish and emit)
leave AT COMMIT, never from a rolled-back handler; an `emit` target is not an
HTTP endpoint (`soma docs serving`, Realtime). `NaN`/`inf` in a path
or query stay Strings. `soma check` warns when a
handler and a route share a name unless the route delegates to that handler. `body: String` is the raw text
(`from_json(body)`); `body: Map` is the parsed JSON (a non-JSON body is a 400
before the handler runs, kind json; `soma run` parses its text argument the
same way). In a test cell pass the Map itself — `request("POST", "/x",
map("a", 1))`: a String argument there is a `type` error, not parsed. A raised error
answers with its kind: not_found → 404, unauthorized → 401, rate_limited → 429, guard_failed → 403, invalid_transition
→ 409, invariant → 422, your own `fail("tag")` / `require … else Tag` → 400, as
`{"error": message, "kind": tag}`. A plain return answers 200: a map/list as
JSON, `()` as `null`, a String or number as `{"result": …}` (a String
that is valid JSON text, like `to_json(x)`, is sent as that JSON). Path segments and
query values are coerced to the parameter's declared type (`/decide/x/true` →
Bool). Every response carries `Access-Control-Allow-Origin: *`. `request` may
be declared in `face` or not; its return type is not checked (a route answers
whatever it returns). `serve` binds 127.0.0.1 (`--host 0.0.0.0`
to expose), refuses a taken port and a program that fails check, and survives a
handler's runaway recursion (500 `stack_overflow`; the process stays up).

## Verification properties

`soma verify` proves, for every cell with a state machine: reachability,
deadlock-freedom, liveness (every state can reach a terminal — or, with no
terminal state, return to the initial one: a reactive machine passes --strict), refinement (each
handler's `transition()` targets are declared states — the SOURCE of a
transition is the instance's runtime state, so a removed edge is caught at
runtime as `invalid_transition`, not by verify; declare `[verify.before.X]
requires` for the edges you care about), and termination of every
handler whose recursion has a decreasing argument — a handler it cannot prove
(`while true`, `rec(n + 1)`) is a ⚠ warning, not a proof, and the runtime
depth guard is what stops it. `property … forall n in a..b` in tests walks
EVERY value when the range has at most 20,000 values; a wider range is only
sampled (50 values, fixed seed — not a proof). State more in a `soma.toml` beside
the program (`[package]` is optional; an unknown key is an error). The properties
apply to every machine of the cells in `cells = [...]` (all cells when absent):
a property whose TARGET state one machine lacks is vacuously true there (but
`before.X requires [Y]` with X present and Y absent FAILS: X is reachable
without Y) — output names each machine `Cell.machine` when there are several; split
programs, or scope `cells`, when two machines need different properties:

```toml
[verify]
cells = ["Expense"]                 # optional: which cells these apply to
deadlock_free = true                # (always on; the key is accepted)
eventually = ["paid", "rejected"]   # every path reaches one of these (AF)
never = ["corrupt"]                 # unreachable states (AG not)
always = ["a", "b", "c"]            # the machine is only ever in one of these

[verify.after.rejected]
never = ["paid"]                    # `paid` is unreachable once `rejected` was reached
eventually = ["archived"]           # after `rejected`, every path reaches `archived`

[verify.before.paid]
requires = ["manager_approved"]     # precedence: no path reaches `paid` without ONE of these
requires_all = ["held", "picked"]   # …without EACH of these
```
In the machine, `* -> failed` means from EVERY state — it also adds
`paid -> failed`, so `paid` is no longer final (verify says so). Keep states
final with `* -> failed except [paid, denied]`. A property naming a state no
machine declares is an error, and verify ends with one verdict line
(`VERIFY OK` / `VERIFY FAILED — …`). `soma verify` and `soma test` refuse a
program that fails `soma check`. Invariants on computed values are proven by
induction when interval reasoning suffices (`(counts.get(k) ?? 0) + 1` keeps
`counts >= 0`; `let open = …  require open < 3 else Full  set(k, open + 1)` keeps
`<= 3` — an unconditional `require` on a once-bound local counts); the rest
is reported per conjunct as runtime-checked.
`soma verify --strict` fails on every ⚠ too (a proof that degraded to
runtime-checked, an unprovable termination) — the CI gate.
A failed property prints a counter-example path and is an error. What verify
does NOT prove: data-dependent rules inside handlers, and invariants on computed
values (those are runtime-checked — reported as such, never as "proven").
Guards (`a -> b { guard { cond } }`) are enforced at runtime and read the
locals of the handler that calls `transition()` — so EVERY handler whose
`transition()` targets the guarded state must bind those names (check error
otherwise), even one meant for another edge; the model keeps guarded edges.
A guard is a pure condition: calling a handler, think(), next_id() or a slot
write (`.set`/`.delete`/`.push`) inside it is a check error — compute the value
in the handler before `transition()` and test that local. The calls in a
`require` condition and in its `else` detail are part of the termination,
cost and invariant analyses like any other statement.
A `cost { tokens: N }` bounds the REPLY tokens (the sum of the max_tokens
caps of the think() calls a handler can make — ×10 provider rounds in an
agent with tools, or × `map("max_rounds", N)`); prompt tokens are not in it —
`set_budget` / `tokens_used()` count prompt + reply, per request under serve
and per rule in a test (return `tokens_used()` from the handler to assert on
it); `tokens_remaining()` is -1 without a budget, never below 0 with one; a
`set_budget` reached from a model's tool call (a delegated agent's own)
only lowers what is left — it never lifts or resets the caller's. A cost bound that cannot
be proven (a think() without a literal max_tokens) is a check ERROR.

## Agents (LLMs inside the cage)

```soma
cell agent Researcher {
    face {
        signal research(topic: String) -> Map
        tool search(q: String) -> String [capability: "https://api.x.com/*"] "Search"
    }
    cost { tokens: 6000 }                             // PROVEN by soma check: 2000 × 3 rounds
    state job { initial: idle  idle -> working  working -> done  * -> failed except [done] }
    on search(q: String) { return to_json(http_get("https://api.x.com/search?q={q}")) }
    on research(topic: String) {
        set_budget(8000)                              // token cap: a prompt that alone overruns what is left raises kind budget before it is sent; otherwise the provider round that crosses it completes and the NEXT round (a later tool round of the same think() too) raises kind budget
        transition(topic, "working")                  // one machine instance per topic
        let r = try { think("Research {topic}", map("max_tokens", 2000, "max_rounds", 3)) }
        if r.error != () {
            transition(topic, "failed")
            return map("error", r.kind)
        }
        transition(topic, "done")
        return map("facts", r.value, "spent", tokens_used())
    }
}
// `on ask(q: String) [task] { … think(…) … }` runs as STEPS: each think() ends
// the current step (its writes commit) and waits for the model OUTSIDE the
// handler lock, so concurrent requests overlap their model calls (200 × 2 s
// waits in ~9 s instead of 400 s); a failure rolls back the current step only
// (writes before the last think() stay — a `try` cannot undo them either);
// the prover does not carry a read or `require` across a think (another
// request may write meanwhile): read, require and write AFTER the last think.
// Only the ENTRY POINT decides: a [task] handler called from a plain handler
// (`on request` routing to it, a listener, a tick) runs inside the caller's
// atomic unit and holds the lock — mark the caller [task] too:
// `on request(method: String, path: String, body: String) [task]`,
// `every 1min [task] { … }`, `after 5s [task] { … }`. check warns on each
// of these. SOMA_LLM_MOCK_LATENCY_MS gives a mock a latency to test it. A
// plain handler stays one atomic unit. Unknown handler annotations
// ([tsak]) are errors; known: [native], [task], [deterministic], [record].
// HORDES — one [task] handler over many inputs with a bounded pool:
//   let h = horde(Reviewer.review, docs, map("concurrency", 200,
//       "on_result", "_store", "on_done", "_summarize", "on_error", "_failed",
//       "max_attempts", 2))                // returns "Audit:h1" at once
//   on _store(v: Map) { verdicts.set(v.id, v) }       // or _store(input, result)
//   horde_status(h)  → {state, total, queued, running, done, failed, cancelled, tokens}
//   horde_results(h) → results in input order (() if not done); horde_cancel(h)
// The target takes one parameter; mark it [task] (check warns when it
// thinks: each task would hold the lock). Write the target and the options
// AT THE CALL (a literal map with literal handler names — check refuses a
// computed target or options: they decide what runs and what it costs);
// name callbacks `_…` (a public one is an HTTP endpoint). Only the owner
// cell (and test rules) can read or cancel a horde. The queue is stored in
// soma.db under serve / run, even without a [persistent] slot: a restart
// resumes it; with several servers on one .soma_data each horde runs in one
// of them (a lease, taken over ~6 s after its server stops). A task's
// result is recorded — and on_result called — in the same atomic unit as
// its LAST step, so each result is written once even after kill -9; steps
// before its last think() may run again. on_error(input, error: Map
// {error, kind, detail}) after max_attempts (default 1); on_done(id) once,
// when nothing is left (cancel included). concurrency default 8, max 1000.
// Without workers (`soma test`) the horde runs right after the calling
// handler commits — its next statements run first, as under serve — one
// task per unit. A restart does not resume a horde whose target or
// callbacks the new code renamed (it says so; the tasks wait).
// BUDGET: map("budget_tokens", 2000000) is a hard ceiling for the whole horde — every think() of its
// tasks and callbacks first RESERVES an upper bound (request bytes +
// max_tokens), waits outside the lock for calls in flight to settle if it
// does not fit yet, and is refused (kind budget) when it never will; the
// horde then stops (state "exhausted"; tasks it stopped count as
// cancelled, no on_error). A horde started inside a task or callback of a
// budgeted horde runs under that budget too (nested hordes cannot spend
// past it). on_done's think() also counts: keep headroom for it. A
// provider that ignores max_tokens raises kind llm, charged what it
// reported. The ceiling counts SETTLED calls: calls in flight
// at a kill -9 were sent, then are sent again after the restart. soma verify prints each horde's bound:
// the literal budget_tokens, else inputs × per-task × max_attempts for a
// literal list/range (reply tokens), else unbounded — a horde in a cell
// with `cost { tokens: N }` needs a literal budget_tokens to prove it.
// ROUNDS (simulations): map("snapshot", world, "apply", "_apply", "seed", 7,
// "instance", "id") — the target takes (input, snapshot): every agent of
// the round sees the same world; `apply(result)` / `apply(input, result)`
// runs at the END, in input order, once per task (not as replies arrive),
// then on_done — which may start the next round (a horde() in on_done).
// seed: random() in task i draws the same numbers on every run. instance:
// the input field naming an agent; its remember()/recall() keys and its
// conversation are its own and persist across rounds. 10 000 agents × 20
// rounds: 46 s, identical on every run. After a crash, steps before a
// task's last think() may run again — write memory in the last step.
// vote(Cell.handler, input, k) → {winner, count, k, unanimous, errors,
// votes}: k agents on one input (in a [task] step under serve/run they run
// at once, outside the lock); the most common answer wins. Provider limits
// for every think() of
// the process: soma.toml [agent] rpm = 500, tpm = 200000 (or SOMA_LLM_RPM /
// SOMA_LLM_TPM): at most rpm requests / tpm tokens in ANY 60 s window; a
// 429 pauses every caller. Measured: 10 000 tasks with a
// 2 s mocked model, concurrency 500, in 41 s.
// soma verify PROVES the lifecycle; `cost { tokens: N }` (also latency:,
// usd:) is PROVEN when every think() has a literal max_tokens and runs a
// known number of times — with tools, × the rounds (`max_rounds`, else 10).
// `latency` counts WAITING: each think()'s `timeout` (a total, retries
// included — the wait for a rate limit and a mock's latency too) × its
// rounds, http timeouts, literal sleep()s, vote() × k; approve(), file/stdin
// reads and computed sleeps make it advisory; CPU time is not in it. `usd`
// is the REPLY tokens × the price the table knows for the cell's model
// (prompts are not counted; a model the table does not know makes it
// advisory) — an estimate of the provider's bill, not the bill.
// The model may call only the face's `tool`s (never a private or other
// handler), with typed arguments, within their capabilities (URL patterns with
// `*`: "https://api.x.com/*"; a tool with no capability is unrestricted; a
// tool that calls think() makes a `cost` bound unprovable, a tool doing I/O a
// `latency` bound; I/O in a loop or lambda leaves a `tokens` bound provable) — the scope binds
// MODEL calls only (your own code calling the tool handler is not
// restricted), and a tool is not an HTTP endpoint; `mock think` scripts text
// replies only (to test tool calls offline, point [agent] url at a fake
// OpenAI-chat-compatible server: tools go out as `tools`, results come back
// as `role: "tool"` messages, think_json sets response_format json_object,
// usage.total_tokens feeds tokens_used(), usage.completion_tokens is held to
// max_tokens); a tool call that raises is rolled
// back. `map("max_rounds", N)` caps the tool-call rounds of one think();
// `map("tools_allowed", ["lookup"])` offers only those tools to that call
// (classify with no refund tool in reach); a `*` in a capability stays in
// its part of the URL (host or path), `..` segments and userinfo are
// refused, and a tool's scope holds for the tools of any agent it calls;
// a scoped tool reads/writes no file (read_file, load, include, …) and opens
// no link/socket. An unknown option, or a tools_allowed name that is not a
// tool, is an error. A reply longer than its max_tokens (a provider ignoring
// the cap) raises kind `llm`; a tool that calls back its think() handler is a
// termination ⚠ (the model drives that recursion). Each agent cell keeps its OWN multi-turn
// context (clear_context() resets it); every/after ticks use the same
// [agent] config as requests. `soma test` mocks think() only when no key is
// configured — set SOMA_LLM_MOCK=echo for offline tests with a soma.toml key;
// `mock h [[1, 2]]` scripts ONE List answer ([1, 2] is a queue of two).
// approve(msg) is a gate a PERSON answers: tests script it (mock approve),
// serve raises approval_required unless SOMA_APPROVE says otherwise (and
// the handler rolls back) — for a web flow, commit a pending state in one
// request and decide in another (POST /decide/…); approve() is for run/test.
// think(prompt, map(..)) or think(prompt, system, map(..)): options go LAST.
// Offline: `mock think …` in tests, SOMA_LLM_MOCK=echo | fixed:TEXT |
// rules:mocks.json — a list of {"match": "substring of the prompt",
// "cell": "AgentCell", "reply": "text" or a JSON value}: the first rule whose
// match / cell fit answers, none: an echo — or
// [agent] mock = "echo" in soma.toml. Record/replay: `soma run --record` (not serve) logs each top-level
// call; `soma replay` re-runs them from EMPTY storage with the soma.toml
// [agent], calls think() again (replies are not recorded) and compares the
// RESULTS — a state difference shows only in a later result.
```

## Top gotchas (full list: /docs/gotchas.md or /gotchas.json — all verified)

1. `f(args)` calls YOUR handler `f` when one takes that many arguments, the
   builtin `f` otherwise (`on list() { return list(1, 2) }` reaches the
   builtin). `soma check` warns when an argument count sends a call to a
   builtin you probably did not mean. Another cell's handler: `Ledger.post(x)`
   (or bare `post(x)` when the name is unique); `get_status(id)` answers the
   initial state for an unknown id — `has_state(id)` tells them apart.
2. `match` arms use `->` (`=>` is lambdas). Handlers don't declare return
   types (face signals do).
3. An unescaped `"` inside `{...}` ends the string — escape it (`{m[\"k\"]}`) or bind a let first.
4. `==` is structural on lists, maps and variants (`[] == []`, key order
   irrelevant). `null`/`None` do not exist: null is `()`, test with `x == ()`
   or default with `x ?? 0`.
5. `transition()` returns {id, from, to}; read state with get_status(id).
   Wrap fallible transitions in try { }.
6. Slot methods (.set/.get) are for `memory` slots; local maps use m[k].
7. `assert_fails expr` needs an expression that RAISES (not a falsy bool).
8. serve routes only the cell that owns `request` — put routable signals
   there, delegating to domain cells.
9. Adjacent string literals don't concatenate (`return "a" "b"` is a check
   error). Language keywords (on, given, cell, agent, tool, use, require,
   promise, let, if, match, return, …) are not names — `soma check` says
   which one and how to rename it. Reserved HANDLER names (they would replace the
   builtin): transition, approve, fail, get_status, has_state,
   valid_transitions, think, think_json, set_budget, tokens_used.
10. Floats: compare with a tolerance, never ==.
11. `7 / 2` is `3.5` — everywhere, `[native]` included. `idiv(7, 2)` is the
    integer quotient (truncates toward zero, BigInt-exact). `pow` is a Float
    power; `ipow(3, 40)` is the exact Int power (no `**` operator).
12. One memory invariant names one slot; `size` invariants also guard
    `delete`. A cost bound is *proven* only when every `think()` runs a
    known number of times (literal `range`, or an annotated loop: `for [loop_bound(50)] x in xs { … }`, `while [loop_bound(50)] cond { … }` — checked: more iterations raise kind
    `loop_bound`); a declared
    bound that cannot be proven is a check ERROR.

## Packages

```toml
[dependencies]
matrix = "^0.2"                  # semver; registry at soma-lang.dev/repo
local = { path = "../pkg" }      # or git = "...", subdir = "packages/x"
```
`soma install` → .soma_env/packages/, commit-pinned in soma.lock with a
sha256 of the files (sub-directories included): a package modified after
install, or holding a file the lock does not list, is refused at import
(`soma install` restores it); an imported cell that defines `request` or
`ws`, or declares `every` / `after`, is a check warning (it would own HTTP routing / the WebSocket port).
`use matrix` imports it. A package's API = its face; its proofs (cell test)
re-run on YOUR toolchain: `soma test .soma_env/packages/matrix/matrix.cell`.

## Performance

Interpreter is the reference semantics (linear-time `map`/`filter`/indexing;
a 20k-row CSV aggregation runs in ~0.3 s interpreted). Annotate hot handlers
`[native]` for Rust-codegen: measured at rustc -O parity (16.8 ns/op) on
numeric loops; a native compile failure aborts the run (there is no silent
fall-back to the interpreter). It needs `cargo` (rustup) on PATH; the first
compile takes seconds and is cached in `.soma_cache/` beside the program.
Arguments are type-checked at the call like any handler; `random(n)` /
`random(lo, hi)` are Ints, `random()` a Float; buffer indexes are Ints from 0
(no negative indexes); an Int literal beyond 64 bits is refused (build it:
`shl(1, 64) - 1`); `[loop_bound(N)]` is checked; a `[native]` handler's
recursion deeper than 20,000 calls raises stack_overflow (interpreted
handlers: 512 — walk deep structures with an explicit stack). Floats print with the shortest
round-trip digits; print/to_string never use exponent form (`1e-7` prints `0.0000001`, a Float inside
a printed map or list too; `format("%.3e", x)` for scientific notation); to_json — HTTP bodies included — uses JSON's shortest form (`1.18e21`).
An SSE `data:` line and a WebSocket push carry the value as JSON on one line
(a String payload is quoted, so a client cannot forge another event).
Native math: sqrt, log, exp, pow, abs, min, max, floor, ceil, round, sin,
cos, tan, atan, atan2, asin, acos, pi() (asin/acos outside [-1, 1] raise
kind range, as interpreted). `soma check` verifies the native vocabulary (every handler, every error at
once). Same semantics as the interpreter: `7 / 2` is 3.5, a division by zero
is an ordinary `try`-catchable error, an Int overflow promotes to BigInt, and
an Int slot refuses a non-exact `/` instead of truncating. One difference:
native code is statically typed: a quotient returned or stored as an Int
is the exact Int (`return a / b` gives -7 for -7 / 1; an exact quotient past
2^53 raises natively — use idiv(a, b) there), but inside an
expression that needs its type — `to_string(a / b)` — it is a Float
("-7.0") — `soma check` warns; write idiv(a, b) for an integer quotient. A native local keeps the
type of its `let` (assigning a String to a number local is a check error).

What a `[native]` handler may use — nothing else:
- parameters and locals: Int, Float, Bool, String (a List cannot cross the
  boundary in either direction: parse the input into buffers inside the
  handler, return a String)
- arithmetic, comparisons, `if`/`while`/`for i in range(a, b)`, `return`,
  sqrt log exp pow abs min max floor ceil round sin cos random, idiv gcd
  pow_mod sqrt_int, band bor bxor bnot shl shr bit_len bit_test bit_set
  bit_clr bit_next, to_int to_float to_string, str_len str_at str_eq,
  sibling `[native]` handlers
- arrays: `buffer(n) -> Buf` (n Ints, zeroed), `buf_get(b, i) -> Int`,
  `buf_set(b, i, v)`; `buffer_f(n)` / `buf_get_f` / `buf_set_f` for Floats
- maps: `hashmap() -> HMap` (Int → Int), `hm_get(m, k)`, `hm_set(m, k, v)`,
  `hm_inc(m, k)`, `hm_len(m)`, `hm_has(m, k)`
- strings: `strbuf() -> SBuf`, `sb_push(b, s)`, `sb_push_int(b, n)`,
  `sb_push_char(b, c)`, `sb_len(b)`, `sb_finish(b) -> String`;
  `regex_count / regex_replace / regex_match`; `read_file read_stdin
  write_str` (write_str flushes; an Int overflow re-runs the handler in
  BigInt mode, so text written BEFORE the overflow is repeated — keep
  write_str away from overflow-prone arithmetic, or return the text)
- a Buf/HMap/SBuf lives in ONE variable of ONE handler: it cannot be
  re-bound (`let t = u  u = v` — copy elements instead), returned, or passed
  to a sibling (pack results into a String with strbuf). A Buf holds 64-bit
  Ints: a value that overflows i64 while stored into it is a `range` error
  (scalars promote to BigInt; mask the value or keep it scalar). `for` takes
  `range(a, b)` only (a step → `while`). A literal `/ 0` does not compile.
  `soma check` reports all of these.
- one FFI call costs ~2 µs: make the LOOP native, not just the per-element
  kernel (10^7 sibling calls inside a native loop: 20 ms; 2·10^6 calls from
  an interpreted loop: 3.5 s).
Not available natively: maps/lists/records, think(), memory slots, `try`,
`match`, string interpolation — call an interpreted handler for those. The
buffer / hashmap / strbuf primitives exist ONLY in `[native]` handlers
(`soma check` refuses them elsewhere); everything else in the list, `sin`,
`regex_*`, `read_stdin` included, works in interpreted handlers too.

## Learn from working code

- https://soma-lang.dev/corpus/index.json — 300+ programs, all passing
  check+test (algorithms, web, agents, state machines, finance, games,
  data, safety interlocks, medical, aerospace…). Before writing a cell,
  fetch one with the features you need and adapt it.
- treasury/ airlock/ poker/ elevator/ hft/ delivery/ — complete apps where
  the safety property is a verified theorem
- packages/matrix/ — the reference package (numpy-style linalg, 43 proofs)

---

# Robotics robustness audit — 100 scenarios

These scenarios exercise Soma behavior relevant to robot controllers. They do not
qualify hardware, real-time performance or a lunar system. Each scenario is a
separate Rust integration test in `compiler/tests/robotics_robustness.rs`.

## Results — Soma 2.8.3, 2026-09-20

- Robotics campaign: **100 passed, 0 failed, 0 ignored**.
- Complete Rust suite: **523 passed, 0 failed, 0 ignored**.
- Core CLI fixtures: **118 passed, 0 failed**.
- Published corpus: **321 programs passed the website build checks**.

Measured locally on macOS ARM64. Linux CI reruns the full suite on every push
and pull request. This campaign confirmed the tested behavior without finding
an additional runtime defect. The source of every scenario is in
[robotics_robustness.rs](https://github.com/soma-dev-lang/soma/blob/v2.8.3/compiler/tests/robotics_robustness.rs).

## Scope and reproduction

Added in Soma 2.8.3 on 2026-09-20. This is a regression campaign for the
language, with inputs chosen for robot-controller use. The motor and sensor
values are simulated data; no physical hardware is driven.

Run all 100 independently named scenarios from the repository root:

```sh
cargo test --release --locked --manifest-path compiler/Cargo.toml --test robotics_robustness
```

Run them with every existing Rust test:

```sh
cargo test --release --locked --manifest-path compiler/Cargo.toml --no-fail-fast
```

IDs 001–080 cover numeric boundaries, sensor validation, mission transitions,
storage invariants, rollback and collection/JSON boundaries. IDs 081–090 test
the distinction between static rejection, proof, runtime checks and unproved
distribution. IDs 091–095 run native handlers, including comparison with the
interpreter. IDs 096–099 use fresh processes to check committed data and
rollback persistence; 100 distinguishes recorded errors from returned data.
`verify_fail` and `check_fail` mean the expected rejection is asserted, including
its diagnostic. A refusal is a passing test, not a waived failure.

The separate existing `compiler/tests/cluster.rs` suite covers actual network
replicas, seed failure, reconnect, stale updates, restart, and partition recovery.
The 100 scenarios below do not add consensus or distributed safety proofs.

## Limits

These are finite examples, not a proof for every input. They do not measure
worst-case execution time, memory exhaustion, radiation tolerance, sensor or
actuator faults, abrupt power loss, or hardware fail-safe behavior. Restart tests
exit processes normally after a commit or a rejected handler; they do not inject
power loss during a disk write. Local transaction rollback cannot undo a command
already sent to a physical actuator. The cluster remains experimental and
eventually consistent, with local reads and no fenced scheduler. Use the
[guarantees](https://soma-lang.dev/docs/guarantees.md) and
[cluster limits](https://soma-lang.dev/docs/cluster.md) when assessing a design.

| ID | Scenario | Check |
|---|---|---|
| 001 | encoder counts above float precision | runtime |
| 002 | odometer integer promotion | runtime |
| 003 | negative odometer promotion | runtime |
| 004 | wide distance products | runtime |
| 005 | large finite calibration ratio | runtime |
| 006 | negative fixed point division | runtime |
| 007 | subnormal measurement ratio | runtime |
| 008 | nearby large sensor variance | runtime |
| 009 | high dynamic range median | runtime |
| 010 | exact message sequence sorting | runtime |
| 011 | divide zero is catchable | runtime |
| 012 | integer divide zero is catchable | runtime |
| 013 | remainder zero is catchable | runtime |
| 014 | nan rejected by sensor guard | runtime |
| 015 | positive infinity rejected by sensor guard | runtime |
| 016 | negative infinity rejected by sensor guard | runtime |
| 017 | nan cannot become integer command | runtime |
| 018 | huge integer cannot silently become infinity | runtime |
| 019 | non numeric actuator math is rejected | runtime |
| 020 | failed math does not poison later commands | runtime |
| 021 | sensor guard accepts exact endpoints | runtime |
| 022 | sensor guard rejects out of range | runtime |
| 023 | missing telemetry is not zero | runtime |
| 024 | false telemetry is not missing | runtime |
| 025 | zero measurement survives coalescing | runtime |
| 026 | control vector arithmetic | runtime |
| 027 | vector shape mismatch is rejected | runtime |
| 028 | large sequence dedup is exact | runtime |
| 029 | sensor maps compare structurally | runtime |
| 030 | no sensor fusion from empty set | runtime |
| 031 | new rover is docked | runtime |
| 032 | nominal mission round trip | runtime |
| 033 | cannot drive before arming | runtime |
| 034 | repeated arm is not a second command | runtime |
| 035 | low power prevents arming | runtime |
| 036 | abort is terminal | runtime |
| 037 | abort stops driving motor | runtime |
| 038 | different robots have independent states | runtime |
| 039 | cannot skip to sampling | runtime |
| 040 | unknown transition is rejected | runtime |
| 041 | battery bounds are inclusive | runtime |
| 042 | battery underflow preserves old value | runtime |
| 043 | battery overflow preserves old value | runtime |
| 044 | invalid battery type is rejected | runtime |
| 045 | nan motor command is rejected | runtime |
| 046 | infinite motor command is rejected | runtime |
| 047 | motor bounds are inclusive | runtime |
| 048 | command queue capacity is enforced | runtime |
| 049 | immutable audit cannot be rewritten | runtime |
| 050 | immutable audit cannot be deleted | runtime |
| 051 | failed sample rolls back state and data | runtime |
| 052 | failed batch rolls back every slot | runtime |
| 053 | create then delete is undone | runtime |
| 054 | delete rollback restores existing record | runtime |
| 055 | repeated overwrites restore original | runtime |
| 056 | failed immutable append does not burn id | runtime |
| 057 | try is a nested savepoint | runtime |
| 058 | error kind and detail survive catch | runtime |
| 059 | short circuit and avoids invalid read | runtime |
| 060 | short circuit or avoids invalid read | runtime |
| 061 | negative list index reads last | runtime |
| 062 | out of range list index raises | runtime |
| 063 | fractional list index is not truncated | runtime |
| 064 | invalid range step is rejected | runtime |
| 065 | long command stream can stop early | runtime |
| 066 | queue elements obey declared type | runtime |
| 067 | map cannot silently accept list push | runtime |
| 068 | json preserves large command id | runtime |
| 069 | json overflow is rejected | runtime |
| 070 | untrusted json cannot forge unknown variants | runtime |
| 071 | empty string value is present | runtime |
| 072 | null value is distinct from missing key | runtime |
| 073 | null cannot be an accidental key | runtime |
| 074 | private storage keys are reserved | runtime |
| 075 | key and value views stay consistent | runtime |
| 076 | missing delete has no side effect | runtime |
| 077 | text command ids are not coerced | runtime |
| 078 | nested map update does not alias another value | runtime |
| 079 | unicode command payload roundtrips | runtime |
| 080 | integer clock difference stays exact | runtime |
| 081 | unbounded recursion is not a proof | verify_fail |
| 082 | guarded counter induction is provable | verify_ok |
| 083 | invalid state target is static error | check_fail |
| 084 | unsafe literal write cannot verify | verify_fail |
| 085 | dynamic state target cannot pass strict | verify_fail |
| 086 | replica count does not prove consensus | verify_fail |
| 087 | eventual cluster is not a strict safety proof | verify_fail |
| 088 | missing handler is rejected | check_fail |
| 089 | proven decreasing recursion terminates | verify_ok |
| 090 | typed boundary mismatch is reported | runtime |
| 091 | native encoder add promotion | runtime |
| 092 | native distance multiply promotion | runtime |
| 093 | native negative integer division | runtime |
| 094 | native zero divisor is catchable | runtime |
| 095 | native wide bit shift preserves encoder bits | runtime |
| 096 | committed telemetry survives process restart | process |
| 097 | failed handler leaves no persistent writes | process |
| 098 | failed transition leaves no persistent state | process |
| 099 | immutable audit survives process restart | process |
| 100 | record replay preserves failure classification | process |

---

# Experimental cluster runtime

The replication protocol described here is available since Soma 2.8.2 and is
included in the current [Soma 2.8.10 release](https://github.com/soma-dev-lang/soma/releases/tag/v2.8.10).

## What is implemented

A `scale` block with `shard: records` and `consistency: eventual` selects a
mutable Map for full replication. Despite the syntax name, entries are not
physically partitioned: each connected replica eventually holds the selected
slots. All cells are supported; `Cell.slot` identities keep same-named slots
separate. Other slots stay local. A resource-only `scale { memory: "32Mi" }`
does not enable the cluster or open a bus port.

Updates retain their stored types, including large integers, nested values,
empty strings and null. A failing handler or `try` block publishes no rolled
back writes. Remote writes are serialized with local handlers and checked
against the declared slot type. Replication cannot target an unselected slot;
legacy `_cluster_*` events cannot directly mutate storage.

Each key carries a `(Lamport counter, originating node ID)` version. The
higher version wins, including on a deletion. Reordered and duplicate
updates do not overwrite a newer version. This is a deterministic conflict
rule, **not wall-clock last-writer order**. Concurrent read-modify-write
operations can lose an application's increments. There are no cross-node
transactions, multi-key snapshots, linearizable reads, quorum acknowledgements
or consensus. `get`, `has`, `keys`, `values` and `len` read the local replica.

Discovery builds direct links between members, so leaves can communicate
after a seed stops. Each outgoing link retries failed connections with a
1–30 second backoff. State is exchanged on connection and roughly every
three seconds thereafter, including deletion markers. Persistent slots
require SQLite: data and versions commit in the same transaction. Each
replica must have its own project/data directory. Ephemeral data and its
versions are lost when the process stops. Keep the whole `.soma_data`
directory in backups; deleting cluster metadata can resurrect stale values.

## Start two nodes

Save this as `app.cell` in **two distinct directories**, `node-a` and `node-b`:

```soma
cell Replicated {
    memory { records: Map<String, String> [persistent, consistent] }
    scale { replicas: 2 shard: records consistency: eventual tolerance: 1 }
    on put(key: String, value: String) { records.set(key, value) }
    on get(key: String) { return records.get(key) }
}
```

Run in separate terminals:

```sh
cd node-a
SOMA_NODE_ID=127.0.0.1:8082 soma serve app.cell -p 8080
```

```sh
cd node-b
SOMA_NODE_ID=127.0.0.1:8092 soma serve app.cell -p 8090 --join 127.0.0.1:8082
```

The bus uses HTTP port + 2. Choose a fixed HTTP port in 1–65533 and avoid
HTTP, dashboard and bus port overlap. Across machines, bind the appropriate
interface with `--host` and set `SOMA_NODE_ID` to an address reachable by
peers. Seeds may also come from `SOMA_SEEDS` or `[cluster] seeds` in
`soma.toml`. A successful protocol acknowledgement establishes membership;
an unreachable or incompatible seed is retried, never reported as joined.
The cluster bus has no authentication or TLS: use a trusted private network.
Do not connect it to untrusted clients or mix unrelated applications.

## Scheduling and signals

After membership settles, `every` checks the lowest live node ID at each
tick. Missing heartbeats expire after 15 seconds, checked every three
seconds. The surviving node can then take over. This is **advisory
leadership**: discovery delays and partitions can produce simultaneous
ticks. There is no fencing, consensus lease or exactly-once scheduler.

Committed `emit` events reach connected cluster peers once per direct link.
They are fire-and-forget and are not part of state resynchronization; use
application IDs, deduplication and an outbox for reliable workflows. Do not
also declare the same nodes in `[peers]`, which creates a second event path.

## Verification and upgrade

`strong` and `causal` are rejected: the runtime does not implement their
protocols. Replicated Lists, immutable slots and memory invariants are also
refused. `replicas` and `tolerance` are declarations, not provisioning or
fault-tolerance proofs. `soma verify --strict` fails on the explicit warning
that distribution is unproved; a successful non-strict run is not a cluster
proof.

Protocol v2 is incompatible with 2.8.1 and earlier cluster traffic. Stop
all nodes and upgrade them together, retaining each data directory. Existing
local entries acquire replication metadata at startup. Do not run older
binaries or use `soma run` to mutate a live replica's store.

This implementation uses a full mesh, periodic full-state exchange and
retained tombstones, with at most 256 discovered peer addresses per node.
An encoded update must fit the 16 MiB bus line limit; larger local writes
are refused and rolled back. It is intended for small experimental clusters. It has no demonstrated
large-cluster throughput or bound on tombstone growth.

## Regression coverage

`compiler/tests/cluster.rs` starts real server processes with distinct stores.
It covers initial sync, types, rollback, same-named slots, event duplication,
concurrent writes during a TCP partition and convergence after healing, seed
failure, stale replica restart, tombstones, reordered
updates, private slot boundaries and scheduler takeover. Unit tests check
hash-ring balance/minimal movement and monotonic heartbeat expiry. These are
regression tests, not a model-checked proof of arbitrary partitions.

---

# What Soma guarantees — and what it does not

Three columns, no adjectives. If a claim about Soma is not in the first two
columns, it is not a guarantee.

## 1. PROVEN statically — by `soma verify`, before the program runs

On the **state machine** of each cell (a finite graph, model-checked):

| Property | Meaning | How to ask |
|---|---|---|
| Reachability | every declared state can be reached from `initial` | always |
| Deadlock-freedom | no reachable non-final state without an exit | always |
| Liveness | every state can reach some final state — or, for a REACTIVE machine with no final state (a pump, an interlock), every reachable state can return to the initial one | always (a cyclic machine that cannot return home is a ⚠) |
| Stored history | `[verify]` properties are proven for the CURRENT graph: an instance that took an edge an older version of the program allowed keeps that history (the start-up audit reports only instances in undeclared states) — migrate or reset those instances when you remove an edge; one `soma serve` per program and data directory runs the every/after ticks (a second one logs that it does not, and takes over within ~2 s if the first stops) | — |
| `eventually = [...]` | every path reaches one of these states | `soma.toml [verify]` |
| `never = [...]` | these states are unreachable | `soma.toml [verify]` |
| `always = [...]` | the machine is only ever in one of these states | `soma.toml [verify]` |
| after … `never` | once X was reached, Y is unreachable | `[verify.after.X] never = ["Y"]` |
| after … `eventually` | after X every path reaches one of … | `[verify.after.X] eventually = [...]` |
| precedence | no path reaches T without one of / each of … | `[verify.before.T] requires / requires_all` |

On the **handlers**:

| Property | Meaning |
|---|---|
| Refinement | every `transition(id, "x")` with a literal target is a declared edge, and every declared edge is taken by some handler (or reported) |
| Termination | in every cell: bounded loops, recursion on an Int argument that decreases towards a lower-bound base case (`if n <= 0 { return … }`), no call cycles; anything else is a ⚠ (a failure under `--strict`) |
| Think-isolation | with only literal transition targets, the properties above hold whatever an LLM returns |
| Cost bound | `cost { tokens: N }` holds when every `think()` has a literal `max_tokens` and runs a known number of times (across sibling handlers) — a declared bound that cannot be proven is a `soma check` error (worded "bound is advisory"), never a silent pass |
| Invariants on known values | a write of a literal, a `clamp(..)`, or a value interval reasoning can bound — including by induction on the slot's own invariant: `(counts.get(k) ?? 0) + 1` keeps `counts >= 0` |

A failed property prints a counter-example path. A property that names a
state no machine declares is an error. `soma verify` refuses a program that
fails `soma check`.

**"Eventually" is a statement about the graph.** It says no path avoids the
target forever; it does not say anyone will call your handlers. A payment can
sit in `authorized` until someone acts.

## 2. ENFORCED at runtime — always on, cannot be bypassed from Soma code

| Mechanism | Guarantee |
|---|---|
| Memory invariants | checked **before** every `set`, bracket write, `push` and `delete` (for `size`). A violating write raises (`kind "invariant"`) and the slot is unchanged. `soma verify` lists each write it could not prove as *runtime-checked*. On a Float slot a computed value may be NaN (`sqrt(-1.0)`, `inf - inf`), which fails every comparison: such writes are runtime-checked, never "proven". The prover reasons about numbers: an invariant on a FIELD of a record-valued slot (`plans.price >= 0`) or over a structure (`sum_by(inv.lines, "amount") == inv.total`) is runtime-checked, so it is a ⚠ under `verify --strict` — keep a number you need proven in its own `Map<String, Int>` slot. |
| Transitions | `transition()` to an undeclared edge raises `invalid_transition` with the valid targets. Guards raise `guard_failed`. |
| `[immutable]` slots | an entry, once written, never changes: a List slot only grows by `push`, a Map slot only gains new keys — overwriting or deleting an entry raises `kind "invariant"` and the slot is unchanged (an append-only audit log). |
| **Atomic handlers** | A normal handler's SQLite and in-memory slot writes and transitions commit together or are rolled back on failure. SQLite begin/commit failures are errors; queued events, replication and horde starts are released only after commit. A failing `try` rolls back its writes and pushes, while assigned locals and successfully drawn counter IDs remain. A lost transaction or storage read failure aborts the invocation even inside `try`. A `[task]` handler is atomic per step: earlier committed steps remain after a later failure. External HTTP/file/model effects are not undone. |
| **Cross-cell rules** | NOT verified: proofs are per cell. `soma verify` now NAMES each handler that transitions its own machine while acting on another cell with a machine (`note: cross-cell: …`) — enforce those rules yourself with a `require` that reads the other cell (`require Subjects.status(id) != "withdrawn" else Withdrawn`). |
| **Invariants between slots** | `invariant (reserved ?? 0) <= (stock ?? 0)` in a cell's `memory` holds on every write to either slot: the written one is its new value, the others are read at the same key. Enforced at run time, never proven by induction (verify lists it as runtime-checked). |
| **Storage adapters** | Read failures are errors, not missing keys or empty collections. The legacy JSON backend rejects malformed/unreadable files and changes its in-memory state only after a successful file replacement; it has no multi-slot transaction or cross-process isolation. The HTTP adapter validates replies and has bounded requests, but no remote transactions or exactly-once protocol: a failed write can have an unknown remote outcome. HTTP provider selection is available to provider tooling, not wired into `run`/`serve`. |
| **Serialized handlers** | within each `soma serve` process, top-level handler invocations run one at a time: read-modify-write needs no lock. Exception: a `[task]` handler (or tick) runs as steps and waits for each `think()` outside the lock — each step is serialized and atomic, the task as a whole is not (see serving.md). |
| `require` / `ensure` / `fail` | raise; errors carry a `kind` a caller can branch on. |
| Token budget | `set_budget(N)` stops `think()` when the budget is spent; a `set_budget` inside a model's tool call can only lower it. |
| Exhaustive `match` | a missing sum-type arm is a `soma check` error, not a runtime surprise. |

## Cluster scope (available since Soma 2.8.2)

`scale.shard` selects mutable Map slots for **eventual full replication**.
Typed updates are sent only after the local handler commits; incoming
updates use the handler lock and a local transaction. Local `get`, `keys`,
`values` and `len` read the same replica. Logical versions order conflicts;
deletes retain tombstones, persisted with SQLite data for persistent slots.
Reconnect and periodic state exchange repair missed updates when peers can
communicate again. These behaviors have process-level regression tests;
**the verifier does not prove distributed convergence or fault tolerance**.

`strong` and `causal` declarations fail verification and server startup.
A distributed slot with memory invariants, `immutable`, or List operations
is refused because the runtime cannot preserve its guarantees across nodes.
`replicas` does not provision processes, and `tolerance` does not establish a
quorum. A resource-only scale block leaves memory local. Advisory scheduler
leadership follows live membership and can split during a partition.
`verify --strict` rejects the explicit warning about unproved distribution.
See [cluster.md](cluster.md) for setup and migration.

## 3. NOT COVERED — know this before you rely on Soma

- **Data-dependent rules inside handlers** ("amount ≤ order total", "no refund
  after 30 days"). They are your `if`s and guards. Guards are enforced at
  runtime, not proven; the model checker keeps guarded edges.
- **Cross-cell composition.** Verification is per cell. "stock was taken iff
  the reservation is held" across two cells is tested, not proven (atomic
  handlers do cover the rollback of both cells' writes within one invocation).
- **Conservation / aggregate properties** ("the sum of balances never
  changes"). An invariant sees one written value at a time.
- **Effects outside the process** are not rolled back: HTTP calls, `think()`,
  files, events sent over the `[peers]` bus to another process. (An `emit`
  handled by a cell of the same process IS inside the handler's transaction:
  synchronous, and rolled back with it.)
- **Untyped records.** A record is a map: a typo'd field name reads as `()`.
  Ordering against `()` raises, equality does not.
- **Authentication, authorization, TLS, rate limiting**: `soma serve` has none.
  Put it behind a reverse proxy.
- **Throughput.** Handlers are serialized and the interpreter walks the AST;
  `[native]` is for numeric kernels only.
- **Maturity.** Experimental, one author, one package in the registry. The
  verifier itself is tested (adversarially, with mutation and differential
  runs) but not mechanically verified.

---

# `soma serve` — exactly what gets exposed, and how

```
soma serve app.cell -p 8080          # HTTP on :8080
soma run   app.cell request GET /stats ""     # call the router with no server
```

## Routing: three rules, in this order

1. `GET /static/<file>` serves `<project>/static/<file>` — confined to that
   directory (`..` and symlinks cannot escape it; dotfiles such as `.env`
   are never served). A request carrying both Content-Length and
   Transfer-Encoding, or a repeated / non-numeric Content-Length, is refused
   (400); a declared body past 256 MB is refused (413) before it is read.
2. A path that the cell's `request(method, path, body)` handler **matches
   explicitly** — a literal (`"/stats"`) or a prefix pattern (`"/hold/" + id`)
   in one of its `match` arms, or a path it tests (`path == "/reset"`,
   `starts_with(path, "/wipe/")`) — goes to `request`.
3. Otherwise, if the first path segment is the name of a **public handler** of
   the request-owning cell, that handler is called with the remaining segments
   and query values as arguments: `POST /add/5` → `add(5)`. This is how an HTML
   form posts to `/add`. Anything else goes to `request` (or 404 without one).

**Every public handler of the request-owning cell is therefore an HTTP
endpoint** — except `request` itself, which is only ever the router, and
the handlers `request` calls (directly or through its own helpers): those
are reachable ONLY through `request`, so the checks it makes before calling
them (an Authorization header, a method) cannot be walked around with
`POST /wipe/a`. A handler is private when its name starts with `_`
(`on _debit(account, amount)`), or when it lives in another cell. Put domain
logic in its own cell and keep the HTTP cell thin. `soma check` warns when a
handler and one of `request`'s routes share a name.

Only the cell that defines `request` is routed. Other cells are reachable from
it by calling their handlers by name — not by reading their slots:
`Store.config.get(k)` from another cell is a check error (a cell's memory is
its own; add a handler to Store that returns the value).

## Requests and responses

`request` receives `(method, path, body)` — plus `query: Map` and
`headers: Map` when it declares them, bound BY NAME (a 4th parameter called
`headers` gets the headers, anything else the query): `on request(method:
String, path: String, body: Map, query: Map, headers: Map)`. Header names
are lower-case (`headers.authorization`); a repeated header is one entry,
its values joined with ", " (a repeated QUERY key keeps its last value). `OPTIONS`
requests are answered 204 with permissive CORS headers before any handler. A trailing `Map` parameter may be left out by a
caller (it is `map()`), so a test still calls `request("GET", "/x", "")`.
Query keys without `=` are present with an empty String (`?flag` gives
`query.flag == ""`). In query keys and values, `+` means a space and `%2B`
means a literal plus sign. Decoding happens once; empty separators are ignored.

The declared type of `body` decides its shape:

- `body: String` — the raw request text; `from_json(body)` parses a JSON body
  (it raises kind `json` on invalid JSON: wrap it in `try`).
- `body: Map` — the JSON object (or form fields) already parsed; a request
  whose body is not JSON is answered `400 {"kind": "json"}` before the handler
  runs; an empty body is `map()`. `soma run` parses its text argument the
  same way; in a test cell pass the Map itself (`request("POST", "/x",
  map("a", 1))`) — a String there is a `type` error, not parsed.

A handler may return:

| Return value | HTTP |
|---|---|
| a Map or a List | `200`, JSON |
| a String or a number | `200`, `{"result": …}` (JSON); a String that is valid JSON text (`to_json(x)`) is sent as that JSON |
| `()` | `200`, `null` |
| `response(status, body)` | that status; the value is `{_status, _body}` — assert `r._status == 404` in tests |
| `html(body)` / `html(status, body)` | HTML |
| `redirect(url)` | `302` |

An error the handler does not catch is answered by its kind, as
`{"error": message, "kind": kind}` (the message names the refusal, e.g. `require failed: MyTag: …`, `guard failed for transition a → b`): `not_found` → 404; `unauthorized`,
`unauthenticated` → 401; `rate_limited`, `too_many_requests` → 429; `guard_failed`,
`forbidden`, `approval_required` → 403; `invalid_transition`, `conflict` →
409; `invariant`, `ensure` → 422; `json`, `type`, `date` (parse_date / add_days on a bad date), `range`, `division_by_zero` and your
own `require … else Tag` / `fail("tag")` → 400; `stack_overflow`, `llm`,
`budget`, undefined names → 500 (the full table is in operations.md). Map a
kind yourself only when you want a different status or body:

```soma
let r = try { _hold(id) }
if r.kind == "invalid_transition" { return response(410, map("error", r.detail)) }
if r.error != ()                  { fail(r) }      // re-raise: the default mapping answers (under serve; a test sees the raised error)
```

Path segments reach `request` percent-decoded (`/stock/a%20b` → `"/stock/a b"`),
except an encoded slash: `%2F` stays `%2F`, so a value cannot fake a path
segment (`split(rest, "/")` sees the segments the client meant).
Path patterns hold ONE variable, at the end (`"/loans/" + rest`); split
`rest` for more segments, or take the rest from the body or query. Public
handlers (no `_` prefix, `request` aside) are also reachable directly at
`/<handler>/<arg>/…`: arguments are coerced to the declared parameter types
(`/decide/x/true` → Bool), a trailing `Map`/`List` parameter takes the JSON
body (a non-JSON body → `400 {"kind": "json"}`). At start-up `serve` calls a
zero-argument `start()` and `init()` handler (each one the cell has); neither
name is an HTTP endpoint (a request could re-run it). A handler that changes
state — a slot write, a transition, an emit, a call into another cell —
answers `GET`/`HEAD` with `405` (`Allow: POST`) — for the auto-exposed
`/<handler>` endpoints; routes of your own `request` answer every method you
match (a HEAD request reaches `request` with method `"HEAD"` — match it next
to `"GET"` if clients send it), so match on `method` for the ones that write: with CORS open to every
origin, a GET that writes is writable by any web page (`<img src=…>`). A JSON
body (or a Map-typed path/query argument) carrying `_type`, `_variant` or
`_values` anywhere is refused (400), whatever the type of `body` — also for
`body: String`: a client cannot forge a record or a sum-type variant.
`from_json` on other text that names a declared variant checks its shape
(a missing or mistyped field raises kind `type`).

## Realtime: WebSocket, SSE, events

- `on ws(msg: String)` receives each text frame on port+1
  (`ws://127.0.0.1:<port+1>`). Its return value is sent back to that client:
  a String as-is, a Map/List as JSON, `()` sends nothing. A raise answers
  `{"error": …, "kind": …}` like HTTP. The handler is atomic and rolled back
  like any other; `ws` is not an HTTP endpoint. A browser connection is
  accepted only from a localhost / 127.0.0.1 Origin (and from the Host's own
  origin only when serving beyond loopback with `--host`).
- `publish("stream", data)` is pushed to every WebSocket client as
  `{"event": "stream", "data": …}` and to the SSE clients subscribed to that
  name; an `emit ev(data)` is cell-to-cell: it reaches only SSE clients that
  NAME it (`sse("ev")`), never WebSocket clients (a client that stops reading
  sees the stream simply END (there is no `id:` line and no Last-Event-ID
  replay: re-fetch state after a reconnect). A subscriber
  is dropped after 1024 queued events (a WebSocket client also at 64 MB
  queued) and the drop is logged — so a stalled SSE subscriber can hold
  1024 × the size of one event in memory (100 KB events: ~100 MB each): keep
  events small, or put a proxy with its own buffering in front; a bus peer that stops
  reading is disconnected after 1024 queued events). Both are sent AT COMMIT: a handler
  that raises (or a `try` that rolls back) pushes nothing. WebSocket clients
  have no per-client routing: EVERY one receives every `publish`, so do not
  publish one user's or tenant's data where others hold a WebSocket — give
  each an SSE stream of its own.
- SSE: a `request` route returns `sse("stream1", "ev")`; the client receives
  only the named streams (`sse()` with no name: every `publish` stream) — so per-tenant
  streams (`sse("t_" + tenant)`) behind your own auth check in `request` keep
  tenants apart. The first event is `connected`. There is no replay — after
  a reconnect, re-fetch state.
- A handler that some `emit` targets is an event listener, not an HTTP
  endpoint (a client could forge the event); `publish` counts as a state
  change (GET → 405).

## Concurrency and atomicity

Each request runs on its own thread, and **top-level handler invocations are
serialized**: one handler at a time, process-wide. A handler that raises is
rolled back (writes and transitions). You do not need locks or compensation
code; you do pay for it in throughput, and in a plain handler a `think()` call
holds the line for as long as the model takes.

### `[task]` handlers: think outside the lock

`on review(d: Doc) [task] { … }` runs as **steps**: each `think()` ends the
current step (its writes commit), waits for the model outside the lock, then a
new step starts. Concurrent requests overlap their model calls (200 × 2 s
mocked calls finish in about 9 s instead of 400 s). Rules:

- A failure rolls back the **current step only**; steps before the last
  `think()` stay committed. A `try` around a `think()` cannot undo writes made
  before that `think()` (check warns: write after the think instead).
- Anything read before a `think()` may have changed after it: read, `require`
  and write in the step after the last `think()` (check warns when a slot is
  read before and written after). The prover carries no fact across a
  `think()` in a `[task]` handler; such writes are checked at run time.
- Only the entry point decides. A `[task]` handler called from a plain handler
  — `on request(…)` routing to it, an `emit` listener, another cell — runs
  inside that caller's atomic unit and holds the lock; mark the caller
  `[task]` too (`on request(method: String, path: String, body: String) [task]`).
  Ticks take it after the period: `every 1min [task] { … }`, `after 5s [task] { … }`.
  Check warns when a plain handler or tick calls a `[task]` handler.
- A `[task]` handler without `think()` is one atomic unit, like a plain one;
  `[task]` and `[native]` exclude each other.
- `SOMA_LLM_MOCK_LATENCY_MS=2000` gives the mock a latency, to test the overlap.

### Hordes: one `[task]` handler over many inputs

```soma
on audit(docs: List) {
    return horde(Reviewer.review, docs, map("concurrency", 200,
        "on_result", "_store", "on_done", "_summarize", "max_attempts", 2))
}
on _store(v: Map) { verdicts.set(v.id, v) }      // verdicts: [persistent, immutable]
```

`horde()` returns an id (`Audit:h1`) at once; a pool of `concurrency`
workers (default 8, at most 1000) runs the target once per input. Poll
`horde_status(id)`, read `horde_results(id)`, stop with `horde_cancel(id)`.

- **Persisted queue.** The horde and its tasks are written in the caller's
  transaction (a rolled-back caller starts nothing) to soma.db — under serve and
  run always, even without a `[persistent]` slot. A restarted server resumes
  unfinished hordes. With several servers on one `.soma_data`, each horde runs
  in one of them (a lease renewed every second); when that server stops,
  another takes it over about 6 s later.
- **Written at the call.** The target and the options are part of the call:
  `horde(Reviewer.review, docs, map(…))` with literal option names and
  literal handler names. Check refuses a computed target or an options map
  from a variable or a request (an HTTP client could otherwise pick the
  handler or drop the budget); name callbacks `_store` (a public callback is
  an HTTP endpoint too — check warns). Only the owner cell (and test rules)
  can read or cancel a horde.
- **Exactly once, where it matters.** A task's result is recorded, and
  `on_result` called, in the same atomic unit as the target's last step: after
  a `kill -9`, a task is either recorded or run again, never recorded twice.
  Steps before its last `think()` may run again — keep them idempotent or
  write only in the last step.
- **Failures.** A task that raises is retried (at the back of the queue) up to
  `max_attempts` (default 1), then `on_error(input, error)` runs — `error` is
  the Map a `try` gives, `{error, kind, detail}` — and the task counts as
  failed. `on_done(id)` runs once when nothing is left, cancellation included.
- **Deploys.** A restart resumes unfinished hordes only if the target and the
  callbacks still exist with the same arities; otherwise it prints why and
  leaves the tasks waiting (restore the handler, or cancel the horde).
- **Status.** `running` counts tasks waiting for the rate limiter too; right
  after `horde_cancel` in the same handler the state is `cancelling`.
- **Rate limits.** `[agent] rpm` / `tpm` in soma.toml (or `SOMA_LLM_RPM` /
  `SOMA_LLM_TPM`) bound every `think()` of the process, workers included: at
  most `rpm` requests and `tpm` tokens in any 60 s window. A 429 from the
  provider pauses every caller.
- **Budget.** `map("budget_tokens", 2000000)` is a hard ceiling for the whole
  horde: before each `think()` of a task (or of `on_result` / `on_done`) the
  runtime reserves an upper bound of the call — the request's bytes (a token
  is at least a byte) plus its `max_tokens` — and settles the real count after.
  A call that does not fit yet waits, outside the lock, for calls in flight to
  settle; one that can never fit is refused (kind `budget`) and the horde stops
  (`state: "exhausted"`; the tasks it stopped count as cancelled, without
  `on_error`). Measured: 600 tasks, 100 in flight, budget 10 000 → exhausted at
  9 900–10 000, never above. The ceiling assumes the provider honors
  `max_tokens` (one that does not is detected, kind `llm`, and charged), and it
  counts settled calls: calls in flight at a `kill -9` reached the provider and
  are sent again after the restart — up to `concurrency` × (request +
  `max_tokens`) more than the counter shows.
- **Nested hordes.** A horde started inside a task or a callback of a
  budgeted horde runs under that budget too: the whole tree cannot spend past
  the root's ceiling. `on_done`'s `think()` counts as well — keep headroom for
  it (it fails, kind `budget`, on an exhausted horde).
- **Cost proof.** `soma verify` prints each horde's bound: a literal
  `budget_tokens`; else inputs × per-task cost × `max_attempts` when the inputs
  are a literal list or range; else unbounded. In a cell with
  `cost { tokens: N }`, a horde without a literal `budget_tokens` over inputs
  of unknown size makes the bound unprovable (a check error).
- **Rounds.** For a simulation, `map("snapshot", world, "apply", "_apply",
  "seed", 7, "instance", "id")`: the target takes `(input, snapshot)`, so every
  agent of the round sees the same world; `apply` runs at the end, in input
  order, once per task — the result does not depend on which reply came back
  first; `on_done` may start the next round. `seed` makes `random()` in task
  *i* draw the same numbers on every run; `instance` names the input field
  that identifies an agent — its `remember()` / `recall()` and its model
  conversation carry over to its next round. Measured: 10 000 agents × 20
  rounds in 46 s, identical on two runs.
- **Votes.** `vote(Judge.check, claim, 5)` asks 5 agents the same thing and
  returns `{winner, count, k, unanimous, errors, votes}`; inside a `[task]`
  step under serve / run the calls run at once.
- Without workers (`soma test`) a horde runs right after the calling handler
  commits — its next statements (mapping the id to a batch, …) run first, as
  under serve — one task per unit; `soma run` waits for its hordes before
  exiting.
- Measured: 10 000 tasks against a 2 s mocked model at concurrency 500 in 41 s;
  a `kill -9` after 2 500 of them, then a restart: 10 000 results, each once.

## Storage

`[persistent]` slots live in `<project>/.soma_data/soma.db` (SQLite). `soma
run` uses the same database, so state carries over between runs; `soma test`
uses fresh in-memory storage every time.

## What `soma serve` does not do

No TLS, no built-in authentication (read `headers.authorization` in
`request` and refuse; make tokens with `random_token()`, store
`hmac_sha256(secret, password + salt)`, compare secrets with `secure_eq`;
cookies arrive in `headers.cookie` and are set with
`response(303, "", "Location", "/", "Set-Cookie", "sid=…; HttpOnly; SameSite=Strict")`
or `html(200, page, "Set-Cookie", …)`; a repeated form or query field keeps
its last value; the `/__soma/` dashboard is unauthenticated — firewall it), no rate limiting, no cap on open connections (one
thread each: at the machine's thread limit the process exits with status 70
so a supervisor restarts it — cap connections in the reverse proxy).
It binds 127.0.0.1 (`--host 0.0.0.0` to expose it). `PORT + 2` (the signal
bus) is opened only when soma.toml lists `[peers]` or events in `[bus]
accept`, a cell declares `scale`, or `--join` is given (an `emit` alone
stays in this process: no port) — the start-up log says `bus:
listening` or `bus: not started`. The bus speaks one line per event,
`EVENT <name> <json>\n` (a line past 16 MB, or holding more than a
million JSON values, closes the connection); a
receiver runs only the events its program emits itself (with `[peers]` or a cluster) or lists in
`[bus] accept = ["reading"]` in soma.toml, and never `request`, `ws`,
`start`/`init` or a `_private` handler. An `emit` goes to every connected
peer AT COMMIT (a handler that raises sends nothing). An incoming bus event
waits for the process-wide handler lock like a request (keep handlers short
on busy links); `start()` runs BEFORE the links to `[peers]` are up, so an
`emit` there reaches no other process (use `after 2s { … }`). Each
`[peers]` link is re-established when it drops (a peer that restarted, was
down at start-up, or was cut off for reading too slowly); events emitted
meanwhile are logged NOT delivered, not queued; `PORT +
1` only when a cell declares `on ws`. Every response, static files, the
dashboard and the pre-handler 400s included, carries
`Access-Control-Allow-Origin: *` (browsers on any origin may call it; put a
proxy in front to restrict). `--no-schedule` starts the HTTP side without the
`every` / `after` threads (tests, debugging). Run it behind a reverse proxy
and firewall the bus port.

## Security notes for handlers

- **Loopback servers** (the default bind) refuse a request whose `Host` names
  another site (DNS rebinding) and a state-changing request whose `Origin`
  is another site (a cross-site form POST) — 403. With `--host` the server is
  public: authenticate every writing route.
- **`http_*` with a client URL** reaches whatever the URL names (SSRF): allow
  only known hosts. A call to this very server (its HTTP, WebSocket or bus
  port) answers `kind: "self_call"` at once — a handler cannot call its own
  endpoints (the handler lock is held); call the handler directly.
- **`http_*` results**: a success returns the body itself (a Map, List or
  String); a failure returns `{error, kind, status, body}`. Test
  `type_of(r) == "Map" && r.status != ()` before reading `r.kind`.
- **Templates**: `render` / `render_each` / `load` substitute values as they
  are — wrap client text with `escape_html(…)`; `html()` does not escape
  either.
- **`redirect(url)`** sends whatever URL it is given: redirect only to paths
  you build (`"/orders/{id}"`), never to a client-supplied URL.
- **CSV exports** keep cells as written: a cell starting with `=`, `+`, `-`
  or `@` is a formula to a spreadsheet — prefix client text with `'` when
  the file is meant for one.

---

# Operating a Soma service — what happens when it goes wrong

Tested facts about the process, not intentions. Version: `soma --version`
(the website's `/version.json` says which release is published; a served
program has no such route).

## What kills the process, what does not

| Event | Effect |
|---|---|
| A handler raises (require, invariant, transition, `fail`, division by zero, a String reaching an `Int` parameter) | That request is answered with a 4xx/5xx JSON body (table below); every write and transition of the request is rolled back; the process stays up |
| Runaway recursion in a handler | Answered `500 {"kind": "stack_overflow"}` at depth 512; request threads have a 64 MB stack so the guard fires before the OS does; the process stays up |
| A `[native]` handler panics (a `buf_get` past the end, an `idiv` by zero) | Caught at the boundary: an ordinary `try`-catchable error with the same kind the interpreter would raise (`index` → 400, `division_by_zero` → 400); the process stays up. Int overflow does not panic: it promotes to BigInt exactly as interpreted code does |
| `think()` fails or times out | Kind `llm`, rolled back like any error; the request is answered, not hung: one provider round-trip is capped at 60 s (`timeout_ms` in the options map, or `SOMA_LLM_TIMEOUT_MS`), retried up to 3 times on 429/5xx — never after a timeout (the provider may still be generating and billing that reply); `timeout` and `timeout_ms` are the same option |
| A scheduled `every` / `after` block raises | Logged, rolled back (writes and transitions — it is a handler invocation), next tick runs |
| Port already answering, `soma check` errors, an unreadable file | `soma serve` refuses to start and exits 1 — it never serves a program that does not check (`--no-check` overrides) |
| Out of memory, SIGKILL, `kill -9`, SIGTERM | The process dies at once (no draining: an in-flight client gets an empty reply); committed handlers are in `.soma_data/soma.db` (SQLite); the handler in flight is lost as a whole — its writes sat in one uncommitted SQLite transaction |
| Disk full while writing | Expected (not exercised): the SQLite write fails, the request is rolled back and answered 500 |
| A slow upstream (`http_post` to a service that hangs) | The handler holds the process-wide lock for the whole call: every other request waits. Every http builtin has a timeout (default 30 s; pass `map("timeout", ms)`) — keep it short; the upstream is not cancelled |
| A slow handler (a quadratic loop, a huge `to_json`, a loop of 100 000 `slot.set`) | Handlers run one at a time: every other request and every scheduler tick WAITS for it — there is no per-request time limit. `soma verify` proves termination, not speed. A persistent slot write is an SQLite statement inside the handler's transaction (about 0.1 ms measured under serve; more on a slow disk; an invariant that reads `size` adds a COUNT of the slot per write — keep size invariants on small slots): a rebuild of hundreds of thousands of keys in one handler holds the process for a minute or more. Keep handlers short; batch bulk loads outside the request path; put a proxy timeout in front |
| The program changed and `.soma_data/` is older | A renamed slot is a new empty slot (the old rows stay in the file); a slot whose value TYPE changed gives back the old values with their old type; an invariant added later is not checked against stored values (verify proves it for future writes only); a state-machine instance stored in a state the new machine no longer declares takes no transition, `*` edges included. `soma serve` first runs SQLite's `quick_check` and refuses to start on a damaged file (restore a backup or move `.soma_data` aside); a file that is not a database stops any command with the same advice. `soma serve` and `soma run` audit the database at start-up and print one `warning: stored data: …` line per problem: instances in undeclared states, values an invariant refuses (List slots and `size` clauses included), values of another type than declared, a slot re-declared List ↔ Map. `soma serve` (which owns its data directory) also reports slot data no slot declares any more and tables of cells the program no longer declares (renamed/removed) — `soma run` does not, since several programs often share one directory. Migrate (below) or delete `.soma_data/` |

## Addresses and ports

- `soma serve app.cell -p 8080` binds **127.0.0.1:8080**. Nothing is reachable from the network until you pass `--host 0.0.0.0` (or put a reverse proxy in front — recommended: TLS, auth and headers are the proxy's job; Soma reads none).
- The event bus for `emit` between processes binds port **+2** (8082), the WebSocket endpoint port **+1** (8081) only when a cell declares `on ws(...)`. Both follow `--host`.
- `serve` probes the port first: a process already answering there is an error (exit 1), not a silent bind beside it.
- The dashboard is `/__soma/` on the same port; static files are served from `./static/` only.

## Exit codes

| Command | 0 | 1 |
|---|---|---|
| `soma check` | no errors (warnings allowed) | at least one error |
| `soma verify` | `VERIFY OK` (vacuous when the program has no state machine — it says so) | `VERIFY FAILED …` (also when `soma check` fails) |
| `soma test` | every assertion passed | any failure, or `soma check` fails, or no test cell |
| `soma run` | the handler returned | the handler raised, or the program does not check, or the handler name is unknown |
| `soma serve` | (runs until stopped) | cannot start: port taken, check errors, bind failure |
| `soma deploy` | provider CLI succeeded | the CLI is missing or failed (the Dockerfile is still generated) |
| `soma docs`, `soma example` | printed | unknown topic / no match |

`--json` on `check`, `verify`, `test`, `describe`, `example` prints machine-readable stdout (also for a fatal error such as an unreadable file); diagnostics go to stderr. `soma verify --strict` turns every ⚠ into a failure.

## HTTP answers for a raised error

Body: `{"error": "<message>", "kind": "<kind>"}`.

| kind | status | raised by |
|---|---|---|
| `not_found` | 404 | `fail("not_found", …)` |
| `unauthorized`, `unauthenticated` | 401 | `require token_ok else unauthorized` |
| `rate_limited`, `too_many_requests` | 429 | `require hits < 10 else rate_limited` |
| `guard_failed`, `forbidden`, `approval_required` | 403 | a transition guard; `fail("forbidden")`; `approve()` with nobody to answer |
| `invalid_transition`, `conflict` | 409 | `transition()` off the machine; `fail("conflict")` |
| `invariant`, `ensure` | 422 | a memory invariant refusing a write; `ensure` |
| `json`, `division_by_zero`, `type`, `index` | 400 | a non-JSON body for `body: Map`; arithmetic; a wrong-typed argument or a value that does not fit the slot's declared type; a list index out of range (also from a `[native]` buffer) |
| your own `require … else Tag` / `fail("tag", …)` | 400 | the program refused the request |
| `stack_overflow`, `llm`, `budget`, `undefined_variable`, `undefined_function`, `no_handler` | 500 | the program itself is wrong or the world failed |

A handler that returns normally answers 200 with its value as JSON (`()` is `null`, a String is `{"result": "…"}`), or the status inside a `response(status, body)` map.

## Limits

- Int is arbitrary precision (i64 fast path, BigInt beyond); Float is f64; `7 / 2` is `3.5`.
- Recursion depth: 512 frames, then `stack_overflow`.
- Request bodies: a declared body past 256 MB is refused (413), and a JSON body holding more than ~1 000 000 values (objects and lists weigh more) is refused (413) before it is parsed; paths have no configured cap (20 KB paths were served). Put tighter caps on the proxy.
- Handlers run one at a time (a process-wide lock): correct under contention, no parallelism inside one process. Throughput is not a goal.
- `forall` properties in tests walk every value up to 20 000, then sample with a fixed seed.
- One process, one SQLite file (`.soma_data/soma.db`, created beside the program); no replication unless a `scale` section and a bus join are configured (experimental).

## Migrating stored data

There is no migration command: a migration is a handler, run once with
`soma run` against the same `.soma_data/` (it shares the database with a
running `soma serve`, and like every handler it is one transaction).

- **Added slot / field**: old rows read `()`. Backfill in a one-shot handler
  (`for id in skus.keys { if prio.get(id) == () { prio.set(id, 2) } }`), or
  default at read time (`prio.get(id) ?? 2`).
- **Renamed state**: run a copy of the program that still declares the old
  state and an edge out of it (`picked -> packed`), with a `_migrate` handler
  calling `transition(id, "packed")` for each stuck id; then serve the new
  program. `soma run migrate.cell _migrate`.
- **Renamed slot**: keep the old slot declared next to the new one for one
  release, copy in `_migrate`, then drop it. The audit names the orphaned
  rows until then.
- **Re-typed slot**: read, convert, `set` — or rename the slot.
- **Tightened invariant**: stored values that violate it are served but can
  not be written back; fix them in `_migrate` or keep the old bound.

Make `_migrate` idempotent (check before writing) and back up
`.soma_data/soma.db` first.

## Environment variables

| Variable | Effect |
|---|---|
| `SOMA_LLM_KEY` (or `ANTHROPIC_API_KEY`, `OPENAI_API_KEY`) | the provider key for `think()`; without one `soma test` mocks and `soma serve` raises kind `llm` |
| `SOMA_LLM_MOCK=echo` \| `fixed:<text>` \| `rules:<file.json>` | `think()` never reaches a provider (overrides `[agent] mock` in soma.toml); `soma serve` prints `llm: MOCK …` at start-up when the program calls think; an `echo` reply is cut at max_tokens (~4 characters per token) like a provider's, a `fixed:` reply over max_tokens raises kind `llm` as a scripted `mock think` does; `rules:` reads a JSON list of `{"match": "…", "cell": "…", "reply": …}` — the first rule whose `match` is in the prompt (and `cell` is the calling agent) answers, none: an echo |
| `SOMA_LLM_MOCK_LATENCY_MS=2000` | a mocked `think()` waits that long (outside the lock in a `[task]` handler): tests concurrency and hordes offline |
| `SOMA_LLM_RPM` / `SOMA_LLM_TPM` | provider limits (requests / tokens per minute) shared by every `think()` of the process — override `[agent] rpm` / `tpm`; 0 = none |
| `SOMA_LLM_TIMEOUT_MS` | one provider round-trip cap (default 60 000) |
| `SOMA_APPROVE=always` \| `never` | answers `approve()` when no terminal is attached (`soma serve` fails closed otherwise: 403 `approval_required`) |
| `PORT` | not read — pass `-p` |

Other environment variables are not readable from a program. A secret or a
config value (an admin token) goes in a file read once in `on start()`:
`let t = read_file("secrets/admin_token.txt")` then
`require type_of(t) == "String" && len(trim(t)) >= 16 else NoSecret` — on a
missing file read_file returns an `{error}` Map, and a check such as
`t != ()` or an interpolation (`"Bearer {t}"`) would turn that error text
into a token anyone can guess (fail closed: the start-up then fails). Relative `read_file` /
`write_file` paths resolve against the directory `soma` was started in, not
the `.cell` file's — keep that file out of `static/`. File builtins — `read_file`,
`read_csv`, `load` / `include` / `load_template`, `read_files` included —
refuse a path with a `..` segment, and a write that would replace a `.cell` source,
`soma.toml`, `soma.lock` or `.soma_data` (kind `path`); a path built from
client input still needs a fixed directory and a validated name.

## Between processes

`emit` reaches every cell of the same process synchronously. Across
processes it needs the bus: a `[peers]` table in soma.toml
(`other = "host:PORT+2"`) on the sending side, and on the RECEIVING side
the events it accepts from other processes: `[bus] accept = ["paid"]` (an
event this program emits itself is accepted too; anything else — any
other handler — is refused). The event reaches every cell with `on paid`. `--join host:bus-port`
forms an experimental cluster and also forwards committed `emit` events to
connected cluster members. Selected Map slots replicate independently of
application events. See [cluster.md](cluster.md) for the protocol, recovery
and the exact limits; avoid configuring the same connection through both
`[peers]` and cluster discovery.
An event sent while the peer is down is logged `bus: event '…' NOT
delivered` (also after a linked peer disconnects); `soma run` opens no bus,
so an `emit` meant for `[peers]` is reported not delivered there too. A JSON
request body or bus event with more than 1 000 000 values is refused (413 /
connection closed) before it is parsed.
Each `[peers]` link is supervised: a peer that is down at start-up, that
restarts, or that was dropped for reading too slowly is reconnected (every
1 s, backing off to 30 s; `peer: … linked again`). Two processes that list
each other exchange each event once (a link opens with `HELLO`, and the
side that has its own link to the other only receives on it); a `[peers]`
address that is this process's own bus port is refused. A bus connection
must send its first line within 10 s, and at most 256 are open at once.
There is no loop detection ACROSS processes: `A.on tick { emit pong }` with
`B.on pong { emit tick }` runs forever — guard such chains with a hop count
or an id already seen. Events emitted while it
is down are logged NOT delivered — they are not queued. This
is the experimental corner of Soma; single-process is the supported shape.
Delivery is fire-and-forget: an event emitted while no peer is connected (or
to a peer that dropped) is NOT delivered — the sender logs `bus: event '…'
NOT delivered` (naming each `[peers]` peer whose link is down, even while
other links are up), and the handler still commits. `emit` goes to EVERY
connected link — the `[peers]` you list and the processes linked to you;
there is no addressing: each receiver keeps only the events in its
`[bus] accept` list and drops (and logs) the rest, so keep event names
distinct per receiver and expect refusals in the logs of the others. To move value between
processes, keep an outbox slot on the sender (the transfer, with an id),
have the receiver deduplicate by id and emit an acknowledgement, and let an
`every` tick re-send what is unacknowledged. The bus port has no
authentication: any local process can send an accepted event — firewall it.

## Persistence

`[persistent]` slots and state-machine instances live in `.soma_data/soma.db` next to the `.cell` file (wherever the command is run from), shared by `soma serve` and `soma run`; `soma run --fresh` deletes it first (when other programs' cells also keep tables there, only this program's own tables are reset). `soma test` starts from empty storage every run. Back up the file; there is no migration tool — a renamed slot is a new, empty slot. Values round-trip exactly: an Int beyond 64 bits comes back as that Int, a variant as a variant, `()` as `()`. A write that does not fit the slot's declared value type (`Map<String, Int>` given a String or `1.0`; `Map<String, Pay>` given a plain map) is refused with kind `type` before it commits; an Int written to a `Float` slot is stored as a Float. One process holds one connection to the database and each handler runs inside `BEGIN IMMEDIATE … COMMIT`, which also serializes handlers across processes.

## Deploying on Linux

There is no published Linux binary yet; build from source (Rust stable + GMP):

```sh
apt-get install -y build-essential libgmp-dev m4 git
git clone --depth 1 --branch v<version> https://github.com/soma-dev-lang/soma
cd soma/compiler && cargo build --release
# ./target/release/soma serve /srv/app/app.cell -p 8080 --host 0.0.0.0
```

`soma deploy --target fly|cloudflare|aws` generates a multi-stage Dockerfile that does exactly this (build stage `rust:1-bookworm`, runtime `debian:bookworm-slim` + `libgmp10`) and invokes the provider CLI; a missing CLI exits 1 after generating the files. A systemd unit is a one-liner: `ExecStart=/usr/local/bin/soma serve /srv/app/app.cell -p 8080`, `WorkingDirectory=/srv/app` (the database lives there), `Restart=always`.

## Logs

One line per request on stderr: `POST /pay/x → 409 2ms invalid transition …`. Start-up prints the cell, its handlers, the database path, the bind address and the dashboard URL. No log files are written by Soma; use the supervisor's.

---

# Verified wrong→right pairs

# Soma for agents: verified wrong → right

The mistakes an LLM makes writing Soma, each with the **actual compiler
error** and the fix. Every pair below is verified against the current
`soma` binary. This is the self-correction corpus: when `soma check` /
`soma run` emits one of these errors, apply the paired fix.

A rule of thumb: **`soma check` catches most of these before you run.**
Write the file, run `soma check app.cell`, fix what it reports, repeat.

---

## 1. Quotes inside `{...}` interpolation

```soma
// WRONG — an unescaped `"` ends the string: `{len(` is left dangling
return "len: {len("hi")}"
```
```soma
// RIGHT — escape it (`"len: {len(\"hi\")}"` prints len: 2), or, clearer,
// bind the value first and interpolate the variable
let n = len("hi")
return "len: {n}"
```

## 2. `match` arms use `->`, not `=>`

```soma
return match x { 1 => "a"  _ => "b" }
// error: match arms use '->', not '=>'
```
```soma
return match x { 1 -> "a"  _ -> "b" }     // `_` is the catch-all arm
```
`=>` is **lambda** syntax (`p => p + 1`). `->` is match arms and signal
return types. Don't cross them.

## 3. Handlers don't declare return types

```soma
on add(a: Int, b: Int) -> Int { return a + b }
// error: handlers do not declare return types — put '-> Int' on the
//        signal declaration inside face { }
```
```soma
face { signal add(a: Int, b: Int) -> Int }
on add(a: Int, b: Int) { return a + b }
```

## 4. Adjacent string literals do NOT concatenate

```soma
return "hello " "world"
// error: in G.hello: a string literal follows `return` and is never
//        evaluated — adjacent string literals do not concatenate
```
```soma
return "hello world"        // one literal
let name = "world"
return "hello {name}"       // or interpolate
```
(`soma check` also warns on any other unreachable statement after
`return` / `break` / `continue`.)

## 5. `==` IS structural on lists, maps and variants

```soma
[1, 2] == [1, 2]                                  // true
map("US", 1, "EU", 2) == map("EU", 2, "US", 1)    // true — key order is irrelevant
[] == []                                          // true
```
`<`, `>` on lists or maps is an error (compare a field or `len()`), and values
of different kinds are an error to compare (`1 == "1"`), not `false`.

## 6. Float equality needs a tolerance

```soma
return 0.1 + 0.2 == 0.3      // false — floating point
```
```soma
return abs((0.1 + 0.2) - 0.3) < 0.0001
```

## 7. `transition()` returns a map, not the target string

```soma
on advance(id: String) {
    return transition(id, "next")   // returns {id, from, to}, not "next"
}
```
```soma
on advance(id: String) {
    transition(id, "next")
    return get_status(id)           // the new state as a string
}
```
Guard fallible transitions with `try`:
```soma
let r = try { transition(id, "next") }
if r.error != () { return map("error", r.error) }
```

## 8. `is_a` does not recognize sum-type VARIANTS — match them

```soma
let b = Box { w: 3 }         // Box is a `variants` constructor
return is_a(b, "Box")        // false — variants aren't tagged records
```
```soma
// extract the kind with an exhaustive match handler
on kind(s: Map) {
    return match s {
        Box { w } -> "Box"
        // ... every variant
    }
}
```
(`is_a` / `is_type` DO work on record literals: `is_a(Game { x: 1 }, "Game")` is `true`.)

## 9. There is no `cell type X { fields { ... } }`

Records are plain map-shaped values. Construct them with a literal:
```soma
let g = Game { bet: 10, pot: 0 }   // a field-accessible value (a Map)
g.bet = 20                          // mutate fields in place
let b = g.bet
return is_a(g, "Game")              // true — record literals carry _type
```
Use `cell type X { variants { ... } }` only for *sum types* (tagged unions).

## 10. `soma serve` routes only the cell that owns `request`

```soma
// other cells' signals are NOT auto-routed as HTTP endpoints
```
```soma
// put every routable signal on the request-owning cell, delegating
// to domain cells:
cell Api {
    face { signal request(...) -> String  signal place(...) -> Map }
    on place(...) { return place_order(...) }   // delegate to Orders
    on request(method: String, path: String, body: String) { ... }
}
```

---

## These USED to be limitations and now WORK — use them freely

Older Soma code worked around these; the current language supports them
directly. Prefer the direct form.

```soma
// bracket indexing (read + write) on lists, maps, strings
let x = xs[2]      xs[2] = 99      let v = m["key"]   m["key"] = 1   let c = s[0]
// negative literals
let n = -1                         // not `0 - 1`
// descending / stepped ranges
for r in range(10, 0, -1) { }      // not build-then-reverse
// numeric reductions over a list
sum(xs)   product(xs)   avg(xs)   min(xs)   max(xs)
// UFCS — any builtin is a method
xs.sum()   xs.sort()   xs.reverse()   m.det()   m.transpose()
// nested record/list mutation
g.board[0] = 99    g.meta.turn = 5    xs[i][j] = v
// matrices are first-class, with vectorized (numpy-style) operators
let M = [1,0,0,1].reshape(2,2)     let P = A * B      let t = M.T      det(M)
A + 10    A / 2    1 - A           // scalar broadcast on matrices
v * 2     v - 1    v * v   v + v   // vector broadcast + elementwise (+ * / -)
A > 2     v >= 2.0                 // comparison masks (0/1)
// list CONCATENATION is concat(a, b); non-numeric lists keep + = concat
// `with` is functional copy-update for maps AND lists
let m2 = with(m, "k", 9)           let l2 = with(xs, 0, 9)
```

---

## The agent loop, in commands

```
soma check  app.cell        # contracts, interpolation, dispatch — fix these first
soma verify app.cell        # PROVE state machines + memory invariants
soma test   app.cell        # run `cell test` assertions (assert / assert_fails)
soma run    app.cell sig a  # execute a handler
soma serve  app.cell -p 8080
soma describe app.cell --faces      # token-cheap contract summary of every cell
soma describe --builtins --json     # the exact builtin signatures (never guess)
```

When unsure of a builtin's signature, run `soma describe --builtins` —
do not guess. When unsure of a cell's API, run `soma describe --faces`.

---

## More verified footguns (found generating 168 programs)

## 11. Your handler shadows a builtin of the same name — when the argument count matches

`f(args)` calls the program's handler `f` if one takes that many arguments,
the builtin `f` otherwise. User code shadows the library, as everywhere else.

```soma
on merge(a: Int, b: Int) { return a + b + 1000 }
on use_it()  { return merge(1, 2) }      // 1003 — your handler
on list()    { return list(1, 2) }       // [1, 2] — 2 ≠ 0 arguments: the builtin
```
`soma check` warns on the two confusing cases:
```soma
on merge(a: Int, b: Int, c: Int) { … }
on use_it() { return merge(m1, m2) }
// warning: call to 'merge' with 2 argument(s) … resolves to the BUILTIN merge():
//          the handler G.merge takes [3]
on list() { let items = list() … }
// warning: inside G.list, `list(…)` with 0 argument(s) calls the handler ITSELF
//          (recursion), not the builtin list(). For an empty list write []
```
Method calls (`xs.count(p)`) always go to builtins.

## 12. `assert_fails` needs an expression that RAISES, not a falsy bool

```soma
assert_fails 1 == 2          // FAILS the test: 1==2 is just `false`, no error
```
```soma
assert_fails xs[99]          // passes: out-of-bounds RAISES
assert_fails transition(id, "illegal") matching "invalid_transition"   // passes for THAT reason
// (with several state machines, call a handler of the owning cell instead)
assert !(1 == 2)             // for a falsy predicate, use plain assert + !
```

## 13. Slot methods work on declared `memory` slots, not local maps

```soma
let seen = map()
seen.set("k", 1)             // error: `.set()` is a memory-slot method and 'seen' is a local — a local map is written with brackets: `seen[k] = v`
```
```soma
let seen = map()
seen["k"] = 1                // local maps use bracket indexing
let v = seen["k"] ?? 0
```
`.get`/`.set`/`.has`/`.delete`/`.keys` are for `memory { slot: ... }` slots.

## 14. `on` is a reserved keyword

It can't be a parameter name or a map field read as `.on`. Use `enabled`,
`active`, etc.

## 15. No semicolons; statements are newline-separated

```soma
{ a = 1; b = 2 }             // error: unexpected character ';' — Soma has no semicolons, one statement per line
```
```soma
{
    a = 1
    b = 2
}
```

## 16. `given` is reserved (like `on`)

It's a face-declaration keyword — can't be a state name, param, or
identifier. `error: expected identifier, found Given`. Use `granted`, `input`, etc.

## 17. What a test cell's `rules { }` accepts

`assert`, `assert_fails` (optionally `… matching "text"`), `let name = expr`
(a fixture for the rules below), `mock think "reply"` / `mock think ["a", "b"]`
/ `mock think error "timeout"`, `mock http_get map(...)` / `mock Cell.handler v`,
and `property`. No bare statements: put logic in a handler and call it.
A List given to any `mock` is a QUEUE — one reply per call, in order — so a
handler or `http_get` that answers a JSON array is mocked with a nested list:
```soma
mock http_get [1, 2]       // two calls: the first gets 1, the second 2
mock http_get [[1, 2]]     // one call gets the list [1, 2]
```
`soma test` notes a scripted reply that no call consumed.

## 18. An invariant between two slots defaults both sides

An invariant is checked on every write to either slot it names: the written
slot is its new value, the other one is read at the SAME key — and a key it
has no entry for reads as `()`, which no comparison accepts.
```soma
memory { a: Map<String, Int>  b: Map<String, Int>  invariant a + b <= 100 }
// error: memory invariant between slots (a, b) — the other slot is read at the
//        SAME key, and a key it has no entry for reads as (), which no
//        comparison accepts: default the sides (`(reserved ?? 0) <= (stock ?? 0)`)
```
```soma
memory {
    stock: Map<String, Int>  reserved: Map<String, Int>
    invariant (reserved ?? 0) <= (stock ?? 0)   // runtime-checked on both slots
}
```
A rule between two slots stays runtime-checked (`verify` cannot prove it by
induction). `size` invariants are enforced on `delete` too: `invariant size >= 1`
rejects removing the last entry.

## 19. `7 / 2 = 3.5` everywhere — say `idiv` when you mean the integer quotient

`/` on two Ints is 3.5 (an Int only when exact) in the interpreter AND in
`[native]` handlers. Native code is statically typed, so where the quotient
must be an Int it is checked instead of truncated:

```soma
on mid(lo: Int, hi: Int) [native] {
    let m = lo
    m = (lo + hi) / 2        // m is an Int slot
    return m
}
// mid(1, 2) → error: Int / Int is not exact here, and this spot can only
//             hold an Int (7 / 2 is 3.5) — write idiv(a, b) ...
```
```soma
on mid(lo: Int, hi: Int) [native] { return idiv(lo + hi, 2) }   // 1, everywhere
```
`soma check` warns on Int / Int in native handlers; `soma fix f.cell --native-idiv`
rewrites them (for code written when native `/` truncated). A `[native]`
division by zero is an ordinary, `try`-catchable runtime error.

## 20. A cost bound is only *proven* when every `think()` count is known

`think()` reached through a loop over a list, a lambda (`map(xs, x => think(..))`)
or a recursive helper makes the bound unprovable — and an unprovable declared
bound is a `soma check` **error** (the message reads `cost: 'tokens' bound is
advisory — …`, exit 1), not a note: a bound nobody can prove is a lie in the
program's own words. Give the loop a literal `range(0, N)` or `[loop_bound(N)]`
to get `bound proven` back, or remove the `cost` block. Calls to sibling
handlers are composed: `for i in range(0, 3) { helper() }` costs 3 × helper.

## 21. Habits from Python / TypeScript that `soma check` now redirects

```soma
if x == null { }          // error: 'null' does not exist — Soma's null is `()`; also `x ?? default`
xs.includes(v)            // error: no method 'includes' — in Soma: contains(xs, v)
rows.push(o)              // warning: result discarded — push returns a NEW list: rows = push(rows, o)
[a[0]] + rest             // warning: `+` ADDS numeric lists element-wise — concat(a, b) / push(xs, x)
let t = lefft + 1         // error: undefined variable 'lefft' (did you mean 'left'?)
```
Everyday collection builtins: `contains(list|map|string, x)`, `slice(xs, start, end?)`
(negative indexes count from the end), `keys(m)` / `values(m)` / `entries(m)`,
`sort_by(rows, "field")` or `sort_by(rows, r => [0 - r.total, r.name], "desc"?)`
(stable; a list key sorts on several keys), `round(x, digits)`.

## 22. Transition guards see the calling handler's locals

```soma
state expense { initial: approved   approved -> paid { guard { amount < 10000 } } }
on pay(id: String) {
    let amount = amounts.get(id) ?? 0      // the guard reads THIS `amount`
    transition(id, "paid")                 // raises "guard failed…" when false
}
```
A guard sees: the locals of the handler calling `transition()`, the cell's
memory slots, `_id`, `_from`, `_to`. `soma check` rejects a guard that reads a
name its calling handler never binds. Guards are enforced at runtime; the
model checker keeps the edge (an over-approximation, so safety results hold).

## 23. `soma.toml` is validated

A `soma.toml` that does not parse — or has an unknown key under `[verify]` — is
an error for every command (it used to be ignored silently, so `[verify]`
properties were never checked). `[package]` is optional.

## 24. Handlers are atomic; errors have kinds

A handler that raises leaves nothing behind: its writes and transitions are
rolled back (a failing `try { }` block too, to where it began). Do not write
compensation code. Raise with `fail("kind", "detail")` or
`require cond else Tag`; catch with `let r = try { … }` and branch on `r.kind`
(`"not_found"`, `"invalid_transition"`, `"guard_failed"`, `"invariant"`, …);
`fail(r)` re-raises.

## 25. `* -> failed` leaves EVERY state, final ones included

```soma
state s { initial: a   a -> paid   * -> failed }               // paid -> failed exists: paid is not final
state s { initial: a   a -> paid   * -> failed except [paid] }  // paid stays final
```
`soma verify` warns about the first form and prints the second.

## 26. A route in `request` and a handler of the same name

`soma serve` exposes every public handler at `/<name>/<args>`. With
`on hold(id, qty)` and a route `"/hold/" + id`, the explicit route wins — but
other `/hold/…` shapes still reach the handler. Prefix internal handlers with
`_`. `soma check` warns.