Fleet sync — no activation until every node runs the same code
The other half of the Knight Capital disaster: a technician deployed the new router to only 7 of 8 servers. The fleet was split-brained — one machine interpreted the activation flag as 2003-era "Power Peg" logic. Activating a half-deployed fleet is what turned a deploy slip into $440M of runaway orders. This controller makes the split-brain activation unrepresentable. `activated` is only reachable from `synced`, and the handler that enters `synced` requires the pending-node ledger to read zero. The ledger itself is invariant-walled: it can never go negative (no double-counting a node) and never exceed the fleet size.
A Soma program from the devops part of the verified corpus: 100 lines, cells FleetSync, FleetTests. It passes soma check with soma 3.2.4.
How it is built
The cell FleetSync declares 4 signals in its face: begin_rollout(deploy: String, fleet_size: Int) -> Map, node_updated(deploy: String) -> Map, activate(deploy: String) -> Map and deploy_state(deploy: String) -> Map; keeps 1 memory slot: pending (Map<String, Int>, persistent and consistent) under the invariant pending >= 0 && pending <= 8. Its state machine rollout_phase starts in idle and allows 4 transitions: idle -> rolling, rolling -> synced, synced -> activated and rolling -> abandoned. abandoned and activated are terminal. Handlers: begin_rollout (line 43), node_updated (line 51), activate (line 63) and deploy_state (line 69).
The file also holds 1 test cell (FleetTests) with 16 assertions, run by soma test.
The source
fleet_sync_activation.cell
// ============================================================================
// FLEET SYNC — no activation until every node runs the same code
// ============================================================================
//
// The other half of the Knight Capital disaster: a technician deployed
// the new router to only 7 of 8 servers. The fleet was split-brained —
// one machine interpreted the activation flag as 2003-era "Power Peg"
// logic. Activating a half-deployed fleet is what turned a deploy slip
// into $440M of runaway orders.
//
// This controller makes the split-brain activation unrepresentable.
// `activated` is only reachable from `synced`, and the handler that
// enters `synced` requires the pending-node ledger to read zero. The
// ledger itself is invariant-walled: it can never go negative (no
// double-counting a node) and never exceed the fleet size.
// ============================================================================
cell FleetSync {
face {
signal begin_rollout(deploy: String, fleet_size: Int) -> Map
signal node_updated(deploy: String) -> Map
signal activate(deploy: String) -> Map
signal deploy_state(deploy: String) -> Map
}
memory {
// nodes still running OLD code. The wall: 0..8 — a phantom
// ninth node or a negative count is rejected at the write.
pending: Map<String, Int> [persistent, consistent]
invariant pending >= 0 && pending <= 8
}
// `activated` has exactly one inbound edge — from `synced`.
// There is no rolling -> activated: a split fleet cannot go live.
state rollout_phase {
initial: idle
idle -> rolling
rolling -> synced
synced -> activated
rolling -> abandoned
}
on begin_rollout(deploy: String, fleet_size: Int) {
let r = try { transition(deploy, "rolling") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
let w = try { pending.set(deploy, fleet_size) }
if w.error != () { return map("ok", false, "reason", "{w.error}") }
return map("ok", true, "pending", fleet_size)
}
on node_updated(deploy: String) {
if get_status(deploy) != "rolling" {
return map("ok", false, "reason", "no rollout in progress")
}
let left = pending.get(deploy) ?? 0
// a node reporting twice would drive this to -1: memory refuses
let w = try { pending.set(deploy, left - 1) }
if w.error != () { return map("ok", false, "reason", "{w.error}") }
if left - 1 == 0 { transition(deploy, "synced") }
return map("ok", true, "pending", left - 1, "phase", get_status(deploy))
}
on activate(deploy: String) {
let r = try { transition(deploy, "activated") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "phase", "activated")
}
on deploy_state(deploy: String) {
return map("phase", get_status(deploy), "pending", pending.get(deploy) ?? 0)
}
}
cell test FleetTests {
rules {
assert begin_rollout("d1", 8).ok == true
// THE KNIGHT MOVE: 7 of 8 nodes updated, then flip the switch.
assert node_updated("d1").ok == true
assert node_updated("d1").ok == true
assert node_updated("d1").ok == true
assert node_updated("d1").ok == true
assert node_updated("d1").ok == true
assert node_updated("d1").ok == true
assert node_updated("d1").ok == true
assert deploy_state("d1").pending == 1
assert_fails transition("d1", "activated") // split fleet: no edge
// the eighth node lands; only NOW does activation exist
assert node_updated("d1").ok == true
assert deploy_state("d1").phase == "synced"
assert activate("d1").ok == true
// the pending ledger never lies: no negatives, no phantom fleet
assert node_updated("d1").ok == false // rollout is over
assert_fails pending.set("d2", 9)
assert_fails pending.set("d2", -1)
}
}What the toolchain says
$ soma check fleet_sync_activation.cell
✓ All checks passed.$ soma test fleet_sync_activation.cell
test FleetTests ...
✓ assert begin_rollout("d1", 8).ok == true
✓ assert node_updated("d1").ok == true
✓ assert node_updated("d1").ok == true
✓ assert node_updated("d1").ok == true
✓ assert node_updated("d1").ok == true
✓ assert node_updated("d1").ok == true
✓ assert node_updated("d1").ok == true
✓ assert node_updated("d1").ok == true
✓ assert deploy_state("d1").pending == 1
✓ assert_fails transition("d1", "activated") — raised invalid transition: rolling → activated. Current state: 'rolling'. Valid targets: [synced, abandoned]
✓ assert node_updated("d1").ok == true
✓ assert deploy_state("d1").phase == "synced"
✓ assert activate("d1").ok == true
✓ assert node_updated("d1").ok == false
✓ assert_fails pending.set("d2", 9) — raised memory invariant violated on 'pending': pending >= 0 && pending <= 8 — rejected write of 9 (key "d2"); the slot is unchanged
✓ assert_fails pending.set("d2", -1) — raised memory invariant violated on 'pending': pending >= 0 && pending <= 8 — rejected write of -1 (key "d2"); the slot is unchanged
16 tests: 16 passed, 0 failed$ soma verify fleet_sync_activation.cell
Verifying fleet_sync_activation.cell...
State machine 'rollout_phase': 5 states, initial 'idle'
States: [abandoned, activated, idle, rolling, synced]
✓ 5 states, 4 transitions
✓ all states reachable from 'idle'
✓ terminal states: [activated, abandoned]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
✓ termination: all 4 handlers structurally terminate
⚠ refinement: declared transition `rolling → abandoned` is never reached by any handler — spec may be aspirational or stale
✓ refinement: handler `begin_rollout` ⟶ {rolling}
✓ refinement: handler `node_updated` ⟶ {rolling → synced [if left - 1 == 0]}
✓ refinement: handler `activate` ⟶ {activated}
· transition sources: `begin_rollout`, `activate` 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)
FleetSync/invariants:
✓ invariant pending <= 8 — writer 'node_updated' proven by induction (writes left - 1)
⚠ invariant pending >= 0 && pending <= 8 — runtime-checked (computed values): begin_rollout → pending because `fleet_size` is a parameter (narrow it: `require fleet_size >= 0 && fleet_size <= 8 else …`), node_updated → pending [pending >= 0] because `left - 1` is only known to lie in [-1, 7] — narrow it: `require (left - 1) >= 0 else …`
11 passed, 2 warnings, 0 failures
Temporal properties for 'rollout_phase':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK