Add robotics policy prover experiment and Dev Note

[zredlined]

Summary

• publish a Dev Note exploring whether an SMT-backed policy check can govern AI-generated robot plans before execution
• include the recorded experiment, an OpenShell-inspired runtime architecture, and DGX Spark latency results
• add the focused Three.js, Rust, and Z3 prototype plus its benchmark harness and machine-readable results under projects/robotics-policy-prover

Scope and caveats

• this is a research prototype, not a safety-rated robotics system
• the current implementation combines sampled geometry checks with Boolean policy composition in Z3; it does not prove continuous full-body robot motion
• the recorded initial path used an OpenAI-compatible endpoint, while the repeatable revised path used the fixture planner; the Dev Note discloses this because the recording did not capture the exact model identifier
• the benchmark measures the in-process policy decision and excludes model inference, transport, simulator stepping, and low-level robot control

Validation

• python3 tests/test_render_dev_notes.py — 11 passed
• scripts/build-docs.sh — clean strict Zensical build and all rendered-site checks passed
• npm run build — production frontend build passed
• npm audit — 0 vulnerabilities after refreshing Vite/PostCSS within their existing compatible ranges
• cargo test --release --manifest-path policy-prover-service/Cargo.toml — 4 passed
• inspected the generated Dev Note and index in Chrome in light and dark modes

[github-actions]

Documentation preview

View the deployed preview

Built from 221eb80.

[johnnygreco]

Thanks for making the decision packet and executor handoff so visible—this is a strong demo surface. Could we apply the returned contract before emitting execution here? In the repaired flow, the action still requests 0.18 m/s after the decision caps it at 0.08 m/s; additionally, the world reports human_distance_m = 0.48 while the returned obligation says to pause below 0.5 m, yet execution proceeds. That makes the audit event claim enforcement while still carrying the original over-limit action. I’d suggest materializing an effective action with speed/force constraints applied, evaluating active obligations before and during execution, emitting that effective envelope, and covering this path with an end-to-end test. -- Codex ;)

[johnnygreco]

I appreciate the explicit four-way decision contract; it makes the policy boundary easy to understand. One important distinction gets lost here, though: ApprovalRequired receives an approved_path, and check_and_execute blocks only Deny, so an action that needs human approval can proceed without an approval transition. Could we reserve approved_path and execution for Allow/AllowWithConstraints, then add a test showing that ApprovalRequired remains stopped until explicit approval is recorded? -- Codex ;)

[johnnygreco]

This is a compelling framing, and I’m grateful for how carefully the later limitations are discussed. I think the opening should be more explicit about the current Z3 role, however: solver.check() is run but its result is discarded, after which the facts and verdict are recomputed in Rust. Calling the boundary “SMT-backed” this early can therefore leave readers believing Z3 governs admission, while making the solver authoritative is identified much later as future work. Could we say up front—and again before the benchmark—that deterministic Rust rules currently produce the verdict while a non-authoritative Boolean Z3 composition check is executed and timed? Alternatively, making the solver result authoritative would support the current framing. -- Codex ;)

[johnnygreco]

Could we make this external decision boundary fail closed on malformed envelopes? An empty or one-waypoint path currently has no out-of-bounds point and no segment intersection, so it can return allow; from and to also do not need to agree with the path. Validating at least two finite waypoints, positive finite speed/force and zone dimensions, plus endpoint consistency—and adding malformed-envelope tests—would make the stated path invariants meaningful for callers. Thanks for exposing this endpoint cleanly; a little validation here would make it much more trustworthy. -- Codex ;)

[johnnygreco]

The event-by-event visualization is a really helpful way to explain the boundary. Could movement begin only on execution_update rather than as soon as a prover decision exposes an approved_path? Today the scene starts animating during the intentional 600 ms gap before the executor event, which undercuts the UI’s “checks before anything moves” explanation. Keeping a proven candidate path separate from the actively executing path, with a browser assertion for this transition, would preserve the story the demo is telling. -- Codex ;)

[johnnygreco]

This diagram does an excellent job of making the intended boundary legible. Could we label it explicitly as the target/OpenShell-inspired architecture, and visually distinguish the implemented path (planner → Rust service → Three.js) from future pieces? As drawn, the sandboxed non-bypassable runtime, Isaac Sim, MuJoCo, and real robot look like parts of the recorded prototype, while the note later identifies them as next experiments. A small current-versus-target cue would keep readers oriented without losing the broader vision. -- Codex ;)

[johnnygreco]

Since the Vite app already proxies /api from the same origin, could we remove permissive CORS or restrict it to an explicitly configured frontend origin? With OPENAI_API_KEY configured, an arbitrary page may be able to create localhost sessions that trigger billable model calls, and completed sessions remain in the map. I’d also consider bounding session creation and cleaning up completed sessions. The local-first setup is nicely straightforward; tightening this default would keep that experience safe. -- Codex ;)

[johnnygreco]

Thanks for giving the experiment such a prominent visual entry point—the screenshot makes the issue clear. The source PNG is 2656×1820 (native ratio 664:455, about 1.46:1), but .dev-note-figure--hero img forces 1200 / 630 (about 1.90:1), so the rendered hero looks stretched. Could we preserve the image’s true aspect ratio here by removing/overriding that forced ratio for this asset (or setting it to 2656 / 1820)? One alternative worth trying is to move the recorded demo into this top hero position and let it autoplay so readers immediately see the experiment in motion. If we explore that, I’d keep it muted playsinline, retain controls and the poster fallback, use the video’s native aspect ratio, and respect reduced-motion preferences; we could then remove the duplicate video lower in the note. -- Codex ;)

[johnnygreco]

This “not X, but Y” structure, with a phrase like "...applies formal methods to a narrower artifact:" is a bit too AI for me 🙃. Might be worthwhile to have a few passes to catch stuff like this.