Foundation models, the large general purpose AIs now steering robots, are too opaque for classical safety proofs. A new framework routes formal checks through a small, bounded safety module while letting the expressive controller handle the task.
The robots getting the most attention in research labs right now are not the ones with the most carefully engineered control software. They are the ones being steered by foundation models, the same family of large, general-purpose AI systems that powers image generators and chatbots. That expressivity is the point, and it is also the safety problem.
Classical safety engineering leans on formal verification, the practice of producing mathematical proofs that a system will satisfy specific properties such as never crossing a workspace boundary or never colliding with a human. The catch is that those proofs require a tractable model of the system being checked. A foundation-model controller, which takes in raw camera images, language instructions, and other high-dimensional inputs and emits motor commands, does not fit inside that box. The space of possible behaviors is too large and too dependent on perception for existing verification tools to bound. The result is a widening gap between what robots can do in the lab and what safety engineers can certify them to do in a factory, warehouse, or home.
A new arXiv preprint, Verifiable Foundation Models for Robot Safety, proposes a structural fix. The framework, called FEARL (Foundation-Enabled Assured Robot Learning), argues that the right move is to stop trying to verify the foundation model end to end and instead decompose the control stack.
The split works like this. A large Controller (C) handles the messy perceptual and reasoning work: reading the scene, parsing instructions, picking a strategy. A small Safety module (S) sits alongside it, fed only by dedicated, low-dimensional safety sensors, think proximity readings, joint limits, or simplified occupancy maps, plus a bounded context embedding passed down from the Controller. The Safety module, not the Controller, emits the final action. Formal verification is then applied to S, not to C, because S's observation space is small and structured enough for classical tools to analyze.
This preserves the Controller's expressive multimodal reasoning power, its ability to fuse vision, language, and action plans, while keeping the safety analysis tractable. A collision-avoidance property, for instance, can be expressed entirely over the Safety module's proximity observations and joint state. That is the kind of statement existing model checkers and reachability tools can actually evaluate.
The trade-off is real, and the paper is honest about it. Because verification runs on the Safety module, any safety property that depends on the Controller's rich, high-dimensional perception is not covered by the formal analysis. If a deployment scenario requires the robot to avoid an obstacle that can only be identified in a camera image, the formal guarantee does not extend to that property. The decomposition narrows the formal scope in exchange for keeping the foundation model's task capability intact, and that is a limitation, not a footnote.
The authors evaluate the decomposed policy across three simulated domains with multiple Controller backbones, including pretrained off-the-shelf vision-language-action models (controllers that fuse visual perception, language commands, and motor outputs in a single neural network), and transfer a learned policy from one of the simulated tasks to a physical robot. That last step matters: the low-dimensional safety interface is what makes the sim-to-real transfer practical, because the safety envelope can be checked in both worlds against the same mathematical property.
The paper lands inside a larger argument. A Science Robotics position piece by Corsi et al. (2026) argues that robotic foundation models need safety that goes beyond simple alignment with human preferences, including context-aware guarantees about what the robot should not do in the environment it actually operates in. FEARL is one answer to that call, an attempt to give regulators and safety engineers something to point at without freezing the field at today's model architectures.
Lead author Davide Corsi's homepage lists related work and lab context. The result is not a certified robot. It is a tractable interface where formal guarantees, the same kind used in classical industrial robotics, can re-enter the conversation about AI-controlled machines.
What to watch next: whether the same decomposition survives controllers that are even larger, more multimodal, or trained with different objectives, and whether standards bodies and safety regulators treat a low-dimensional Safety module as an acceptable boundary for certification. The architectural restraint is the story; the open question is who else is willing to design around it.