Subscription billing state machine
trialing -> active -> past_due (on a failed charge) -> active (recovery) or -> canceled. Active subscriptions can be canceled directly. The past_due -> active retry loop is bounded by `canceled` being reachable from every state, so liveness holds. Memory tracks the failed-charge count so the handler can escalate to cancellation.
A Soma program from the state_machines part of the verified corpus: 93 lines, cells Billing, BillingTests. It passes soma check with soma 3.2.4.
How it is built
The cell Billing declares 6 signals in its face: start_trial(id: String) -> String, activate(id: String) -> String, charge_failed(id: String) -> Map, recover(id: String) -> String, cancel(id: String) -> String and status(id: String) -> String; keeps 1 memory slot: fails (Map<String, Int>, persistent and consistent) under the invariant fails >= 0. Its state machine sub starts in trialing and allows 6 transitions: trialing -> active, active -> past_due, past_due -> active, past_due -> canceled, active -> canceled and trialing -> canceled. canceled is terminal. Handlers: start_trial (line 34), activate (line 36), charge_failed (line 42), recover (line 57), cancel (line 63) and status (line 68).
The file also holds 1 test cell (BillingTests) with 11 assertions, run by soma test.
The source
subscription_billing.cell
// Subscription billing state machine.
// trialing -> active -> past_due (on a failed charge) -> active (recovery)
// or -> canceled. Active subscriptions can be canceled directly. The
// past_due -> active retry loop is bounded by `canceled` being reachable
// from every state, so liveness holds. Memory tracks the failed-charge
// count so the handler can escalate to cancellation.
cell Billing {
face {
signal start_trial(id: String) -> String
signal activate(id: String) -> String
signal charge_failed(id: String) -> Map
signal recover(id: String) -> String
signal cancel(id: String) -> String
signal status(id: String) -> String
promise "every subscription can reach canceled"
}
memory {
fails: Map<String, Int> [persistent, consistent]
invariant fails >= 0
}
state sub {
initial: trialing
trialing -> active
active -> past_due
past_due -> active
past_due -> canceled
active -> canceled
trialing -> canceled
}
on start_trial(id: String) { return get_status(id) }
on activate(id: String) {
transition(id, "active")
fails.set(id, 0)
return get_status(id)
}
on charge_failed(id: String) {
// only an active subscription can newly enter dunning; a repeat
// failure while already past_due keeps it there (self-loop avoided)
if get_status(id) == "active" {
transition(id, "past_due")
}
let n = (fails.get(id) ?? 0) + 1
fails.set(id, n)
// after 3 failed charges, auto-cancel
if n >= 3 {
transition(id, "canceled")
}
return map("state", get_status(id), "fails", n)
}
on recover(id: String) {
transition(id, "active")
fails.set(id, 0)
return get_status(id)
}
on cancel(id: String) {
transition(id, "canceled")
return get_status(id)
}
on status(id: String) { return get_status(id) }
}
cell test BillingTests {
rules {
// trial -> active -> fail -> recover
assert start_trial("s1") == "trialing"
assert activate("s1") == "active"
assert charge_failed("s1").state == "past_due"
assert recover("s1") == "active"
// three consecutive failures auto-cancels
assert activate("s2") == "active"
assert charge_failed("s2").fails == 1
assert charge_failed("s2").fails == 2
assert charge_failed("s2").state == "canceled"
// a trialing subscription can be canceled directly
assert cancel("s3") == "canceled"
// illegal: a canceled subscription is terminal — no resurrection
assert cancel("s4") == "canceled"
assert_fails recover("s4")
}
}What the toolchain says
$ soma check subscription_billing.cell
note: promise on 'Billing' is documentation (not machine-verifiable): "every subscription can reach canceled"
--> subscription_billing.cell:16:17
|
16 | promise "every subscription can reach canceled"
| ^
✓ All checks passed (1 note above).$ soma test subscription_billing.cell
test BillingTests ...
✓ assert start_trial("s1") == "trialing"
✓ assert activate("s1") == "active"
✓ assert charge_failed("s1").state == "past_due"
✓ assert recover("s1") == "active"
✓ assert activate("s2") == "active"
✓ assert charge_failed("s2").fails == 1
✓ assert charge_failed("s2").fails == 2
✓ assert charge_failed("s2").state == "canceled"
✓ assert cancel("s3") == "canceled"
✓ assert cancel("s4") == "canceled"
✓ assert_fails recover("s4") — raised invalid transition: canceled → active. Current state: 'canceled'. Valid targets: []
11 tests: 11 passed, 0 failed$ soma verify subscription_billing.cell
Verifying subscription_billing.cell...
State machine 'sub': 4 states, initial 'trialing'
States: [active, canceled, past_due, trialing]
✓ 4 states, 6 transitions
✓ all states reachable from 'trialing'
✓ terminal states: [canceled]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 5 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
✓ refinement: handler `activate` ⟶ {active}
✓ refinement: handler `charge_failed` ⟶ {active → past_due [if get_status(id) == "active"], canceled [if n >= 3]}
✓ refinement: handler `recover` ⟶ {active}
✓ refinement: handler `cancel` ⟶ {canceled}
· transition sources: `activate`, `charge_failed`, `recover`, `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)
Billing/invariants:
✓ invariant fails >= 0 — writer 'activate' proven (writes 0)
✓ invariant fails >= 0 — writer 'charge_failed' proven by induction (writes n)
✓ invariant fails >= 0 — writer 'recover' proven (writes 0)
14 passed, 0 warnings, 0 failures
Temporal properties for 'sub':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK