Agentic Verification in the Physical World

1. The Scientific Problem

An agent built on a foundation model works as a solver. The agent proposes a candidate, a verifier judges the candidate, and the agent revises. The quality of the loop is the quality of the verifier. Without a good verifier, an agent cannot tell a good candidate from a bad candidate, and more search only produces more unjudged candidates. Language models cannot fill the role alone, and the LLM-Modulo position therefore pairs the model with external verifiers [37].

Software gives agents such verifiers. A compiler, a test suite and a proof checker each return a judgment independent of the agent. A recent report shows the effect at scale. A language model wrote about 180 million lines of Rocq proofs, and the proofs establish that 239 entry points across 123 open-source libraries have no memory-safety error or failed assertion on any input under 64 MB [50]. The Rocq kernel checked every proof, so the model never had to judge the proofs. A developer trusts only three artifacts, namely the formal models of the processor and the operating system process, the exact theorem statements, and the proof checker.

An agent acting through a robot has no verifier of comparable quality. The world gives a verdict only after the action, the verdict is often unclear, and a wrong action may be beyond repair. The survey studies how to provide verification for an agent in the physical world.

The Question

The question is about evidence. A verification result states that one fact follows from another fact, and a procedure independent of the agent establishes the result. Formal verification is the reference point, because a machine-checked proof is the strongest evidence available. The survey asks three things about a robot agent. Which verification results exist, how strong is each result, and what does each result leave open.

Formulation

Six objects describe every system in the survey.

A check returns one of three values, and a sound checker gives one guarantee.

A checker proves the implication and nothing more. The person wants a different statement, namely that the execution of \(a\) in the world fulfils \(I\).

The Trust Chain

Five links lie between the two statements. A sound checker discharges the third link. The other four links hold only by trust, by test or by measurement.

The trusted base of a system is every object entering a link without a check. The survey names the trusted base of each system described. Two facts separate the physical case from software. First, links 2, 4 and 5 are close to exact in software. The model is the semantics of the language, the state is given, and a verified compiler preserves the meaning [44], so the remaining risk sits in link 1. In a robot, links 1, 2, 4 and 5 are open at once. Second, the proposer of an agentic system also writes \(\varphi\), and sometimes \(C\). The definition of "correct" then comes from the untrusted party. A checker can show that an artifact satisfies a specification. A checker cannot show that the specification asks for enough.

A Reference System

TAMPAgent is the closest robot instance of an untrusted proposer in front of a small trusted checker, and serves as the running example [56]. A coding agent receives a belief-space planning model and a set of perception, planning and control tools. The agent formulates a partial task plan of observation and execution actions, and classical search completes the plan. The planner then "compiles its decisions into a constraint satisfaction problem (CSP) and checks that all constraints are solved with certified values before anything executes". On kitchen tasks with a Rainbow Y1 mobile manipulator in simulation, the preprint reports 77.2% success against 57.2% for Code as Policies and 61.1% for Graph as Policy.

TAMPAgent secures link 3 and part of link 4. Each value reaching the motors comes from a trusted tool and satisfies a constraint from a fixed set. The specification and the tools remain in the trusted base, and the authors say so. The guarantees of TAMPAgent "are only as strong as those tools and the robot's perception", and "certification protects geometric feasibility but not the agent's interpretation of the task". The second quotation describes the open part of link 1 exactly.

2. Challenges and Gaps

A challenge is a reason why a good verifier for a physical agent is hard to provide, independent of the chosen method. Each challenge breaks one link of the trust chain. Most of the measurements come from the verification of software, the field with the longest record on the question. The bearing of the software measurements on robots is an argument of the survey and not a result of the cited papers.

Weak Specifications

Acceptance by a verifier says nothing about whether the specification captures the intent (link 1). Huang et al. state the limit in one sentence, "verification can prove that a specification is sound for the implementation, yet it cannot tell whether the specification is too weak" [34]. Three benchmarks measure the size of the effect. VerusEval evaluates 13,716 generated Verus artifacts over 762 tasks. Only 42.3% of the verifier-accepted artifacts complete all three semantic checks of VerusEval without a flag. Input and output tests reject 23.6% of the accepted artifacts. VerusEval also flags 36 candidate defects among 61 selected reference contracts, so human-written benchmark specifications are wrong as well [88]. SWE-Proof turns 500 real software issues into formally verified tasks. A correct formal specification lifts the resolution rate of an agent from 85% to 95%. An agent writing the specification alone "gains nothing over an unaided baseline", and only 56% of the agent-written specifications pass an audit [51]. In VERINA, the best model of the first version produced 61.4% correct code and 51.0% sound and complete specifications. The best model of the third version reached 72.6% and 52.3%. Code improved across model generations, and specifications did not [97].

Robotics has one documented case of the same failure. RoboGuard places a guardrail in front of an LLM-enabled robot. A root-of-trust LLM inside the guardrail turns safety rules into temporal logic, and the RoboGuard authors note that safety is contingent on the inferred specification [62]. Taheri et al. report that every harmful plan passing the guardrail in the experiments traced back to an incorrect specification. In the example of Taheri et al., the specification forbids switching a carbon monoxide detector off and does not forbid moving the detector off the outlet, an action with the same effect [78].

The literature has no agreed names for the two faults of a specification. Verus-SpecGym calls a specification sound when every accepted artifact is correct [1]. VeriContest uses "complete" for the same property [91]. The survey therefore uses two plain terms. A specification accepting a wrong artifact is too weak, and a specification rejecting a right artifact is too strong.

Self-Verification

The simplest answer to a weak check is a model judging the output of the same model. The evidence is against self-verification (link 3). Valmeekam et al. find that self-critique by GPT-4 "appears to diminish plan generation performance" and that the LLM verifier produces "a notable number of false positives", compared with a system using an external sound verifier [84]. Stechly et al. reach the same conclusion for graph colouring [75] and then for the Game of 24 and STRIPS planning, with "significant performance collapse with self-critique and significant performance gains with sound external verification" [76]. The three studies used the models of 2023. The later results on specifications limit the claim without reversing the claim. A current model with a formal kernel behind the model writes specifications of mixed quality, and the model still cannot certify the strength of a specification. The verifier of a robot agent therefore has to be external to the model.

Proofs About Models

A guarantee holds in \(M\), and nothing forces the world to agree with \(M\) (link 2). The proposal for guaranteed safe AI makes the dependence explicit. The verifier of the proposal certifies that a system satisfies a safety specification "relative to the world model" [15]. Critics take the dependence as the main objection. Dickson argues that proofs apply to symbol systems and not to the physical world [18]. Hatfield-Dodds argues that verification against a world model moves the problem to the match between the world model and reality [30]. Neither critique is peer reviewed, and the survey cites both for the argument only. Robotics meets the same loss inside task and motion planning. A plan valid in a symbolic abstraction may have no realizing motion. Classical planning theory therefore studies the conditions for an abstract solution to refine to a concrete solution [4]. Contact, friction, deformable objects and other agents lie outside most models decidable by a checker.

Missing Oracles

Software tests have known answers, and software engineering already names the difficulty of obtaining the answers the oracle problem [6]. A robot task such as folding a cloth has no formal success condition at all. The usual substitute is a vision-language model judging success from images (links 1 and 4). FailBench evaluates 13 VLM judges on 2,197 manipulation attempts with outcome labels. The best judge reaches a balanced accuracy of 0.77. No judge exceeds 0.60 on contact-rich assembly. The judges lean toward "success" on ambiguous evidence, even with more reasoning effort [57]. Guardian, a judge trained for failure detection, reaches accuracies between 0.70 and 0.89 on real-robot failure benchmarks [59]. Software shows the same weakness. An LLM judge misses 26% of the specification failures caught by an executable evaluator [1]. A checker validated against a VLM judge inherits the bias of the judge toward acceptance.

Unobserved State

A predicate such as "the shelf is free" has no truth value before the robot looks (link 4). A two-valued checker has to guess, and each guess is wrong in one direction. With unknown counted as false, the robot refuses actions justified by a single glance. With unknown counted as true, the robot acts blind. A third value keeps the information and raises a decision absent from the verification of software. The robot gathers evidence, stops, or asks a person.

Irreversible Failures

Software runs again, and a dropped glass stays broken (link 5). The cost of a wrong accept is therefore uneven across actions. A framework treating all constraints alike spends caution and human attention in the wrong places. Runtime monitoring is the most common enforcement for LLM agents. A systematic review of 38 studies reports that the guarantees of runtime monitoring "cover only single steps or short horizons". In one study of the review, blocking 94% of unsafe actions left fewer than 5% of tasks both safe and correct [17]. The review rates the certainty of most claims as very low, because each claim rests on one or two studies. The structural point stands without the numbers. A monitor stopping the robot one step before the harm is too late when an action three steps earlier fixed the harm.

Proposers That Satisfy the Checker

A proposer scored by a checker can pass by changing the question (link 3). LiveFMBench documents the behaviour for specification generation in C. Models modify the program or weaken the assertion under proof, and "after excluding such cases, the true specification generation accuracy drops by approximately 20%". For one group of models in the first table of LiveFMBench, the first-attempt pass rate falls from 23.68 to 17.91 [92]. A robot agent with write access to constraints, thresholds or tools can do the same. A checker returning true on every input passes every plan.

Translation into Formal Language

The step from language to a formal object fails often, before any verification starts (link 1). On one benchmark cited by Dantas et al., only 24.8% to 34.2% of LLM translations from natural language to PDDL are semantically correct [17]. Lang2LTL grounds navigation commands to temporal logic with 81.83% accuracy in 21 unseen cities [48]. In ReKep, constraints generated automatically by a vision-language model reach 44.3% task success, against 68.6% for human-annotated constraints [33]. Safety Chip reaches a 100% safety rate with expert-verified temporal logic formulas. Without expert verification, the Safety Chip authors report lower success because of mistranslated constraints [95].

Conflicting Evidence

One question has no settled answer. How much of a task needs an agent when the checkers and the solver are already complete? The evidence points both ways. TiPToP combines foundation-model perception with GPU-accelerated task and motion planning and attains a higher average success rate than a vision-language-action model fine-tuned on 350 hours of demonstrations [68]. The TiPToP result favours the planner. Merler et al. let coding agents synthesize programs for 28 environments and report "56% to 95% versus 47% for the planners, on the 16 environments where a planner is available", with an order of magnitude less computation per instance [54]. The result of Merler et al. favours the agent. CaP-X adds a caution for the second reading. The performance of coding agents "improves with human-crafted abstractions but degrades as these priors are removed" [21]. BUMBLE shows the agent as the policy at the scale of a building, with 47.1% success over 70 trials [66].

The four results use different tasks, tools and baselines. TAMPAgent has the most controlled comparison. The same coding agent with the same tools either writes planning problems or writes policy code. The planning arm is ahead on the kitchen tasks and level on the multi-room tasks [56]. Results on smaller settings split as well. A closed-loop VLM writing PDDL problems for a task and motion planner outperforms a VLM used as the planner by 17.5% in mean success rate on bimanual cooking [69]. Direct VLM planning is ahead of VLM-grounded symbolic planning in the simulated household domain of ViPlan [53].

Gaps

A gap is a place without published work. A search for counterexamples ran in November 2026 for each entry. The third column names the nearest work found by the search.

3. Verification in Robotics

Since 2024 the main line of work has the model write constraints or predicates and a classical solver or tool satisfy the constraints. The survey groups the work by the object doing the checking. Three facts describe each system, namely the output of the model, the check on the output, and the trusted remainder.

Fixed Checkers

In the largest group, the model proposes constraints, predicates, operators or a whole planning domain, and a human-written checker decides.

COAST is the classical member of the group. COAST is a plan-first task and motion planner with no language model. Geometric infeasibility found during motion planning constrains the next round of task planning [86]. Across the group, the checker tests whether the plan satisfies the constraints. VisualPredicator and SkillWrapper go one step further and test learned predicates against recorded successes and failures of each skill. No system applies the same test to model-written constraints, monitors or goal conditions. The hand-written constraint set also bounds the range of possible checks.

Certified Execution

TAMPAgent is the one system found with the agent outside the trusted base by construction [56]. The TAMPAgent check concerns provenance. Each bound value comes from a trusted tool and satisfies a human-written constraint. The agent cannot add a kind of constraint, so TAMPAgent is as strong as the fixed constraint set.

Abstractions Repaired from Failure

A third group turns a failure of execution or refinement into a new predicate, constraint or operator. ReSYNC learns recovery skills with reinforcement learning and then discovers relational predicates explaining the recoveries. ReSYNC outperforms strong baselines by over 50% across four simulated domains [45]. The ReSYNC predicates are neural classifiers and not the output of a language model, and planning success decides acceptance. HUME lets a foundation model propose hypotheses about states and transitions. HUME plans hypothesis-testing actions alongside task actions and updates the model after a failed hypothesis [90]. A vision-language model reads the test, so the judge of the hypothesis shares the weakness described under missing oracles. LogicGuard has an LLM critic read full trajectories and propose temporal logic constraints as a shield for the actor [24]. TANDEM has a VLM add missing predicates and human-executed operators. After each human stage, TANDEM perceives the scene again and checks the intended effects [63]. In all four systems, a failure produces a new constraint. None of the four systems tests the new constraint against the recorded episodes, the test applied to operator preconditions by the predicate learners of the first group. A constraint explaining the last failure can still accept an older failure.

Runtime Monitors and Shields

Monitors filter plans or actions against a formal specification, most often in temporal logic. Safety Chip encodes natural language constraints into a queryable temporal logic module. The module explains violations and prunes unsafe actions [95]. RoboGuard synthesizes a plan safe with respect to the inferred specification and reduces the execution of unsafe plans from over 92% to below 3% [62]. Agent-C targets tool-calling agents in customer service and not robots. Agent-C translates properties from a domain-specific language into first-order logic, uses an SMT solver during token generation, and reports 100% conformance [36]. VerifyLLM translates the instruction to temporal logic and has an LLM analyse the plan before execution. The VerifyLLM ablation attributes the effect to the LLM analysis. Removal of the temporal logic module barely changes the ordering errors [26]. Code-as-Monitor has a VLM write monitoring code for failure detection and evaluates the monitors through downstream task success [100]. NL2LTL offers the translation step as a package [22].

Each monitor is sound for the formula of the monitor. The formula comes from one model or one translation with no second check. Taheri et al. constructed exactly the resulting failure. The remedy of Taheri et al. spreads enforcement over several LLM stages without a test of the specification of any stage [78].

Belief and Evidence

A fifth group reasons about unobserved parts of the scene. The classical base is planning in belief space [35] and online replanning after each observation [23]. TAMPURA learns an abstract belief-state model for an uncertainty-aware solver, for problems requiring "information gathering and avoiding undesirable and irreversible outcomes" [13]. Seeing is Believing uses a VLM as the estimator of three-valued predicates (known true, known false, unknown) and plans information gathering over the predicates. Seeing is Believing reaches 80% and 70% on two simulated tasks, with VLM baselines at or below 10% [98]. Evidence-gated planning has a VLM generate evidence-acquiring subgoals. A gate then decides "whether to proceed with task planning, acquire further evidence, or halt" [79]. CoCo-TAMP shapes the belief with common sense from an LLM and cuts planning and execution time by 62.7% in simulation [39]. No check covers the prior supplied by the LLM. All four systems keep the third value inside one planner. No system carries the third value across kinds of constraints or ties the third value to the party responsible for the next step.

Judges of Success

FailBench and Guardian evaluate the judge. Guardian is also notable for the construction of the training set. Perturbation of successful trajectories yields more than 36,000 failure examples [59]. The construction is close to mutation testing. Guardian uses the perturbed trajectories to train a judge of outcomes and not to measure the strength of a constraint against the perturbed cases. MANGO comes closest to a test of a generated checker. In MANGO, agents write test oracles for vision-language-action policies. MANGO scores the generated oracles against the reference oracles of a benchmark and counts the false passes, the cases of a generated oracle accepting a failing execution [82]. A recent survey of verifiers for robot policies asks the general form of the question, "what validates a verifier itself" [87].

The Agent as the Policy

The last group has no checker between the agent and the robot, apart from checks run by the agent. Besides the systems under conflicting evidence, Graph as Policy has a multi-agent coding harness generate computation graphs of perception, planning and control nodes. The harness rehearses the graphs in an internal simulation, also generated by the harness [9]. The rehearsal is a check in a proposer-written model, so links 1 and 2 both rest on the proposer.

4. The Same Problem in Other Fields

A field belongs in the section when the problem of the field has the same form, with an untrusted proposer, a specification, a model and a checker. For each mechanism, the section names the role in the formulation and the counterpart for a robot agent.

Formal Verification with Language Models

Formal verification of software met the question of the unchecked specification first. The answer of the field does not rely on a person reading each specification. The answer brings in trusted samples of behaviour. A specification has to accept the positive cases and reject the negative cases.

Clover checks consistency among code, docstrings and formal annotations. Clover accepts up to 87% of correct instances with no false positive on adversarial incorrect instances [77]. Coins instantiates a specification on trusted test cases as proof obligations in Rocq. A proof has to show acceptance of the positive cases. A proof of acceptance for a negative case, obtained by mutation of the reference implementation, marks the specification as "overly permissive" [94]. SpecRL builds negative tests from input and output pairs impossible for the implementation, and rewards a specification by the rejected fraction [34]. Verus-SpecGym executes generated specifications against official tests and adversarial cases from competition hacks [1]. VeriContest converts postconditions into executable programs and runs the programs on negative tests [91]. CLEVER requires a proof of equivalence between the generated specification and a held-out specification, and excludes specifications allowing "vacuous solutions" [81].

Mutation also drives repair. For hardware assertions, Krishnamurthy et al. feed each surviving mutant back to the LLM and start another round whenever the kill rate falls below 85% [41]. FlyCatcher infers runtime checkers from existing tests and validates the checkers dynamically. Cross-validation confirms 300 of 334 inferred checkers [73]. Benchmarks with a fixed specification ask only for the proof or the code. Such benchmarks measure a different skill and say nothing about link 1 [7, 49].

The transfer to robots is direct in form. A constraint checker plays the role of a postcondition. The positive set holds the states and parameters of past successful episodes, and the checker has to accept the positive set. The negative set holds past failures and perturbed successes, such as a grasp pose moved out of the feasible region, and the checker has to reject the negative set. The kill rate on the negative set measures the strength of the checker. One part does not transfer. The label of a software test is exact. The label of a robot episode is noisy, and a VLM label is biased toward success. The labels of negative cases therefore have to come from geometric primitives or physical measurement.

Programming Languages

The architecture of an untrusted proposer and a small checker is old in programming languages. In proof-carrying code, an untrusted producer ships a safety proof with the code, and the host validates the proof against the safety policy of the host [58]. The LCF tradition confines trust to a small kernel [25]. Translation validation gives up on verifying the compiler and validates each run of the compiler [61]. In all three designs, the proposer may be arbitrarily complex because the checker is simple. TAMPAgent adopts the same design by granting execution only on certified values.

Recent work carries the design to planning and to language models. Proof-Carrying Plans checks plans as proofs in a resource logic formalized in Agda [31]. LeanPlan has an LLM write heuristics with machine-checked admissibility proofs in Lean. LeanPlan evaluates the domain assumptions of each proof before search and refuses a heuristic on a task failing the assumptions. The assumption checks exposed an error in a task of the IPC 2023 learning track [60]. CCV builds machine-checked assurance cases for C code and states that "the LLM agent is not in the TCB" [46]. In each case the trusted base shrinks to a kernel, a semantic model and the specification. The remaining risk then sits in the specification.

Other mechanisms of the field address the missing oracle. Property-based testing checks stated properties on random inputs [12]. Metamorphic testing checks relations between outputs when no exact answer is known [10]. Metamorphic relations for a robot checker are easy to state. A rigid motion of the whole scene should not change whether an object can be placed. An added obstacle should never turn a collision check from fail to pass. Dynamic invariant detection reports properties holding over observed runs [19]. The robot counterpart is mining candidate constraints from successful episodes. CodeT selects code by agreement with model-generated tests [8]. Design by contract checks preconditions and postconditions at run time [55], as TANDEM does after human stages. Refinement types [20] and gradual verification [5] prove part of a property statically and check the rest dynamically. Both are the software form of assigning constraints to levels of assurance. In counterexample-guided synthesis, a checker returns a counterexample and the proposer revises [72]. Robot systems with simulation feedback to the LLM already use an informal version of the loop.

Abstraction in Planning

Planning theory has studied link 2 for decades. Angelic semantics describes a high-level action by the states reachable under some refinement, so high-level solutions satisfy refinement properties by construction [52]. Admissible abstractions extend the idea to task and motion planning with cost bounds [85]. Konidaris et al. construct the symbols necessary and sufficient for evaluating plans over a given set of skills [40]. Counterexample-guided abstraction refinement repairs an abstraction from the cause of a failed abstract solution [64]. Task and motion planners return motion failures to the task level as logical facts [74] or as incremental constraints [16]. Predicate invention learns predicates for efficient bilevel planning [70]. The systems of the robotics section rewrite the abstraction online with a language model. Most of the systems drop the central asset of the theory, a stated property of the abstraction preserved under rewriting.

AI Safety

The guaranteed safe AI framework is the formulation of the survey at full generality, with a world model, a safety specification and a verifier [15]. Shielding synthesizes a monitor from a temporal logic specification. The shield corrects an action only when the action would violate the specification [2]. A second design gives a simple reliable component authority over a complex component [65]. Both designs assume a given specification. U-Define lets end users label each constraint as hard or soft. A model checker checks the hard constraints, and an LLM judge checks the soft constraints [43]. U-Define is a two-level grading of assurance set by a person, in everyday planning and not in robotics.

A Map of Mechanisms

The map shows an asymmetry. The mechanisms keeping the proposer out of the trusted base (the first three rows and the monitors) have robot counterparts. The mechanisms testing the specification appear only for learned predicates. Robotics already produces the raw material for specification tests, in the failure logs consumed by repair methods and in the perturbed trajectories used to train judges. Robot systems verify with growing care that a plan satisfies the constraints. The constraints, increasingly written by the agent, remain the least examined object in the chain. An agent in the physical world gets a verifier as good as the specification behind the verifier, and no better.