# Exact Verification of ReLU Neural Control Barrier Functions

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

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 45 references that are in the map.
- First posted on arXiv 13 Oct 2023.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [Safe Model-based Reinforcement Learning with Stability Guarantees](https://mlsanity.com/paper/1705.08551/) (2017)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificates](https://mlsanity.com/paper/2101.05436/) (2021)
- [Control Barrier Functions for Systems with High Relative Degree](https://mlsanity.com/paper/1903.04706/) (2019)
- [Safe Control Under Input Limits with Neural Control Barrier Functions](https://mlsanity.com/paper/2211.11056/) (2022)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions](https://mlsanity.com/paper/2206.07811/) (2022)
- [Convex synthesis and verification of control-Lyapunov and barrier functions with input constraints](https://mlsanity.com/paper/2210.00629/) (2022)
- [Safe Control Synthesis via Input Constrained Control Barrier Functions](https://mlsanity.com/paper/2104.01704/) (2021)
- [Verification and Synthesis of Control Barrier Functions](https://mlsanity.com/paper/2104.14001/) (2021)
- [Safety Index Synthesis via Sum-of-Squares Programming](https://mlsanity.com/paper/2209.09134/) (2022)
- [Quantifying Safety of Learning-based Self-Driving Control Using Almost-Barrier Functions](https://mlsanity.com/paper/2207.13891/) (2022)
- [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)
- [Correctness Guarantees for the Composition of Lane Keeping and Adaptive Cruise Control](https://mlsanity.com/paper/1609.06807/) (2016)
- [A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops](https://mlsanity.com/paper/2210.07918/) (2022)
- [High Relative Degree Control Barrier Functions Under Input Constraints](https://mlsanity.com/paper/2106.10345/) (2021)
- [Verification and Synthesis of Robust Control Barrier Functions: Multilevel Polynomial Optimization and Semidefinite Relaxation](https://mlsanity.com/paper/2303.10081/) (2023)
- [SOS Construction of Compatible Control Lyapunov and Barrier Functions](https://mlsanity.com/paper/2305.01222/) (2023)

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

- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation](https://mlsanity.com/paper/2410.16281/) (2024)
- [Gradient Shaping for Multi-Constraint Safe Reinforcement Learning](https://mlsanity.com/paper/2312.15127/) (2023)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [V-OCBF: Learning Safety Filters from Offline Data via Value-Guided Offline Control Barrier Functions](https://mlsanity.com/paper/2512.10822/) (2025)
- [CP-NCBF: A Conformal Prediction-based Approach to Synthesize Verified Neural Control Barrier Functions](https://mlsanity.com/paper/2503.17395/) (2025)
- [Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation](https://mlsanity.com/paper/2511.06341/) (2025)
- [Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers](https://mlsanity.com/paper/2605.25346/) (2026)
- [Safe PDE Boundary Control with Neural Operators](https://mlsanity.com/paper/2411.15643/) (2024)
- [Neural Control Barrier Functions from Physics Informed Neural Networks](https://mlsanity.com/paper/2504.11045/) (2025)
- [Formal Verification of Neural Certificates Done Dynamically](https://mlsanity.com/paper/2507.11987/) (2025)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Transfer Learning for Control Systems via Neural Simulation Relations](https://mlsanity.com/paper/2412.01783/) (2024)
- [Sample Efficient Certification of Discrete-Time Control Barrier Functions](https://mlsanity.com/paper/2509.03899/) (2025)

## Abstract (arXiv)

Control Barrier Functions (CBFs) are a popular approach for safe control of nonlinear systems. In CBF-based control, the desired safety properties of the system are mapped to nonnegativity of a CBF, and the control input is chosen to ensure that the CBF remains nonnegative for all time. Recently, machine learning methods that represent CBFs as neural networks (neural control barrier functions, or NCBFs) have shown great promise due to the universal representability of neural networks. However, verifying that a learned CBF guarantees safety remains a challenging research problem. This paper presents novel exact conditions and algorithms for verifying safety of feedforward NCBFs with ReLU activation functions. The key challenge in doing so is that, due to the piecewise linearity of the ReLU function, the NCBF will be nondifferentiable at certain points, thus invalidating traditional safety verification methods that assume a smooth barrier function. We resolve this issue by leveraging a generalization of Nagumo's theorem for proving invariance of sets with nonsmooth boundaries to derive necessary and sufficient conditions for safety. Based on this condition, we propose an algorithm for safety verification of NCBFs that first decomposes the NCBF into piecewise linear segments and then solves a nonlinear program to verify safety of each segment as well as the intersections of the linear segments. We mitigate the complexity by only considering the boundary of the safe region and by pruning the segments with Interval Bound Propagation (IBP) and linear relaxation. We evaluate our approach through numerical studies with comparison to state-of-the-art SMT-based methods. Our code is available at https://github.com/HongchaoZhang-HZ/exactverif-reluncbf-nips23.