What is proven, checked, or not covered
The exact guarantees of soma verify and of the runtime, and their limits. Part of the guide to the Soma programming language.
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 | Verified when soma.toml states them: [verify.before."Pay.paid"] requires = ["Approval.signed_off"] explores the PRODUCT of the two cells' machines over every run of the handlers, following one id through both (the instance of Pay and the instance of Approval with the same id). What counts as evidence in a body: a require (or if … { return }) on get_status(id), in the cell itself or through a signal of the other cell whose body is that one return (require Approval.status(id) == "signed_off" else NotSigned), with the SAME id. requires is about the past ("was signed off once"); while = ["Visit.open"] in the same table is about the present (the other machine IS in that state when the target is entered). A rule whose target is an initial state is refused: an instance is there from the start, by no transition. Instances of different ids are tied by via = "Ordo.consult_of" (the slot where the target's instance names the other — written once, when the entry is created, never deleted: verify refuses the rule otherwise). A rule nobody states is not verified: soma verify names each handler that transitions its own machine while acting on another cell with a machine (note: cross-cell: …). Not covered: a link that changes after the entry is created. |
| 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 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 ifs 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.