Spinning reserve — every megawatt you sell must claim real iron
Spinning reserve is capacity a generator is PAID to hold back, ready to inject within minutes when a unit elsewhere trips. The market failure: energy and reserve are sold in separate transactions, so a 500 MW unit can dispatch 450 MW of energy AND sell 100 MW of reserve — 550 MW of promises against 500 MW of iron. During winter storm Uri in February 2021, ERCOT discovered how much of its purchased reserve was paper: units that had sold readiness tripped offline or never ramped, and the shortfall became rolling blackouts in single-digit cold. The fix here is one slot: `claimed` holds energy dispatch PLUS reserve commitments per unit, and its invariant is the nameplate. Both markets write through the same wall, so the double-sell is rejected at the memory — there is no code path on which promises exceed iron.
A Soma program from the energy part of the verified corpus: 109 lines, cells ReserveDesk, ReserveTests. It passes soma check with soma 3.2.4.
How it is built
The cell ReserveDesk declares 5 signals in its face: dispatch_energy(unit: String, mw: Int) -> Map, sell_reserve(unit: String, mw: Int) -> Map, release_reserve(unit: String, mw: Int) -> Map, claimed_of(unit: String) -> Int and reserve_of(unit: String) -> Int; keeps 2 memory slots: claimed (Map<String, Int>, persistent and consistent) under the invariant claimed >= 0 && claimed <= 500 and reserve_mw (Map<String, Int>, persistent and consistent) under the invariant reserve_mw >= 0 && reserve_mw <= 500. Handlers: claimed_of (line 40), reserve_of (line 41), dispatch_energy (line 43), sell_reserve (line 52) and release_reserve (line 65).
The file also holds 1 test cell (ReserveTests) with 15 assertions, run by soma test.
The source
spinning_reserve.cell
// ============================================================================
// SPINNING RESERVE — every megawatt you sell must claim real iron
// ============================================================================
//
// Spinning reserve is capacity a generator is PAID to hold back, ready to
// inject within minutes when a unit elsewhere trips. The market failure:
// energy and reserve are sold in separate transactions, so a 500 MW unit
// can dispatch 450 MW of energy AND sell 100 MW of reserve — 550 MW of
// promises against 500 MW of iron. During winter storm Uri in February
// 2021, ERCOT discovered how much of its purchased reserve was paper:
// units that had sold readiness tripped offline or never ramped, and the
// shortfall became rolling blackouts in single-digit cold.
//
// The fix here is one slot: `claimed` holds energy dispatch PLUS reserve
// commitments per unit, and its invariant is the nameplate. Both markets
// write through the same wall, so the double-sell is rejected at the
// memory — there is no code path on which promises exceed iron.
// ============================================================================
cell ReserveDesk {
face {
signal dispatch_energy(unit: String, mw: Int) -> Map
signal sell_reserve(unit: String, mw: Int) -> Map
signal release_reserve(unit: String, mw: Int) -> Map
signal claimed_of(unit: String) -> Int
signal reserve_of(unit: String) -> Int
}
memory {
// energy dispatch + reserve commitments, MW — nameplate is 500.
// THE wall: promises live in the same slot as the iron they claim.
claimed: Map<String, Int> [persistent, consistent]
invariant claimed >= 0 && claimed <= 500
// reserve component, for settlement reporting
reserve_mw: Map<String, Int> [persistent, consistent]
invariant reserve_mw >= 0 && reserve_mw <= 500
}
on claimed_of(unit: String) { return claimed.get(unit) ?? 0 }
on reserve_of(unit: String) { return reserve_mw.get(unit) ?? 0 }
on dispatch_energy(unit: String, mw: Int) {
if mw <= 0 { return map("ok", false, "reason", "dispatch must be positive") }
let w = try { claimed.set(unit, claimed_of(unit) + mw) }
if w.error != () {
return map("ok", false, "reason", "nameplate wall: {w.error}")
}
return map("ok", true, "claimed", claimed_of(unit))
}
on sell_reserve(unit: String, mw: Int) {
if mw <= 0 { return map("ok", false, "reason", "reserve must be positive") }
// the reserve sale claims the same iron as an energy dispatch —
// if the headroom isn't physically there, this write refuses
let w = try { claimed.set(unit, claimed_of(unit) + mw) }
if w.error != () {
return map("ok", false, "reason",
"reserve exceeds physical headroom: {w.error}")
}
reserve_mw.set(unit, reserve_of(unit) + mw)
return map("ok", true, "reserve", reserve_of(unit), "claimed", claimed_of(unit))
}
on release_reserve(unit: String, mw: Int) {
if mw <= 0 || mw > reserve_of(unit) {
return map("ok", false, "reason",
"cannot release {mw} MW — only {reserve_of(unit)} MW committed")
}
reserve_mw.set(unit, reserve_of(unit) - mw)
claimed.set(unit, claimed_of(unit) - mw)
return map("ok", true, "reserve", reserve_of(unit), "claimed", claimed_of(unit))
}
}
cell test ReserveTests {
rules {
// a 500 MW unit dispatches 450 MW of energy
assert dispatch_energy("u1", 450).ok == true
assert claimed_of("u1") == 450
// THE DOUBLE-SELL: 100 MW of reserve against 50 MW of headroom.
// Refused — the promise has no iron behind it.
assert sell_reserve("u1", 100).ok == false
assert reserve_of("u1") == 0
// 50 MW of reserve fits exactly
assert sell_reserve("u1", 50).ok == true
assert claimed_of("u1") == 500
// now the unit is fully claimed: no more energy, no more reserve
assert dispatch_energy("u1", 1).ok == false
assert sell_reserve("u1", 1).ok == false
// releasing the reserve frees real headroom again
assert release_reserve("u1", 30).ok == true
assert claimed_of("u1") == 470
assert dispatch_energy("u1", 30).ok == true
// you cannot release reserve you never sold
assert release_reserve("u1", 999).ok == false
// THE WALL itself: over-claim and negative-claim writes raise
assert_fails claimed.set("u1", 501)
assert_fails claimed.set("u1", -1)
assert_fails reserve_mw.set("u1", 600)
}
}What the toolchain says
$ soma check spinning_reserve.cell
✓ All checks passed.$ soma test spinning_reserve.cell
test ReserveTests ...
✓ assert dispatch_energy("u1", 450).ok == true
✓ assert claimed_of("u1") == 450
✓ assert sell_reserve("u1", 100).ok == false
✓ assert reserve_of("u1") == 0
✓ assert sell_reserve("u1", 50).ok == true
✓ assert claimed_of("u1") == 500
✓ assert dispatch_energy("u1", 1).ok == false
✓ assert sell_reserve("u1", 1).ok == false
✓ assert release_reserve("u1", 30).ok == true
✓ assert claimed_of("u1") == 470
✓ assert dispatch_energy("u1", 30).ok == true
✓ assert release_reserve("u1", 999).ok == false
✓ assert_fails claimed.set("u1", 501) — raised memory invariant violated on 'claimed': claimed >= 0 && claimed <= 500 — rejected write of 501 (key "u1"); the slot is unchanged
✓ assert_fails claimed.set("u1", -1) — raised memory invariant violated on 'claimed': claimed >= 0 && claimed <= 500 — rejected write of -1 (key "u1"); the slot is unchanged
✓ assert_fails reserve_mw.set("u1", 600) — raised memory invariant violated on 'reserve_mw': reserve_mw >= 0 && reserve_mw <= 500 — rejected write of 600 (key "u1"); the slot is unchanged
15 tests: 15 passed, 0 failed$ soma verify spinning_reserve.cell
Verifying spinning_reserve.cell...
ReserveDesk/invariants:
✓ invariant claimed >= 0 — writer 'dispatch_energy' proven by induction (writes claimed_of(unit) + mw)
✓ invariant claimed <= 500 — writer 'release_reserve' proven by induction (writes claimed_of(unit) - mw)
✓ invariant claimed >= 0 — writer 'sell_reserve' proven by induction (writes claimed_of(unit) + mw)
⚠ invariant claimed >= 0 && claimed <= 500 — runtime-checked (computed values): dispatch_energy → claimed [claimed <= 500] because `claimed_of(unit) + mw` is only known to lie in [1, ∞) — narrow it: `require (claimed_of(unit) + mw) <= 500 else …`, release_reserve → claimed [claimed >= 0] because `claimed_of(unit) - mw` is only known to lie in (-∞, 499] — narrow it: `require (claimed_of(unit) - mw) >= 0 else …`, sell_reserve → claimed [claimed <= 500] because `claimed_of(unit) + mw` is only known to lie in [1, ∞) — narrow it: `require (claimed_of(unit) + mw) <= 500 else …`
✓ invariant reserve_mw <= 500 — writer 'release_reserve' proven by induction (writes reserve_of(unit) - mw)
✓ invariant reserve_mw >= 0 — writer 'sell_reserve' proven by induction (writes reserve_of(unit) + mw)
⚠ invariant reserve_mw >= 0 && reserve_mw <= 500 — runtime-checked (computed values): release_reserve → reserve_mw [reserve_mw >= 0] because `reserve_of(unit) - mw` is only known to lie in (-∞, 499] — narrow it: `require (reserve_of(unit) - mw) >= 0 else …`, sell_reserve → reserve_mw [reserve_mw <= 500] because `reserve_of(unit) + mw` is only known to lie in [1, ∞) — narrow it: `require (reserve_of(unit) + mw) <= 500 else …`
5 passed, 2 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK