Demand response — no payment before measurement, and settlement is final
Demand-response programs pay customers for NOT consuming during a grid emergency — which makes the payout an invitation to invent curtailment. In 2013 FERC penalized Rumford Paper Co. for gaming its DR baseline: the mill ran flat-out during the baseline window, then "curtailed" to its normal level and collected for megawatts it never actually shed. The money leaks wherever settlement can run before measurement, or run twice. Here the event lifecycle is the control: payout can only be posted from `measured` (verified meter data in hand), `settled` is TERMINAL — no re-settlement, no retroactive sweetener — and a cancelled event is terminal too, payable by no path. soma verify proves both. The payout ledger refuses negative or program-cap-busting amounts at the memory.
A Soma program from the energy part of the verified corpus: 124 lines, cells DrEvent, DrTests. It passes soma check with soma 3.2.4.
How it is built
The cell DrEvent declares 7 signals in its face: notify_participants(ev: String) -> Map, begin_curtailment(ev: String) -> Map, meter_data_in(ev: String, verified_mw: Int) -> Map, post_payout(ev: String, dollars: Int) -> Map, cancel_event(ev: String) -> Map, event_state(ev: String) -> String and payout_of(ev: String) -> Int; keeps 2 memory slots: curtailed (Map<String, Int>, persistent and consistent) under the invariant curtailed >= 0 and payout (Map<String, Int>, persistent and consistent) under the invariant payout >= 0 && payout <= 1000000. Its state machine dr_lifecycle starts in scheduled and allows 5 transitions: scheduled -> notified, notified -> active, active -> measured, measured -> settled and scheduled -> cancelled. cancelled and settled are terminal. Handlers: notify_participants (line 50), begin_curtailment (line 56), meter_data_in (line 62), post_payout (line 69), cancel_event (line 81), event_state (line 87) and payout_of (line 88).
The file also holds 1 test cell (DrTests) with 18 assertions, run by soma test.
The source
demand_response.cell
// ============================================================================
// DEMAND RESPONSE — no payment before measurement, and settlement is final
// ============================================================================
//
// Demand-response programs pay customers for NOT consuming during a grid
// emergency — which makes the payout an invitation to invent curtailment.
// In 2013 FERC penalized Rumford Paper Co. for gaming its DR baseline:
// the mill ran flat-out during the baseline window, then "curtailed" to
// its normal level and collected for megawatts it never actually shed.
// The money leaks wherever settlement can run before measurement, or run
// twice.
//
// Here the event lifecycle is the control: payout can only be posted from
// `measured` (verified meter data in hand), `settled` is TERMINAL — no
// re-settlement, no retroactive sweetener — and a cancelled event is
// terminal too, payable by no path. soma verify proves both. The payout
// ledger refuses negative or program-cap-busting amounts at the memory.
// ============================================================================
cell DrEvent {
face {
signal notify_participants(ev: String) -> Map
signal begin_curtailment(ev: String) -> Map
signal meter_data_in(ev: String, verified_mw: Int) -> Map
signal post_payout(ev: String, dollars: Int) -> Map
signal cancel_event(ev: String) -> Map
signal event_state(ev: String) -> String
signal payout_of(ev: String) -> Int
}
memory {
// verified curtailment per event, MW
curtailed: Map<String, Int> [persistent, consistent]
invariant curtailed >= 0
// dollars paid per event — program cap $1M per event
payout: Map<String, Int> [persistent, consistent]
invariant payout >= 0 && payout <= 1000000
}
state dr_lifecycle {
initial: scheduled
scheduled -> notified // day-ahead notice to participants
notified -> active // curtailment window begins
active -> measured // meter data verified against baseline
measured -> settled // payment posted — TERMINAL
scheduled -> cancelled // called off — TERMINAL, nothing payable
}
on notify_participants(ev: String) {
let r = try { transition(ev, "notified") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", get_status(ev))
}
on begin_curtailment(ev: String) {
let r = try { transition(ev, "active") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", get_status(ev))
}
on meter_data_in(ev: String, verified_mw: Int) {
let r = try { transition(ev, "measured") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
curtailed.set(ev, verified_mw)
return map("ok", true, "verified_mw", verified_mw)
}
on post_payout(ev: String, dollars: Int) {
// payment is only legal from `measured`, and settling consumes it
if get_status(ev) != "measured" {
return map("ok", false, "reason",
"no verified measurement (state: {get_status(ev)})")
}
let w = try { payout.set(ev, dollars) }
if w.error != () { return map("ok", false, "reason", "payout wall: {w.error}") }
transition(ev, "settled")
return map("ok", true, "paid", dollars, "state", get_status(ev))
}
on cancel_event(ev: String) {
let r = try { transition(ev, "cancelled") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", get_status(ev))
}
on event_state(ev: String) { return get_status(ev) }
on payout_of(ev: String) { return payout.get(ev) ?? 0 }
}
cell test DrTests {
rules {
// THE RUMFORD MOVE: collect before anything is measured
assert post_payout("e1", 50000).ok == false
assert_fails transition("e1", "settled")
// run the event properly
assert notify_participants("e1").ok == true
assert begin_curtailment("e1").ok == true
// still no money mid-event — measurement isn't in
assert post_payout("e1", 50000).ok == false
assert meter_data_in("e1", 12).ok == true
assert post_payout("e1", 50000).ok == true
assert payout_of("e1") == 50000
// settled is TERMINAL: no second settlement, no re-opening
assert post_payout("e1", 50000).ok == false
assert_fails transition("e1", "measured")
assert_fails transition("e1", "active")
// a cancelled event is terminal and payable by no path
assert cancel_event("e2").ok == true
assert post_payout("e2", 10).ok == false
assert_fails transition("e2", "notified")
// the ledger walls: no negative clawbacks, no cap-busting checks
assert_fails payout.set("e1", -1)
assert_fails payout.set("e1", 2000000)
assert_fails curtailed.set("e1", -3)
assert payout_of("e1") == 50000
}
}What the toolchain says
$ soma check demand_response.cell
✓ All checks passed.$ soma test demand_response.cell
test DrTests ...
✓ assert post_payout("e1", 50000).ok == false
✓ assert_fails transition("e1", "settled") — raised invalid transition: scheduled → settled. Current state: 'scheduled'. Valid targets: [notified, cancelled]
✓ assert notify_participants("e1").ok == true
✓ assert begin_curtailment("e1").ok == true
✓ assert post_payout("e1", 50000).ok == false
✓ assert meter_data_in("e1", 12).ok == true
✓ assert post_payout("e1", 50000).ok == true
✓ assert payout_of("e1") == 50000
✓ assert post_payout("e1", 50000).ok == false
✓ assert_fails transition("e1", "measured") — raised invalid transition: settled → measured. Current state: 'settled'. Valid targets: []
✓ assert_fails transition("e1", "active") — raised invalid transition: settled → active. Current state: 'settled'. Valid targets: []
✓ assert cancel_event("e2").ok == true
✓ assert post_payout("e2", 10).ok == false
✓ assert_fails transition("e2", "notified") — raised invalid transition: cancelled → notified. Current state: 'cancelled'. Valid targets: []
✓ assert_fails payout.set("e1", -1) — raised memory invariant violated on 'payout': payout >= 0 && payout <= 1000000 — rejected write of -1 (key "e1"); the slot is unchanged
✓ assert_fails payout.set("e1", 2000000) — raised memory invariant violated on 'payout': payout >= 0 && payout <= 1000000 — rejected write of 2000000 (key "e1"); the slot is unchanged
✓ assert_fails curtailed.set("e1", -3) — raised memory invariant violated on 'curtailed': curtailed >= 0 — rejected write of -3 (key "e1"); the slot is unchanged
✓ assert payout_of("e1") == 50000
18 tests: 18 passed, 0 failed$ soma verify demand_response.cell
Verifying demand_response.cell...
State machine 'dr_lifecycle': 6 states, initial 'scheduled'
States: [active, cancelled, measured, notified, scheduled, settled]
✓ 6 states, 5 transitions
✓ all states reachable from 'scheduled'
✓ terminal states: [settled, cancelled]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (5 handlers, 5 literal transitions, 0 dynamic)
✓ termination: all 7 handlers structurally terminate
✓ refinement: handler `notify_participants` ⟶ {notified}
✓ refinement: handler `begin_curtailment` ⟶ {active}
✓ refinement: handler `meter_data_in` ⟶ {measured}
✓ refinement: handler `post_payout` ⟶ {measured → settled}
✓ refinement: handler `cancel_event` ⟶ {cancelled}
· transition sources: `notify_participants`, `begin_curtailment`, `meter_data_in`, `cancel_event` 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)
DrEvent/invariants:
⚠ invariant curtailed >= 0 — runtime-checked (computed values): meter_data_in → curtailed because `verified_mw` is a parameter (narrow it: `require verified_mw >= 0 else …`)
⚠ invariant payout >= 0 && payout <= 1000000 — runtime-checked (computed values): post_payout → payout because `dollars` is a parameter (narrow it: `require dollars >= 0 && dollars <= 1000000 else …`)
12 passed, 2 warnings, 0 failures
Temporal properties for 'dr_lifecycle':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK