Lesson 4 — A lifecycle the compiler checks

A lesson of the course on the Soma programming language. Every output on this page was printed by soma 3.2.4: the build writes each file to an empty folder and runs each command.

Most bugs in business software are a step taken out of order: paid before approved, shipped after cancelled. In Soma the lifecycle is a state machine next to the handlers, and the properties you care about go in soma.toml:

expense.cell

cell Expense {
    state flow {
        initial: submitted
        submitted -> approved
        submitted -> rejected
        approved -> paid
        submitted -> paid          // "small amounts skip approval"
    }
    on sign_off(id: String) { transition(id, "submitted", "approved") }
    on reject(id: String)   { transition(id, "submitted", "rejected") }
    on pay(id: String)      { transition(id, "paid") }
}

soma.toml

[verify]
eventually = ["paid", "rejected"]    # every expense ends one way or the other

[verify.before.paid]
requires = ["approved"]              # nothing is paid without approval

$ soma verify expense.cell
Verifying expense.cell...

State machine 'flow': 4 states, initial 'submitted'
  States: [approved, paid, rejected, submitted]

  ✓ 4 states, 4 transitions
  ✓ all states reachable from 'submitted'
  ✓ terminal states: [rejected, paid]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 3 handlers structurally terminate
  ✓ refinement: handler `sign_off` ⟶ {submitted → approved}
  ✓ refinement: handler `reject` ⟶ {submitted → rejected}
  ✓ refinement: handler `pay` ⟶ {paid}
  · transition sources: `pay` 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)

10 passed, 0 warnings, 0 failures

  Temporal properties for 'flow':
  ✓ deadlock_free — no deadlocks in any reachable state
  ✓ eventually(state in [paid, rejected]) — all paths eventually satisfy the predicate
  ✗ requires('paid' only after one of [approved]) — 'paid' is reachable without passing through any of [approved]
    counter-example: submitted → paid
soma.toml: 2 user-defined properties loaded
Temporal: 2 passed, 1 failed
VERIFY FAILED — 1 temporal property failed

The verifier found the shortcut and printed the path that breaks the rule. Remove the edge, and name the source state in pay so the proof sees where it starts:

expense.cell

cell Expense {
    state flow {
        initial: submitted
        submitted -> approved
        submitted -> rejected
        approved -> paid
    }
    on sign_off(id: String) { transition(id, "submitted", "approved") }
    on reject(id: String)   { transition(id, "submitted", "rejected") }
    on pay(id: String)      { transition(id, "approved", "paid") }
}

$ soma verify expense.cell
Verifying expense.cell...

State machine 'flow': 4 states, initial 'submitted'
  States: [approved, paid, rejected, submitted]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'submitted'
  ✓ terminal states: [rejected, paid]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 3 handlers structurally terminate
  ✓ refinement: handler `sign_off` ⟶ {submitted → approved}
  ✓ refinement: handler `reject` ⟶ {submitted → rejected}
  ✓ refinement: handler `pay` ⟶ {approved → paid}

10 passed, 0 warnings, 0 failures

  Temporal properties for 'flow':
  ✓ deadlock_free — no deadlocks in any reachable state
  ✓ eventually(state in [paid, rejected]) — all paths eventually satisfy the predicate
  ✓ requires('paid' only after one of [approved]) — every path to 'paid' passes through one of [approved]
soma.toml: 2 user-defined properties loaded
Temporal: 3 passed, 0 failed
VERIFY OK

$ soma run expense.cell reject e1
{"id": "e1", "from": "submitted", "to": "rejected"}

$ soma run expense.cell pay e1
error: invalid transition: rejected → paid — transition(id, "approved", "paid") declares its source, and 'e1' is in 'rejected', not 'approved'
  --> expense.cell:10:31
   |
10 |     on pay(id: String)      { transition(id, "approved", "paid") }
   |                               ^

At run time a transition the machine forbids is refused too, and the error says which state the instance is really in. Handlers are atomic: one that fails leaves no write and no transition behind.