Can Formal Methods Govern AI-Generated Robot Actions?
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, runtime compliance over agent traces, 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:
{
"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, 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, 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 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:
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:
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.
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.
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, 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 offers an interesting direction for representing that uncertainty while retaining the deterministic envelope as a separate layer.
Related research such as 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. 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:
- Robotics policy-prover project source
- Machine-readable DGX Spark benchmark results
- Machine-readable Terra planning-loop sample
- NVIDIA OpenShell
- ENPIRE: Agentic Robot Policy Self-Improvement in the Real World
- Z3 theorem prover
- Safe Reinforcement Learning via Shielding
- Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning
- Agent Behavioral Contracts
- Runtime Compliance Verification for AI Agents
- VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation
- Efficient and Sound Probabilistic Verification for AI Agents