The killer feature: an agent whose termination is PROVEN by soma verify

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"]

verified_termination.cell

// The killer feature: an agent whose termination is PROVEN by soma verify.
// The lifecycle has a single terminal set {done, failed} reachable from every
// state, a `* -> failed` catch-all, and the matching soma.toml below drives
// `soma verify` to prove deadlock-freedom and liveness (eventually done|failed).
//
// Check:  soma check verified_termination.cell
// Verify: soma verify verified_termination.cell   (uses the soma.toml beside it)
// Run:    SOMA_LLM_MOCK=echo soma run verified_termination.cell --signal solve "x"
// Test:   SOMA_LLM_MOCK=echo soma test verified_termination.cell

cell agent Solver {
    face {
        signal solve(task: String) -> Map
        promise "eventually reaches done or failed"
    }

    state workflow {
        initial: idle
        idle        -> understanding
        understanding -> solving
        solving     -> verifying
        verifying   -> done
        *           -> failed
    }

    on solve(task: String) {
        set_budget(4000)
        let id = to_string(next_id())

        transition(id, "understanding")
        let u = try { think("Restate the task precisely: {task}") }
        if u.error != () { transition(id, "failed")  return map("status", "failed", "error", u.error) }

        transition(id, "solving")
        let s = try { think("Solve it: {u.value}") }
        if s.error != () { transition(id, "failed")  return map("status", "failed", "error", s.error) }

        transition(id, "verifying")
        let v = try { think("Double-check the solution: {s.value}") }
        if v.error != () { transition(id, "failed")  return map("status", "failed", "error", v.error) }

        transition(id, "done")
        map("status", "done", "task", task, "tokens", tokens_used())
    }
}

cell test SolverTests {
    rules {
        assert solve("compute 2+2").status == "done"
    }
}