An elevator door + motion interlock
Two facts the machine enforces: the car only moves when doors are shut, and doors only open when the car is idle. The cycle idle -> doors_open -> idle -> moving_up/down -> idle keeps the machine live; `idle` is the recurrent hub every state returns to.
A Soma program from the state_machines part of the verified corpus: 60 lines, cells Elevator, ElevatorTests. It passes soma check with soma 3.2.4.
How it is built
The cell Elevator declares 6 signals in its face: open_doors(id: String) -> String, close_doors(id: String) -> String, go_up(id: String) -> String, go_down(id: String) -> String, arrive(id: String) -> String and phase(id: String) -> String. Its state machine car starts in idle and allows 6 transitions: idle -> doors_open, doors_open -> idle, idle -> moving_up, idle -> moving_down, moving_up -> idle and moving_down -> idle. Handlers: open_doors (line 28), close_doors (line 29), go_up (line 30), go_down (line 31), arrive (line 32) and phase (line 33).
The file also holds 1 test cell (ElevatorTests) with 11 assertions, run by soma test.
The source
elevator.cell
// An elevator door + motion interlock.
// Two facts the machine enforces: the car only moves when doors are shut,
// and doors only open when the car is idle. The cycle
// idle -> doors_open -> idle -> moving_up/down -> idle keeps the machine
// live; `idle` is the recurrent hub every state returns to.
cell Elevator {
face {
signal open_doors(id: String) -> String
signal close_doors(id: String) -> String
signal go_up(id: String) -> String
signal go_down(id: String) -> String
signal arrive(id: String) -> String
signal phase(id: String) -> String
promise "doors only open while idle; car only moves while shut"
}
state car {
initial: idle
idle -> doors_open
doors_open -> idle
idle -> moving_up
idle -> moving_down
moving_up -> idle
moving_down -> idle
}
on open_doors(id: String) { transition(id, "doors_open") return get_status(id) }
on close_doors(id: String) { transition(id, "idle") return get_status(id) }
on go_up(id: String) { transition(id, "moving_up") return get_status(id) }
on go_down(id: String) { transition(id, "moving_down") return get_status(id) }
on arrive(id: String) { transition(id, "idle") return get_status(id) }
on phase(id: String) { return get_status(id) }
}
cell test ElevatorTests {
rules {
// open then close
assert open_doors("e1") == "doors_open"
assert close_doors("e1") == "idle"
// travel up and arrive
assert go_up("e2") == "moving_up"
assert arrive("e2") == "idle"
// travel down and arrive
assert go_down("e3") == "moving_down"
assert arrive("e3") == "idle"
// INTERLOCK: cannot move while doors are open
assert open_doors("e4") == "doors_open"
assert_fails go_up("e4")
assert_fails go_down("e4")
// INTERLOCK: cannot open doors while moving
assert go_up("e5") == "moving_up"
assert_fails open_doors("e5")
}
}What the toolchain says
$ soma check elevator.cell
note: promise on 'Elevator' is documentation (not machine-verifiable): "doors only open while idle; car only moves while shut"
--> elevator.cell:15:17
|
15 | promise "doors only open while idle; car only moves while shut"
| ^
✓ All checks passed (1 note above).$ soma test elevator.cell
test ElevatorTests ...
✓ assert open_doors("e1") == "doors_open"
✓ assert close_doors("e1") == "idle"
✓ assert go_up("e2") == "moving_up"
✓ assert arrive("e2") == "idle"
✓ assert go_down("e3") == "moving_down"
✓ assert arrive("e3") == "idle"
✓ assert open_doors("e4") == "doors_open"
✓ assert_fails go_up("e4") — raised invalid transition: doors_open → moving_up. Current state: 'doors_open'. Valid targets: [idle]
✓ assert_fails go_down("e4") — raised invalid transition: doors_open → moving_down. Current state: 'doors_open'. Valid targets: [idle]
✓ assert go_up("e5") == "moving_up"
✓ assert_fails open_doors("e5") — raised invalid transition: moving_up → doors_open. Current state: 'moving_up'. Valid targets: [idle]
11 tests: 11 passed, 0 failed$ soma verify elevator.cell
Verifying elevator.cell...
State machine 'car': 4 states, initial 'idle'
States: [doors_open, idle, moving_down, moving_up]
✓ 4 states, 6 transitions
✓ all states reachable from 'idle'
✓ reactive machine: no terminal state, and every reachable state can return to 'idle'
✓ no deadlocks
✓ liveness: every reachable state can return to 'idle' (reactive machine)
✓ think-isolated: CTL safety properties hold regardless of LLM output (5 handlers, 5 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
✓ refinement: handler `open_doors` ⟶ {doors_open}
✓ refinement: handler `close_doors` ⟶ {idle}
✓ refinement: handler `go_up` ⟶ {moving_up}
✓ refinement: handler `go_down` ⟶ {moving_down}
✓ refinement: handler `arrive` ⟶ {idle}
· transition sources: `open_doors`, `close_doors`, `go_up`, `go_down`, `arrive` 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)
12 passed, 0 warnings, 0 failures
Temporal properties for 'car':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK