Stanford and NASA's RoVer-CoRe Formally Verifies Self-Driving AI 3x Tighter Than Rivals

Verifying that a self-driving car, aircraft autopilot, or lunar rover will stay safe even when its cameras and state estimators are wrong is one of the hardest open problems in autonomy. A new framework called RoVer-CoRe, from researchers at Stanford and NASA's Jet Propulsion Laboratory, brings Hamilton-Jacobi (HJ) reachability analysis into that setting for the first time, producing formal safety guarantees for perception-based controllers under bounded perceptual uncertainty.

Why perception makes verification painful

Modern autonomous systems increasingly rely on controllers that consume perception outputs like camera-based state estimates. Verifying these stacks is hard because the controllers are often nonlinear, nonconvex, learning-based, or black-box, which makes formal analysis difficult even before adding perceptual uncertainty.

Existing approaches typically bolt neural network verifiers onto approximate reachable-set methods, propagating hyper-rectangles, zonotopes, polytopes, or Taylor models through the closed loop. These representations and the propagation schemes that use them can incur significant approximation costs, resulting in overly conservative analyses that fail to certify safety. Certificate-based alternatives like measurement-robust and robust control barrier functions exist too, but they can be infeasible depending on how large the estimation error is.

HJ reachability, by contrast, computes optimal reachable sets for general nonlinear systems under worst-case disturbances by solving a partial differential equation on a grid. The catch is that the standard HJ formulation assumes the controller has perfect state information, which breaks under perceptual uncertainty.