Wildcard failure — * -> failed with an eventually property
A job that can fail from any working state is the first thing people write, and the first thing that traps them: `* -> failed` also leaves the terminal states (a `done` job could "fail"), and `eventually = ["done", "failed"]` only holds if no cycle can dodge both. The recipe: - `except [done]` keeps the terminal state final; - the retry loop `running -> queued` is bounded by data, not by the graph, so `verify` proves deadlock-freedom and liveness on the graph and the `eventually` property on the declared machine; - each handler declares the edge it takes (`transition(id, from, to)`), so `verify` shows `start ⟶ {queued → running}` instead of a bare target. Run: soma verify wildcard_failure.cell (soma.toml carries the property)
A Soma program from the state_machines part of the verified corpus: 68 lines, cells Job, JobTests. It passes soma check with soma 3.2.4.
How it is built
The cell Job keeps 1 memory slot: attempts (Map<String, Int>, persistent) under the invariant attempts >= 0 && attempts <= 3 and status != "done" || (attempts ?? 0) <= 3. Its state machine job starts in queued and allows 4 transitions: queued -> running, running -> done, running -> queued (guarded) and * -> failed. done and failed are terminal. Handlers: start (line 30), finish (line 34), retry (line 38), abort (line 46) and read (line 50).
The file also holds 1 test cell (JobTests) with 12 assertions, run by soma test.
The source
wildcard_failure.cell
// WILDCARD FAILURE — `* -> failed` with an `eventually` property.
//
// A job that can fail from any working state is the first thing people
// write, and the first thing that traps them: `* -> failed` also leaves the
// terminal states (a `done` job could "fail"), and `eventually = ["done",
// "failed"]` only holds if no cycle can dodge both. The recipe:
// - `except [done]` keeps the terminal state final;
// - the retry loop `running -> queued` is bounded by data, not by the
// graph, so `verify` proves deadlock-freedom and liveness on the graph
// and the `eventually` property on the declared machine;
// - each handler declares the edge it takes (`transition(id, from, to)`),
// so `verify` shows `start ⟶ {queued → running}` instead of a bare target.
//
// Run: soma verify wildcard_failure.cell (soma.toml carries the property)
cell Job {
memory {
attempts: Map<String, Int> [persistent]
invariant attempts >= 0 && attempts <= 3
// a failed or done job never keeps a live attempt counter above 3
invariant status != "done" || (attempts ?? 0) <= 3
}
state job {
initial: queued
queued -> running
running -> done
running -> queued { guard { tries < 3 } }
* -> failed except [done]
}
on start(id: String) {
transition(id, "queued", "running")
return get_status(id)
}
on finish(id: String) {
transition(id, "running", "done")
return get_status(id)
}
on retry(id: String) {
let tries = (attempts.get(id) ?? 0) + 1
require tries <= 3 else TooManyRetries
attempts.set(id, tries)
require tries < 3 else LastAttempt
transition(id, "running", "queued")
return get_status(id)
}
on abort(id: String) {
transition(id, "failed")
return get_status(id)
}
on read(id: String) { return [get_status(id), attempts.get(id) ?? 0] }
}
cell test JobTests {
rules {
assert Job.start("a") == "running"
assert Job.retry("a") == "queued"
assert Job.start("a") == "running"
assert Job.retry("a") == "queued"
assert Job.start("a") == "running"
assert_fails Job.retry("a") matching "LastAttempt"
assert Job.read("a") == ["running", 2]
assert Job.finish("a") == "done"
assert_fails Job.abort("a") matching "invalid_transition"
assert Job.start("b") == "running"
assert Job.abort("b") == "failed"
assert_fails Job.start("b") matching "invalid_transition"
}
}What the toolchain says
$ soma check wildcard_failure.cell
✓ All checks passed.$ soma test wildcard_failure.cell
test JobTests ...
✓ assert Job.start("a") == "running"
✓ assert Job.retry("a") == "queued"
✓ assert Job.start("a") == "running"
✓ assert Job.retry("a") == "queued"
✓ assert Job.start("a") == "running"
✓ assert_fails Job.retry("a") matching "LastAttempt" — raised require failed: LastAttempt: constraint violated
✓ assert Job.read("a") == ["running", 2]
✓ assert Job.finish("a") == "done"
✓ assert_fails Job.abort("a") matching "invalid_transition" — raised invalid transition: done → failed. Current state: 'done'. Valid targets: []
✓ assert Job.start("b") == "running"
✓ assert Job.abort("b") == "failed"
✓ assert_fails Job.start("b") matching "invalid_transition" — raised invalid transition: failed → running — transition(id, "queued", "running") declares its source, and 'b' is in 'failed', not 'queued'
12 tests: 12 passed, 0 failed$ soma verify wildcard_failure.cell
Verifying wildcard_failure.cell...
State machine 'job': 4 states, initial 'queued'
States: [done, failed, queued, running]
✓ 4 states, 5 transitions
✓ all states reachable from 'queued'
✓ terminal states: [done, failed]
✓ 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): running -> queued
✓ wildcard transitions: * -> [failed]
✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 4 literal transitions, 0 dynamic)
✓ termination: all 5 handlers structurally terminate
✓ refinement: handler `start` ⟶ {queued → running}
✓ refinement: handler `finish` ⟶ {running → done}
✓ refinement: handler `retry` ⟶ {running → queued}
✓ refinement: handler `abort` ⟶ {failed}
· transition sources: `abort` 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)
✓ guard `tries < 3` on running -> queued: proven — every caller narrows it with require before transition() (`retry`)
Job/invariants:
· invariant status != "done" || (attempts ?? 0) <= 3 — reads `status`: checked at run time on every write to attempts and on every transition() of the written key (a rule between lifecycle and data is not proven by induction)
✓ invariant attempts >= 0 && attempts <= 3 — writer 'retry' proven by induction (writes tries)
14 passed, 0 warnings, 0 failures
Temporal properties for 'job':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK