soma.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.

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.

Generated from soma describe on this file.

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

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ 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

Builtins used

get_status, map, transition

Source file: /corpus/safety_interlocks/robot_cell_gate.cell · examples/corpus/safety_interlocks/robot_cell_gate.cell