Soma 3.1.0 — 2026-11-13

This page describes Soma as of release 3.1.0. Some of it may have changed since: the current release is 3.2.4, and the current language is in the guide.

Skeleton first: a large program is written structure first, proven before its bodies exist, and filled body by body from a brief the compiler enforces. Summary in soma docs releases; the course at https://soma-lang.dev/learn (six lessons, every output printed by the binary — docs/site/learn.md, built by tools/build_learn.py, which fails the site build when a lesson stops behaving as written).

• A hole is not judged for termination (found writing the course): the hole model (while ? { … }, what a body may do) was read as a loop by the termination analysis in a cell without a machine, and through a call from another cell — ⚠ while-loop without provable termination bound on every skeleton. Holes are left out, as the docs said. The invariant line of a hole now says why in words (take → copies because it is a hole …) instead of "? has no known range". Test a_hole_is_not_judged_for_termination_with_or_without_a_machine.

Skeleton first: skeleton / flesh, frames, holes, soma skeleton, soma holes, skeleton.lock

Goal of the release line: let programming agents design large applications in a solid manner. Design and measurements: SKELETON_DESIGN.md.

• skeleton Name { … } (and skeleton agent): a cell without handler bodies — memory, invariants, state machines, and a face whose signals each carry a frame: reads a, b, writes a, moves s -> t (moves Cell.machine: s -> t, moves * -> t, moves * -> *), calls f, Cell.g, think, emits s. The frame is closed: a signal without a clause is a pure function of its parameters. skeleton, flesh and the five clause words are contextual — every existing program parses as before (none of the repository's 1,059 valid programs changes verdict).

• flesh Name { on … }: the bodies, and nothing else, in the same file or in one a use brings in. A parameter takes its type from the signal (on pay(id)); a handler the face does not declare is a private helper, named _helper and typed. A flesh reads its skeleton's consts. After parsing, a skeleton and its flesh are an ordinary cell: the interpreter, [native], serve and the verifier are unchanged.

• Conformance (soma check, kind frame, E0120). Everything a body does — and the helpers it reaches do — must be inside its signal's frame: a write, a read, a call (of a signal or of a builtin with an effect), an emit, a machine edge (the edge itself when the body names or established the source, the target otherwise). Effects written inside string interpolations count. Each error names the clause to add. The frame itself must make sense on the skeleton alone (slots, edges and signals that exist; another cell's slot is refused with the way through its signals). A schedule in a skeleton only calls signals. Warnings (W, frame_warning): a frame wider than its body, an edge no signal moves, a slot no signal writes, a helper nothing calls.

• Holes. A signal no flesh fills: check passes and counts them, verify proves the machines and ends VERIFY OK (skeleton — the holes above are open obligations), an edge only a hole will take "waits for a hole" instead of being called stale, a call fails with kind not_implemented. soma holes app.cell [--json] lists them in the order to write them (callees first).

• soma skeleton app.cell: any program as its skeleton — on plain cells the frames are inferred from the bodies. soma skeleton app.cell Cell.signal is the brief for one signal: its slots with their invariants, its edges with their guards, and the signature, frame and contract of everything it may call. --json for both. On the demo apps the map is 9–20% of the source.

• soma skeleton app.cell --split: the file rewritten as skeleton + flesh — structure and comments verbatim, each signal with the frame its body has, bodies unchanged; a handler the outside could call joins the face. tools/split_roundtrip.py splits every valid program of the repository (1,049) and requires the same check, test tally and verify verdict.

• soma skeleton app.cell --freeze / --amend: skeleton.lock holds each skeleton's token hash and text; check, run, test, serve and verify refuse a program whose skeletons differ (kind skeleton_lock, E0121), printing the lines that changed. Comments, layout and flesh are free. --amend accepts a change on purpose.

• soma init --skeleton: a starter laid out skeleton-first (app.cell + lib/counter.cell), with one hole.

• soma describe --faces prints a skeleton with its frames (--json: skeleton, frames, hole); soma fmt hangs frame clauses under their signal.

