Skip to content

Physical AI

The scene

A learned policy — a VLA model, an RL controller, an LLM planner — proposes a motion command for a mobile manipulator. The proposal is probably fine. "Probably" is not the standard for a robot arm moving near a person. The established pattern is a shield: a deterministic layer between the policy and the actuator that checks each proposed action against a specification of safe states and blocks or attenuates the ones that violate it (Alshiekh et al., "Safe Reinforcement Learning via Shielding", AAAI 2018). The policy stays free to be clever inside the envelope; the envelope is not negotiable.

The 2026 agent-safety literature the research wiki tracks converges on the same shape for software agents — deterministic pre-execution gates over declared constraints and current state (research/neurosymbolic-landscape/pivot-alignment.md, C6): SMT policies checked before a call, temporal-logic monitors over action traces, in-kernel enforcement because "tool-call guardrails cannot intercept system actions that bypass the tool layer," and freshness-bounded approval because a verdict "correct at check time" can be "stale by actuation." A robot makes every one of those concerns physical.

The overlay

Typed preconditions over the world state gate the command. The gate's range constraint on requestedSpeed means a command above the mechanical limit never becomes a fact at all; the rules decide the rest:

# Gallery overlay: a shield for a mobile manipulator's motion commands.
# A learned policy proposes a command; this fragment decides whether it may
# reach the actuator. Thresholds are illustrative teaching values, not a
# safety-standard implementation.

@prefix :      <https://example.org/shield#> .
@prefix horis: <https://w3id.org/horismos#> .
@prefix rdf:   <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs:  <http://www.w3.org/2000/01/rdf-schema#> .
@prefix xsd:   <http://www.w3.org/2001/XMLSchema#> .

## Domain (doc 02)

:MotionCommand a rdfs:Class ;
    rdfs:label "Proposed motion command" .

:requestedSpeed a rdf:Property ;
    rdfs:domain :MotionCommand ; rdfs:range xsd:decimal ;
    horis:unit "m/s" ;
    horis:min 0 ; horis:max 2.0 ;          # the gate refuses anything above the mechanical limit
    horis:cardinality "1" .

:nearestHumanDistance a rdf:Property ;
    rdfs:domain :MotionCommand ; rdfs:range xsd:decimal ;
    horis:unit "m" ;
    horis:min 0 ;
    horis:cardinality "0..1" .

:eStopEngaged a rdf:Property ;
    rdfs:domain :MotionCommand ; rdfs:range xsd:boolean ;
    horis:cardinality "1" .

:Zone a rdfs:Class ;
    horis:oneOf ( :OpenFloor :SharedCell :Restricted ) .

:zone a rdf:Property ;
    rdfs:domain :MotionCommand ; rdfs:range :Zone ;
    horis:cardinality "1" .

:Verdict a rdfs:Class ;
    horis:oneOf ( :Permitted :Attenuated :Blocked ) .

:verdict a rdf:Property ;
    rdfs:domain :MotionCommand ; rdfs:range :Verdict ;
    horis:cardinality "0..1" ;
    horis:assignedBy horis:RulesOnly .   # the policy network cannot mark its own command safe

## Rules (doc 04)

:blockOnEStop a horis:Rule ;
    horis:priority 100 ;
    horis:when [
        horis:subject :MotionCommand ; horis:property :eStopEngaged ; horis:is true
    ] ;
    horis:then [ horis:property :verdict ; horis:value :Blocked ] ;
    horis:explain "Emergency stop is engaged — no motion" .

:blockRestrictedZone a horis:Rule ;
    horis:priority 95 ;
    horis:when [
        horis:subject :MotionCommand ; horis:property :zone ; horis:is :Restricted
    ] ;
    horis:then [ horis:property :verdict ; horis:value :Blocked ] ;
    horis:explain "Motion into a restricted zone is never permitted" .

