Deploy canary — the staged rollout you cannot skip
On July 19, 2024, CrowdStrike pushed a content update to every Windows sensor on Earth at once. No canary ring, no staged expansion — 8.5 million machines blue-screened, grounding airlines and closing hospitals. The fix that day would have been boring: ship to 1% first. Here "ship to 1% first" is not a policy document. The release machine has NO edge from `built` to `expanding` or `complete` — global blast radius without a canary is unrepresentable, and `soma verify` proves it. A rolled-back release is TERMINAL: you cut a new build, you never re-push the one that burned. The canary slice itself is walled by a memory invariant: a "canary" taking more than 5% of traffic is rejected at the write.
A Soma program from the devops part of the verified corpus: 102 lines, cells DeployPipeline, PipelineTests. It passes soma check with soma 3.2.4.
How it is built
The cell DeployPipeline declares 5 signals in its face: start_canary(id: String) -> Map, promote(id: String) -> Map, finish(id: String) -> Map, abort_release(id: String) -> Map and release_state(id: String) -> String; keeps 1 memory slot: canary_traffic (Map<String, Int>, persistent and consistent) under the invariant canary_traffic >= 0 && canary_traffic <= 5. Its state machine release starts in built and allows 5 transitions: built -> canary, canary -> expanding, expanding -> complete, canary -> rolled_back and expanding -> rolled_back. complete and rolled_back are terminal. Handlers: start_canary (line 46), promote (line 53), finish (line 59), abort_release (line 65) and release_state (line 71).
The file also holds 1 test cell (PipelineTests) with 13 assertions, run by soma test.
The source
deploy_canary.cell
// ============================================================================
// DEPLOY CANARY — the staged rollout you cannot skip
// ============================================================================
//
// On July 19, 2024, CrowdStrike pushed a content update to every Windows
// sensor on Earth at once. No canary ring, no staged expansion — 8.5
// million machines blue-screened, grounding airlines and closing
// hospitals. The fix that day would have been boring: ship to 1% first.
//
// Here "ship to 1% first" is not a policy document. The release machine
// has NO edge from `built` to `expanding` or `complete` — global blast
// radius without a canary is unrepresentable, and `soma verify` proves
// it. A rolled-back release is TERMINAL: you cut a new build, you never
// re-push the one that burned. The canary slice itself is walled by a
// memory invariant: a "canary" taking more than 5% of traffic is
// rejected at the write.
// ============================================================================
cell DeployPipeline {
face {
signal start_canary(id: String) -> Map
signal promote(id: String) -> Map
signal finish(id: String) -> Map
signal abort_release(id: String) -> Map
signal release_state(id: String) -> String
}
memory {
// Percent of traffic a canary may take. >5% is not a canary —
// the slot refuses the write no matter what a handler computes.
canary_traffic: Map<String, Int> [persistent, consistent]
invariant canary_traffic >= 0 && canary_traffic <= 5
}
// No path skips the canary ring. `complete` and `rolled_back` are
// terminal: shipped is history, burned is buried.
state release {
initial: built
built -> canary
canary -> expanding
expanding -> complete
canary -> rolled_back
expanding -> rolled_back
}
on start_canary(id: String) {
let r = try { transition(id, "canary") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
canary_traffic.set(id, 1)
return map("ok", true, "stage", get_status(id), "traffic_pct", 1)
}
on promote(id: String) {
let r = try { transition(id, "expanding") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "stage", get_status(id))
}
on finish(id: String) {
let r = try { transition(id, "complete") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "stage", get_status(id))
}
on abort_release(id: String) {
let r = try { transition(id, "rolled_back") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "stage", get_status(id))
}
on release_state(id: String) {
return get_status(id)
}
}
cell test PipelineTests {
rules {
// THE CrowdStrike move: built -> global. The edge does not exist.
assert_fails transition("r1", "expanding")
assert_fails transition("r1", "complete")
// the only way forward is through the canary ring
assert start_canary("r1").ok == true
assert promote("r1").ok == true
assert finish("r1").ok == true
// complete is terminal — a shipped release is history
assert_fails transition("r1", "canary")
assert_fails transition("r1", "rolled_back")
// a burned release is buried: rolled_back has no exit
assert start_canary("r2").ok == true
assert abort_release("r2").ok == true
assert_fails transition("r2", "canary")
assert_fails transition("r2", "expanding")
// a "canary" at 40% of traffic is not a canary — memory refuses
assert_fails canary_traffic.set("r3", 40)
assert canary_traffic.set("r3", 5) == ()
}
}What the toolchain says
$ soma check deploy_canary.cell
✓ All checks passed.$ soma test deploy_canary.cell
test PipelineTests ...
✓ assert_fails transition("r1", "expanding") — raised invalid transition: built → expanding. Current state: 'built'. Valid targets: [canary]
✓ assert_fails transition("r1", "complete") — raised invalid transition: built → complete. Current state: 'built'. Valid targets: [canary]
✓ assert start_canary("r1").ok == true
✓ assert promote("r1").ok == true
✓ assert finish("r1").ok == true
✓ assert_fails transition("r1", "canary") — raised invalid transition: complete → canary. Current state: 'complete'. Valid targets: []
✓ assert_fails transition("r1", "rolled_back") — raised invalid transition: complete → rolled_back. Current state: 'complete'. Valid targets: []
✓ assert start_canary("r2").ok == true
✓ assert abort_release("r2").ok == true
✓ assert_fails transition("r2", "canary") — raised invalid transition: rolled_back → canary. Current state: 'rolled_back'. Valid targets: []
✓ assert_fails transition("r2", "expanding") — raised invalid transition: rolled_back → expanding. Current state: 'rolled_back'. Valid targets: []
✓ assert_fails canary_traffic.set("r3", 40) — raised memory invariant violated on 'canary_traffic': canary_traffic >= 0 && canary_traffic <= 5 — rejected write of 40 (key "r3"); the slot is unchanged
✓ assert canary_traffic.set("r3", 5) == ()
13 tests: 13 passed, 0 failed$ soma verify deploy_canary.cell
Verifying deploy_canary.cell...
State machine 'release': 5 states, initial 'built'
States: [built, canary, complete, expanding, rolled_back]
✓ 5 states, 5 transitions
✓ all states reachable from 'built'
✓ terminal states: [complete, rolled_back]
✓ 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 5 handlers structurally terminate
✓ refinement: handler `start_canary` ⟶ {canary}
✓ refinement: handler `promote` ⟶ {expanding}
✓ refinement: handler `finish` ⟶ {complete}
✓ refinement: handler `abort_release` ⟶ {rolled_back}
· transition sources: `start_canary`, `promote`, `finish`, `abort_release` 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)
DeployPipeline/invariants:
✓ invariant canary_traffic >= 0 && canary_traffic <= 5 — writer 'start_canary' proven (writes 1)
12 passed, 0 warnings, 0 failures
Temporal properties for 'release':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK