Multi-agent content pipeline with verified handoffs
Demonstrates: delegate() across agent cells, each agent owning its own lifecycle machine, and a coordinator whose pipeline state machine proves the chain always terminates. Deterministic tool stubs keep it testable. Run: SOMA_LLM_MOCK=echo soma run multi_agent_pipeline.cell --signal produce "soma" Test: SOMA_LLM_MOCK=echo soma test multi_agent_pipeline.cell
A Soma program from the agents part of the verified corpus: 70 lines, cells Outliner, Drafter, Editor, PipelineTests. It passes soma check with soma 3.2.4.
How it is built
The cell Outliner declares 1 signal in its face: outline(topic: String) -> Map. Its state machine w starts in idle and allows 3 transitions: idle -> active, active -> done and * -> failed. done and failed are terminal. Handlers: outline (line 12).
The cell Drafter declares 1 signal in its face: draft(topic: String, points: Int) -> Map. Its state machine w starts in idle and allows 3 transitions: idle -> active, active -> done and * -> failed. done and failed are terminal. Handlers: draft (line 24).
The cell Editor declares 1 signal in its face: produce(topic: String) -> Map; keeps 1 memory slot: articles (Map<String, Map>, persistent). Its state machine pipeline starts in idle and allows 4 transitions: idle -> outlining, outlining -> drafting, drafting -> done and * -> failed. done and failed are terminal. Handlers: produce (line 43).
The file also holds 1 test cell (PipelineTests) with 5 assertions, run by soma test.
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"]multi_agent_pipeline.cell
// Multi-agent content pipeline with verified handoffs.
// Demonstrates: delegate() across agent cells, each agent owning its own
// lifecycle machine, and a coordinator whose pipeline state machine proves
// the chain always terminates. Deterministic tool stubs keep it testable.
//
// Run: SOMA_LLM_MOCK=echo soma run multi_agent_pipeline.cell --signal produce "soma"
// Test: SOMA_LLM_MOCK=echo soma test multi_agent_pipeline.cell
cell agent Outliner {
face { signal outline(topic: String) -> Map }
state w { initial: idle idle -> active active -> done * -> failed }
on outline(topic: String) {
let id = to_string(next_id())
transition(id, "active")
let pts = list("intro to {topic}", "details", "conclusion")
transition(id, "done")
map("status", "done", "points", pts)
}
}
cell agent Drafter {
face { signal draft(topic: String, points: Int) -> Map }
state w { initial: idle idle -> active active -> done * -> failed }
on draft(topic: String, points: Int) {
let id = to_string(next_id())
transition(id, "active")
let words = points * 40
transition(id, "done")
map("status", "done", "topic", topic, "words", words)
}
}
cell agent Editor {
face { signal produce(topic: String) -> Map }
memory { articles: Map<String, Map> [persistent] }
state pipeline {
initial: idle
idle -> outlining
outlining -> drafting
drafting -> done
* -> failed
}
on produce(topic: String) {
let id = to_string(next_id())
transition(id, "outlining")
let o = delegate("Outliner", "outline", topic)
if o.status == "failed" { transition(id, "failed") return o }
transition(id, "drafting")
let d = delegate("Drafter", "draft", topic, len(o.points))
if d.status == "failed" { transition(id, "failed") return d }
transition(id, "done")
let result = map("topic", topic, "words", d.words, "status", "done")
articles.set(topic, result)
result
}
}
cell test PipelineTests {
rules {
assert outline("ai").status == "done"
assert len(outline("ai").points) == 3
assert draft("ai", 3).words == 120
assert produce("soma").status == "done"
assert produce("soma").words == 120
}
}What the toolchain says
$ soma check multi_agent_pipeline.cell
✓ All checks passed.$ soma test multi_agent_pipeline.cell
test PipelineTests ...
✓ assert outline("ai").status == "done"
✓ assert len(outline("ai").points) == 3
✓ assert draft("ai", 3).words == 120
✓ assert produce("soma").status == "done"
✓ assert produce("soma").words == 120
5 tests: 5 passed, 0 failed$ soma verify multi_agent_pipeline.cell
Verifying multi_agent_pipeline.cell...
note: soma.toml [verify] cells names 'Solver', which this file does not define — its properties are not checked here
State machine 'Outliner.w': 4 states, initial 'idle'
States: [active, done, failed, idle]
✓ 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, 2 literal transitions, 0 dynamic)
✓ termination: all 1 handlers structurally terminate
⚠ refinement: declared transition `* → failed` is never reached by any handler — spec may be aspirational or stale
✓ refinement: handler `outline` ⟶ {active, active → done}
· transition sources: `outline` 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)
State machine 'Drafter.w': 4 states, initial 'idle'
States: [active, done, failed, idle]
✓ 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, 2 literal transitions, 0 dynamic)
✓ termination: all 1 handlers structurally terminate
⚠ refinement: declared transition `* → failed` is never reached by any handler — spec may be aspirational or stale
✓ refinement: handler `draft` ⟶ {active, active → done}
· transition sources: `draft` 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)
State machine 'Editor.pipeline': 5 states, initial 'idle'
States: [done, drafting, failed, idle, outlining]
✓ 5 states, 7 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, 5 literal transitions, 0 dynamic)
✓ termination: all 1 handlers structurally terminate
✓ refinement: handler `produce` ⟶ {outlining, failed [if o.status == "failed"], drafting, failed [if d.status == "failed"], done}
· transition sources: `produce` 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)
27 passed, 5 warnings, 0 failures
note: cross-cell: `Editor.produce` transitions its own machine and acts on `Drafter`, `Outliner` — a rule BETWEEN the two cells' machines ("not while the subject is withdrawn") is not verified unless soma.toml states it (`[verify.before."Cell.state"] requires = ["Other.state"]`); enforce it with a `require` reading the other cell
Temporal properties for 'Outliner.w':
✓ deadlock_free — no deadlocks in any reachable state
Temporal properties for 'Drafter.w':
✓ deadlock_free — no deadlocks in any reachable state
Temporal properties for 'Editor.pipeline':
✓ 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: 3 passed, 0 failed
note: state machines are verified per cell. A value crosses a cell boundary by a face contract (`requires` / `ensures` on the signal); a rule between two cells' machines is proven when soma.toml states it — `[verify.before."Pay.paid"] requires = ["Approval.signed_off"]` explores the product of the machines.
VERIFY OK