:blockTooClose a horis:Rule ;
    horis:priority 90 ;
    horis:when [
        horis:subject :MotionCommand ; horis:property :nearestHumanDistance ; horis:below 0.5
    ] ;
    horis:then [ horis:property :verdict ; horis:value :Blocked ] ;
    horis:explain "A person is inside the minimum separation distance" .

:attenuateInSharedCell a horis:Rule ;
    horis:priority 50 ;
    horis:when [
        horis:all (
            [ horis:subject :MotionCommand ; horis:property :eStopEngaged ; horis:is false ]
            [ horis:subject :MotionCommand ; horis:property :zone ; horis:is :SharedCell ]
            [ horis:subject :MotionCommand ; horis:property :requestedSpeed ; horis:exceeds 0.25 ]
            [ horis:subject :MotionCommand ; horis:property :nearestHumanDistance ; horis:atLeast 0.5 ]
        )
    ] ;
    horis:then [ horis:property :verdict ; horis:value :Attenuated ] ;
    horis:explain "Shared cell with a person present — speed is capped, command is attenuated" .

:permitOpenFloor a horis:Rule ;
    horis:priority 10 ;
    horis:when [
        horis:all (
            [ horis:subject :MotionCommand ; horis:property :eStopEngaged ; horis:is false ]
            [ horis:subject :MotionCommand ; horis:property :zone ; horis:is :OpenFloor ]
            [ horis:subject :MotionCommand ; horis:property :nearestHumanDistance ; horis:atLeast 1.0 ]
        )
    ] ;
    horis:then [ horis:property :verdict ; horis:value :Permitted ] ;
    horis:explain "Open floor with clear separation — command permitted as proposed" .

:permitSlowSharedCell a horis:Rule ;
    horis:priority 10 ;
    horis:when [
        horis:all (
            [ horis:subject :MotionCommand ; horis:property :eStopEngaged ; horis:is false ]
            [ horis:subject :MotionCommand ; horis:property :zone ; horis:is :SharedCell ]
            [ horis:subject :MotionCommand ; horis:property :requestedSpeed ; horis:atMost 0.25 ]
            [ horis:subject :MotionCommand ; horis:property :nearestHumanDistance ; horis:atLeast 0.5 ]
        )
    ] ;
    horis:then [ horis:property :verdict ; horis:value :Permitted ] ;
    horis:explain "Shared cell at collaborative speed with separation kept — permitted" .

# PRP-005 completeness-cover:start
# Two regions had no verdict until PRP-005's completeness check named them.
#
# 1. No proximity reading at all: :blockTooClose needs `below 0.5` and both permit
#    rules need `atLeast 0.5`, and a condition over an unassigned property is false
#    (doc 02), so an unread sensor matched nothing. The separation guarantee cannot
#    be established from a missing measurement, so the shield refuses.
:noProximityReadingBlocks a horis:Rule ;
    horis:priority 80 ;
    horis:when [ horis:all (
        [ horis:subject :MotionCommand ; horis:property :eStopEngaged ; horis:is false ]
        [ horis:subject :MotionCommand ; horis:property :zone ; horis:isNot :Restricted ]
        [ horis:subject :MotionCommand ; horis:property :nearestHumanDistance ; horis:isEmpty true ]
    ) ] ;
    horis:then [ horis:property :verdict ; horis:value :Blocked ] ;
    horis:explain "No proximity reading — the minimum separation distance cannot be established, so motion is refused" .

# 2. Open floor with a person between 0.5 m and 1.0 m: :blockTooClose stops below
#    0.5 m and :permitOpenFloor needs 1.0 m of clearance, so the band between them
#    fell through. A person that close on the open floor is a shared cell in all but
#    name, so the two rules below mirror the :SharedCell speed split exactly.
:attenuateOpenFloorNearHuman a horis:Rule ;
    horis:priority 45 ;
    horis:when [ horis:all (
        [ horis:subject :MotionCommand ; horis:property :eStopEngaged ; horis:is false ]
        [ horis:subject :MotionCommand ; horis:property :zone ; horis:is :OpenFloor ]
        [ horis:subject :MotionCommand ; horis:property :requestedSpeed ; horis:exceeds 0.25 ]
        [ horis:subject :MotionCommand ; horis:property :nearestHumanDistance ; horis:atLeast 0.5 ]
        [ horis:subject :MotionCommand ; horis:property :nearestHumanDistance ; horis:below 1.0 ]
    ) ] ;
    horis:then [ horis:property :verdict ; horis:value :Attenuated ] ;
    horis:explain "Open floor but a person is inside the shared-cell distance — speed is capped, command is attenuated" .

