Releases: soma-dev-lang/soma
Release list
Soma 2.7.0 — hordes
Hordes: thousands of agents on one subject, under one token ceiling.
horde(Reviewer.review, docs, map("concurrency", 500, "budget_tokens", 2000000, "on_result", "_store")) runs a [task] agent once per input with a bounded pool — model calls wait outside the lock, every call reserves its worst case against the ceiling first, the queue survives a restart and each result is recorded once (also across kill -9). soma verify prints each horde's cost bound. Rounds (snapshot, ordered apply, seed, per-agent instance memory) make population simulations reproducible; vote() asks k agents the same question. Measured with a mocked 2 s model: 10 000 tasks at concurrency 500 in 41 s; 10 000 agents × 20 rounds in 46 s, identical on two runs.
Docs: https://soma-lang.dev/docs/serving.md (Hordes) · design: docs/design/horde.md
-
Hordes (attack pass): nested hordes and hordes started from callbacks run
under their parent's budget (a nested horde spent 6 000 tokens past a
"proven" 100); check refuses a computed target or options (an HTTP client
could pick a private handler or drop the budget) and literal options out of
range, and warns on public callbacks; two servers on one.soma_datarun
each horde once (a lease, taken over when its server stops); hordes are
persisted under serve / run even without a[persistent]slot; the queue
tables cannot be reached from a slot named_hordes; only the owner cell
reads or cancels a horde; the rate limiter is an exact 60 s sliding window. -
Hordes (quality pass, phase 5): a crash while a horde was cancelling
resumes it as cancelled with counts that add up; a restart does not resume
a horde whose handlers the new code renamed (it says why, statepaused);
undersoma testa horde runs after the caller commits, like serve (a
callback can cancel it);on_errorreceives{error, kind, detail};
tasks the budget stopped count as cancelled;soma verifyprints each
horde bound once and--strictfails on an unbounded one; each task
starts with a fresh model context. Dashboard: live hordes at/__soma/.
SOMA_LLM_MOCK=rules:mocks.jsonanswers by prompt pattern. Corpus:
agents/horde_audit.cell,agents/horde_rounds.cell. -
Hordes (phase 4): rounds for simulations —
snapshot(every agent sees
the same world),apply(results applied at the end in input order, once),
seed(reproduciblerandom()per task),instance(per-agent
remember/recall and conversation across rounds);vote(handler, input, k).
10 000 agents × 20 rounds: 46 s, identical on every run. -
Hordes (phase 3):
budget_tokensis a hard ceiling — each think() of a
horde reserves an upper bound (request bytes + max_tokens) before calling
the model, waits outside the lock for calls in flight when it does not fit
yet, and is refused (kindbudget, stateexhausted) when it never will.
soma verifyprints each horde's cost bound; in a cell withcost { }a
horde over inputs of unknown size needs a literalbudget_tokens. -
Hordes (phase 2):
horde(Reviewer.review, docs, map("concurrency", 200, "on_result", "_store", "on_done", "_done"))runs a[task]handler once
per input with a bounded pool and returns an id at once;horde_status,
horde_results,horde_cancel. The queue is persisted with the data and
resumes after a restart; each result is recorded (andon_resultcalled)
with the task's last step, so once even afterkill -9. Retries
(max_attempts),on_error,on_done. Provider limits[agent] rpm/
tpm(SOMA_LLM_RPM / SOMA_LLM_TPM) shared by every think(). 10 000 tasks
with a 2 s mocked model at concurrency 500: 41 s. Check validates the
target, callbacks and options. -
[task]handlers (hordes, phase 1):on h(…) [task]runs as steps —
eachthink()commits the current step and waits for the model outside
the handler lock, so concurrent requests overlap their model calls (200 ×
2 s mocked calls in ~9 s). A failure rolls back the current step only; the
prover carries no fact across athink(). Ticks take it too:
every 1min [task] { … },after 5s [task] { … }.
SOMA_LLM_MOCK_LATENCY_MSgives the mock a latency. -
Check warns when a plain handler or tick (
on requestrouting, a
listener) calls a[task]handler — it would hold the lock; when a
[task]reads a slot before athink()and writes it after; when atry
writes and thinks; when a[task]has nothink().[task, native]and
unknown handler annotations ([tsak]) are errors. -
Records:
r.field = von a record,is_a(r, "Line"),keys(r)/
values(r); a record printsLine { sku: a, qty: 2 }. -
Cost: a loop over a collection of unknown size counts once (a lower
bound, the bound stays advisory) instead of an invented ×100 that could
report a false "budget exceeded"; verify counts think() call sites. -
"undefined function" points at the call, not the handler header.
-
Scheduler: a second
soma servetakes over the every/after blocks when
the owner stops; the lock is per program; each tick's token budget starts
fresh. -
Records: a JSON object / Map given for a one-variant
cell typebecomes
that record (errors name the field); variant fields read asv.field;
deleting from an[immutable]slot is a check warning. -
Your handler named
subscribe,link,ws_connectorws_sendwins
over the network builtin at its arity;cell testhelpers are held to
the declaring cell's invariants and[immutable]. -
soma runcheckpoints the WAL on exit; a damaged BigInt row is reported
instead of reading as 0;--freshresets data only after the check
passes; handlers reached fromrequestthrough a model tool are not
endpoints;ensureafter an earlyreturnis a check warning; a raising
forallnames its value; notes are not counted as warnings. -
Soundness: a
requireon a slot read no longer proves writes made after
the slot was rewritten (here, through a helper ordelegate); handlers
reached fromrequestthrough anemitat any depth are not endpoints. -
[immutable]slots are enforced: append-only Lists, add-only Maps. -
CSV "NaN" / "inf" stay text;
soma testnever touches.soma_data;
delegatekeeps the callee's error kind;soma runrefuses a damaged
database;--fresh --recordstarts a new log. -
Soundness: a negative List index is checked at its real index; a List
delete re-checks shifted elements againstkeyinvariants (verify
reports it runtime-checked); a self-recursive writer counts for size
proofs; untyped / Any slots get no integer narrowing; file writes and
subscribemake a latency bound advisory,subscribehas connect and
handshake timeouts. -
()is refused for a List parameter; a slot-less invariant over several
slots is a check warning;write_file/write_csvcreate the directory;
to_csvkeeps every column. -
Site: external effects are not rolled back (/agents); replay re-runs LLM
and HTTP calls live (README).
Soma 2.6.1
- Site and README: the stated guarantees now match the documented ones —
distribution checks prove the declarations' coherence (the prototype
replicates eventually), rollback covers slot writes and transitions (not
external effects),set_budgetstops the next call, default liveness
means an exit stays reachable (eventuallyfor every run), the paper's
quorum is ⌊N/2⌋ + 1; the /agents payment example requiresamount > 0;
a homepage demo shows proven / runtime-checked / not covered. soma run --freshresets exactly this program's tables (a cellA
reset another program'sA_b); an unreadable soma.toml fails closed;
soma runwithout a handler prefersmain/runand never runs a
_privateone;soma build -o x.cellis refused andsoma deploy
keeps existing files;verify --jsonis JSON when check fails.soma fixhandles non-ASCII lines;soma replaykeeps numeric-looking
Strings as Strings and fails on unreadable or empty logs; the dashboard
is same-origin only.- New
asin,acos,pi();tan,atan,atan2,asin,acos,pi
in[native]. - Bus: a connection must send its first line within 10 s; at most 256
are open at once (half-open connections held a thread each). require <Int builtin>is a check error likeif;soma run --fresh
resets only this program's tables when other programs share the database.- New
to_csv(rows);roundnever returns -0.0; clearer errors for
negativerounddigits and multi-variableforall; recursion limits
documented (512 interpreted, 20 000[native]). - Peer bus: two processes listing each other exchange each event once
(links open withHELLO); closed connections free their thread and
socket; a[peers]address that is this process is refused; the
reconnect back-off holds for links that drop at once. - The start-up audit no longer reports write-once rows; a prompt that
alone overruns the remainingset_budgetraises before it is sent. body: Stringis the exact bytes received;to_jsonescapes</and
<!--; the injected htmx script is pinned with SRI;hmac_sha256with
an empty key fails closed;--recordlogs are owner-only.[peers]links are supervised: a peer down at start-up, restarted, or
dropped for reading too slowly is reconnected.- Packages: sub-directories are installed and covered by the lock's
sha256; a file the lock does not list, or a case-variantuse, cannot
bypass the check; an installed package missing from the lock is refused. - Latency bound: http without timeout counts 30 s; a think without a
literal timeout makes it advisory. The JSON cap weighs objects and lists;
self_callcatches IPv4-mapped IPv6; CSV cannot carry_type/
_variantcolumns; invariant source is not sent to clients; duplicate
Origin headers are refused; importedevery/afteris warned. split(s, "")splits into characters;parse_int(s, base); numbers
beyond the Float range are refused byfrom_json, HTTP bodies and bus
events; NaN sorts last in descendingsort_by;ipowof 0 / ±1 to huge
exponents;sum_byof a non-list raises.
Soma 2.6.0
- soma.lock records a sha256 of each package's files: a package modified
after install is refused at import, andsoma installrestores it. - Check warns when an imported cell defines
requestorws(it would
own HTTP routing / the WebSocket port). self_callcounts only ports this process listens on; a failed guard's
source is not sent to clients; 204 / 304 carry no Content-Type; a quote
inside{…}in a call argument gets the escaping hint.- Performance: a lambda's captured lists and maps are no longer copied
per element —|> map/filter/ … over a captured list is linear
(was quadratic). [native]: an Int/stays exact after the BigInt re-run (it truncated
the docs' midpoint example); a handler returning its String parameter
compiles; an Int overflow inside a Float/Bool expression is kindrange.sort_byputs NaN last; an unclosed CSV quote is an error;quantile
refuses q outside [0, 1]; blank CSV cells are missing values for
sum_by/avg_by; operator chains count toward the nesting limit."s" |> map(f)and"s".map(f)raise a type error; kinds
rate_limited/too_many_requestsanswer 429.- WebSocket: a returned
response(…)sends its body; error bodies hide
private handler names; binary frames are answered with an error. - Clearer errors for reserved words used as JSON fields (
d["cell"]) and
for guard locals of a handler that may take a guarded edge. - Soundness:
"C".delegate(…)/"C" |> delegate(…)are seen by the
termination and size proofs; alethiding a slot no longer lends the
slot's bound; thelatencybound counts retries (thinktimeoutnow
covers them), tool rounds,sleep, and is advisory with approve / file
I/O; an interpolated transition target is treated as computed. [native]: an exact Int / Int with operands past 2^53 is exact; stdin
read before a BigInt re-run is replayed.- New
ipow(exact Int power) andfrom_csv(text);read_csvtakes
delimiterand refuses unknown options;map/filter/… on a non-list
raise a type error;format("%.2f", Int)is exact;to_floatpast the
Float range raisesrange;powof a non-number raises. - In an invariant,
slot.get(key)reads the stored value on Map- and
record-valued slots too: write-once invariants onMap<String, Map>/
List<Map>slots were not enforced. - approve() shows control characters as escapes (a model could redraw the
prompt); every reply shape is measured against max_tokens and the budget,
a reply with no text raises kindllm; aset_budgetreached from a tool
call can only lower the caller's budget;..;/is refused by capability
path scopes. - A List
deleteis checked by size invariants only (as verify says);
require … else budgetanswers 400. - A JSON request body or bus event with more than 1 000 000 values is
refused before parsing (a 15 MB line became 2.4 GB in memory). - Events sent after a linked peer disconnected are logged NOT delivered;
soma runwarns when anemitmeant for[peers]goes nowhere. - Check warns on
m.size ?? default(.sizeis the entry count, never
()); a negative[native]buffer index is reported as written. - Every path-taking builtin (
load,include,load_template,
read_files,par_read_files,word_count) refuses a..segment:
load("templates/" + name)could serve any file. - The bus port opens only for
[peers],[bus] accept,scaleor
--join: an in-processemitno longer exposes the program's listeners. - Kinds
unauthorized/unauthenticatedanswer 401; error bodies no
longer name private handlers; the loopback Host check parses the whole
authority and refuses duplicate Host headers. SOMA_LLM_MOCK=fixed:over max_tokens raises kindllmlike a scripted
mock; guard locals bound after a transition to another state are accepted.- The file write guard is case-insensitive;
self_callrecognises every
spelling of this machine;Origin: null/file://writes are refused
on loopback servers. - LLM replies are measured as well as counted: an under-reported reply
cannot pass max_tokens or the proven cost bound. - File builtins refuse
..segments and writes over the program, its
configuration or storage; a loopback server refuses foreign Host headers
and cross-origin writes; an HTTP call to the server itself answers
self_call; tool capabilities match query spaces encoded. - get_status & co. from a machine-less cell with several machines, and
variant literals with wrong fields, are check errors; the secret recipe
fails closed; security notes in the serving docs. pow_modwork is bounded (bits(exp) × bits(m) ≤ 2^30);to_int/
parse_intrefuse text past the 2^24-bit Int cap.- A bus event that reaches no peer is logged as NOT delivered; the docs
give an outbox + acknowledgement pattern for transfers between processes. - An Int holds at most 2^24 bits: products,
shlandproduct()past it
raise kindrangebefore they are built (interpreter and native);
matmulis capped at 10^9 multiply-adds. substringandrangerefuse wrongly typed arguments (kindtype).- A huge declared Content-Length no longer aborts
soma serve(tiny_http
vendored with a chunked drain; bodies past 256 MB are refused 413). - A scripted
mock thinkreply longer than max_tokens raises kindllm. - Bus peers have bounded send queues (a peer that stops reading is
disconnected); WebSocket clients are also dropped past 64 MB queued; the
WebSocket Origin check refuses userinfo and control characters. - A split string as the last statement of a loop body is a check error;
disjunctive invariants over the written value are proven. - Duplicate or list-valued Content-Length is refused and the connection's
pipelined bytes never run; request-log lines escape control characters. - Unary operator chains count toward the nesting limit; a List slot's
invariantkeyis the Int index;html()with header pairs passes the
arity check; guard variables bound in a loop body are recognised. emitarity mismatches are check errors; a computed Float is refused by
an Int parameter; CSV rows of empty cells survive a round trip and
duplicate CSV headers are refused.- Parameter types are checked all the way down (HTTP, bus, tools, calls);
a Float past 2^53 is not coerced into an Int parameter;[native]
handlers and mocks are held to the face's return type. from_jsonrefuses undeclared_types; misspelled builtin types and
extra builtin arguments are check errors;()is refused where a nested
scalar is declared;write_csvkeeps rows holding an empty String.- The equal-clause proof tolerates callees that cannot write the slot;
contextual keywords work as statement variables. - A handler parameter may not take a slot's name; face parameter types must
match the handler's. - verify and the guard rule see every / after ticks of machine-less cells;
instance ids are Strings or Ints (()refused); a renamed machine is
reported undersoma runtoo. soma runtreats any non-data token as a handler name when several
exist; NaN / lambdas in responses are valid JSON.[native]bnotis exact past 2^63; nativeloop_bounderrors keep
their kind;soma run … requestdecodes the path like serve.- Guards of transitions taken from machine-less cells are checked;
--strictfails when[verify] cellsnames no cell of the file;for
over any finite value terminates; anemitin an imported file opens the
bus. - The equal-clause proof applies only to pure clauses (locals, arithmetic,
??,.getof the written slot) with a plain key — other slots,
nondeterministic or external reads between the require and the write
made it prove refused writes. - Invariant slot references are counted deep (interpolation, lambdas,
match arms) by the checker and the runtime; verify hints never name
size / key / value; undefined functions in properties are check errors. mock Cell.handlerstubs that cell's handler only; mocks naming nothing,
test helpers shadowing program handlers or builtins, and test cells with no
assertion are errors; mocks reach[native]sibling calls.--recordlogs calls that raised;describe/ the dashboard keep
excepton*edges;soma fixexits 1 when errors remain.- A
requirethat is exactly an invariant clause over the written value
proves it (monotone versions);value/key/sizeoutside an
invariant are check errors; slots in nested lambdas are not function values. soma serverefuses to start on a damaged database (quick_check); a
file that is not a database is a clean error, not a panic.- A materialized
range()is capped at 10M elements; dotfiles under
static/ are not served; Content-Length + Transfer-Encoding is a 400. - Quant builtins enforce
max_obs/max_assetsand a confidencealphain
(0, 1); no false "share the path" warning for emit listeners. - The invariant prover is exact for Ints past 2^53 (intervals widen
outward instead of rounding), counts think() tools and computed delegates
among a handler's callees, and does not prove a bare slot read that may be
(). http_getin a loop, lambda or tool no longer makes a token bound
advisory (only a latency bound); a saturated cost peak is advisory.[native]i64::MIN / -1raises instead of returning a rounded Float;
guarded transitions in lambdas see the handler's locals; refinement paths
keep their parentheses.- Statements inside block lambdas,
try { }, if-expressions and match arms
(slot[k] = v,emit) are seen by GET→405, the listener set, the
termination graph, the size prover and guard / invariant purity. returninside a block lambda is a check error; a barereturnreturns
();soma run … request GET "/a?x=1"splits the query;every 90m
names the duration units.x |> hwith a bare handler n...
v2.5.1 — the hardening release
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_roundswins. 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:
emitis not pushed to WebSocket clients (onlypublishis; 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_roundtake Ints;sum_by/avg_by
refuse non-numbers;distinctkeeps 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_tokenis nondeterministic for replay. - Check: a test rule calling transition() in a multi-machine program; foreign
slots throughCell["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'sescape_htmldisabled escaping);soma installrefuses
dependency names with/or... - New builtins:
sha256,hmac_sha256,random_token,secure_eq. useimports each file once (cycles and diamonds load);soma runtakes
everything after the handler as arguments;--jsonis always JSON.response()honours an explicit Content-Type;html()takes headers;
properties see the rules'letfixtures.- 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; oneinitial: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_filesis 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). rangenear i64::MAX ends (the step wrapped);format("%.Nf")past 1000
decimals is arangeerror, not a crash;round/floor/ceilof 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;
recallworks 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 literaldelegateto a missing handler is a check error. - Prover soundness: calls in
requireconditions 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
requestcalls is reachable only throughrequest
(auth checks written asif/starts_withwere bypassable); one builtin
call builds at most 10^8 elements (a single request aborted the process);
sleepbounded; bus lines capped at 16 MB; cross-processemitsent at
commit;[bus] acceptfilters outbound links too. - Data:
next_id()ids stay unique across a failingtry; sum-typed
parameters and generic variant fields are checked;write_csvquotes
Lists, headers and numeric Strings; exact Int vectors, matrices and
median; date builtins bounded;forover()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 serveno longer exposes the start-up hook (init/start) as an
HTTP endpoint; static text files get real content types.soma verifyalways ends with a verdict line, prints check errors on
stdout, and says whichrequirewould 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 therangeerror. soma verifyfails when[verify] cellsnames 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%ZZliteral. - The prover narrows by
ifbranches and accepts update loops over a
slot's keys;cost { tokens }is stated as reply tokens. - Data safety: persistent List slots enforce
sizeinvariants 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; neitherstartnorinitis an endpoint. soma runrefuses 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_statusstored or echoed forged status, headers and XSS);
CR/LF header values dropped; the bus port refuses HTTP and private events. - Prover: a
requireproves only the writes after it; reassignments in match
arms,tryand if-expressions;every/afterwriters; termination through
pipes, qualified self-calls and tick loops. - Hints for
requirewithoutelse,and/or/not, a quote inside{…};
CI builds Linux and Intel macOS binaries for every release tag.
v2.5.0 — the agent-experience release
The agent-experience release. Nine cycles of fresh AI agents (none had seen
Soma) built services, ported Python/Java/TypeScript/Go/Ruby programs, ran
data jobs and LLM pipelines, and attacked the prover, the runtime and the
parser — learning only from the website. Every finding below was reproduced,
fixed, and pinned by a regression test; the whole repository (1,405 .cell
files) was re-run through check / verify / test after every batch.
Soundness and atomicity
- A handler with persistent slots is one SQLite transaction: a process
killed mid-handler (kill -9) leaves nothing of it on disk (writes used to
commit one statement at a time).every/afterticks are rolled back
when they raise, like handlers. - Slots give back exactly what they stored: an Int beyond 64 bits stayed a
String; records keep their field order;.keys/.valuesare sorted. - Slot value types are enforced on every write (
Map<String, Int>refuses a
String,1.5or1.0;Map<String, Pay>refuses a plain map). - List slots:
rows[i] = v,rows[i].f = v,rows.delete(i)used to be
silently dropped. - The prover no longer issues false ✓: a
requirein a loop that may run
zero times, bindings that shadow a narrowed name, interval overflow past
2^53, termination without a lower-bound base case, cost bounds that skipped
everyblocks anddelegate, liveness that assumed guards pass (now said). - The prover proves more: a
requirecounts for the writes of its own block,
early exits (if n >= 1 { return … }),require a + b <= Kon the written
expression, one slot's invariant chained through a local,size/
len(slot)invariants, deletes against value invariants. Every ⚠ says why. requestis never an HTTP endpoint (a GET could run a POST route);
path segments are percent-decoded; CORS on every response.- A bare call to a name two cells define is a check error (it resolved at
random);*edges no longer fire from states a program stopped declaring.
Language and builtins
format(fmt, …)(printf subset),div_round(HALF_UP),floor_div,
mod,divmod,to_fixed, exactround(x, d); dates:parse_date,
add_days,add_months,days_between,months_between,
days_in_month;chr,ord;stdev/varianceare sample statistics
(pstdev/pvariancepopulation);sin cos tan atan atan2,regex_*,
read_stdin,write_strin interpreted handlers too.- HTTP client:
http_get/post/put/patch/deletewith a default 30 s timeout,
headers, and{error, kind, status, body}on failure (the upstream body is
kept); mockable in tests. think_jsonraises kindjsonon a non-object reply; mockedthink
costs tokens (budgets testable offline);trace()survives requests under
soma serveand records the system prompt.- Variants round-trip through
to_json/from_json;soma runand
soma serveanswer valid JSON (NaN/inf → null). - Literals
1_000_000,0xFF,0b101,"\u{1F600}"; negative range
patterns; bare state names; keyword field names (j.state = …). |> map,|> filterandxs[i]are linear (a 20k-row job went from
104 s to 0.1 s).
Toolchain
soma checkcatches what used to fail at run time: native-only
primitives outside[native], what the native codegen refuses (buffer
re-binding, list returns, stepped ranges, literal/ 0),breakoutside
a loop,transition()arity, values thrown away (let j = 1 2), rules
outside a test cell, empty test cells, writes to a loop copy (warning),
emitwith no listener (warning). 10 000 nested blocks no longer crash it.soma verify --strictrepeats the ⚠ lines by the verdict and always ends
with one verdict line; orphan[verify]properties fail.soma test --jsonrecords carry rule, message, left/right, raised;
assert_fails … matchingmatches the kind too;mockworks for any
handler,Cell.handler,now, and builtins such ashttp_post.soma serve:--no-schedule, anllm:start-up line, endpoints listed,
whitespace-padded JSON bodies accepted, stored-data audit at start-up
(undeclared states, invariant violations, re-typed values, renamed slots)
— also undersoma run.soma run --fresh;.soma_data/lives beside the program; exact big-Int
CLI arguments.soma fixrepairs;,=>arms,-> Ton handlers,
null/True.soma describe --jsonlists sum types.
Site and docs
- New
docs/operations.md(failure modes, statuses, exit codes, migration
guide, environment variables); serving/guarantees/reference corrected
against the binary; builtins regenerated from the compiler; the landing
page links status, guarantees and serving, and states what verify proves. - The
soma initstarter and the corpus exemplars pass--strict.
Install
curl -fsSL https://soma-lang.dev/setup.sh | shmacOS Apple Silicon binary attached (soma-aarch64-apple-darwin, checksum in SHA256SUMS). Other platforms: build from source (cargo build --release in compiler/, needs GMP) — see docs/operations.md.
v2.4.0 — audit release: soundness, security, agent onboarding
An audit release: the verifier and the runtime were attacked with adversarial
programs, a differential interpreter/native harness and a fuzzer; everything
found is fixed here, each fix with a regression test (274 Rust tests, and
all 1,083 .cell programs of the repository re-run with no regression).
Language
7 / 2is3.5everywhere.[native]handlers used to truncate
(3). Native/on two Ints is now a Float; an exact quotient is still an
Int (BigInt-exact); a slot that can only hold an Int refuses a non-exact
quotient with a runtime error instead of truncating.idiv(a, b)is the
integer quotient on every backend (now supported in[native], and
BigInt-exact in the interpreter, where it used to turn any value beyond
i64 into 0).soma fix f.cell --native-idivmigrates old code.soma checknow rejects: a string literal dangling afterreturn
(return "a" "b"silently returned"a"), a memory invariant naming
several slots (every write would have been rejected at runtime), a
non-exhaustivematchinside a lambda. It now warns on: a call that
resolves to a builtin instead of the homonymous handler, unreachable code,
Int / Int in a[native]handler.
Soundness
- Memory invariants:
deletebypassedsizeinvariants;soma verifydid
not see bracket writes (slot[k] = v) or deletes. - Termination proof: mutual recursion, recursion hidden in an operand
(1 + f(n + 1)) and decreasing recursion without a base case were all
reported as "structurally terminate". - Cost proof: "
tokensbound proven" was claimed for athink()reached
through a sibling handler, a lambda, or a loop over a list of unknown
size. Calls are now composed; unknown counts make the bound advisory.
Runtime
- Security:
soma serveserved/static/../soma.toml(API keys), the
.cellsources and.soma_data. Static files are confined tostatic/. [native]: a division by zero aborted the whole process (SIGABRT); a
panic in native code is now an ordinary,try-catchable error. Concurrent
native builds in one directory poisoned the dylib cache (wrong results,
silently): builds take a lock, publish atomically, and every dylib carries
a build id verified at load.soma testignored[agent]/[models]insoma.toml(somockhad no
effect);soma replayblamed nondeterminism when the source had changed;
soma run f.cell -7rejected negative arguments.
For agents
soma initcreatesapp.cell(the name every doc uses — it used to write
main.cell), a starter that passes check/verify/test, and anAGENTS.md.
The stdlib is embedded in the binary: a fresh project no longer warns
unknown property 'persistent'.soma docs agent|reference|gotchas|builtins|all— embedded, offline.soma example <terms…>searches the verified corpus;soma example <id>
prints a program's source.- soma-lang.dev is generated by
tools/build_site.py:llms-full.txt,
builtins.json,gotchas.json,corpus/index.json(316 programs, each
re-verified at build time),agent.md, real 404s, open CORS.
Examples
rebalancer:POST /approvereached theapprove()builtin, not the
handler — the human approval gate was unreachable throughrequest.
examples/atlas: same shadowing inverdict.examples/padovan.cell
checked against wrong expected values.
MIT license added.
Install
curl -fsSL https://soma-lang.dev/install.sh | sh
Pre-built binary attached for macOS arm64 (soma-aarch64-apple-darwin, self-contained: the stdlib is embedded). Other platforms build from source through the installer.
v2.1.0 — Native pipes + parallel: 275x faster
Native pipes
Pipes in [native] handlers compile to Rust iterator chains:
on simulate(n: Int) [native] {
return range(0, n)
|> map(i => compute_hit(i))
|> reduce(0.0, p => p.acc + p.val)
/ n * 4.0
}
Parallel via soma.toml
[compute]
backend = "threads"
threads = 8
[compute.parallel]
handlers = ["simulate"]Benchmarks: 50M Monte Carlo paths
| Mode | Time | vs interpreted |
|---|---|---|
| Interpreted | ~8,000ms | 1x |
| [native] | 177ms | 45x |
| [native] + parallel | 29ms | 275x |
Same code. Different config. Four axes of the property system:
- Storage:
[persistent]→ SQLite - Transport:
signal/on→ TCP bus - Verification:
state {}→ model checker - Compute:
[native]→ LLVM + threads
v2.0.0 — [native] compilation: 200x speedup
[native] — Compute as a property
Add [native] to any handler. It compiles to machine code via LLVM.
on simulate(n: Int) [native] {
let total = 0.0
let i = 0
while i < n {
let x = random()
if x * x <= 1.0 { total = total + 1.0 }
i = i + 1
}
return 4.0 * total / n
}
Performance
| Paths | Interpreted | [native] | Speedup |
|---|---|---|---|
| 1M | 801ms | 3ms | 267x |
| 10M | ~8000ms | 33ms | 242x |
How it works
- Soma validates the numeric subset at compile time
- Generates Rust source code
- Compiles with
rustc -O(LLVM backend) - Loads the .dylib via FFI
- Cached by hash — first run ~2s, after that 0ms
The property pattern
[persistent] on memory → runtime resolves SQLite
[native] on handler → compiler resolves LLVM
Same philosophy. Declare intent. The toolchain resolves.
Allowed in [native]
Int, Float, Bool, arithmetic, comparisons, if/else, while, for, break, continue, math builtins (sqrt, log, exp, pow, sin, cos), random(), calls to other [native] handlers.
Not allowed
String, Map, List, pipes, storage, HTTP, signals — use interpreted handlers for orchestration, [native] for computation.
v1.2.0 — Sobol Monte Carlo, write_csv, CONTRIBUTING
Sobol Monte Carlo Option Pricing
New example: examples/sobol_monte_carlo.cell
European call option pricing comparing Sobol quasi-random sequences vs pseudo-random Monte Carlo.
Black-Scholes: 8.021
Pseudo-random Sobol
Paths 100: error 1.73 error 0.73 ← 2.4x more precise
Paths 5000: error 0.21 error 0.04 ← 5.8x more precise
Implements Van der Corput sequence, inverse normal CDF (Beasley-Springer-Moro), Black-Scholes analytical, and Monte Carlo — all in pure Soma.
Also new
write_csv(path, list_of_maps)— CSV exportavg_bynow returns Float (was truncating to Int)CONTRIBUTING.md— how to add Rust builtins with templates
v1.1.0 — Column-wise pipes and DataFrame ops
Column-wise statistics
percentile(stocks, "score", 0.9) // value at 90th percentile
median(stocks, "score") // median
std_by(stocks, "score") // standard deviation
Column transforms
stocks |> zscore("momentum") // adds momentum_z column
stocks |> rank("score") // adds score_rank column
stocks |> normalize("score", 0, 100) // adds score_norm column
stocks |> winsorize("mom", 0.05, 0.95) // clamp at percentile bounds
DataFrame ops
stocks |> select("ticker", "score") // project fields
stocks |> rename("score", "alpha") // rename field
Also new
nth(list, index)— list index accessread_file,write_file,read_csv— file I/Oreduce(list, init, lambda)— foldlog,exp,log10— mathdate_now(),format_date()— datessort(list)— plain list sortingInt / Int→ Float when non-exact (like Python 3)
A 25-line winsorization becomes one pipe:
stocks |> winsorize("momentum", 0.05, 0.95) |> zscore("momentum") |> rank("composite")