• Soundness check of the frames. SOMA_EFFECT_TRACE=<file> makes the interpreter log every slot read and write, handler call, effectful builtin, transition and emit with the handler stack; tools/frame_oracle.py runs the test cells of every program (358 have some) and requires each observed effect to be inside the inferred frame of the signal that made it.

• Hardening after review (2026-11-13). Closed, each with a test (compiler/tests/skeleton.rs, reproducers in compiler/tests/fixtures/skeleton_review/): [hole] on a handler with a body disabled conformance (it is no longer writable); a local that only MAY be bound (dead branch, loop, later let, lambda / match binder elsewhere) hid a call, a cell or a slot — names are now resolved by lexical scope, which also ends two false positives; an interior cell named like a skeleton; an emit reaching a private helper; transition(id, to) taking an edge the frame did not list (every edge into the target is now required, or the three-argument form); calls in method form, pipes, require messages and std.. soma verify reads a hole as its frame: a rule its frame can break is ⚠ open obligation, an invariant on a slot it may write is ⚠ runtime-checked, never ✓ (tools/skeleton_monotone.py: every ✓ of a derived skeleton is a ✓ of the program, on every valid program of the repository). skeleton.lock covers interior skeletons, outside movers of a frozen machine and soma.toml's [verify] tables, holds under any file name of its directory and for eval / build / replay / deploy / serve --no-check, has a checksum (unreadable = error; --freeze never overwrites), and its difference names the signal. Also fixed on the way: horde(variable, …) was reported "its tasks call no think()"; a guard the face's requires already establishes was "runtime-checked".

• The brief is enough to write a body. soma skeleton app.cell Cell.signal adds the skeleton's comments (cell, signal, slots, edges), the cell's constants, the types named, each machine touched in full, builtin signatures, callee comments and contracts, callers. soma holes app.cell [Cell] groups by cell; soma verify --summary; soma init --skeleton .; get_status is documented per edition.

• Red-team rounds 2 and 3 (2026-11-13), 14 then 26 confirmed problems, closed with tests r2_* / r3_*. A local named like a slot is the local at run time too (let acct = 1 acct.set(…) wrote the slot: an interpreter fix). Only transition(id, from, to) pins an edge for a frame — what a body infers from get_status is no longer evidence; without the source, every edge into the target must be in the frame. An impure lambda may only be written as the direct argument of a builtin that applies it at once (xs.map(x => …), xs |> filter(…)); bound, stored, passed to a signal or returned, a lambda must be pure. std.f(…) is charged as the builtin f. A cost bound is not "proven" while a hole may call or emit. skeleton.lock reads [verify] as TOML, holds the edition, follows types into the types they name, and is looked up beside every file that declares a skeleton and above. The effect trace logs the edge each transition takes, so the oracle sees a move by the wrong edge. soma fix reports the lock.

• soma docs flesh: one page (100 lines) with the syntax a body needs, for whoever fills a hole from its brief; every construct in it is run by a test. The brief adds /* … */ comments, a tool's description, the listeners of what it emits and emitted by.

• Pilot harness bench/agents/pilot.py (--selftest): three arms (plain cells / skeleton first, one agent / skeleton first, one tool-less sub-agent per hole given the brief alone), hidden tests, a token ceiling that counts design, refusal of anything but flesh after the freeze, an audit of every prompt for hidden material. Applications: bench/agents/pilot/marketplace (27 signals) and hotel (40).

• Red-team rounds 4 and 5 (2026-11-13), tests r4_* / r5_*. The lambda line is held twice. Statically: an impure lambda is written only as the last argument of a builtin that applies it (xs.map(x => …), a pipe). At run time, for every program: a lambda carries the cell that wrote it; applied in another cell it may only compute — a slot (also len(slot) and slot[i], which went round the guard), a handler call, a transition, an effectful builtin (also link, subscribe, ws_connect, ws_send) or an emit raises kind lambda. A lambda is at home anywhere in its own cell, whatever carried it there (a helper _each(xs, f), a combinator returned by another cell). soma verify, rules between machines: the right side of && / || / ??, a require's detail, a while condition, a match guard and a try no longer count the calls in their string interpolations as having run once for sure; a variable assigned in a nested block, a loop variable at each turn, a match binder and a lambda parameter are values of their own (a binder named like the id, or like a state, was read as the id or the state — false ✓); under edition 2027 get_status(id) == "initial" is false for an id never moved and is read so (get_status(id) ?? "initial" is read exactly in both editions). A brief whose comment leans on the one above ("The same, paid with points.") brings that comment along.

• Round 6 (2026-11-13): a red team (about 520 probes) and a builder agent that wrote a 14-cell, 115-signal clinic from the embedded docs alone (bench/agents/large/clinic, with its journal). Tests r6_*. The static frame and the run-time guard held; soma verify did not, in seven ways, all closed: continue lost the following turns of its loop; std.transition(…) / std.delegate(…) / std.think(…) were invisible to the product search, the guard proof and termination; an interpolated string ("{x}") was read as a constant id or target; two states differing by case; a guard "proven" although an effect in the same statement (or in the condition leading to it) ran before its transition; assuming = "amount > 5" reasoned in integers (5.5 passes < 6); a lambda that moves a machine and is kept for later is no longer read where it is written — the rule is then "not proven". For large programs: soma skeleton app.cell --index (one line per cell, then who calls whom), soma skeleton app.cell Cell (one cell with its comments and outside callers); a rule between machines accepts the evidence people write — require Other.status(id) == "x" through the other cell's getter, or a status held in a variable until the next call; verify --summary on an empty skeleton says once how many contracts wait for a body and names the run that leaves a rule open; sizes, counts and sums of a non-negative slot are proven >= 0; [verify.after."Cell.state"] says that only before reads qualified states; no "cross-cell not verified" note for a cell whose rule soma.toml states. Fixed on the way: return Rec { … } where the face says -> Rec (it was "a Map literal", E0040); a wrong argument count in a test cell's helper passes check no more; reads Other.machine is refused where it is declared when no body could read it; a handler whose transition(id, "ready", "paid") names another source no longer owes the guard of due -> paid; the frozen [verify] tables and edition hold for every entry file of the lock's directory; soma run app.cell _helper is refused for a skeleton; describe and lint refuse what the lock refuses. The brief prints the types of the slots it lists and how to build a value; soma docs flesh adds emit, declared types and variants, .entries / .values, sort_by.

• Round 7, maintenance (2026-11-13): an agent that did not know the clinic made five change requests on it without reading its sources, with --index, the one-cell view and the briefs. Tests r7_*. Its blocking finding: [verify.before."Lab.asked"] requires = […] on an INITIAL state was ticked whatever the bodies did — such a rule is now refused (an instance is there from the start, by no transition). New: while = ["Visit.open"] in a [verify.before."Cell.state"] table — the other machine IS in that state when the target is entered (requires is the past: "was open once"); read on holes like the rest. A property that proves nothing on a machine (its state is not one the machine reaches) prints ·, not ✓. soma refs app.cell Cell.signal: where the signal is declared, where its body is, every call and emit — program and tests — as file:line; the brief gives the two places to edit. soma check . is the project gate: skeleton and flesh files are checked through the file that imports them (each flesh failed alone), so the entry and every test file are judged in one command; soma test . ends with one total. soma rename app.cell Cell.signal new [--dry-run] rewrites the declaration, the body, every call (also inside a string's {…}), the frame clauses and the tests under the entry's directory, and renames an event in every cell that hears it (on the 115-signal clinic: one command, then --amend, check ., test .). A body left behind by a rename says which signal has no body; the one-cell view prints each helper's parameters.

• Round 7, red team on soma verify alone (423 probes, 11 false ✓, closed; reproducers in fixtures/skeleton_review/round7/red/). Invariants and contracts: a match binder or a let inside an expression block named like an outer local kept that local's range (let v = 5 let u = match x { v -> v }), and a Float reached % through a local — binders and Float marks are now known before any range is computed; a slot named size, key, status or _slot_len took the invariant on that word for a bound on its values; x.count() / len / size were Ints even when a handler of that name ran; k |> c.set(x) and x |> log.push() were not writes ("no handler writes to guarded slots"); a requires was "proven at N call sites" while an emit, a call that leaves trailing parameters out or a schedule's call went unjudged. Guards: a call into a cell with a lower-case name, or a builtin applying a lambda it is handed (xs.map(f)), between the require and the transition(). Rules between machines: a lambda kept for later in any form (an indexed list, ??, an if-expression, a Map); assuming with a literal past 2^62. Run time, found by the frame oracle on one of these: x.count() — a method call named like a builtin that the builtin does not take — ran the handler count of ANOTHER cell, in a signal whose frame said nothing of it; it is refused now, as count(x) already was at check ("a handler of another cell never replaces a builtin").

• Round 8 (2026-11-13), about 960 probes: 30 causes of false ✓, one frame leak, gaps in refs and check <dir>. Tests r8_*, reproducers in fixtures/skeleton_review/round8/. Run time: a call the builtin does not take (std.count(5, 1, 2, 3, 4), or count(x) written in a cell) no longer falls through to a handler of that name in ANOTHER cell. Rules between machines: a string's calls are read where the string stands, a require's operand once; a condition that moved a machine narrows nothing (a status read before the move, or held in a variable, is stale); vote(Cell.h, …) runs h; deliver, resume and horde make the rule "not proven" (so does a hole whose frame calls one); two cells of the same name keep their own machines; a rule that is only a while no longer ends in "lists no state". Guards: never "proven" by a hole, by if cap > 0 && zero(k) == 0 { transition… }, by an assignment inside a require, by o.get_status(). Invariants and contracts: lets at any depth of an expression block, a local / parameter / slot named like a cell (L.bal()), a handler max or keys of the cell where the rule expected the builtin, the written key rebound in the value, interpolation in what is proven, facts carried across await / resume / deliver, a string in a match pattern, slot[k] = v in an if-expression of a require, _slot_len on a delete; requires sites reached by vote, horde, or a method call on a local. Tools: soma check <dir> checks a part that has tests of its own, files that import each other and an entry only tests import, and resolves use name / use lib::x as the loader does; soma refs finds the method form (x.f()), a bare call from another cell, vote / horde / delegate, strings inside strings, files under target/, and reads only the files an import ties to the program (a backup lying there is not the program; a test that does not parse is named). Also closed, in 3.0 analyses beside the skeleton: two state machines kept under one storage key (A + B_m, A_B + m) are refused at check; the [task] wait report says which calls before the wait it does not follow, and no longer counts a transition(id, "b", "c") as a way out of a; effects reads a think() without options (or with options it cannot list) as offering every tool; composition sees an emit inside a try or a lambda; cost counts std.sleep(…), d.sleep() and a method call on a local named like a cell; [deterministic] follows a handler hidden by a local bound in a branch; verify --attest hashes imported files.

• Round 9 (2026-11-13): 20 causes of false ✓, 7 frame leaks, 15 tool gaps (rename attacked for the first time). Tests r9_*, reproducers in fixtures/skeleton_review/round9/. Three roots, treated as such. (1) Two name resolvers: the run looked a name up in every cell and in the caller first, the checker in cell / cell agent only and read std.f as the builtin. The run now agrees with the checker: std.f(…) is the builtin f and nothing else (not the cell's own handler f, not a handler elsewhere, await_* included); a bare or method call from a cell never reaches a handler of a cell test, cell type, cell property…; x |> slot.method no longer writes the slot NAMED BY THE VALUE of a local; a frame counts vote("Cell.h", …) as the call it is; a skeleton's slot may not bear the name of a cell or of its machine. (2) An evaluation order rewritten by hand: the product search follows the interpreter (a method call's arguments before its receiver, an index before what is indexed, a pattern's string where the arm is tried), counts edges taken so that a round trip narrows nothing, follows x.h() to the handler h also when x bears a cell's name, vote("Cell.h"), and reads a bare name as a state only when it is one. (3) Facts compared by their text: a text that leaves a body out (if c { … } else { … }) is no longer a key — in the interval prover and in the guard proof — and a local named size / key no longer satisfies an invariant clause by spelling. Also: the monotone-counter rule compares the ?? defaults and wants integers for a strict >; effects reads m[k] = think(…) and a require's operands; the wait report counts the enclosing condition and the wait's arguments, and says when it cannot place a transition. soma rename: cells declared cell agent or in lower case, method form, bare calls from another cell, delegate("Cell", "h"), tools_allowed, every listener's direct calls for an event; it rewrites only the program and its tests, only inside a string's {…}, never a slot or a local that follows a frame clause; a new name that is a word of the language or already a name in the program is refused. soma check <dir> follows use lib::dir (a directory) and installed packages as the loader does; --index counts a plain cell's handlers.

• Round 10 (2026-11-13): the red team was asked for DISAGREEMENTS between components, question by question (who runs a name, in what order, what binds a name, what writes a slot, what "the same" expression is, what a cell of the program is): about 25, with 52 reproducers (fixtures/skeleton_review/round10/, test r10_*). Settled by making the run and the analyses answer alike. Who runs a name: x.f(a) now resolves like f(x, a) — this cell's own handler first (the builtin ran in method form, the handler in bare form); x |> obj.f without a call is refused at run time (it reached a slot or a handler under no analysis); delegate reaches signals of cell / cell agent only, never a _helper; an emit is heard by cell / cell agent (and by the test cell under soma test), no longer by a cell type or by a test cell under soma run; a handler named transition … is refused in interior cells too; the product reads std.f as the builtin whatever handler bears the name, a tuple variant Opener(id) as a value, vote by its target or not at all, a slot before a cell of the same name. Order: a lambda handed to a method runs after the receiver; the arms of a match chain (a tried arm has run its pattern and guard); a condition's baseline is its own; a status in a variable is stale from the first call of the very statement; a variable assigned inside an expression is unknown from the start of its statement. Binding: a frame counts x.h() as the call of h when a local MAY bear the name of the cell or of the slot x (an assignment without let, one alternative of an || pattern) — two leaks; a slot is the slot before a cell of the same name in inferred frames. Same expression: quotes are escaped in the text of an expression; a function a fact calls is a name it reads; a slot named key / size / status is that binding, not the value. Guards: a handler named like a builtin is a call; a call hoisted out of a string is judged with what its statement does. soma refs / rename read vote("Cell.h"), horde("Cell.h"), std.delegate("Cell", "h").

• Round 11 (2026-11-13): the answers of round 10 held (frames over 57 forms of slot write, the product over 36 neighbours, guards, requires sites); 10 disagreements in what had not been compared. Test r11_*, reproducers in fixtures/skeleton_review/round11/. The hole model: a hole was read as ONE ordered pass over what its frame allows, so a rule ticked on a skeleton could be broken by a conforming body that calls twice or takes two edges in the other order — the model is now that set of steps under a loop ("a ✓ on a skeleton holds for every flesh that conforms" is true again, with a test). Frames: a handler run by vote("_w", …), vote(_w, …) or named in a horde's options (map("on_result", "_store")) is this signal's call — two leaks. Rules between machines: a [task] that awaits, called by a handler, hands {waiting} back at the wait — the rule is "not proven" rather than read as if the callee had finished; the statements of runtime { } are an entry like a handler's for every proof (they wrote slots, moved machines and called contracted signals unseen). Agent tools: tools_allowed is read in the LAST argument of think(), as the run reads it; a tool that thinks, or a helper that does, offers every tool again. Taint: q.think(), std.think(q), id.transition(d) are the source and the sink they are. soma rename rewrites a handler named in vote / horde options.

• Round 12 (2026-11-13): the hole model and the product search on a flat program held everything thrown at them; 28 causes in what had never been compared (interior cells, timers, runtime { } under check, the type names, tools over several folders). Test r12_*, reproducers in fixtures/skeleton_review/round12/. Fewer answers, rather than more cases: "is this name a cell?" is asked of the program (names::cellish) where a capital letter decided it in a dozen places (cell counter was a local to the invariant prover, the taint check, termination, the wait report, soma serve's GET rule); the statements of runtime { } are an entry of every analysis that reads the exposed program (cost, taint and capabilities at check as well as the proofs), and in a skeleton they only call signals or raise events, as a schedule does; a schedule may not call another cell's private helper. Frames: vote / horde whose target is a variable count every handler of the cell; at run time a private helper is reached by name from its own cell only. Interior cells: a bare call goes to a top-level handler (the proofs took the first homonym in file order, interior included), an event a parent raises is heard by its interior (rules between machines, cost). tools_allowed is narrowed only when nothing the handler runs can think again (helpers of helpers, an emit, another cell). Guards: a literal built by interpolation is no constant; a slot written is another value for a fact that read it by its bare name. Numbers: -> Int answering a whole Float gives the Int it promises (the proofs read an Int; a + 1 - a was 0 past 2^53); BigInt, a name the run does not check, is no Int for the prover. Tools: refs / rename find the project from an entry in a sub-folder (the nearest soma.toml above) and read runtime { }; an imported folder is read one level deep, as the loader reads it.

• After the review (2026-11-13). A signal's comment is the brief its body is written from: skeleton.lock records a digest of it, and soma check WARNS when it changed since the freeze (not an error: a retouched sentence is no amendment); --amend records the new one. checker/bodies.rs: one list of what runs in a cell — handlers, every / after, runtime { } — read by effects, capabilities and budget, which saw handlers only. tools/verdicts.sh compares the files of main. What is left to unify, and two proposals that need a decision (one rule for events and interior cells; rules between machines over different ids): STRUCTURE_DESIGN.md.

• The structural work (2026-11-13), STRUCTURE_DESIGN.md. One rule for who hears an event, whatever started the program and for every analysis: raised by a top-level cell, the top-level cells and its own interior; raised by an interior cell, its siblings and its parent (Interpreter::hears; check counts a parent's events as reaching its interior). One store per slot: the scope runtime of soma run app.cell takes its back-ends from the registry like every other command — a [persistent] slot was a JSON file there and a sqlite table elsewhere (data written by soma run app.cell in a JSON file under .soma_data/ is not read any more). The start-up audit covers interior cells and every cell of a slot name. One answer to "where is the project" (project::root): a test file in a sub-folder that imports the program gets the program's manifest — its edition and its [verify] tables. The older analyses follow values and calls: taint through a list, an index write, a lambda parameter and vote; composition by the arity of the listener and only among cells of the program; budget with the largest callee frame and map over an unknown length as no bound. A rule between machines in the frame: moves drafted -> delivered when Consult.done [|| …] [via consult_of] — the edge is taken only while the other machine is in one of those states; verify judges it on the bodies and on the holes (whose model takes the edge only under the clause), the brief prints it, the lock holds it. via = "Cell.slot" in a [verify.before."Cell.state"] table: the states required are those of the instance the target's instance names in that slot (written once, when the entry is created, never deleted — checked); the search follows the pair.

• Round 13 (2026-11-13), on the structural work: 14 disagreements, closed (test r13_*, reproducers in fixtures/skeleton_review/round13/). via: the link must be written at a key the writer leaves as it came (a parameter never rebound), by a handler that is no [task], and a write inside a string's {…} counts. Events: signal x(…) in a runtime { } reaches the top-level cells too, as an emit of the cell does; a listener in the emitter's own interior MAY not run (the interior is started only by soma run app.cell, for the cell that drives it) — the proofs no longer count on it; an interior cell may not bear the name of a top-level cell (a running cell is found by its name: the two were taken for each other); check decides who hears an event by the same rule, and warns that the interior of an interior cell never runs. The project of an entry is the folder above that holds both a soma.toml and an import the loader resolves there (a nested soma.toml holding none of them is not it; an import found beside the entry is not the parent's). Taint across loop turns and across the branches of an if or a match; effects follows a bare call into another cell's handler; range(…) costs its list in the budget.

Not covered: a helper's privacy is its _ name (the existing rule for routes and events); frames are per cell and syntactic; an edge's effect { } block and what guards and invariants read belong to the structure, not to a frame; a flesh sees its skeleton's constants when the skeleton is in the same file or in the file that imports the flesh.