Cert rotation — expiry is an escalation ladder, not a surprise
On December 6, 2018, an expired certificate inside Ericsson's SGSN software took mobile data down for 32 million O2 users in the UK and millions more on SoftBank in Japan. In February 2020, Microsoft Teams went down worldwide because an auth certificate simply lapsed. Nobody "decided" to let them expire — the deadline just never escalated. This controller makes expiry a one-way ladder the verifier checks: valid -> renewal_due -> critical -> expired, with rotation available at every rung BEFORE the fall. Both endings are TERMINAL — an expired cert can never quietly become valid again, and a superseded cert is retired for good. The lifetime ledger enforces the CA/Browser-forum ceiling: no handler can mint a certificate longer than 398 days.
A Soma program from the devops part of the verified corpus: 108 lines, cells CertManager, CertTests. It passes soma check with soma 3.2.4.
How it is built
The cell CertManager declares 5 signals in its face: issue(cert: String, lifetime_days: Int) -> Map, escalate(cert: String) -> Map, rotate(cert: String) -> Map, can_serve(cert: String) -> Bool and cert_state(cert: String) -> String; keeps 1 memory slot: lifetime (Map<String, Int>, persistent and consistent) under the invariant lifetime >= 1 && lifetime <= 398. Its state machine cert starts in valid and allows 6 transitions: valid -> renewal_due, renewal_due -> critical, critical -> expired, valid -> superseded, renewal_due -> superseded and critical -> superseded. expired and superseded are terminal. Handlers: issue (line 46), escalate (line 54), rotate (line 64), can_serve (line 70) and cert_state (line 75).
The file also holds 1 test cell (CertTests) with 15 assertions, run by soma test.
The source
cert_rotation.cell
// ============================================================================
// CERT ROTATION — expiry is an escalation ladder, not a surprise
// ============================================================================
//
// On December 6, 2018, an expired certificate inside Ericsson's SGSN
// software took mobile data down for 32 million O2 users in the UK and
// millions more on SoftBank in Japan. In February 2020, Microsoft Teams
// went down worldwide because an auth certificate simply lapsed. Nobody
// "decided" to let them expire — the deadline just never escalated.
//
// This controller makes expiry a one-way ladder the verifier checks:
// valid -> renewal_due -> critical -> expired, with rotation available
// at every rung BEFORE the fall. Both endings are TERMINAL — an expired
// cert can never quietly become valid again, and a superseded cert is
// retired for good. The lifetime ledger enforces the CA/Browser-forum
// ceiling: no handler can mint a certificate longer than 398 days.
// ============================================================================
cell CertManager {
face {
signal issue(cert: String, lifetime_days: Int) -> Map
signal escalate(cert: String) -> Map
signal rotate(cert: String) -> Map
signal can_serve(cert: String) -> Bool
signal cert_state(cert: String) -> String
}
memory {
lifetime: Map<String, Int> [persistent, consistent]
invariant lifetime >= 1 && lifetime <= 398
}
// The ladder only climbs. `expired` and `superseded` are terminal:
// the outage state cannot be un-happened, and a rotated-out cert
// never returns to service.
state cert {
initial: valid
valid -> renewal_due
renewal_due -> critical
critical -> expired
valid -> superseded
renewal_due -> superseded
critical -> superseded
}
on issue(cert: String, lifetime_days: Int) {
let w = try { lifetime.set(cert, lifetime_days) }
if w.error != () {
return map("ok", false, "reason", "lifetime outside CA/B limits: {w.error}")
}
return map("ok", true, "cert", cert, "state", get_status(cert))
}
on escalate(cert: String) {
let s = get_status(cert)
let next = "renewal_due"
if s == "renewal_due" { next = "critical" }
if s == "critical" { next = "expired" }
let r = try { transition(cert, next) }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", get_status(cert))
}
on rotate(cert: String) {
let r = try { transition(cert, "superseded") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "superseded")
}
on can_serve(cert: String) {
let s = get_status(cert)
return s == "valid" || s == "renewal_due" || s == "critical"
}
on cert_state(cert: String) {
return get_status(cert)
}
}
cell test CertTests {
rules {
// the CA/B forum wall: no 10-year certs, ever
assert issue("api.example", 90).ok == true
assert_fails lifetime.set("api.example", 3650)
assert_fails lifetime.set("api.example", 0)
// the ladder climbs one rung at a time — no skipping to expired
assert_fails transition("api.example", "expired")
assert escalate("api.example").state == "renewal_due"
assert escalate("api.example").state == "critical"
// rotation at the last rung still saves the day
assert rotate("api.example").ok == true
assert can_serve("api.example") == false
// and a superseded cert never returns to service
assert_fails transition("api.example", "valid")
// THE ERICSSON ENDING: nobody rotates. Expired is forever —
// there is no quiet path back to valid.
assert escalate("sgsn.core").state == "renewal_due"
assert escalate("sgsn.core").state == "critical"
assert escalate("sgsn.core").state == "expired"
assert can_serve("sgsn.core") == false
assert_fails transition("sgsn.core", "valid")
assert_fails transition("sgsn.core", "superseded")
}
}What the toolchain says
$ soma check cert_rotation.cell
✓ All checks passed.$ soma test cert_rotation.cell
test CertTests ...
✓ assert issue("api.example", 90).ok == true
✓ assert_fails lifetime.set("api.example", 3650) — raised memory invariant violated on 'lifetime': lifetime >= 1 && lifetime <= 398 — rejected write of 3650 (key "api.example"); the slot is unchanged
✓ assert_fails lifetime.set("api.example", 0) — raised memory invariant violated on 'lifetime': lifetime >= 1 && lifetime <= 398 — rejected write of 0 (key "api.example"); the slot is unchanged
✓ assert_fails transition("api.example", "expired") — raised invalid transition: valid → expired. Current state: 'valid'. Valid targets: [renewal_due, superseded]
✓ assert escalate("api.example").state == "renewal_due"
✓ assert escalate("api.example").state == "critical"
✓ assert rotate("api.example").ok == true
✓ assert can_serve("api.example") == false
✓ assert_fails transition("api.example", "valid") — raised invalid transition: superseded → valid. Current state: 'superseded'. Valid targets: []
✓ assert escalate("sgsn.core").state == "renewal_due"
✓ assert escalate("sgsn.core").state == "critical"
✓ assert escalate("sgsn.core").state == "expired"
✓ assert can_serve("sgsn.core") == false
✓ assert_fails transition("sgsn.core", "valid") — raised invalid transition: expired → valid. Current state: 'expired'. Valid targets: []
✓ assert_fails transition("sgsn.core", "superseded") — raised invalid transition: expired → superseded. Current state: 'expired'. Valid targets: []
15 tests: 15 passed, 0 failed$ soma verify cert_rotation.cell
Verifying cert_rotation.cell...
State machine 'cert': 5 states, initial 'valid'
States: [critical, expired, renewal_due, superseded, valid]
✓ 5 states, 6 transitions
✓ all states reachable from 'valid'
✓ terminal states: [expired, superseded]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
⚠ dynamic transition targets: handler `escalate` uses a dynamic (computed) transition target — the state these handlers move to is computed at run time (from input or an LLM answer), so the machine's safety is checked at run time for them, not proven
✓ termination: all 5 handlers structurally terminate
⚠ refinement (partial — dynamic targets fall back to runtime check): handler `escalate` calls transition() with a computed target — which edge it takes is checked at run time (invalid_transition), not proven; write the target as a literal state to have it verified
✓ refinement (partial — dynamic targets fall back to runtime check): handler `escalate` ⟶ <dynamic>
✓ refinement (partial — dynamic targets fall back to runtime check): handler `rotate` ⟶ {superseded}
· transition sources: `rotate` calls 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)
CertManager/invariants:
⚠ invariant lifetime >= 1 && lifetime <= 398 — runtime-checked (computed values): issue → lifetime because `lifetime_days` is a parameter (narrow it: `require lifetime_days >= 1 && lifetime_days <= 398 else …`)
8 passed, 3 warnings, 0 failures
Temporal properties for 'cert':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK