Backup retention — the floor you cannot prune through
On January 31, 2017, a GitLab engineer cleaning up replication lag ran `rm -rf` on what turned out to be the PRIMARY database directory. That was survivable — until all five backup mechanisms turned out to be broken: pg_dump silently producing empty files, S3 uploads failing, snapshots disabled. Six hours of production data were gone forever. Two structural fixes here. First, a backup is only trusted after a restore drill: the lifecycle forces created -> verifying -> verified, and a backup that fails its drill lands in `corrupt`, a TERMINAL state that can never be counted or restored from. Second, the count of verified copies lives behind a memory invariant with a floor of 3: the prune that would leave you with two copies is refused by the MEMORY, not by a retention script somebody edits at 2 a.m.
A Soma program from the devops part of the verified corpus: 102 lines, cells BackupVault, RetentionTests. It passes soma check with soma 3.2.4.
How it is built
The cell BackupVault declares 5 signals in its face: record_backup(b: String) -> Map, drill_pass(b: String) -> Map, drill_fail(b: String) -> Map, prune_one(dataset: String) -> Map and restorable(b: String) -> Bool; keeps 1 memory slot: copies (Map<String, Int>, persistent and consistent) under the invariant copies >= 3 && copies <= 30. Its state machine backup starts in created and allows 3 transitions: created -> verifying, verifying -> verified and verifying -> corrupt. corrupt and verified are terminal. Handlers: record_backup (line 44), drill_pass (line 50), drill_fail (line 56), prune_one (line 62) and restorable (line 71).
The file also holds 1 test cell (RetentionTests) with 16 assertions, run by soma test.
The source
backup_retention.cell
// ============================================================================
// BACKUP RETENTION — the floor you cannot prune through
// ============================================================================
//
// On January 31, 2017, a GitLab engineer cleaning up replication lag ran
// `rm -rf` on what turned out to be the PRIMARY database directory. That
// was survivable — until all five backup mechanisms turned out to be
// broken: pg_dump silently producing empty files, S3 uploads failing,
// snapshots disabled. Six hours of production data were gone forever.
//
// Two structural fixes here. First, a backup is only trusted after a
// restore drill: the lifecycle forces created -> verifying -> verified,
// and a backup that fails its drill lands in `corrupt`, a TERMINAL
// state that can never be counted or restored from. Second, the count
// of verified copies lives behind a memory invariant with a floor of 3:
// the prune that would leave you with two copies is refused by the
// MEMORY, not by a retention script somebody edits at 2 a.m.
// ============================================================================
cell BackupVault {
face {
signal record_backup(b: String) -> Map
signal drill_pass(b: String) -> Map
signal drill_fail(b: String) -> Map
signal prune_one(dataset: String) -> Map
signal restorable(b: String) -> Bool
}
memory {
// verified copies per dataset. The floor: never below 3.
copies: Map<String, Int> [persistent, consistent]
invariant copies >= 3 && copies <= 30
}
// `corrupt` is terminal: a backup that failed its restore drill is
// dead evidence, never a candidate for "maybe it's fine actually".
state backup {
initial: created
created -> verifying
verifying -> verified
verifying -> corrupt
}
on record_backup(b: String) {
let r = try { transition(b, "verifying") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "verifying")
}
on drill_pass(b: String) {
let r = try { transition(b, "verified") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "verified")
}
on drill_fail(b: String) {
let r = try { transition(b, "corrupt") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "corrupt")
}
on prune_one(dataset: String) {
let n = copies.get(dataset) ?? 0
let w = try { copies.set(dataset, n - 1) }
if w.error != () {
return map("ok", false, "reason", "retention floor: pruning to {n - 1} copies refused")
}
return map("ok", true, "copies", n - 1)
}
on restorable(b: String) {
return get_status(b) == "verified"
}
}
cell test RetentionTests {
rules {
// a backup is not a backup until the restore drill passes
assert record_backup("db-0131").ok == true
assert restorable("db-0131") == false
// GITLAB'S DISCOVERY: you cannot restore from an unverified file
assert_fails transition("db-0131", "restored")
assert drill_pass("db-0131").ok == true
assert restorable("db-0131") == true
// a failed drill is terminal — no second opinion revives it
assert record_backup("db-0201").ok == true
assert drill_fail("db-0201").ok == true
assert_fails transition("db-0201", "verified")
assert_fails transition("db-0201", "verifying")
assert restorable("db-0201") == false
// the retention floor: 5 -> 4 -> 3 is fine, 3 -> 2 is refused
assert copies.set("prod-pg", 5) == ()
assert prune_one("prod-pg").copies == 4
assert prune_one("prod-pg").copies == 3
assert prune_one("prod-pg").ok == false
assert_fails copies.set("prod-pg", 2)
assert_fails copies.set("prod-pg", 0)
}
}What the toolchain says
$ soma check backup_retention.cell
✓ All checks passed.$ soma test backup_retention.cell
test RetentionTests ...
✓ assert record_backup("db-0131").ok == true
✓ assert restorable("db-0131") == false
✓ assert_fails transition("db-0131", "restored") — raised invalid transition: verifying → restored. Current state: 'verifying'. Valid targets: [verified, corrupt]
✓ assert drill_pass("db-0131").ok == true
✓ assert restorable("db-0131") == true
✓ assert record_backup("db-0201").ok == true
✓ assert drill_fail("db-0201").ok == true
✓ assert_fails transition("db-0201", "verified") — raised invalid transition: corrupt → verified. Current state: 'corrupt'. Valid targets: []
✓ assert_fails transition("db-0201", "verifying") — raised invalid transition: corrupt → verifying. Current state: 'corrupt'. Valid targets: []
✓ assert restorable("db-0201") == false
✓ assert copies.set("prod-pg", 5) == ()
✓ assert prune_one("prod-pg").copies == 4
✓ assert prune_one("prod-pg").copies == 3
✓ assert prune_one("prod-pg").ok == false
✓ assert_fails copies.set("prod-pg", 2) — raised memory invariant violated on 'copies': copies >= 3 && copies <= 30 — rejected write of 2 (key "prod-pg"); the slot is unchanged
✓ assert_fails copies.set("prod-pg", 0) — raised memory invariant violated on 'copies': copies >= 3 && copies <= 30 — rejected write of 0 (key "prod-pg"); the slot is unchanged
16 tests: 16 passed, 0 failed$ soma verify backup_retention.cell
Verifying backup_retention.cell...
State machine 'backup': 4 states, initial 'created'
States: [corrupt, created, verified, verifying]
✓ 4 states, 3 transitions
✓ all states reachable from 'created'
✓ terminal states: [verified, corrupt]
✓ 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 5 handlers structurally terminate
✓ refinement: handler `record_backup` ⟶ {verifying}
✓ refinement: handler `drill_pass` ⟶ {verified}
✓ refinement: handler `drill_fail` ⟶ {corrupt}
· transition sources: `record_backup`, `drill_pass`, `drill_fail` 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)
BackupVault/invariants:
✓ invariant copies <= 30 — writer 'prune_one' proven by induction (writes n - 1)
⚠ invariant copies >= 3 && copies <= 30 — runtime-checked (computed values): prune_one → copies [copies >= 3] because `n - 1` is only known to lie in [-1, 29] — narrow it: `require (n - 1) >= 3 else …`
11 passed, 1 warnings, 0 failures
Temporal properties for 'backup':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK