Reefer setpoint — the typo that thaws forty tonnes of tuna
Refrigerated containers are programmed by hand at the terminal: a tech keys the setpoint from the booking sheet. The classic, expensive typo is sign and unit confusion — +18 instead of -18 (cargo claims files are full of them), or a Fahrenheit value keyed into a Celsius controller. Frozen tuna, ice cream, plasma: one transposed character and the claim runs to hundreds of thousands of dollars, discovered three weeks later at the destination port. This controller's setpoint memory carries the frozen-cargo envelope as an invariant: nothing outside [-30, -10] C can ever BE the setpoint. The +18 typo isn't caught by a validator someone forgot to call on one code path — the memory itself refuses, and the reefer keeps its last safe value. Power state is a verified machine: you cannot program a unit that isn't on, and a tripped unit must be inspected before reuse.
A Soma program from the logistics part of the verified corpus: 111 lines, cells ReeferController, FrozenEnvelope. It passes soma check with soma 3.2.4.
How it is built
The cell ReeferController declares 6 signals in its face: power_on(unit: String) -> Map, program_setpoint(unit: String, celsius: Int) -> Map, trip_alarm(unit: String) -> Map, inspect_unit(unit: String) -> Map, setpoint_of(unit: String) -> Int and unit_state(unit: String) -> String; keeps 1 memory slot: setpoint_c (Map<String, Int>, persistent and consistent) under the invariant setpoint_c >= -30 && setpoint_c <= -10. Its state machine reefer starts in unpowered and allows 5 transitions: unpowered -> running, running -> unpowered, running -> tripped, tripped -> under_inspection and under_inspection -> unpowered. Handlers: power_on (line 46), program_setpoint (line 52), trip_alarm (line 65), inspect_unit (line 71), setpoint_of (line 78) and unit_state (line 79).
The file also holds 1 test cell (FrozenEnvelope) with 16 assertions, run by soma test.
The source
reefer_setpoint.cell
// ============================================================================
// REEFER SETPOINT — the typo that thaws forty tonnes of tuna
// ============================================================================
//
// Refrigerated containers are programmed by hand at the terminal: a tech
// keys the setpoint from the booking sheet. The classic, expensive typo
// is sign and unit confusion — +18 instead of -18 (cargo claims files are
// full of them), or a Fahrenheit value keyed into a Celsius controller.
// Frozen tuna, ice cream, plasma: one transposed character and the claim
// runs to hundreds of thousands of dollars, discovered three weeks later
// at the destination port.
//
// This controller's setpoint memory carries the frozen-cargo envelope as
// an invariant: nothing outside [-30, -10] C can ever BE the setpoint.
// The +18 typo isn't caught by a validator someone forgot to call on one
// code path — the memory itself refuses, and the reefer keeps its last
// safe value. Power state is a verified machine: you cannot program a
// unit that isn't on, and a tripped unit must be inspected before reuse.
// ============================================================================
cell ReeferController {
face {
signal power_on(unit: String) -> Map
signal program_setpoint(unit: String, celsius: Int) -> Map
signal trip_alarm(unit: String) -> Map
signal inspect_unit(unit: String) -> Map
signal setpoint_of(unit: String) -> Int
signal unit_state(unit: String) -> String
}
memory {
// frozen-cargo envelope, deg C. The +18 typo cannot exist here.
setpoint_c: Map<String, Int> [persistent, consistent]
invariant setpoint_c >= -30 && setpoint_c <= -10
}
state reefer {
initial: unpowered
unpowered -> running
running -> unpowered
running -> tripped
tripped -> under_inspection
under_inspection -> unpowered
}
on power_on(unit: String) {
let r = try { transition(unit, "running") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "unit", unit, "state", "running")
}
on program_setpoint(unit: String, celsius: Int) {
if get_status(unit) != "running" {
let s = get_status(unit)
return map("ok", false, "reason", "unit {unit} is {s} — cannot program")
}
let w = try { setpoint_c.set(unit, celsius) }
if w.error != () {
return map("ok", false,
"reason", "REFUSED: {celsius} C is outside the frozen envelope [-30, -10]")
}
return map("ok", true, "unit", unit, "setpoint_c", celsius)
}
on trip_alarm(unit: String) {
let r = try { transition(unit, "tripped") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "unit", unit, "state", "tripped")
}
on inspect_unit(unit: String) {
let r = try { transition(unit, "under_inspection") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
transition(unit, "unpowered")
return map("ok", true, "unit", unit, "state", "unpowered")
}
on setpoint_of(unit: String) { return setpoint_c.get(unit) ?? -18 }
on unit_state(unit: String) { return get_status(unit) }
}
cell test FrozenEnvelope {
rules {
// programmed correctly for frozen tuna
assert power_on("RF-201").ok == true
assert program_setpoint("RF-201", -18).ok == true
assert setpoint_of("RF-201") == -18
// THE TYPO: +18. The memory refuses; last safe value survives.
assert program_setpoint("RF-201", 18).ok == false
assert setpoint_of("RF-201") == -18
assert_fails setpoint_c.set("RF-201", 18)
assert_fails setpoint_c.set("RF-201", -45)
// boundary values of the envelope are legal
assert program_setpoint("RF-201", -30).ok == true
assert program_setpoint("RF-201", -10).ok == true
assert program_setpoint("RF-201", -9).ok == false
// you cannot program a unit that is not running
assert program_setpoint("RF-999", -18).ok == false
// a tripped unit must pass inspection before it runs again
assert trip_alarm("RF-201").ok == true
assert program_setpoint("RF-201", -20).ok == false
assert_fails transition("RF-201", "running")
assert inspect_unit("RF-201").ok == true
assert power_on("RF-201").ok == true
}
}What the toolchain says
$ soma check reefer_setpoint.cell
✓ All checks passed.$ soma test reefer_setpoint.cell
test FrozenEnvelope ...
✓ assert power_on("RF-201").ok == true
✓ assert program_setpoint("RF-201", -18).ok == true
✓ assert setpoint_of("RF-201") == -18
✓ assert program_setpoint("RF-201", 18).ok == false
✓ assert setpoint_of("RF-201") == -18
✓ assert_fails setpoint_c.set("RF-201", 18) — raised memory invariant violated on 'setpoint_c': setpoint_c >= -30 && setpoint_c <= -10 — rejected write of 18 (key "RF-201"); the slot is unchanged
✓ assert_fails setpoint_c.set("RF-201", -45) — raised memory invariant violated on 'setpoint_c': setpoint_c >= -30 && setpoint_c <= -10 — rejected write of -45 (key "RF-201"); the slot is unchanged
✓ assert program_setpoint("RF-201", -30).ok == true
✓ assert program_setpoint("RF-201", -10).ok == true
✓ assert program_setpoint("RF-201", -9).ok == false
✓ assert program_setpoint("RF-999", -18).ok == false
✓ assert trip_alarm("RF-201").ok == true
✓ assert program_setpoint("RF-201", -20).ok == false
✓ assert_fails transition("RF-201", "running") — raised invalid transition: tripped → running. Current state: 'tripped'. Valid targets: [under_inspection]
✓ assert inspect_unit("RF-201").ok == true
✓ assert power_on("RF-201").ok == true
16 tests: 16 passed, 0 failed$ soma verify reefer_setpoint.cell
Verifying reefer_setpoint.cell...
State machine 'reefer': 4 states, initial 'unpowered'
States: [running, tripped, under_inspection, unpowered]
✓ 4 states, 5 transitions
✓ all states reachable from 'unpowered'
✓ reactive machine: no terminal state, and every reachable state can return to 'unpowered'
✓ no deadlocks
✓ liveness: every reachable state can return to 'unpowered' (reactive machine)
✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 4 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
✓ refinement: handler `power_on` ⟶ {running}
✓ refinement: handler `trip_alarm` ⟶ {tripped}
✓ refinement: handler `inspect_unit` ⟶ {under_inspection, unpowered}
· transition sources: `power_on`, `trip_alarm`, `inspect_unit` 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)
ReeferController/invariants:
⚠ invariant setpoint_c >= -30 && setpoint_c <= -10 — runtime-checked (computed values): program_setpoint → setpoint_c because `celsius` is a parameter (narrow it: `require celsius >= -30 && celsius <= -10 else …`)
10 passed, 1 warnings, 0 failures
Temporal properties for 'reefer':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK