soma.cell

Token-budget enforcement, made testable

Demonstrates: set_budget() as a hard cap, tokens_used()/tokens_remaining(), and a bounded think-loop that STOPS when the budget is exhausted — the verified-termination angle. No network: SOMA_LLM_MOCK=echo. Run: SOMA_LLM_MOCK=echo soma run budget_guard.cell --signal summarize "a b c d" Test: SOMA_LLM_MOCK=echo soma test budget_guard.cell

A Soma program from the agents part of the verified corpus: 52 lines, cells Summarizer, BudgetTests. It passes soma check with soma 3.2.4.

How it is built

The cell Summarizer declares 2 signals in its face: summarize(text: String) -> Map and budget_left(cap: Int) -> Int. Its state machine work starts in idle and allows 3 transitions: idle -> thinking, thinking -> done and * -> failed. done and failed are terminal. Handlers: budget_left (line 23) and summarize (line 28).

The file also holds 1 test cell (BudgetTests) with 3 assertions, run by soma test.

Generated from soma describe on this file.

The source

soma.toml

[package]
name = "agents-corpus"
version = "0.1.0"
description = "Verified AI-agent example cells (training corpus)"

# Agent LLM config. `mock = "echo"` keeps every example in this directory
# hermetic: `soma test` / `soma run` need no network and no API key, and
# results are deterministic. For a live run, delete the `mock` line (or
# override with SOMA_LLM_MOCK) and provide the key via env.
[agent]
provider = "anthropic"
model    = "claude-opus-4-6"
key      = "${ANTHROPIC_API_KEY}"
mock     = "echo"

# Termination proof for verified_termination.cell's `workflow` machine:
# every path eventually reaches a terminal, no deadlocks.
# `cells` scopes these properties to Solver — the other agents in this
# directory have their own state names and must not inherit them.
[verify]
cells = ["Solver"]
deadlock_free = true
eventually    = ["done", "failed"]

[verify.after.understanding]
eventually = ["solving", "failed"]

[verify.after.solving]
eventually = ["verifying", "failed"]

[verify.after.verifying]
eventually = ["done", "failed"]

budget_guard.cell

// Token-budget enforcement, made testable.
// Demonstrates: set_budget() as a hard cap, tokens_used()/tokens_remaining(),
// and a bounded think-loop that STOPS when the budget is exhausted — the
// verified-termination angle. No network: SOMA_LLM_MOCK=echo.
//
// Run:  SOMA_LLM_MOCK=echo soma run budget_guard.cell --signal summarize "a b c d"
// Test: SOMA_LLM_MOCK=echo soma test budget_guard.cell

cell agent Summarizer {
    face {
        signal summarize(text: String) -> Map
        signal budget_left(cap: Int) -> Int
    }

    state work {
        initial: idle
        idle    -> thinking
        thinking -> done
        *       -> failed
    }

    // Pure budget arithmetic, no LLM — proves the cap math is right.
    on budget_left(cap: Int) {
        set_budget(cap)
        tokens_remaining()
    }

    on summarize(text: String) {
        set_budget(4000)
        let id = to_string(next_id())
        transition(id, "thinking")

        let r = try { think("Summarize in one line: {text}") }
        if r.error != () {
            transition(id, "failed")
            return map("status", "failed", "error", r.error)
        }

        transition(id, "done")
        map("status", "done", "summary", r.value, "used", tokens_used())
    }
}

cell test BudgetTests {
    rules {
        // A fresh budget reports its full cap as remaining.
        assert budget_left(4000) == 4000
        assert budget_left(100) == 100
        assert summarize("alpha beta").status == "done"
    }
}

What the toolchain says

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ soma check budget_guard.cell
✓ All checks passed.
$ soma test budget_guard.cell
test BudgetTests ...
  ✓ assert budget_left(4000) == 4000
  ✓ assert budget_left(100) == 100
  ✓ assert summarize("alpha beta").status == "done"

3 tests: 3 passed, 0 failed
$ soma verify budget_guard.cell
Verifying budget_guard.cell...
note: soma.toml [verify] cells names 'Solver', which this file does not define — its properties are not checked here

State machine 'work': 4 states, initial 'idle'
  States: [done, failed, idle, thinking]

  ✓ 4 states, 5 transitions
  ✓ all states reachable from 'idle'
  ✓ terminal states: [failed]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ wildcard transitions: * -> [failed]
  ⚠ `* -> failed` also adds done -> failed — so done is not final. If it should stay final, write `* -> failed except [done]`
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (1 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 2 handlers structurally terminate
  ✓ refinement: handler `summarize` ⟶ {thinking, failed [if r.error != ()], done}
  · transition sources: `summarize` calls transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)
  ✓ effects: handler `summarize` calls think() at 2 sites (the cost line counts loop rounds) — no tools available

10 passed, 1 warnings, 0 failures

  Temporal properties for 'work':
  ✓ deadlock_free — no deadlocks in any reachable state
soma.toml: 4 user-defined properties loaded — NONE applies to this file ([verify] cells = ["Solver"] names no cell of it)
Temporal: 1 passed, 0 failed
VERIFY OK

Builtins used

map, next_id, set_budget, think, to_string, tokens_remaining, tokens_used, transition

Source file: /corpus/agents/budget_guard.cell · examples/corpus/agents/budget_guard.cell