Multi-step expense-approval workflow with guarded transitions
A submitted expense needs manager sign-off; anything over a threshold also needs finance. Rejection at either gate sends it back to draft. Guards on the state machine encode the business rule: the manager_ok -> finance_review arrow is only taken for large amounts.
A Soma program from the state_machines part of the verified corpus: 81 lines, cells ExpenseApproval, ExpenseTests. It passes soma check with soma 3.2.4.
How it is built
The cell ExpenseApproval declares 6 signals in its face: submit(id: String, amount: Int) -> Map, manager_sign(id: String) -> String, finance_sign(id: String) -> String, reject(id: String) -> String, pay_out(id: String) -> String and status(id: String) -> String; keeps 1 memory slot: amounts (Map<String, Int>, persistent and consistent) under the invariant amounts >= 0. Its state machine claim starts in draft and allows 7 transitions: draft -> pending_manager, pending_manager -> pending_finance, pending_manager -> approved, pending_finance -> approved, pending_manager -> draft, pending_finance -> draft and approved -> paid. paid is terminal. Handlers: submit (line 33), manager_sign (line 40), finance_sign (line 51), reject (line 52), pay_out (line 53) and status (line 54).
The file also holds 1 test cell (ExpenseTests) with 12 assertions, run by soma test.
The source
expense_approval.cell
// Multi-step expense-approval workflow with guarded transitions.
// A submitted expense needs manager sign-off; anything over a threshold
// also needs finance. Rejection at either gate sends it back to draft.
// Guards on the state machine encode the business rule: the manager_ok ->
// finance_review arrow is only taken for large amounts.
cell ExpenseApproval {
face {
signal submit(id: String, amount: Int) -> Map
signal manager_sign(id: String) -> String
signal finance_sign(id: String) -> String
signal reject(id: String) -> String
signal pay_out(id: String) -> String
signal status(id: String) -> String
}
memory {
amounts: Map<String, Int> [persistent, consistent]
invariant amounts >= 0
}
state claim {
initial: draft
draft -> pending_manager
pending_manager -> pending_finance
pending_manager -> approved
pending_finance -> approved
pending_manager -> draft
pending_finance -> draft
approved -> paid
}
on submit(id: String, amount: Int) {
require amount > 0 else bad_amount
amounts.set(id, amount)
transition(id, "pending_manager")
return map("state", get_status(id), "amount", amount)
}
on manager_sign(id: String) {
let amt = amounts.get(id) ?? 0
// large claims escalate to finance; small ones are approved outright
if amt > 1000 {
transition(id, "pending_finance")
} else {
transition(id, "approved")
}
return get_status(id)
}
on finance_sign(id: String) { transition(id, "approved") return get_status(id) }
on reject(id: String) { transition(id, "draft") return get_status(id) }
on pay_out(id: String) { transition(id, "paid") return get_status(id) }
on status(id: String) { return get_status(id) }
}
cell test ExpenseTests {
rules {
// small claim: manager approves outright, then paid
assert submit("e1", 200).state == "pending_manager"
assert manager_sign("e1") == "approved"
assert pay_out("e1") == "paid"
// large claim: escalates to finance before approval
assert submit("e2", 5000).state == "pending_manager"
assert manager_sign("e2") == "pending_finance"
assert finance_sign("e2") == "approved"
assert pay_out("e2") == "paid"
// rejection bounces back to draft, then can be resubmitted
assert submit("e3", 300).state == "pending_manager"
assert reject("e3") == "draft"
assert submit("e3", 300).state == "pending_manager"
// a zero/negative amount is refused before any state change
assert_fails submit("e4", 0)
// illegal: cannot pay an expense that isn't approved yet
assert_fails pay_out("e5")
}
}What the toolchain says
$ soma check expense_approval.cell
✓ All checks passed.$ soma test expense_approval.cell
test ExpenseTests ...
✓ assert submit("e1", 200).state == "pending_manager"
✓ assert manager_sign("e1") == "approved"
✓ assert pay_out("e1") == "paid"
✓ assert submit("e2", 5000).state == "pending_manager"
✓ assert manager_sign("e2") == "pending_finance"
✓ assert finance_sign("e2") == "approved"
✓ assert pay_out("e2") == "paid"
✓ assert submit("e3", 300).state == "pending_manager"
✓ assert reject("e3") == "draft"
✓ assert submit("e3", 300).state == "pending_manager"
✓ assert_fails submit("e4", 0) — raised require failed: bad_amount: constraint violated
✓ assert_fails pay_out("e5") — raised invalid transition: draft → paid. Current state: 'draft'. Valid targets: [pending_manager]
12 tests: 12 passed, 0 failed$ soma verify expense_approval.cell
Verifying expense_approval.cell...
State machine 'claim': 5 states, initial 'draft'
States: [approved, draft, paid, pending_finance, pending_manager]
✓ 5 states, 7 transitions
✓ all states reachable from 'draft'
✓ terminal states: [paid]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (5 handlers, 6 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
✓ refinement: handler `submit` ⟶ {pending_manager}
✓ refinement: handler `manager_sign` ⟶ {pending_finance [if amt > 1000], approved [if not (amt > 1000)]}
✓ refinement: handler `finance_sign` ⟶ {approved}
✓ refinement: handler `reject` ⟶ {draft}
✓ refinement: handler `pay_out` ⟶ {paid}
· transition sources: `submit`, `manager_sign`, `finance_sign`, `reject`, `pay_out` call 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)
ExpenseApproval/invariants:
✓ invariant amounts >= 0 — writer 'submit' proven by induction (writes amount)
13 passed, 0 warnings, 0 failures
Temporal properties for 'claim':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK