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

The preview has been removed.