# Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 44 references that are in the map.
- First posted on arXiv 9 Nov 2025.

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

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [Control Barrier Function Based Quadratic Programs for Safety Critical Systems](https://mlsanity.com/paper/1609.06408/) (2016)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [The Safety Filter: A Unified View of Safety-Critical Control in Autonomous Systems](https://mlsanity.com/paper/2309.05837/) (2023)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation](https://mlsanity.com/paper/2210.07394/) (2022)
- [Robust Explanation Constraints for Neural Networks](https://mlsanity.com/paper/2212.08507/) (2022)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [Parameter Synthesis for Markov Models: Covering the Parameter Space](https://mlsanity.com/paper/1903.07993/) (2019)
- [Exact Verification of ReLU Neural Control Barrier Functions](https://mlsanity.com/paper/2310.09360/) (2023)
- [Verification and Synthesis of Control Barrier Functions](https://mlsanity.com/paper/2104.14001/) (2021)
- [Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation](https://mlsanity.com/paper/2410.16281/) (2024)
- [Efficient Error Certification for Physics-Informed Neural Networks](https://mlsanity.com/paper/2305.10157/) (2023)
- [Control Barrier Functions for Mechanical Systems: Theory and Application to Robotic Grasping](https://mlsanity.com/paper/1903.09816/) (2019)
- [Robust Control Barrier Functions under High Relative Degree and Input Constraints for Satellite Trajectories](https://mlsanity.com/paper/2107.04094/) (2021)
- [Abstraction of Elementary Hybrid Systems by Variable Transformation](https://mlsanity.com/paper/1403.7022/) (2014)
- [Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates](https://mlsanity.com/paper/2406.00826/) (2024)
- [Certified Neural Approximations of Nonlinear Dynamics](https://mlsanity.com/paper/2505.15497/) (2025)

## Built on by (most cited first, 2 of 2)

- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations](https://mlsanity.com/paper/2605.07757/) (2026)

## Abstract (arXiv)

Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems. Recently, CBFs represented as neural networks have shown great promise due to their expressiveness and applicability to a broad class of dynamics and safety constraints. However, verifying that a trained neural network is indeed a valid CBF is a computational bottleneck that limits the size of the networks that can be used. To overcome this limitation, we present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF. Our approach is rooted in linear bound propagation (LBP) for neural networks, which we extend to compute bounds on the gradients of the network. Combined with McCormick relaxation, we derive linear upper and lower bounds on the CBF conditions, thereby eliminating the need for computationally expensive verification procedures. Our approach applies to arbitrary control-affine systems and a broad range of nonlinear activation functions. To reduce conservatism, we develop a parallelizable refinement strategy that adaptively refines the regions over which these bounds are computed. Our approach scales to larger neural networks than state-of-the-art verification procedures for CBFs, as demonstrated by our numerical experiments.