Soma 2.4.0 — 2026-09-18
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 / 2 is 3.5 everywhere. [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-idiv migrates old code.
-
soma check now rejects: a string literal dangling after return (return "a" "b" silently returned "a"), a memory invariant naming several slots (every write would have been rejected at runtime), a non-exhaustive match inside 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: delete bypassed size invariants; soma verify did 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: "tokens bound proven" was claimed for a think() 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 serve served /static/../soma.toml (API keys), the .cell sources and .soma_data. Static files are confined to static/.
-
[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 test ignored [agent] / [models] in soma.toml (so mock had no effect); soma replay blamed nondeterminism when the source had changed; soma run f.cell -7 rejected negative arguments.
For agents
-
soma init creates app.cell (the name every doc uses — it used to write main.cell), a starter that passes check/verify/test, and an AGENTS.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 /approve reached the approve() builtin, not the handler — the human approval gate was unreachable through request. examples/atlas: same shadowing in verdict. examples/padovan.cell checked against wrong expected values.
MIT license added.