soma.cell

Agent lifecycle typed against a sum type — typos become compile errors

Demonstrates: `cell type` variants typing a `state X: T { }` machine, transition() taking a VARIANT not a string, get_status() returning the variant name as a string, and an exhaustive match over the status. Run: SOMA_LLM_MOCK=echo soma run typed_lifecycle.cell --signal handle "refund" Test: SOMA_LLM_MOCK=echo soma test typed_lifecycle.cell

A Soma program from the agents part of the verified corpus: 57 lines, cells TaskStatus, Worker, WorkerTests. It passes soma check with soma 3.2.4.

How it is built

The cell Worker declares 2 signals in its face: handle(kind: String) -> Map and label(s: String) -> String. Its state machine task starts in Queued and allows 4 transitions: Queued -> Working, Working -> Reviewed, Reviewed -> Shipped and * -> Aborted. Aborted and Shipped are terminal. Handlers: label (line 28) and handle (line 39).

The file also holds 1 test cell (WorkerTests) with 4 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"]

typed_lifecycle.cell

// Agent lifecycle typed against a sum type — typos become compile errors.
// Demonstrates: `cell type` variants typing a `state X: T { }` machine,
// transition() taking a VARIANT not a string, get_status() returning the
// variant name as a string, and an exhaustive match over the status.
//
// Run:  SOMA_LLM_MOCK=echo soma run typed_lifecycle.cell --signal handle "refund"
// Test: SOMA_LLM_MOCK=echo soma test typed_lifecycle.cell

cell type TaskStatus {
    variants { Queued  Working  Reviewed  Shipped  Aborted }
}

cell agent Worker {
    face {
        signal handle(kind: String) -> Map
        signal label(s: String) -> String
    }

    state task: TaskStatus {
        initial: Queued
        Queued   -> Working
        Working  -> Reviewed
        Reviewed -> Shipped
        *        -> Aborted
    }

    // Exhaustive match over the sum type — drop an arm and check fails.
    on label(s: String) {
        match s {
            "Queued"   -> "waiting in queue"
            "Working"  -> "in progress"
            "Reviewed" -> "passed review"
            "Shipped"  -> "delivered"
            "Aborted"  -> "cancelled"
            _          -> "unknown"
        }
    }

    on handle(kind: String) {
        set_budget(1000)
        let id = to_string(next_id())
        transition(id, Working)
        transition(id, Reviewed)
        transition(id, Shipped)
        map("kind", kind, "state", get_status(id), "label", label(get_status(id)))
    }
}

cell test WorkerTests {
    rules {
        assert label("Working") == "in progress"
        assert label("Shipped") == "delivered"
        assert handle("refund").state == "Shipped"
        assert handle("refund").label == "delivered"
    }
}

What the toolchain says

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

$ soma check typed_lifecycle.cell
✓ All checks passed.
$ soma test typed_lifecycle.cell
test WorkerTests ...
  ✓ assert label("Working") == "in progress"
  ✓ assert label("Shipped") == "delivered"
  ✓ assert handle("refund").state == "Shipped"
  ✓ assert handle("refund").label == "delivered"

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

State machine 'task': 5 states, initial 'Queued'
  States: [Aborted, Queued, Reviewed, Shipped, Working]

  ✓ 5 states, 7 transitions
  ✓ all states reachable from 'Queued'
  ✓ terminal states: [Aborted]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ wildcard transitions: * -> [Aborted]
  ⚠ `* -> Aborted` also adds Shipped -> Aborted — so Shipped is not final. If it should stay final, write `* -> Aborted except [Shipped]`
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (1 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 2 handlers structurally terminate
  ⚠ refinement: declared transition `* → Aborted` is never reached by any handler — spec may be aspirational or stale
  ✓ refinement: handler `handle` ⟶ {Working, Working → Reviewed, Reviewed → Shipped}
  · transition sources: `handle` 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)

9 passed, 2 warnings, 0 failures

  Temporal properties for 'task':
  ✓ 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

get_status, map, next_id, set_budget, to_string, transition

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