Order lifecycle as a verified state machine: an order flows from new to filled or rejected, and a fill settles
Every state can reach a terminal (settled / rejected / cancelled). Pairs with order_lifecycle.toml so `soma verify` proves deadlock-freedom and eventual settlement.
A Soma program from the finance part of the verified corpus: 63 lines, cells OrderLifecycle, OrderLifecycleTests. It passes soma check with soma 3.2.4.
How it is built
The cell OrderLifecycle declares 5 signals in its face: place(id: String) -> String, fill(id: String) -> String, settle(id: String) -> String, reject(id: String) -> String and cancel(id: String) -> String. Its state machine order starts in new and allows 5 transitions: new -> working (guarded), working -> filled, working -> rejected, filled -> settled and * -> cancelled. cancelled, rejected and settled are terminal. Handlers: place (line 24), fill (line 29), settle (line 34), reject (line 39) and cancel (line 44).
The file also holds 1 test cell (OrderLifecycleTests) with 6 assertions, run by soma test.
The source
order_lifecycle.cell
// Order lifecycle as a verified state machine: an order flows from new to
// filled or rejected, and a fill settles. Every state can reach a terminal
// (settled / rejected / cancelled). Pairs with order_lifecycle.toml so
// `soma verify` proves deadlock-freedom and eventual settlement.
cell OrderLifecycle {
face {
signal place(id: String) -> String
signal fill(id: String) -> String
signal settle(id: String) -> String
signal reject(id: String) -> String
signal cancel(id: String) -> String
}
state order {
initial: new
new -> working { guard { true } }
working -> filled
working -> rejected
filled -> settled
* -> cancelled
}
on place(id: String) {
transition(id, "working")
return get_status(id)
}
on fill(id: String) {
transition(id, "filled")
return get_status(id)
}
on settle(id: String) {
transition(id, "settled")
return get_status(id)
}
on reject(id: String) {
transition(id, "rejected")
return get_status(id)
}
on cancel(id: String) {
transition(id, "cancelled")
return get_status(id)
}
}
cell test OrderLifecycleTests {
rules {
// happy path: new -> working -> filled -> settled
assert place("o1") == "working"
assert fill("o1") == "filled"
assert settle("o1") == "settled"
// reject path
assert place("o2") == "working"
assert reject("o2") == "rejected"
// cancel from any state
assert cancel("o3") == "cancelled"
}
}What the toolchain says
$ soma check order_lifecycle.cell
✓ All checks passed.$ soma test order_lifecycle.cell
test OrderLifecycleTests ...
✓ assert place("o1") == "working"
✓ assert fill("o1") == "filled"
✓ assert settle("o1") == "settled"
✓ assert place("o2") == "working"
✓ assert reject("o2") == "rejected"
✓ assert cancel("o3") == "cancelled"
6 tests: 6 passed, 0 failed$ soma verify order_lifecycle.cell
Verifying order_lifecycle.cell...
State machine 'order': 6 states, initial 'new'
States: [cancelled, filled, new, rejected, settled, working]
✓ 6 states, 9 transitions
✓ all states reachable from 'new'
✓ terminal states: [cancelled]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
· guarded edges kept in the model (liveness and `eventually` above assume they can pass): new -> working
✓ wildcard transitions: * -> [cancelled]
⚠ `* -> cancelled` also adds rejected -> cancelled, settled -> cancelled — so rejected, settled are not final. If they should stay final, write `* -> cancelled except [rejected, settled]`
✓ think-isolated: CTL safety properties hold regardless of LLM output (5 handlers, 5 literal transitions, 0 dynamic)
✓ termination: all 5 handlers structurally terminate
✓ refinement: handler `place` ⟶ {working}
✓ refinement: handler `fill` ⟶ {filled}
✓ refinement: handler `settle` ⟶ {settled}
✓ refinement: handler `reject` ⟶ {rejected}
✓ refinement: handler `cancel` ⟶ {cancelled}
· transition sources: `place`, `fill`, `settle`, `reject`, `cancel` 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)
✓ guard `true` on new -> working: trivially true
14 passed, 1 warnings, 0 failures
Temporal properties for 'order':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK