Incident ladder — severity only climbs, and closure needs a postmortem
Two ways incident processes rot. First, "sev gaming": an on-call quietly downgrades a Sev1 to Sev3 so the SLA clock stops and the VP page never fires — the 2013 Target breach unfolded exactly this way, with FireEye alerts dismissed for weeks while card data walked out. Second, closing without learning: the incident is marked resolved, no postmortem happens, and the same outage returns in six months. Both rots are unrepresentable here. Severity is a one-way ladder — there is no de-escalation edge, only mitigation. And `closed` is reachable ONLY through `postmortem_done`: the machine has no edge from mitigated to closed, so "we'll write it up later" cannot compile. `soma verify` proves closed is terminal and that every state can still reach it — no incident is ever stuck open forever.
A Soma program from the devops part of the verified corpus: 118 lines, cells IncidentDesk, LadderTests. It passes soma check with soma 3.2.4.
How it is built
The cell IncidentDesk declares 6 signals in its face: raise_sev3(inc: String) -> Map, escalate_sev(inc: String) -> Map, mitigate(inc: String) -> Map, file_postmortem(inc: String) -> Map, close_incident(inc: String) -> Map and incident_state(inc: String) -> String; keeps 1 memory slot: severity (Map<String, Int>, persistent and consistent) under the invariant severity >= 1 && severity <= 3. Its state machine incident starts in detected and allows 8 transitions: detected -> sev3, sev3 -> sev2, sev2 -> sev1, sev3 -> mitigated, sev2 -> mitigated, sev1 -> mitigated, mitigated -> postmortem_done and postmortem_done -> closed. closed is terminal. Handlers: raise_sev3 (line 51), escalate_sev (line 58), mitigate (line 70), file_postmortem (line 76), close_incident (line 82) and incident_state (line 88).
The file also holds 1 test cell (LadderTests) with 13 assertions, run by soma test.
The source
incident_ladder.cell
// ============================================================================
// INCIDENT LADDER — severity only climbs, and closure needs a postmortem
// ============================================================================
//
// Two ways incident processes rot. First, "sev gaming": an on-call
// quietly downgrades a Sev1 to Sev3 so the SLA clock stops and the VP
// page never fires — the 2013 Target breach unfolded exactly this way,
// with FireEye alerts dismissed for weeks while card data walked out.
// Second, closing without learning: the incident is marked resolved,
// no postmortem happens, and the same outage returns in six months.
//
// Both rots are unrepresentable here. Severity is a one-way ladder —
// there is no de-escalation edge, only mitigation. And `closed` is
// reachable ONLY through `postmortem_done`: the machine has no edge
// from mitigated to closed, so "we'll write it up later" cannot
// compile. `soma verify` proves closed is terminal and that every
// state can still reach it — no incident is ever stuck open forever.
// ============================================================================
cell IncidentDesk {
face {
signal raise_sev3(inc: String) -> Map
signal escalate_sev(inc: String) -> Map
signal mitigate(inc: String) -> Map
signal file_postmortem(inc: String) -> Map
signal close_incident(inc: String) -> Map
signal incident_state(inc: String) -> String
}
memory {
// 1, 2 or 3. There is no severity 0 ("not really an incident")
// and no severity 4 ("look how bad!") — the ledger refuses both.
severity: Map<String, Int> [persistent, consistent]
invariant severity >= 1 && severity <= 3
}
// No edge points DOWN the ladder, and `closed` only follows
// `postmortem_done`. Absence is the policy.
state incident {
initial: detected
detected -> sev3
sev3 -> sev2
sev2 -> sev1
sev3 -> mitigated
sev2 -> mitigated
sev1 -> mitigated
mitigated -> postmortem_done
postmortem_done -> closed
}
on raise_sev3(inc: String) {
let r = try { transition(inc, "sev3") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
severity.set(inc, 3)
return map("ok", true, "state", "sev3")
}
on escalate_sev(inc: String) {
let s = get_status(inc)
let next = "sev2"
if s == "sev2" { next = "sev1" }
let r = try { transition(inc, next) }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
let lvl = 2
if next == "sev1" { lvl = 1 }
severity.set(inc, lvl)
return map("ok", true, "state", next)
}
on mitigate(inc: String) {
let r = try { transition(inc, "mitigated") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "mitigated")
}
on file_postmortem(inc: String) {
let r = try { transition(inc, "postmortem_done") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "postmortem_done")
}
on close_incident(inc: String) {
let r = try { transition(inc, "closed") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "closed")
}
on incident_state(inc: String) {
return get_status(inc)
}
}
cell test LadderTests {
rules {
assert raise_sev3("inc-401").ok == true
assert escalate_sev("inc-401").state == "sev2"
assert escalate_sev("inc-401").state == "sev1"
// THE TARGET MOVE: quietly downgrade. No edge points down.
assert_fails transition("inc-401", "sev2")
assert_fails transition("inc-401", "sev3")
// closing without a postmortem cannot compile into a path
assert mitigate("inc-401").ok == true
assert_fails transition("inc-401", "closed")
assert file_postmortem("inc-401").ok == true
assert close_incident("inc-401").ok == true
// closed is terminal: history does not reopen for editing
assert_fails transition("inc-401", "mitigated")
assert_fails transition("inc-401", "sev1")
// the severity ledger admits only 1..3
assert_fails severity.set("inc-999", 0)
assert_fails severity.set("inc-999", 4)
}
}What the toolchain says
$ soma check incident_ladder.cell
✓ All checks passed.$ soma test incident_ladder.cell
test LadderTests ...
✓ assert raise_sev3("inc-401").ok == true
✓ assert escalate_sev("inc-401").state == "sev2"
✓ assert escalate_sev("inc-401").state == "sev1"
✓ assert_fails transition("inc-401", "sev2") — raised invalid transition: sev1 → sev2. Current state: 'sev1'. Valid targets: [mitigated]
✓ assert_fails transition("inc-401", "sev3") — raised invalid transition: sev1 → sev3. Current state: 'sev1'. Valid targets: [mitigated]
✓ assert mitigate("inc-401").ok == true
✓ assert_fails transition("inc-401", "closed") — raised invalid transition: mitigated → closed. Current state: 'mitigated'. Valid targets: [postmortem_done]
✓ assert file_postmortem("inc-401").ok == true
✓ assert close_incident("inc-401").ok == true
✓ assert_fails transition("inc-401", "mitigated") — raised invalid transition: closed → mitigated. Current state: 'closed'. Valid targets: []
✓ assert_fails transition("inc-401", "sev1") — raised invalid transition: closed → sev1. Current state: 'closed'. Valid targets: []
✓ assert_fails severity.set("inc-999", 0) — raised memory invariant violated on 'severity': severity >= 1 && severity <= 3 — rejected write of 0 (key "inc-999"); the slot is unchanged
✓ assert_fails severity.set("inc-999", 4) — raised memory invariant violated on 'severity': severity >= 1 && severity <= 3 — rejected write of 4 (key "inc-999"); the slot is unchanged
13 tests: 13 passed, 0 failed$ soma verify incident_ladder.cell
Verifying incident_ladder.cell...
State machine 'incident': 7 states, initial 'detected'
States: [closed, detected, mitigated, postmortem_done, sev1, sev2, sev3]
✓ 7 states, 8 transitions
✓ all states reachable from 'detected'
✓ terminal states: [closed]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
⚠ dynamic transition targets: handler `escalate_sev` uses a dynamic (computed) transition target — the state these handlers move to is computed at run time (from input or an LLM answer), so the machine's safety is checked at run time for them, not proven
✓ termination: all 6 handlers structurally terminate
⚠ refinement (partial — dynamic targets fall back to runtime check): handler `escalate_sev` calls transition() with a computed target — which edge it takes is checked at run time (invalid_transition), not proven; write the target as a literal state to have it verified
✓ refinement (partial — dynamic targets fall back to runtime check): handler `raise_sev3` ⟶ {sev3}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `escalate_sev` ⟶ <dynamic>
✓ refinement (partial — dynamic targets fall back to runtime check): handler `mitigate` ⟶ {mitigated}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `file_postmortem` ⟶ {postmortem_done}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `close_incident` ⟶ {closed}
· transition sources: `raise_sev3`, `mitigate`, `file_postmortem`, `close_incident` 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)
IncidentDesk/invariants:
✓ invariant severity >= 1 && severity <= 3 — writer 'escalate_sev' proven by induction (writes lvl)
✓ invariant severity >= 1 && severity <= 3 — writer 'raise_sev3' proven (writes 3)
13 passed, 2 warnings, 0 failures
Temporal properties for 'incident':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK