Db migration — applied migrations are immutable history
Every schema-drift horror story starts the same way: someone edits a migration that already ran in production. Staging replays the edited file, prod keeps the old shape, and three weeks later a column that "must exist" doesn't. Flyway and Liquibase bolt on checksum errors; here immutability is the machine itself: `applied` is a TERMINAL state `soma verify` proves you cannot leave. Undoing means writing a NEW down-migration, never rewriting the past. The second wall is the migrator lock — the GitLab-style disaster of two operators running migrations concurrently is refused by a memory invariant that admits at most one lock holder.
A Soma program from the devops part of the verified corpus: 104 lines, cells Migrator, MigrationTests. It passes soma check with soma 3.2.4.
How it is built
The cell Migrator declares 5 signals in its face: start_apply(mig: String) -> Map, confirm_applied(mig: String) -> Map, mark_failed(mig: String) -> Map, retry(mig: String) -> Map and migration_state(mig: String) -> String; keeps 1 memory slot: lock_holders (Map<String, Int>, persistent and consistent) under the invariant lock_holders >= 0 && lock_holders <= 1. Its state machine migration starts in pending and allows 4 transitions: pending -> applying, applying -> applied, applying -> failed and failed -> applying. applied is terminal. Handlers: start_apply (line 43), confirm_applied (line 57), mark_failed (line 64), retry (line 71) and migration_state (line 75).
The file also holds 1 test cell (MigrationTests) with 11 assertions, run by soma test.
The source
db_migration.cell
// ============================================================================
// DB MIGRATION — applied migrations are immutable history
// ============================================================================
//
// Every schema-drift horror story starts the same way: someone edits a
// migration that already ran in production. Staging replays the edited
// file, prod keeps the old shape, and three weeks later a column that
// "must exist" doesn't. Flyway and Liquibase bolt on checksum errors;
// here immutability is the machine itself: `applied` is a TERMINAL
// state `soma verify` proves you cannot leave. Undoing means writing a
// NEW down-migration, never rewriting the past.
//
// The second wall is the migrator lock — the GitLab-style disaster of
// two operators running migrations concurrently is refused by a memory
// invariant that admits at most one lock holder.
// ============================================================================
cell Migrator {
face {
signal start_apply(mig: String) -> Map
signal confirm_applied(mig: String) -> Map
signal mark_failed(mig: String) -> Map
signal retry(mig: String) -> Map
signal migration_state(mig: String) -> String
}
memory {
// 0 = unlocked, 1 = locked. A second concurrent migrator would
// write 2 — the memory refuses it before any DDL runs.
lock_holders: Map<String, Int> [persistent, consistent]
invariant lock_holders >= 0 && lock_holders <= 1
}
// `applied` has no exit: production history cannot be rewritten.
state migration {
initial: pending
pending -> applying
applying -> applied
applying -> failed
failed -> applying
}
on start_apply(mig: String) {
let held = lock_holders.get("schema") ?? 0
let w = try { lock_holders.set("schema", held + 1) }
if w.error != () {
return map("ok", false, "reason", "migrator lock is held — refusing concurrent DDL")
}
let r = try { transition(mig, "applying") }
if r.error != () {
lock_holders.set("schema", held)
return map("ok", false, "reason", "{r.error}")
}
return map("ok", true, "state", "applying")
}
on confirm_applied(mig: String) {
let r = try { transition(mig, "applied") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
lock_holders.set("schema", 0)
return map("ok", true, "state", "applied")
}
on mark_failed(mig: String) {
let r = try { transition(mig, "failed") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
lock_holders.set("schema", 0)
return map("ok", true, "state", "failed")
}
on retry(mig: String) {
return start_apply(mig)
}
on migration_state(mig: String) {
return get_status(mig)
}
}
cell test MigrationTests {
rules {
// happy path: pending -> applying -> applied
assert start_apply("0042_add_orders").ok == true
// concurrency wall: a second migrator cannot take the lock
assert start_apply("0043_add_index").ok == false
assert_fails lock_holders.set("schema", 2)
assert confirm_applied("0042_add_orders").ok == true
// THE DRIFT MOVE: re-run or rewrite an applied migration.
// `applied` is terminal — no edge exists, verify proves it.
assert_fails transition("0042_add_orders", "applying")
assert_fails transition("0042_add_orders", "pending")
assert_fails transition("0042_add_orders", "failed")
// a failed migration may retry — failure is not terminal
assert start_apply("0043_add_index").ok == true
assert mark_failed("0043_add_index").ok == true
assert retry("0043_add_index").ok == true
assert confirm_applied("0043_add_index").ok == true
}
}What the toolchain says
$ soma check db_migration.cell
✓ All checks passed.$ soma test db_migration.cell
test MigrationTests ...
✓ assert start_apply("0042_add_orders").ok == true
✓ assert start_apply("0043_add_index").ok == false
✓ assert_fails lock_holders.set("schema", 2) — raised memory invariant violated on 'lock_holders': lock_holders >= 0 && lock_holders <= 1 — rejected write of 2 (key "schema"); the slot is unchanged
✓ assert confirm_applied("0042_add_orders").ok == true
✓ assert_fails transition("0042_add_orders", "applying") — raised invalid transition: applied → applying. Current state: 'applied'. Valid targets: []
✓ assert_fails transition("0042_add_orders", "pending") — raised invalid transition: applied → pending. Current state: 'applied'. Valid targets: []
✓ assert_fails transition("0042_add_orders", "failed") — raised invalid transition: applied → failed. Current state: 'applied'. Valid targets: []
✓ assert start_apply("0043_add_index").ok == true
✓ assert mark_failed("0043_add_index").ok == true
✓ assert retry("0043_add_index").ok == true
✓ assert confirm_applied("0043_add_index").ok == true
11 tests: 11 passed, 0 failed$ soma verify db_migration.cell
Verifying db_migration.cell...
State machine 'migration': 4 states, initial 'pending'
States: [applied, applying, failed, pending]
✓ 4 states, 4 transitions
✓ all states reachable from 'pending'
✓ terminal states: [applied]
✓ 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 `start_apply` ⟶ {applying}
✓ refinement: handler `confirm_applied` ⟶ {applied}
✓ refinement: handler `mark_failed` ⟶ {failed}
· transition sources: `start_apply`, `confirm_applied`, `mark_failed` 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)
Migrator/invariants:
✓ invariant lock_holders >= 0 && lock_holders <= 1 — writer 'confirm_applied' proven (writes 0)
✓ invariant lock_holders >= 0 && lock_holders <= 1 — writer 'mark_failed' proven (writes 0)
✓ invariant lock_holders >= 0 — writer 'start_apply' proven by induction (writes held + 1)
✓ invariant lock_holders >= 0 && lock_holders <= 1 — writer 'start_apply' proven by induction (writes held)
⚠ invariant lock_holders >= 0 && lock_holders <= 1 — runtime-checked (computed values): start_apply → lock_holders [lock_holders <= 1] because `held + 1` is only known to lie in [1, 2] — narrow it: `require (held + 1) <= 1 else …`
14 passed, 1 warnings, 0 failures
Temporal properties for 'migration':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK