+
+
+
+
+ Can Formal Methods Govern AI-Generated Robot Actions?
+A robotics experiment asks whether an independent, SMT-backed policy boundary can efficiently govern AI-generated plans before they reach a simulated or physical robot.
+ +
+
+ 
+
+
+ Read note
+
+
+
+
+ Read note
+
+
+ Recent notes
+ The working archive +
+
diff --git a/docs/dev-notes/posts/2026-08-07-formal-methods-ai-generated-robot-actions.md b/docs/dev-notes/posts/2026-08-07-formal-methods-ai-generated-robot-actions.md
new file mode 100644
index 00000000..da00d1f1
--- /dev/null
+++ b/docs/dev-notes/posts/2026-08-07-formal-methods-ai-generated-robot-actions.md
@@ -0,0 +1,392 @@
+---
+title: "Can Formal Methods Govern AI-Generated Robot Actions?"
+date: 2026-08-07
+updated: 2026-08-10
+description: "A robotics experiment asks whether an independent, SMT-backed policy boundary can efficiently govern AI-generated plans before they reach a simulated or physical robot."
+agent_markdown: true
+hero_image: "../../assets/robotics-policy-prover/robotics-policy-prover-hero.png"
+categories:
+ - Physical AI
+tags:
+ - openshell
+ - robotics
+ - physical-ai
+ - formal-methods
+ - policy
+ - agents
+authors:
+ - zredlined
+card_tags:
+ - physical-ai
+ - formal-methods
+ - policy
+---
+
+# 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.*
+
+
+
+ 
+
+
+
+
+
+
+ 
+
+
+ 
+
+
+ );
+}
+
+function storyLabel(event) {
+ if (event.kind === "agent_plan") return "Agent";
+ if (event.kind === "prover_decision") return "Policy prover";
+ if (event.kind === "execution_update" || event.kind === "execution_blocked") return "Executor";
+ return "World";
+}
+
+function storyTone(event) {
+ if (event.kind === "agent_plan") return "agent";
+ if (event.kind === "prover_decision") return event.decision?.decision ?? "prover";
+ if (event.kind === "execution_update" || event.kind === "execution_blocked") return "executor";
+ return "world";
+}
+
+function compactSummary(event) {
+ return event.summary;
+}
+
+function sanitizeDecision(decision) {
+ if (!decision) return null;
+ return {
+ decision: decision.decision,
+ solver_ms: Number(decision.solver_ms?.toFixed?.(2) ?? decision.solver_ms),
+ violations: decision.violations,
+ constraints: decision.constraints,
+ obligations: decision.obligations,
+ counterexample: decision.counterexample,
+ };
+}
+
+function App() {
+ const [seed, setSeed] = useState(42);
+ const [agentMode, setAgentMode] = useState("openai");
+ const [world, setWorld] = useState(fallbackWorld);
+ const [events, setEvents] = useState([]);
+ const [step, setStep] = useState(() => normalizeStep(null, null));
+ const [playbackSpeed, setPlaybackSpeed] = useState(1);
+ const [session, setSession] = useState(null);
+ const sourceRef = useRef(null);
+
+ const storyEvents = useMemo(
+ () => events.filter((event) => ["agent_plan", "prover_decision", "world_event", "execution_update", "execution_blocked"].includes(event.kind)),
+ [events],
+ );
+ const latestDecision = step.decision ?? "pending";
+ const latestDecisionEvent = [...events].reverse().find((event) => event.decision);
+
+ const attachEventSource = useCallback((sessionId) => {
+ sourceRef.current?.close();
+ const source = new EventSource(`/api/sessions/${sessionId}/events`);
+ sourceRef.current = source;
+
+ const handle = (message) => {
+ const event = JSON.parse(message.data);
+ setEvents((items) => [...items.slice(-40), event]);
+ if (event.world) setWorld(event.world);
+ setStep((previous) => normalizeStep(event, previous));
+ };
+
+ ["world_event", "agent_plan", "prover_decision", "execution_update", "execution_blocked", "error"].forEach((kind) =>
+ source.addEventListener(kind, handle),
+ );
+ }, []);
+
+ const startExperiment = useCallback(async () => {
+ setEvents([]);
+ setStep(normalizeStep(null, null));
+ const response = await fetch("/api/sessions", {
+ method: "POST",
+ headers: { "Content-Type": "application/json" },
+ body: JSON.stringify({ goal: DEFAULT_GOAL, seed: Number(seed), agent_mode: agentMode }),
+ });
+ const data = await response.json();
+ setSession(data);
+ setAgentMode(data.agent_mode);
+ attachEventSource(data.session_id);
+ }, [agentMode, attachEventSource, seed]);
+
+ useEffect(() => () => sourceRef.current?.close(), []);
+
+ return (
+
+
+
+
+
+
+
+ Agent Path vs Policy Prover
+One tool-path experiment: propose, prove, adapt, execute.
+
+
+
+
+
+
+
+
+
+ Agent path
+ Admitted path
+ Restricted
+ Human
+
+