Soma 2.5.1 — 2026-09-18
A hardening release: seventeen more fresh-agent cycles (realistic ports — billing, support agents, reservations, analytics, safety interlocks, kanban, eMAR, a game economy, a WMS — each paired with an adversarial round). Every finding is fixed or listed as open in docs/agent-ux/LEDGER.md. Highlights: false proofs closed (require/guards/while conditions in cost and termination, NaN on Float slots, deletes, shadowed builtins), security fixes in serve (route ownership, CSRF through cross-cell calls, SSE/WebSocket isolation and injection, slow-client and flood DoS, capability SSRF, private slots, record forgery), crypto builtins for authentication, and exact BigInt arithmetic across builtins.
-
Cost: think() in a while condition counts per iteration; the last max_rounds wins. Route ownership sees UFCS, interpolation and delegate calls (auth bypass).
-
Storage: an Any slot gives back the String it stored (no JSON re-parse).
-
else { if … } is a value; exhaustiveness ignores refutable sub-patterns; BigInt-exact clamp / pow_mod, 64-bit limits raise; native len counts characters; invariants are per cell; qualified-call arity is checked.
-
verify models transitions from a machine-less cell (single-machine programs); the composition lint flags only callees that swallow failures.
-
serve: emit is not pushed to WebSocket clients (only publish is; SSE clients get an emit only when they name it); each WebSocket client has its own queue (a slow client is dropped instead of starving the others); websocket, tick and bus threads have the 64 MB handler stack (deep recursion there aborted the process).
-
try { … }? re-raises; a guarded match arm does not cover its variant; "{slot}" works; {…} must be one expression.
-
mod / idiv / floor_div / div_round take Ints; sum_by / avg_by refuse non-numbers; distinct keeps values of different kinds.
-
serve: a GET that calls into another cell's handler (bare, UFCS or pipe) is 405 like a qualified call.
-
Crypto builtins take Strings only (secure_eq("null", ()) was true); random_token is nondeterministic for replay.
-
Check: a test rule calling transition() in a multi-machine program; foreign slots through Cell["slot"] and interpolation.
-
Security: a cell's slots are private (reading another cell's slot by bare name is a check error); another cell's handler never replaces a builtin (a library's escape_html disabled escaping); soma install refuses dependency names with / or ...
-
New builtins: sha256, hmac_sha256, random_token, secure_eq.
-
use imports each file once (cycles and diamonds load); soma run takes everything after the handler as arguments; --json is always JSON.
-
response() honours an explicit Content-Type; html() takes headers; properties see the rules' let fixtures.
-
Check: a handler cannot be named after a safety builtin (transition, approve, fail, think…) — it replaced the builtin program-wide while verify still proved the edges; one initial: per machine.
-
verify: a reactive machine (no terminal state, every state returns to the initial one) passes --strict.
-
serve: one scheduler per data directory (a second serve doubled ticks).
-
Capitalised field names in assignments and record literals.
-
A panic inside a builtin is a catchable error (kind internal); matrix builtins cap each dimension (a zero dimension bypassed the size cap).
-
Native: i64-to-BigInt local assignment compiles; mixed Float/String returns are a check error. Regexes are compiled once per pattern; read_files is in name order; format("%d", inf) raises.
-
serve: WebSocket and SSE pushes carry the data as one-line JSON (a String payload could forge envelope fields and SSE events for other clients).
-
range near i64::MAX ends (the step wrapped); format("%.Nf") past 1000 decimals is a range error, not a crash; round/floor/ceil of 2^63.
-
soma test: a test cell's own helpers win its bare calls.
-
Security: &&/||, ensure, match guards and properties take Bools (a list mask or a String passed compound invariants, guards and asserts); tool capabilities match host and path separately and refuse .., userinfo and fragments; a tool's scope holds inside the agents it calls.
-
Agents: map("tools_allowed", [...]) restricts the tools one think() offers; a timeout is not retried (it billed up to 4 × max_tokens past the proven bound); a literal transition in a tool keeps think-isolation; recall works across processes; unknown think() options are check errors.
-
Replay records only top-level calls and uses soma.toml [agent].
-
Check: a function used as a value, () as a slot key, Bool arithmetic and Rust keywords in [native] code.
-
serve: an SSE client receives only the streams it subscribed to (every client received every publish); a connection flood that broke the HTTP worker pool exits the process (status 70) instead of leaving it alive and deaf; a literal delegate to a missing handler is a check error.
-
Prover soundness: calls in require conditions and details are analysed (termination, cost, invariants); transition guards must be pure; a delete voids a key-exists size proof; Float-slot writes that may be NaN are runtime-checked.
-
serve: a handler request calls is reachable only through request (auth checks written as if/starts_with were bypassable); one builtin call builds at most 10^8 elements (a single request aborted the process); sleep bounded; bus lines capped at 16 MB; cross-process emit sent at commit; [bus] accept filters outbound links too.
-
Data: next_id() ids stay unique across a failing try; sum-typed parameters and generic variant fields are checked; write_csv quotes Lists, headers and numeric Strings; exact Int vectors, matrices and median; date builtins bounded; for over () runs zero times.
-
Check: reading another cell's slot, every 0ms, and a native local reassigned to another type are errors with a fix.
-
A bare call inside a cell to a handler name another cell also defines runs the calling cell's own handler (it ran the other cell's).
-
soma serve no longer exposes the start-up hook (init / start) as an HTTP endpoint; static text files get real content types.
-
soma verify always ends with a verdict line, prints check errors on stdout, and says which require would prove an open invariant.
-
Native: a buffer passed to a sibling is a check error; Int-valued calls in Float expressions compile; a constant overflow is the range error.
-
soma verify fails when [verify] cells names a misspelled cell or one without a state machine (every property was silently skipped).
-
serve refuses a request body carrying _status (a handler echoing it let the client pick the status and headers), answers 500 for a status outside 100–599, 400 for a non-UTF-8 body, and keeps %ZZ literal.
-
The prover narrows by if branches and accepts update loops over a slot's keys; cost { tokens } is stated as reply tokens.
-
Data safety: persistent List slots enforce size invariants on push; state machines persist without a persistent slot; match arms are scopes (a failed guard deleted the outer variable).
-
Prover soundness: NaN, shadowing by match/lambda/nested lets, growth and cost through other cells and emits, termination with re-bound parameters.
-
serve: GET/HEAD to a state-changing handler is 405; _type/_variant in client JSON is refused; neither start nor init is an endpoint.
-
soma run refuses a program that fails check; native check runs the code generator; native shifts, sqrt_int, sb_push_char fixed.
-
serve: only response()/html()/redirect() maps are HTTP responses (a client map with _status stored or echoed forged status, headers and XSS); CR/LF header values dropped; the bus port refuses HTTP and private events.
-
Prover: a require proves only the writes after it; reassignments in match arms, try and if-expressions; every/after writers; termination through pipes, qualified self-calls and tick loops.
-
Hints for require without else, and/or/not, a quote inside {…}; CI builds Linux and Intel macOS binaries for every release tag.