soma.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.

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.

Generated from soma describe on this file.

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

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ 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

Builtins used

get_status, map, transition

Source file: /corpus/devops/incident_ladder.cell · examples/corpus/devops/incident_ladder.cell