# Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis

arXiv: https://arxiv.org/abs/2511.14755 · HTML: https://mlsanity.com/paper/2511.14755/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 22 of its 34 references that are in the map.
- First posted on arXiv 18 Nov 2025.

## Builds on (most cited first, 22 of 22)

- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Guaranteeing Safety of Learned Perception Modules via Measurement-Robust Control Barrier Functions](https://mlsanity.com/paper/2010.16001/) (2020)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Neural Network Verification in Control](https://mlsanity.com/paper/2110.01388/) (2021)
- [Reachability Analysis and Safety Verification for Neural Network Control Systems](https://mlsanity.com/paper/1805.09944/) (2018)
- [On Safety and Liveness Filtering Using Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2312.15347/) (2023)
- [Efficient Reachability Analysis of Closed-Loop Systems with Neural Network Controllers](https://mlsanity.com/paper/2101.01815/) (2021)
- [Safety Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2011.05174/) (2020)
- [Measurement-Robust Control Barrier Functions: Certainty in Safety with Uncertainty in State](https://mlsanity.com/paper/2104.14030/) (2021)
- [Reachability Analysis of Neural Network Control Systems](https://mlsanity.com/paper/2301.12100/) (2023)
- [A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis](https://mlsanity.com/paper/2309.06090/) (2023)
- [Discovering Closed-Loop Failures of Vision-Based Controllers via Reachability Analysis](https://mlsanity.com/paper/2211.02736/) (2022)
- [Data-Driven Hamiltonian for Direct Construction of Safe Set from Trajectory Data](https://mlsanity.com/paper/2504.03233/) (2025)
- [Verification of Neural Network Control Systems using Symbolic Zonotopes and Polynotopes](https://mlsanity.com/paper/2306.14619/) (2023)
- [Safety Verification of Neural Network Control Systems Using Guaranteed Neural Network Model Reduction](https://mlsanity.com/paper/2301.07531/) (2023)
- [Model-Free Verification for Neural Network Controlled Systems](https://mlsanity.com/paper/2312.08293/) (2023)
- [Verification of Neural Network Control Systems in Continuous Time](https://mlsanity.com/paper/2406.00157/) (2024)
- [Safety Under State Uncertainty: Robustifying Control Barrier Functions](https://mlsanity.com/paper/2508.17226/) (2025)
- [Safe Navigation under State Uncertainty: Online Adaptation for Robust Control Barrier Functions](https://mlsanity.com/paper/2508.19159/) (2025)

## Abstract (arXiv)

As perception-based controllers for autonomous systems become increasingly popular in the real world, it is important that we can formally verify their safety and performance despite perceptual uncertainty. Unfortunately, the verification of such systems remains challenging, largely due to the complexity of the controllers, which are often nonlinear, nonconvex, learning-based, and/or black-box. Prior works propose verification algorithms that are based on approximate reachability methods, but they often restrict the class of controllers and systems that can be handled or result in overly conservative analyses. Hamilton-Jacobi (HJ) reachability analysis is a popular formal verification tool for general nonlinear systems that can compute optimal reachable sets under worst-case system uncertainties; however, its application to perception-based systems is currently underexplored. In this work, we propose RoVer-CoRe, a framework for the Robust Verification of Controllers via HJ Reachability. To the best of our knowledge, RoVer-CoRe is the first HJ reachability-based framework for the verification of perception-based systems under perceptual uncertainty. Our key insight is to concatenate the system controller, observation function, and the state estimation modules to obtain an equivalent closed-loop system that is readily compatible with existing reachability frameworks. Within RoVer-CoRe, we propose novel methods for formal safety verification and robust controller design. We demonstrate the efficacy of the framework in case studies involving aircraft taxiing and NN-based rover navigation. Code is available at the link in the footnote.