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

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.

Generated from soma describe on this file.

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

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

$ 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

Builtins used

get_status, map, transition

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