Governed motion — admission before actuation

A manipulator that cannot be commanded without a policy decision. Every intent is evaluated during Reasoning; a refusal returns to Idle without entering Planning or Executing, so the arm has no path to motion that skips the gate.
A demonstrator, not an experiment. A two-link planar arm and a discrete lifecycle model: no physics, no hardware, no sensing. The policies, the workcell, and the conditions that trigger a refusal were all written by the same hand, so what you are watching is an architecture doing what it was constructed to do — this is not evidence that a real robot is safer.

Two things it assumes away in particular. The supervisor is handed true workcell state directly, whereas in a real cell the hard question is whether the workspace is occupied — sensing, latency, partial observability. And authorization here can never go stale, because facts are re-resolved every tick; leases, revocation and mid-motion re-checking are not modelled at all. The compile-time guarantee also binds only code routed through this crate's interface: a vendor SDK, a separate process, or firmware sits outside it entirely.

This layer would sit above functional safety — interlocks, e-stops, safety-rated controllers — and never replaces any of it.

Workcell

completed 0 refused 0 queued 0 t 0.0s

Trace — every event carries its intent's id

Lifecycle

The gate sits between Reasoning and Planning. Nothing to its right runs for a refused intent.
no decision yet

Environment — change it and watch the next decision

Lock the sterile zone and the next transfer to the bench is refused before the arm moves — the arm simply never starts.

Runtime invariants

The faults corrupt a copy of the record, never the running system. Each one should drop exactly one invariant — that is what shows the checker discriminates instead of always agreeing.