Can Formal Methods Govern AI-Generated Robot Actions? An OpenShell-Inspired Experiment

Dev Note August 7, 2026 Physical AI

We built a small robotics experiment to test whether OpenShell's approach to policy enforcement can be applied to AI-generated robot plans.

A simulated robot workcell showing a denied six-waypoint path through a red restricted volume and the policy prover's 8.74 millisecond decision.

OpenShell uses policy enforcement to constrain what AI agents can do in digital environments. We wanted to see whether a similar approach could be applied to plans generated for a robot.

To explore that question, we built a small 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 into an agent's planning loop.

Architecture diagram showing an AI agent inside a sandboxed agent runtime. Every proposed plan or short-horizon action passes through a Rust and Z3 action-admission prover that denies it with feedback or admits a constrained contract to either a simulation or a real-world robot. Dedicated controllers retain responsibility for low-level control, while changing world state feeds admission and runtime enforcement. — The agent's plan passes through deterministic action admission before an admitted contract reaches a simulated or real-world environment. Low-level robot control remains outside the prover's planning-cadence role.

The Recorded Experiment

The recorded run follows four steps: propose, check, adapt, execute.

First, the agent proposes a six-waypoint path at 0.35 m/s. One of its segments 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 uses that decision packet to produce a six-waypoint route around the restricted volume at 0.18 m/s. 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.

The decision packet looks like this:

{
  "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.78, -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 does not attempt to explain or verify everything happening inside a model. It applies formal methods to a narrower artifact: 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.

The prototype gives us six design goals to investigate:

Complete mediation. Every policy-relevant path to an external effect passes through the decision point.
Independent. The agent cannot edit, bypass, or reinterpret the policy that governs it.
Auditable. The trusted decision surface stays small enough to model, test, and verify.
Close to the effect. The check occurs after intent becomes a concrete action but before an external side effect.
Compositional. Workspace, authority, freshness, human proximity, budget, speed, and force rules can combine into one decision.
Constructive. A denial includes a failed invariant, counterexample, or narrower admissible contract so the agent can replan 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 points toward stating the property, assumptions, and enforcement point precisely—and testing where each one breaks down as the environment becomes more realistic.

How the Prototype Works

OpenShell moves 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 to the physical action domain. The question is not only, "May this agent call the robot service?" It is also, "May this particular motion run, with this object, at this speed, given the world state we have now?"

The prototype expresses each request as an action envelope:

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. An obligation is a rule the executor must continue enforcing after admission, such as pausing if the measured human distance drops below a threshold or writing a durable audit event.

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.

Latency in the Planning Loop

The two decisions visible in the recorded walkthrough completed in 8.74 ms and 8.55 ms:

Proposed action	Decision	Displayed policy-decision time
6-waypoint initial path	Deny restricted-zone intersection	8.74 ms
6-waypoint revised path with a nearby human	Constrain speed	8.55 ms

One way to screen an AI-generated plan is to ask another model whether the plan looks safe. That can be a useful semantic review, but an LLM-as-judge remains a probabilistic decision and adds another inference pass. If the reviewing model has latency similar to the planning model, the safety check can approach doubling the inference portion of the planning loop.

The prover takes a different role. Model inference produces the plan; the runtime turns that plan into a typed action envelope; and the prover performs a deterministic admission check against explicit invariants. The relevant performance question is therefore whether policy admission is small relative to the agent's planning cadence.

Those walkthrough values motivated a reproducible release-mode benchmark of the current in-process decision path. We exercised allow, deny, and constrained outcomes across 3, 6, 12, 24, and 48 waypoints, with 5,000 measured decisions per case after 1,000 warm-up decisions.

Benchmark charts showing policy-decision p50, p95, and p99 latency as waypoint count increases, plus the policy check in the context of several illustrative agent inference latencies. — Measured policy-decision latency on NVIDIA DGX Spark is shown separately from illustrative inference-time scenarios. Model inference depends on the model, request, hardware, and serving configuration.

Across this matrix, p95 policy latency ranged from 1.321 ms to 1.886 ms. The 48-waypoint cases remained between 1.348 and 1.376 ms p95. On this workload, the current SMT-backed admission check is small relative to the illustrative agent-planning latencies we considered.

Inference time matters to the complete propose-check-adapt loop, but it is not a property of the prover. The lower panel therefore shows a sensitivity analysis, not a model benchmark: measured policy p95 added to illustrative 100, 250, 500, 1,000, and 2,000 ms planning-inference scenarios. Against a 100 ms inference stage, the slowest measured p95 policy check adds about 1.89%; against a 250 ms inference stage, it adds about 0.75%. On these workloads, policy admission is therefore on the order of one percent of a fast agent-planning stage, without requiring another full model inference.

The recording provides a second, less controlled point of context. Its first plan was produced through an OpenAI-compatible endpoint and appears roughly 6–7 seconds after the planner request begins; the UI did not capture the exact model identifier or API latency. The 8.74 ms policy decision shown immediately afterward is roughly 0.1% of that observed planning interval. This is a walkthrough-level comparison, not a benchmark of the model or serving endpoint.

For reproducibility, the revised path in this recording was produced by the demo's deterministic fixture planner after it received the denial packet. The project supports running both planning steps through an OpenAI-compatible endpoint, and a future recording will capture the model identifier and request latency directly in the event stream.

The result is encouraging, not exhaustive. The benchmark measures the current local decision function on an NVIDIA DGX Spark with an NVIDIA GB10 and 20-core Arm CPU, using an arm64 Linux container. It includes deterministic geometry checks and Z3 setup/checking, but excludes HTTP and JSON transport, model inference, replanning, rendering, simulator stepping, and robot execution. It does not establish a hard real-time deadline. These measurements apply to AI-generated plans and short-horizon actions evaluated at the agent's planning cadence. They do not imply that the prover should inspect every sub-millisecond operation used to balance a robot, regulate torque, or track a joint trajectory. Those responsibilities remain with dedicated real-time controllers and safety systems. The admission boundary checks the path or action contract those controllers are being asked to execute. The complete harness and machine-readable results accompany this Dev Note so others can reproduce the measurement and add harder workloads.

What the Prototype Verifies

The phrase "formal methods" needs precision, especially when physical effects are involved.

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. The prototype submits Boolean policy facts to Z3 with a bounded timeout and produces a typed decision packet.

It does not yet encode continuous robot motion, full-body geometry, kinematics, dynamics, braking distance, or perception uncertainty as symbolic constraints. Its segment/volume test samples points along each tool-head segment, and the tool-head—not the complete robot body—is the governed geometry.

There is a second assumption outside the solver: the runtime must observe and mediate every policy-relevant action. An alternate path to the actuator, or a world-state signal that is missing or stale, can invalidate an otherwise correct formal decision. Proving the policy and validating the enforcement boundary are therefore parts of the same assurance claim.

So this is a research prototype, not a safety-rated system or a proof that a real robot trajectory is collision-free. The next formal-methods step is to make the solver result the authoritative source of the verdict and deepen the encoding from Boolean policy composition toward bounded trajectory constraints. The next robotics step is to connect those constraints to a real motion planner and runtime monitor.

Making that boundary explicit is part of the research. The next stages should help us understand how useful the formal specification remains as the model, environment, and enforcement point become more realistic.

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 same boundary into NVIDIA Isaac Sim and MuJoCo, where we can test it against richer robot geometry, dynamics, perception, and planning workloads.

Several steps would turn the prototype into a stronger research result:

Replace sampled tool-head intersections with exact or conservatively bounded geometry checks.
Encode richer trajectory and policy constraints symbolically and use the SMT result directly for the action verdict.
Connect the action contract to NVIDIA Isaac Sim and MuJoCo, then to a small physical platform such as an SO-100 arm.
Run the planner inside OpenShell and place the policy service on the trusted path to the simulator or actuator.
Treat human proximity, sensor freshness, and other changing facts as runtime signals that can revoke or narrow an already-admitted action.
Evaluate the boundary inside a longer-running policy-improvement loop where the agent is allowed to change its code but not its governing invariants.

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.

This question becomes more salient as research systems such as ENPIRE show coding agents managing repeated real-world robot-policy improvement across reset, verification, rollout, and evolution. This project is separate from ENPIRE, but the broader direction raises a related question: as agents gain more authority to improve physical systems, which properties remain outside their authority to change?

A question for the next experiments is:

Can an agent optimize a robot policy while the governing invariants remain outside the agent's control?

In this limited experiment, the agent did not make an admissible plan on its first attempt. The useful behavior was what happened next: the policy boundary stopped the simulated effect, identified the violated invariant, and returned enough structure for the agent to try again without changing the invariant.

We now want to test the same pattern with richer dynamics, uncertain perception, longer plans, and eventually real hardware. Those experiments will show where a separate policy check remains useful and where the model, specification, or enforcement approach needs to change.

Research Questions and Collaboration

The experiment leaves several questions that we would like to study with the OpenShell research community: how formal specifications hold up under changing world state, which solver encodings fit agent-scale latency budgets, 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: