Prove Before You Move: Retrieval-Augmented Deduction for Embodied Agents

Large language models are increasingly the executive of embodied agents, and the failure this invites is not a crash but a fluent, wrong commitment: a hallucinated precondition, a safety constraint paraphrased but never checked. We argue that in bounded-mission deployments the model should be the language interface, not the executive, and that every commitment to act should be gated by a deterministic proof. In embodied retrieval-augmented deduction (RAD), the model matches instructions to a bounded catalogue of skills, fixed code turns facts retrieved from a perceptually grounded world graph into ground assertions, and a symbolic engine proves or fails each skill's dispatch goal against a human-confirmed rule base. Every dispatch carries a certificate; a derived prohibition becomes a safe halt and a blocked proof becomes a clarification, or an active-perception action. We formalise the dispatch decision, state a retrieval adequacy condition, and identify properties that hold by construction.