*We built a small robotics experiment to test whether OpenShell's formal
methods-based policy enforcement can govern robot plans generated by local and
frontier AI models.*
OpenShell uses formal methods-based policy enforcement to constrain what AI
agents can do in digital environments. We wanted to see whether a similar
approach could govern the higher-level plans local and frontier models generate
for robots.
To explore that question, we built a small robotics pick-and-place experiment.
The task is intentionally simple: move a green block into a blue tray. An AI
planner proposes a sequence of 3D waypoints, and a policy prover checks the path
before the simulated tool head moves. The checks cover workspace limits, a
restricted volume, human proximity, sensor freshness, delegated authority,
force, and task budget.
Formal methods are attracting renewed attention as AI systems become agents.
Recent work is exploring
[behavioral contracts](https://arxiv.org/abs/2602.22302),
[runtime compliance over agent traces](https://arxiv.org/abs/2606.19242), and
other ways to turn desired behavior into specifications an external system can
check. Many familiar approaches focus on making the model itself more reliable:
better instructions, safer training, stronger evaluations, or another model
acting as a judge. Those remain important layers. This experiment looks at a
complementary question: can a separate system check a proposed physical action
before it reaches a simulator or robot?
For this prototype, we split responsibility this way:
- The agent proposes a plan it believes will accomplish the task.
- An independent, deterministic policy boundary sits between that plan and the
simulated actuator.
- A rejection returns structured evidence the agent can use to revise its plan.
- Only a version admitted by the policy boundary reaches the executor, with any
returned constraints and runtime obligations attached.
We set out to learn whether that check could return useful feedback to the
planner and run quickly enough to fit a robot-planning loop driven by an AI
model.
---
## The Experiment
The recorded run follows four steps: propose, check, adapt, execute.
First, GPT-5.6 Terra proposes a waypoint path whose direct route crosses the red
restricted volume. The policy service denies the action, identifies
`restricted_zone_intersection`, returns an approximate counterexample point,
and supplies a minimum bypass height. Nothing moves.
The planning loop sends that decision packet back to the model, which proposes
a route around the restricted volume. Before execution, the world changes: a
human enters the caution radius. The policy service evaluates the action again
and changes the contract. The path may proceed, but only at a speed of 0.08 m/s
or less, with an obligation to pause if the human gets closer.
The executor runs the revised path with the returned speed limit. In this run,
the planning loop could propose and revise a path, while the policy boundary
determined which version reached the simulated actuator.
Here is an example decision packet:
```json
{
"decision": "deny",
"violations": ["restricted_zone_intersection"],
"constraints": {
"bypass_z_min": 0.55
},
"obligations": ["emit_audit_event"],
"counterexample": {
"segment_id": "proposed_segment",
"zone_id": "restricted_zone.alpha",
"reason": "restricted_zone_intersection",
"point": [-0.18, 0.35, -0.20]
}
}
```
In this demo, that response gives the planner more to work with than a generic
"unsafe" error. It serves as both an enforcement decision for the executor and
machine-readable feedback for replanning.
---
## Why Check the Proposed Action?
This experiment applies formal methods to the concrete action proposed by the
planner.
This resembles the formal-methods idea of a *shield*. In
[safe reinforcement learning via shielding](https://ojs.aaai.org/index.php/AAAI/article/view/11797),
a learned policy proposes actions while a reactive system monitors them and
intervenes when one would violate a formal specification. Our prototype tests a
similar division of work with an agent-generated robot path.
Agent systems broaden that idea. A proposed action may be a shell command, a
network request, a delegated capability, a financial transaction, or a robot
trajectory. One useful formal object is a typed description of the action, the
relevant state, and the invariant the surrounding system is expected to
enforce—not the model's prose or chain of thought.
The design also resembles the reference-monitor pattern emphasized in recent
agent-security research. For example, [VeriGuard](https://research.google/pubs/veriguard-enhancing-llm-agent-safety-via-verified-code-generation/),
work by Dj Dvijotham and collaborators at Google DeepMind, separates rigorous
policy validation from a lightweight runtime monitor that checks each proposed
action before execution. Applied to robotics, the open systems question is
whether the monitor can cover the relevant paths from a planner's output to an
actuator command.
A robotics-focused prototype gives us a few key design goals to investigate:
- **Close to the effect.** Check the plan after intent becomes a concrete
action, but before the simulator or robot moves.
- **Compositional.** Evaluate overlapping concerns such as workspace,
authority, sensor freshness, human proximity, budget, speed, and force
together.
- **Constructive.** Return a failed invariant, counterexample, or narrower
contract so the agent can improve its plan rather than guess.
Any guarantee from the prototype remains relative to its specification and
world model. Work
on [safe reinforcement learning through proof and learning](https://ojs.aaai.org/index.php/AAAI/article/view/12107)
makes the same essential point: formal verification provides confidence relative
to a model, and cyber-physical reality will always test the completeness of that
model. For this experiment, that means stating the property, assumptions, and
enforcement point precisely, then testing where each breaks down as the
environment becomes more realistic.
---
## How the Prototype Works
OpenShell's architecture is designed to move security policy out of the agent
and into the environment that mediates its actions. A sandboxed agent can
reason, write code, call tools, and delegate work, but filesystem, network,
process, and inference authority are enforced by infrastructure the agent does
not control.
This experiment explores whether the same architectural move can extend from
the digital domain—such as coding or cybersecurity—to physical actions. The
question becomes: can this particular motion safely run, with this object, at
this speed, given the world state we have now?
The prototype expresses each request as an action envelope with multiple,
often-overlapping rules:
```text
actor and delegated subagent
action and target resource
start, end, and waypoint path
requested speed and force
object identity and class
capability grant
human distance and sensor age
restricted and caution volumes
remaining task budget
```
The service turns that envelope into one of four decisions:
- `allow`: execute the proposed action.
- `deny`: do not execute; return violations and a counterexample when possible.
- `allow_with_constraints`: execute only inside narrower speed, force, or path
bounds.
- `approval_required`: stop at a human decision point.
The result also contains obligations for the executor. In this prototype, the
executor applies returned speed and force limits, emits an audit event, and
checks the human-distance pause condition immediately before motion. Continuous
monitoring during execution is part of the next simulator integration, not a
property of this first version.
The prototype divides responsibility this way:
```text
agent runtime propose and revise the plan
policy service decide and return an action contract
executor enforce the contract and emit evidence
```
The policy check admits a plan or short-horizon physical action before execution.
Once admitted, the robot's existing controller remains responsible for the
low-level control loop. The solver is an action-admission boundary; it is not a
motor controller.
---
## Prover Latency
One way to review an AI-generated robot plan is to ask another model whether it
looks safe. An LLM-as-judge can add useful semantic review, but it is another
probabilistic inference call. If it takes as long as the planning model, it can
nearly double the inference time.
The first Terra path was invalid and had to be regenerated regardless of which
review method caught it. The useful comparison is therefore the time spent
checking the plans, not one plan versus two.
The prover runs locally and has a narrower job: evaluate explicit invariants
and return a deterministic admission decision. In ten complete browser
missions, **`openai/openai/gpt-5.6-terra`** generated both the initial and
corrected plans. All ten completed the deny, replan, constrain, and execute flow
without a fixture fallback.
Generating the two plans took **7.53 to 16.90 seconds** per mission. Proving
both plans took **5.76 to 26.23 ms**, with a **17.30 ms median**—or
**0.05–0.26%** of the observed inference time. Model planning varied by seconds;
policy admission remained in milliseconds.
Policy-prover time as a share of AI inference across ten sequential Terra missions. This is not a general benchmark of the model or serving endpoint.
We also isolated the policy decision in a release-mode benchmark on an **NVIDIA
DGX Spark**. Across allow, deny, and constrained outcomes with 3 to 48
waypoints, p95 latency was **1.006–1.250 ms**. Each of the 15 cases used 5,000
measured decisions after 1,000 warm-ups. Against an illustrative 100 ms model
call, the slowest p95 would add about **1.25%**. Against the multi-second
calls observed in this experiment, the share is much smaller.
Release-mode p95 policy latency on NVIDIA DGX Spark.
The Spark benchmark isolates geometry checks and Z3 setup/checking; it excludes
model inference, transport, rendering, and execution. It supports using the
prover at an AI model's planning cadence, where a model proposes a path or
short-horizon action. It does not establish a hard real-time guarantee, and it
does not move balance, torque, or joint control out of the robot's dedicated
controllers and safety systems.
---
## What the Prototype Verifies
The current implementation combines deterministic Rust checks with an
SMT-backed policy check using Z3. Rust derives facts about workspace bounds,
sampled segment/zone intersections, sensor freshness, budget, authority, human
proximity, speed, and force. Z3 composes those Boolean facts into exactly one of
the four policy outcomes with a bounded timeout. The model returned by Z3 is the
source of the verdict; an unknown, inconsistent, or ambiguous result fails
closed. Malformed action envelopes are rejected before they reach the solver.
Rust then constructs the typed decision packet and supporting evidence.
The current scope is a sampled tool-head path. It does not yet encode full-body
geometry, kinematics, dynamics, braking distance, or perception uncertainty.
Its guarantee also depends on complete mediation and accurate world state; an
unobserved route to the actuator or a bad sensor value can invalidate the
decision.
This is a research prototype, not a safety-rated system or proof that a real
trajectory is collision-free. The next steps are richer symbolic trajectory
constraints, a real motion planner, and continuous runtime monitoring.
---
## Next Experiments
The first results are encouraging, and this is an area we are actively exploring
with partners around [OpenShell](https://github.com/NVIDIA/OpenShell), an
Apache-2.0, community-driven project.
Version one uses a Three.js workcell deliberately. Keeping the environment
small let us focus on the policy contract and prover rather than simulator
integration. The next parts of this research series will carry the boundary
into NVIDIA Isaac Sim and MuJoCo, where we can test richer robot geometry,
dynamics, perception, trajectory constraints, and changing world state before
moving to a small physical platform.
Physical perception also makes some policy predicates probabilistic rather than
crisp. A human detector, distance estimate, occupancy map, or object classifier
can be wrong, and their errors may be correlated. Recent work by Dvijotham and
collaborators on
[sound probabilistic verification for AI agents](https://arxiv.org/abs/2606.20510)
offers an interesting direction for representing that uncertainty while
retaining the deterministic envelope as a separate layer.
Related research such as
[ENPIRE](https://research.nvidia.com/labs/gear/enpire/) shows coding agents
managing repeated real-world robot-policy improvement across reset,
verification, rollout, and evolution. That raises a useful question for future
experiments:
> Can an agent optimize a robot policy while the governing invariants remain
> outside the agent's control?
We want to test that pattern with richer dynamics, uncertain perception, longer
plans, and eventually real hardware.
---
## Research Questions and Collaboration
We would like to study how formal specifications hold up under changing world
state, whether constructive counterexamples improve replanning, and how an
admitted contract can be carried reliably into a simulator or actuator.
If you are working on SMT, temporal logic, runtime verification, control barrier
functions, motion planning, digital twins, robot learning, or runtime assurance
for agents, we would like to compare models and workloads. Some useful next
experiments may come from connecting these communities rather than treating
agent security and physical safety as separate problems.
---
## Run and Extend the Experiment
The complete prototype, local setup, benchmark harness, machine-readable
results, and Dev Note live together in the
[OpenShell Research repository](https://github.com/NVIDIA/OpenShell-Research/tree/main/projects/robotics-policy-prover).
The default fixture mode reproduces the interaction without model credentials;
the optional agent mode can be used to explore different planners. We welcome
new policy encodings, adversarial workloads, simulator adapters, and benchmark
results through the normal OpenShell Research contribution process.
Resources:
1. [Robotics policy-prover project source](https://github.com/NVIDIA/OpenShell-Research/tree/main/projects/robotics-policy-prover)
2. [Machine-readable DGX Spark benchmark results](https://github.com/NVIDIA/OpenShell-Research/blob/main/projects/robotics-policy-prover/benchmarks/policy-latency.json)
3. [Machine-readable Terra planning-loop sample](https://github.com/NVIDIA/OpenShell-Research/blob/main/projects/robotics-policy-prover/benchmarks/terra-planning-loop.json)
4. [NVIDIA OpenShell](https://github.com/NVIDIA/OpenShell)
5. [ENPIRE: Agentic Robot Policy Self-Improvement in the Real World](https://research.nvidia.com/labs/gear/enpire/)
6. [Z3 theorem prover](https://github.com/Z3Prover/z3)
7. [Safe Reinforcement Learning via Shielding](https://ojs.aaai.org/index.php/AAAI/article/view/11797)
8. [Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning](https://ojs.aaai.org/index.php/AAAI/article/view/12107)
9. [Agent Behavioral Contracts](https://arxiv.org/abs/2602.22302)
10. [Runtime Compliance Verification for AI Agents](https://arxiv.org/abs/2606.19242)
11. [VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation](https://research.google/pubs/veriguard-enhancing-llm-agent-safety-via-verified-code-generation/)
12. [Efficient and Sound Probabilistic Verification for AI Agents](https://arxiv.org/abs/2606.20510)
