Robot cell gate — full-speed automation only behind a closed gate
A 21-year-old contractor died inside a robot cell at a German auto plant in 2015, struck by an arm that should never have been live with a person inside the fence. ISO 10218 guard interlocking says the gate and the robot mode are ONE state: here `auto_run` exists only behind a closed gate, opening the gate from auto requires the safety-stop edge FIRST, and there is no {gate open, full speed} state to race into. Inside the fence the robot may move only in teach mode, and the speed ledger structurally caps teach motion at the 250 mm/s collaborative limit — a faster write is refused by the memory.
A Soma program from the safety_interlocks part of the verified corpus: 84 lines, cells RobotCell, RobotCellTests. It passes soma check with soma 3.2.4.
How it is built
The cell RobotCell declares 5 signals in its face: close_gate(id: String) -> String, start_auto(id: String) -> String, safety_stop(id: String) -> String, unlock_gate(id: String) -> Map and teach_move(id: String, mm_s: Int) -> Map; keeps 1 memory slot: teach_mm_s (Map<String, Int>, persistent and consistent) under the invariant teach_mm_s >= 0 && teach_mm_s <= 250. Its state machine guard starts in gate_open_teach and allows 4 transitions: gate_open_teach -> gate_closed_standstill, gate_closed_standstill -> gate_open_teach, gate_closed_standstill -> auto_run and auto_run -> gate_closed_standstill. Handlers: close_gate (line 35), start_auto (line 36), safety_stop (line 37), unlock_gate (line 39) and teach_move (line 48).
The file also holds 1 test cell (RobotCellTests) with 11 assertions, run by soma test.
The source
robot_cell_gate.cell
// ROBOT CELL GATE — full-speed automation only behind a closed gate.
// A 21-year-old contractor died inside a robot cell at a German auto
// plant in 2015, struck by an arm that should never have been live with
// a person inside the fence. ISO 10218 guard interlocking says the gate
// and the robot mode are ONE state: here `auto_run` exists only behind a
// closed gate, opening the gate from auto requires the safety-stop edge
// FIRST, and there is no {gate open, full speed} state to race into.
// Inside the fence the robot may move only in teach mode, and the speed
// ledger structurally caps teach motion at the 250 mm/s collaborative
// limit — a faster write is refused by the memory.
cell RobotCell {
face {
signal close_gate(id: String) -> String
signal start_auto(id: String) -> String
signal safety_stop(id: String) -> String
signal unlock_gate(id: String) -> Map
signal teach_move(id: String, mm_s: Int) -> Map
}
memory {
// tool speed with the gate open, mm/s — ISO/TS 15066 limit
teach_mm_s: Map<String, Int> [persistent, consistent]
invariant teach_mm_s >= 0 && teach_mm_s <= 250
}
state guard {
initial: gate_open_teach // person may be inside; reduced speed
gate_open_teach -> gate_closed_standstill
gate_closed_standstill -> gate_open_teach
gate_closed_standstill -> auto_run // full speed ONLY from here
auto_run -> gate_closed_standstill // safety stop BEFORE unlock
}
on close_gate(id: String) { transition(id, "gate_closed_standstill") return get_status(id) }
on start_auto(id: String) { transition(id, "auto_run") return get_status(id) }
on safety_stop(id: String) { transition(id, "gate_closed_standstill") return get_status(id) }
on unlock_gate(id: String) {
// guard locking: the gate only releases from standstill
let r = try { transition(id, "gate_open_teach") }
if r.error != () {
return map("ok", false, "reason", "robot not at standstill — gate stays locked")
}
return map("ok", true, "state", get_status(id))
}
on teach_move(id: String, mm_s: Int) {
if get_status(id) != "gate_open_teach" {
return map("ok", false, "reason", "teach motion only in teach mode")
}
let w = try { teach_mm_s.set(id, mm_s) }
if w.error != () {
return map("ok", false, "reason", "{mm_s} mm/s exceeds the 250 mm/s teach limit")
}
return map("ok", true, "mm_s", mm_s)
}
}
cell test RobotCellTests {
rules {
// full speed with the gate open: the state does not exist
assert_fails transition("r1", "auto_run")
// teach motion is capped by the memory itself
assert teach_move("r1", 200).ok == true
assert teach_move("r1", 900).ok == false
assert_fails teach_mm_s.set("r1", 251)
// lawful start: close the gate, then auto
assert close_gate("r1") == "gate_closed_standstill"
assert start_auto("r1") == "auto_run"
// the gate will not unlock around a moving robot
assert unlock_gate("r1").ok == false
assert_fails transition("r1", "gate_open_teach")
// stop first, then the gate releases — and teach speed still capped
assert safety_stop("r1") == "gate_closed_standstill"
assert unlock_gate("r1").ok == true
assert teach_move("r1", 250).ok == true
}
}What the toolchain says
$ soma check robot_cell_gate.cell
✓ All checks passed.$ soma test robot_cell_gate.cell
test RobotCellTests ...
✓ assert_fails transition("r1", "auto_run") — raised invalid transition: gate_open_teach → auto_run. Current state: 'gate_open_teach'. Valid targets: [gate_closed_standstill]
✓ assert teach_move("r1", 200).ok == true
✓ assert teach_move("r1", 900).ok == false
✓ assert_fails teach_mm_s.set("r1", 251) — raised memory invariant violated on 'teach_mm_s': teach_mm_s >= 0 && teach_mm_s <= 250 — rejected write of 251 (key "r1"); the slot is unchanged
✓ assert close_gate("r1") == "gate_closed_standstill"
✓ assert start_auto("r1") == "auto_run"
✓ assert unlock_gate("r1").ok == false
✓ assert_fails transition("r1", "gate_open_teach") — raised invalid transition: auto_run → gate_open_teach. Current state: 'auto_run'. Valid targets: [gate_closed_standstill]
✓ assert safety_stop("r1") == "gate_closed_standstill"
✓ assert unlock_gate("r1").ok == true
✓ assert teach_move("r1", 250).ok == true
11 tests: 11 passed, 0 failed$ soma verify robot_cell_gate.cell
Verifying robot_cell_gate.cell...
State machine 'guard': 3 states, initial 'gate_open_teach'
States: [auto_run, gate_closed_standstill, gate_open_teach]
✓ 3 states, 4 transitions
✓ all states reachable from 'gate_open_teach'
✓ reactive machine: no terminal state, and every reachable state can return to 'gate_open_teach'
✓ no deadlocks
✓ liveness: every reachable state can return to 'gate_open_teach' (reactive machine)
✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 4 literal transitions, 0 dynamic)
✓ termination: all 5 handlers structurally terminate
✓ refinement: handler `close_gate` ⟶ {gate_closed_standstill}
✓ refinement: handler `start_auto` ⟶ {auto_run}
✓ refinement: handler `safety_stop` ⟶ {gate_closed_standstill}
✓ refinement: handler `unlock_gate` ⟶ {gate_open_teach}
· transition sources: `close_gate`, `start_auto`, `safety_stop`, `unlock_gate` 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)
RobotCell/invariants:
⚠ invariant teach_mm_s >= 0 && teach_mm_s <= 250 — runtime-checked (computed values): teach_move → teach_mm_s because `mm_s` is a parameter (narrow it: `require mm_s >= 0 && mm_s <= 250 else …`)
11 passed, 1 warnings, 0 failures
Temporal properties for 'guard':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK