Soma

One Rule, One Attempt To Break It

A quota of 100 units per user. The rule is written once, next to the data; the handler states its own business preconditions.

cell Quota {
    memory {
        used: Map<String, Int> [persistent]
        invariant used >= 0 && used <= 100
    }
    on consume(user: String, n: Int) {
        require n > 0 else BadAmount
        let before = used.get(user) ?? 0
        require before + n <= 100 else QuotaExceeded
        used.set(user, before + n)
        return 100 - (before + n)
    }
}

What the verifier says, and what the program then does (real output of the 2.6 toolchain):

$ soma verify quota.cell
  ✓ invariant used >= 0 && used <= 100 — writer 'consume' proven by induction (writes before + n)
VERIFY OK

$ soma run quota.cell consume ana 60      →  40
$ soma run quota.cell consume ana 60      →  error: require failed: QuotaExceeded
$ soma run quota.cell consume ana -5      →  error: require failed: BadAmount
$ soma run quota.cell consume ana 40      →  0

Delete the QuotaExceeded line and the verdict changes: the bound is no longer proven, it is checked at runtime — and the write that would exceed it is refused, leaving the slot unchanged (soma verify --strict turns that ⚠ into a failure):

  ⚠ invariant used >= 0 && used <= 100 — runtime-checked (computed values): consume → used [used <= 100]
    because `before + n` is only known to lie in [1, ∞) — narrow it: `require (before + n) <= 100 else …`

$ soma run q2.cell consume ana 60  →  error: memory invariant violated on 'used': … rejected write of 120; the slot is unchanged

Language Shape

A Soma program is organized as cells. The same syntax is used for a small command-line program, an HTTP handler, an agent, or a larger composed system.

cell Store {
    face {
        signal put(key: String, value: String)
        signal get(key: String) -> String
    }

    memory {
        data: Map<String, String> [persistent, consistent]
    }

    state lifecycle {
        initial: empty
        empty -> ready
        ready -> ready
    }

    on put(key: String, value: String) {
        data.set(key, value)
        transition("store", "ready")
    }

    on get(key: String) {
        return data.get(key)
    }
}

Verification And Checking

Soma includes several static analyses. These are useful checks, not a proof of all runtime behavior.

[verify]
deadlock_free = true
eventually = ["settled", "cancelled"]
never = ["invalid"]

[verify.after.sent]
eventually = ["filled", "rejected"]

The repository also contains Coq/Rocq proof files under docs/rigor/coq. They mechanize selected results for the CTL depth bound, memory-budget cost lattice, isolation, abstraction, and runtime-fidelity models. They are evidence for those models, not a full formalization of the whole Rust implementation.

Implementation Status

Current release: Soma 2.8.10. Release validation: 681 Rust tests, 118 CLI checks, 321 corpus programs and 1,280 independent numeric comparisons passed.

Agents

cell agent enables agent-oriented declarations. Agents can use think(), set_budget(), tool declarations in face, and regular state machines.

cell agent Researcher {
    face {
        signal research(topic: String) -> Map
        tool search(q: String) -> String
    }

    state workflow {
        initial: idle
        idle -> researching
        researching -> done
        * -> failed
    }

    on search(q: String) {
        return "result: {q}"
    }

    on research(topic: String) {
        set_budget(1000)
        transition("task", "researching")
        let data = think("Research: {topic}")
        transition("task", "done")
        return map("summary", data)
    }
}

The verifier can check the lifecycle graph and literal transition targets. set_budget tracks token use for real LLM calls. None of this proves the LLM response is correct, safe, or useful.

Hordes

A [task] handler runs as steps: each think() commits the writes before it and waits for the model outside the handler lock, so many requests overlap their model calls. horde() runs such a handler once per input with a bounded pool:

on audit(docs: List) {
    return horde(Reviewer.review, docs, map("concurrency", 500,
        "budget_tokens", 2000000, "on_result", "_store", "on_done", "_summarize"))
}
on _store(v: Map) { verdicts.set(v.id, v) }   // verdicts: [persistent, immutable]

The queue is persisted and resumes after a restart; each result is recorded, and on_result called, with the task's last step — once, also across a kill -9. Every think() of the horde (nested hordes included) reserves its worst case against budget_tokens first, so the spend stays under the ceiling while the provider honors max_tokens. soma verify prints each horde's cost bound. Rounds (snapshot, apply in input order, seed, per-agent instance memory) make a population simulation reproducible. 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.

Runtime And Backends

Native Numeric Handlers

[native] is intended for narrow numeric hot paths. The generated Rust path uses checked fast integer code and a BigInt fallback for overflow-sensitive integer results.

cell Math {
    on sum(n: Int) [native] {
        let total = 0
        for i in range(0, n) {
            total = total + i
        }
        return total
    }
}

Performance depends on workload, machine, cache state, and whether the handler fits the native subset. Benchmark claims should be reproduced with the scripts under bench/ before being used for decisions.

Reproduce Basic Checks

After installing (no repository checkout needed), these commands exercise the core paths:

soma --version
soma init demo && cd demo
soma check app.cell && soma verify app.cell && soma test app.cell
soma run app.cell add 5
soma example invariant state_machine          # verified programs, by feature
soma example services/payments_approval > pay.cell && soma verify pay.cell
soma docs agent | head -40                    # the language, offline
soma serve app.cell -p 8080                   # then: curl -X POST localhost:8080/counter/5

The Coq proof files live in the repository (docs/rigor/coq, make check).

Important Limits

• Soma is experimental: one author, used for the demos in the repository and the author's own trading automata, not yet used in a system that other people depend on (/status has the full maturity table). Expect rough edges in syntax, tooling, installer behavior, and deployment integrations.
• What is proven, what is only checked at runtime, and what is out of scope: docs/guarantees.md. What soma serve exposes and how errors map to statuses: docs/serving.md. What happens when it goes wrong in production: docs/operations.md.
• State-machine verification is over the declared finite graph. It does not exhaustively model runtime data values, external systems, or LLM outputs.
• Strong consistency in scale is currently a checked declaration, not a Raft/Paxos-backed runtime guarantee.
• The current cluster replication path is signal-bus broadcast and should be treated as eventual replication.
• Native codegen supports a subset of handlers. The general interpreter remains the reference path.
• Memory-budget proofs depend on the static cost model and declared bounds such as capacities and loop bounds. Calls to unbounded builtins produce advisory output instead of a proof.
• Agent token budgeting bounds token use; it does not prove semantic correctness or safety of model output.
• A horde's budget_tokens ceiling assumes the provider honors max_tokens and counts settled calls: calls in flight at a crash are sent again after the restart. A [task] handler is atomic per step, not as a whole: steps before its last think() may run again after a crash.
• Cloud deployment commands generate scaffolding and invoke external provider CLIs. They do not remove the need for provider configuration, credentials, or review.

CLI Summary