soma.cell

Kill switch — a dead flag stays dead

On August 1, 2012, Knight Capital repurposed an old feature flag — "Power Peg", dead code from 2003 — for a new router. One of eight servers still ran the old code. When the recycled flag flipped on, the zombie code woke up and bought $7 billion of stock in 45 minutes. Knight lost $440M and the company. The root cause was not the bug; it was that a KILLED flag could come back to life. Here `killed` is a TERMINAL state — `soma verify` proves no path out. Re-enabling a killed feature means minting a NEW flag through a new review, never resurrecting the old one. The rollout percentage rides a memory invariant so no handler can write an out-of-range exposure.

A Soma program from the devops part of the verified corpus: 105 lines, cells FeatureFlags, KillSwitchTests. It passes soma check with soma 3.2.4.

How it is built

The cell FeatureFlags declares 6 signals in its face: launch(flag: String) -> Map, pause(flag: String) -> Map, resume(flag: String) -> Map, kill(flag: String) -> Map, set_rollout(flag: String, pct: Int) -> Map and flag_state(flag: String) -> String; keeps 1 memory slot: rollout (Map<String, Int>, persistent and consistent) under the invariant rollout >= 0 && rollout <= 100. Its state machine flag starts in draft and allows 5 transitions: draft -> live, live -> paused, paused -> live, live -> killed and paused -> killed. killed is terminal. Handlers: launch (line 43), pause (line 50), resume (line 56), kill (line 62), set_rollout (line 69) and flag_state (line 78).

The file also holds 1 test cell (KillSwitchTests) with 11 assertions, run by soma test.

Generated from soma describe on this file.

The source

feature_flag_kill_switch.cell

// ============================================================================
// KILL SWITCH — a dead flag stays dead
// ============================================================================
//
// On August 1, 2012, Knight Capital repurposed an old feature flag —
// "Power Peg", dead code from 2003 — for a new router. One of eight
// servers still ran the old code. When the recycled flag flipped on,
// the zombie code woke up and bought $7 billion of stock in 45 minutes.
// Knight lost $440M and the company. The root cause was not the bug;
// it was that a KILLED flag could come back to life.
//
// Here `killed` is a TERMINAL state — `soma verify` proves no path out.
// Re-enabling a killed feature means minting a NEW flag through a new
// review, never resurrecting the old one. The rollout percentage rides
// a memory invariant so no handler can write an out-of-range exposure.
// ============================================================================

cell FeatureFlags {
    face {
        signal launch(flag: String) -> Map
        signal pause(flag: String) -> Map
        signal resume(flag: String) -> Map
        signal kill(flag: String) -> Map
        signal set_rollout(flag: String, pct: Int) -> Map
        signal flag_state(flag: String) -> String
    }

    memory {
        rollout: Map<String, Int> [persistent, consistent]
        invariant rollout >= 0 && rollout <= 100
    }

    // `killed` has no outgoing edge. Power Peg stays in its grave.
    state flag {
        initial: draft
        draft -> live
        live -> paused
        paused -> live
        live -> killed
        paused -> killed
    }

    on launch(flag: String) {
        let r = try { transition(flag, "live") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        rollout.set(flag, 1)
        return map("ok", true, "state", get_status(flag))
    }

    on pause(flag: String) {
        let r = try { transition(flag, "paused") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", get_status(flag))
    }

    on resume(flag: String) {
        let r = try { transition(flag, "live") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", get_status(flag))
    }

    on kill(flag: String) {
        let r = try { transition(flag, "killed") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        rollout.set(flag, 0)
        return map("ok", true, "state", "killed")
    }

    on set_rollout(flag: String, pct: Int) {
        if flag_state(flag) != "live" {
            return map("ok", false, "reason", "flag is not live")
        }
        let w = try { rollout.set(flag, pct) }
        if w.error != () { return map("ok", false, "reason", "{w.error}") }
        return map("ok", true, "pct", pct)
    }

    on flag_state(flag: String) {
        return get_status(flag)
    }
}

cell test KillSwitchTests {
    rules {
        // normal life: launch, widen, pause, resume
        assert launch("router-v2").ok == true
        assert set_rollout("router-v2", 50).ok == true
        assert pause("router-v2").ok == true
        assert resume("router-v2").ok == true

        // the kill switch fires
        assert kill("router-v2").ok == true

        // THE KNIGHT CAPITAL MOVE: resurrect the dead flag. No edge exists.
        assert_fails transition("router-v2", "live")
        assert_fails transition("router-v2", "paused")
        assert_fails transition("router-v2", "draft")

        // exposure can never leave [0, 100] — memory refuses, not an if
        assert launch("checkout-v3").ok == true
        assert_fails rollout.set("checkout-v3", 150)
        assert_fails rollout.set("checkout-v3", -1)
    }
}

What the toolchain says

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

$ soma check feature_flag_kill_switch.cell
✓ All checks passed.
$ soma test feature_flag_kill_switch.cell
test KillSwitchTests ...
  ✓ assert launch("router-v2").ok == true
  ✓ assert set_rollout("router-v2", 50).ok == true
  ✓ assert pause("router-v2").ok == true
  ✓ assert resume("router-v2").ok == true
  ✓ assert kill("router-v2").ok == true
  ✓ assert_fails transition("router-v2", "live") — raised invalid transition: killed → live. Current state: 'killed'. Valid targets: []
  ✓ assert_fails transition("router-v2", "paused") — raised invalid transition: killed → paused. Current state: 'killed'. Valid targets: []
  ✓ assert_fails transition("router-v2", "draft") — raised invalid transition: killed → draft. Current state: 'killed'. Valid targets: []
  ✓ assert launch("checkout-v3").ok == true
  ✓ assert_fails rollout.set("checkout-v3", 150) — raised memory invariant violated on 'rollout': rollout >= 0 && rollout <= 100 — rejected write of 150 (key "checkout-v3"); the slot is unchanged
  ✓ assert_fails rollout.set("checkout-v3", -1) — raised memory invariant violated on 'rollout': rollout >= 0 && rollout <= 100 — rejected write of -1 (key "checkout-v3"); the slot is unchanged

11 tests: 11 passed, 0 failed
$ soma verify feature_flag_kill_switch.cell
Verifying feature_flag_kill_switch.cell...

State machine 'flag': 4 states, initial 'draft'
  States: [draft, killed, live, paused]

  ✓ 4 states, 5 transitions
  ✓ all states reachable from 'draft'
  ✓ terminal states: [killed]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 4 literal transitions, 0 dynamic)
  ✓ termination: all 6 handlers structurally terminate
  ✓ refinement: handler `launch` ⟶ {live}
  ✓ refinement: handler `pause` ⟶ {paused}
  ✓ refinement: handler `resume` ⟶ {live}
  ✓ refinement: handler `kill` ⟶ {killed}
  · transition sources: `launch`, `pause`, `resume`, `kill` 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)

FeatureFlags/invariants:

  ✓ invariant rollout >= 0 && rollout <= 100 — writer 'kill' proven (writes 0)
  ✓ invariant rollout >= 0 && rollout <= 100 — writer 'launch' proven (writes 1)
  ⚠ invariant rollout >= 0 && rollout <= 100 — runtime-checked (computed values): set_rollout → rollout because `pct` is a parameter (narrow it: `require pct >= 0 && pct <= 100 else …`)

13 passed, 1 warnings, 0 failures

  Temporal properties for 'flag':
  ✓ 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/feature_flag_kill_switch.cell · examples/corpus/devops/feature_flag_kill_switch.cell