:permitSlowOpenFloorNearHuman a horis:Rule ;
    horis:priority 10 ;
    horis:when [ horis:all (
        [ horis:subject :MotionCommand ; horis:property :eStopEngaged ; horis:is false ]
        [ horis:subject :MotionCommand ; horis:property :zone ; horis:is :OpenFloor ]
        [ horis:subject :MotionCommand ; horis:property :requestedSpeed ; horis:atMost 0.25 ]
        [ horis:subject :MotionCommand ; horis:property :nearestHumanDistance ; horis:atLeast 0.5 ]
        [ horis:subject :MotionCommand ; horis:property :nearestHumanDistance ; horis:below 1.0 ]
    ) ] ;
    horis:then [ horis:property :verdict ; horis:value :Permitted ] ;
    horis:explain "Open floor, person beyond the minimum separation, collaborative speed — permitted" .
# PRP-005 completeness-cover:end

The decision, with proof

from horismos import HorismosValidationError, Ontology, World

onto = Ontology.load("examples/gallery/safety-envelope.ttl")
world = World(onto)

def shield(subject: str, **state: object) -> None:
    ref = world.assert_(":MotionCommand", subject=subject, **state)
    proof = world.explain(ref, ":verdict")
    print(proof.render() if proof else f"{subject}: no verdict — command does not proceed")

shield(":cmd-1", requested_speed=1.2, nearest_human_distance=3.4,
       e_stop_engaged=False, zone=":OpenFloor")
shield(":cmd-2", requested_speed=0.8, nearest_human_distance=1.1,
       e_stop_engaged=False, zone=":SharedCell")
shield(":cmd-3", requested_speed=0.2, nearest_human_distance=0.3,
       e_stop_engaged=False, zone=":SharedCell")

:verdict = :Permitted   via permitOpenFloor — "Open floor with clear separation — command permitted as proposed"
  ├─ eStopEngaged false is false   (asserted by the api)
  ├─ zone :OpenFloor is :OpenFloor   (asserted by the api)
  └─ nearestHumanDistance 3.4 atLeast 1.0   (asserted by the api)

:verdict = :Attenuated   via attenuateInSharedCell — "Shared cell with a person present — speed is capped, command is attenuated"
  ├─ eStopEngaged false is false   (asserted by the api)
  ├─ zone :SharedCell is :SharedCell   (asserted by the api)
  ├─ requestedSpeed 0.8 exceeds 0.25   (asserted by the api)
  └─ nearestHumanDistance 1.1 atLeast 0.5   (asserted by the api)

:verdict = :Blocked   via blockTooClose — "A person is inside the minimum separation distance"
  └─ nearestHumanDistance 0.3 below 0.5   (asserted by the api)

Three things a prompt cannot give you. A command over the mechanical limit is refused before any rule runs, in the units the ontology declared. The policy network cannot mark its own command safe. And a command with no distance reading is refused explicitly. An earlier draft of this overlay gave that command no verdict at all and called it safe, on the grounds that an actuator which receives nothing does not move. That is safety resting on silence: it holds only for as long as every consumer downstream — the controller, the retry logic, the operator's dashboard — happens to treat absence as refusal, and nothing in the system says so. verify() reported the region, and closing it required :noProximityReadingBlocks: a :Blocked verdict with a proof that names the reading that never arrived. At an actuator boundary that is the stronger design, because the refusal is now a fact — recomputed with the world, written into the trace, and readable by the auditor — rather than an inference each consumer has to make, correctly, about a value it never saw:

