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