for bad in (dict(requested_speed=3.5, nearest_human_distance=5.0, e_stop_engaged=False, zone=":OpenFloor"),
            dict(requested_speed=0.1, e_stop_engaged=False, zone=":OpenFloor", verdict=":Permitted")):
    try:
        world.assert_(":MotionCommand", subject=":cmd-4", **bad)
    except HorismosValidationError as e:
        print(f"[{e.constraint}] {e}")

shield(":cmd-5", requested_speed=0.1, e_stop_engaged=False, zone=":OpenFloor")

[max] requestedSpeed 3.5 exceeds horis:max 2.0 (m/s) on :MotionCommand
[provenance_refused] verdict may only be assigned by rules (horis:assignedBy horis:RulesOnly); assertion came from the api
:verdict = :Blocked   via noProximityReadingBlocks — "No proximity reading — the minimum separation distance cannot be established, so motion is refused"
  ├─ eStopEngaged false is false   (asserted by the api)
  ├─ zone isNot :Restricted   (closed world)
  └─ nearestHumanDistance isEmpty   (closed world)

The emergency stop is engaged while :cmd-1 is standing. Its verdict is recomputed in the transaction that recorded the stop — there is no window in which a previously permitted command remains permitted under a changed world:

shield(":cmd-1", e_stop_engaged=True)

:verdict = :Blocked   via blockOnEStop — "Emergency stop is engaged — no motion"
  └─ eStopEngaged true is true   (asserted by the api)

Why verification matters here

A shield is only as good as its coverage, and coverage is what verify() proves. Completeness asks whether every reachable combination of zone, speed, distance and e-stop state gets a verdict, and when the check first ran against this overlay it returned two regions that had none. The first: "no verdict assigned when requestedSpeed ∈ [0, 0.25) and nearestHumanDistance < 0 and eStopEngaged is false and zone is :SharedCell" — a shared-cell command with no proximity reading at all, because :blockTooClose needs below 0.5 and both permit rules need atLeast 0.5, and a condition over an unassigned property is false. The second was narrower and easier to miss by eye: an open-floor command with a person between 0.5 m and 1.0 m, falling between :blockTooClose and :permitOpenFloor's 1.0 m of required clearance. Closing them is what :noProximityReadingBlocks and the two :OpenFloor rules in the overlay are for — a missing measurement is refused outright, and a person inside the shared-cell distance is treated as a shared cell whatever the zone label says. Conflict-freedom names every pair of rules that can match one command with different verdicts, and it named three: blockOnEStop (priority 100) against each of attenuateInSharedCell, permitOpenFloor and permitSlowSharedCell — including the open-floor-with-clear-separation case that is exactly the :cmd-1 transition above. Priority already resolved all three in favour of blocking; the witness ("blockOnEStop wins by priority; confirm intended") asked for that ordering to be confirmed rather than assumed, and the three rules now carry an explicit eStopEngaged is false guard that says in the condition what priority was saying silently. Dead-rule detection catches a speed threshold above horis:max; non-vacuity flags a constraint that excludes no reachable value.

What it does not claim: anything about the sensor that produced nearestHumanDistance, the controller that executes an attenuated command, or the physical world between check and actuation. Those are the adapter's and the deployer's, and the assumption manifest lists the unverified external effects explicitly.

Status and honest edges

  • Runs today with structured input at the decision level. Nothing in Horismos runs at control-loop rates or replaces a certified safety PLC; this is the supervisory decision layer between a planner and an actuator interface, and the framework's own posture is that OS- and hardware-level isolation stays the deployer's.
  • The freshness concern is the physical version of the snapshot-scoped guarantee: a verdict is exact for the world state it was given, and the runtime recomputes on every change it is told about. What it is not told about, it cannot gate (Guarantees).
  • Thresholds are teaching values. A real cell derives them from its risk assessment and the applicable standards; the overlay shape is what stays the same.