Verification and Forward Invariance of Control Barrier Functions for Differential-Algebraic Systems

Hongchao Zhang; Mohamad H. Kazma; Meiyi Ma; Taylor T. Johnson; Ahmad F. Taha

eess.SYMar 13, 2026

Verification and Forward Invariance of Control Barrier Functions for Differential-Algebraic Systems

Authors: Hongchao Zhang, Mohamad H. Kazma, Meiyi Ma, Taylor T. Johnson, Ahmad F. Taha

Organizations: Department of Computer Science, Vanderbilt University, Nashville, TN 37235 USA. · Department of Civil and Environmental Engineering, Vanderbilt University, Nashville, TN 37235 USA.

Abstract

Differential-algebraic equations (DAEs) arise in power networks, chemical processes, and multibody systems, where algebraic constraints encode physical conservation laws. The safety of such systems is critical, yet safe control is challenging because algebraic constraints restrict allowable state trajectories. Control barrier functions (CBFs) provide computationally efficient safety filters for ordinary differential equation (ODE) systems. However, existing CBF methods are not directly applicable to DAEs due to potential conflicts between the CBF condition and the constraint manifold. This paper introduces DAE-aware CBFs that incorporate the differential-algebraic structure through projected vector fields. We derive conditions that ensure forward invariance of safe sets while preserving algebraic constraints and extend the framework to higher-index DAEs. A systematic verification framework is developed, establishing necessary and sufficient conditions for geometric correctness and feasibility of DAE-aware CBFs. For polynomial systems, sum-of-squares certificates are provided, while for nonpolynomial and neural network candidates, satisfiability modulo theories are used for falsification. The approach is validated on wind turbine and flexible-link manipulator systems.

Figures & tables

Figure 1: Conceptual illustration of hidden infeasibility in standard CBF safety filters when applied to DAE systems. The algebraic constraint manifold

\mathcal{M}=\{x:\phi(x)=0\}

imposes an additional compatibility requirement on the control input that is not accounted for by standard CBF conditions, which may render the safety filter infeasible even when the state lies within the safe set

\mathcal{C}

Figure 2: Geometric illustration of Problem 1 . The state space contains the constraint manifold

\mathcal{M}

, the safe set

\mathcal{C}

, and the candidate barrier set

\mathcal{D}

. The goal is to design a barrier function

b(x)

and a safe control policy

\mu

such that

\mathcal{D}\cap\mathcal{M}\subseteq\mathcal{C}\cap\mathcal{M}

is positively invariant under the closed-loop DAE dynamics ( 1 ), ensuring that all system trajectories initialized in

\mathcal{D}\cap\mathcal{M}

evolve on the constraint manifold and remain within the safe set for all

t\geq 0

Figure 3: Simulation results for Example 1 using a DAE-unaware CBF. The figure shows (a) the CBF-QP trajectory on the constraint manifold

\phi(x)=0

, (b) the evolution of the barrier function

b(x)

(with

b(x_{0})=0.130

and a minimum

b(x)=-0.1059

), and (c) the evolution of the safe set function

h(x)

(a minimum

h(x)=-0.1059

). The CBF-QP becomes infeasible when the CBF inequality conflicts with the algebraic equality constraints, leading to violation of the safety condition

b(x)\geq 0

Subsection	Key Concept	Main Results
3.1 Preliminaries	Lie derivatives + relative deg.	Defs. 5 - 6 ; Thm. 2
3.2 Projected Fields	Revealing hidden dynamics	Eq. 10 ; Lem. 1
3.3 Index-1 DAEs	Compatibility + safety	Thm. 4 ; Cor. 4.1
3.4 Higher-Index	$\nu$ -order diff. + projection	Prop. 1 ; Thm. 5

Table I: Summary of Main Results for DAE-Aware CBF Construction, outlining the key concepts in each subsection.

Panel of Figure 4 — Figure 4: Roadmap for the derivation of DAE-aware CBF conditions for index-1 systems. The algebraic constraints $\phi(x)=0$ are differentiated to expose the compatibility condition and the constraint Jacobians $J_{d}(x)$ and $J_{a}(x)$ . Under the invertibility assumption on $J_{a}(x)$ , the algebraic states are eliminated via the implicit function theorem, and the DAE ( 1 ) is projected onto the constraint manifold $\mathcal{M}$ . The CBF condition is then lifted back to the full state space, producing DAE-aware CBF conditions that jointly enforce manifold compatibility and positive invariance of $\mathcal{D}\cap\mathcal{M}$ .

Panel of Figure 5 — Figure 5: Roadmap for deriving DAE-aware CBF conditions for higher-index systems ( $\nu\geq 2$ ). The algebraic constraint $\phi(x)=0$ is differentiated successively up to order $\nu$ , eliminating time derivatives via ( 1a ) at each step, until the control input appears explicitly in the extended constraint system. Full row rank of $J_{ext}^{(\nu)}(x)$ then yields a projected control-affine representation on $\mathcal{M}$ , from which the DAE-aware CBF conditions follow analogously to the index-1 case.

Panel of Figure 6 — Figure 6: Roadmap for the verification of a candidate DAE-aware CBF $b(x)$ (Problem 2 ). The framework consists of Left: the correctness branch verifies that $\mathcal{D}\cap\mathcal{M}\subseteq\mathcal{C}\cap\mathcal{M}$ via an SOS program ( 28 ) for polynomial systems, or a nonlinear program (NLP) counterexample search ( 29 ) in the general case. Right: the feasibility branch applies Farkas duality to the affine input constraint system $(A_{\mathrm{dae}},\boldsymbol{r}_{\mathrm{dae}})$ , decomposing the feasibility certificate into an interior condition ( 36 ) and a boundary tangency condition ( 37 ). Both branches are unified in Theorem 7 : if correctness, interior feasibility, and boundary tangency all hold, then $b(x)$ is certified as a valid DAE-aware CBF.

Figure 7: Simulation results for the DAE system ( 4 ) using a DAE-aware CBF. The figure shows (a) the CBF-QP trajectory on the constraint manifold

\phi(x)=0

remaining in the safe region, (b) the evolution of the barrier function

b(x)

(with

b(x_{0})=0.014

and a minimum

b(x(t))=0.0131

), and (c) the evolution of the safe set function

h(x)

(with a minimum

h(x(t))=0.0128

). Both

b(x)

and

h(x)

remain positive over the horizon, indicating safety and feasibility.

Property	SMT (Z3)		SOS ( $d{=}2$ )		SOS ( $d{=}4$ )
Property	#params	time (s)	#params	time (s)	#params	time (s)
Correctness	3	0.01	60	0.04	280	N/A
Interior	7	120.65	405	5.77	8,235	N/A
Boundary	7	126.08	405	5.30	7,695	N/A
Total	17	246.74	870	11.11	16,360	N/A

Table II: Wind turbine: problem size and runtime. Each entry reports the number of parameters and runtime for verifying the corresponding property. Degree-4 SOS timing is omitted due to excessive cost (N/A).

Item	Polynomial		NN (Z3)
Arch	$b(\mathbf{x})=h(\mathbf{x})$		8–8–tanh–8–tanh–1
Verifier	SOS ( $d{=}2$ )		Z3
Subproblem	#params	time (s)	#SMT vars	time (s)
Correctness	165	0.09	3	1.84 ( UNSAT )
Interior	2,565	4.90	4	1.77 ( UNSAT )
Boundary	2,565	4.48	5	1.74 ( UNSAT )

Table III: Flexible link manipulator: problem size and runtime. Each entry reports the problem size and runtime for the corresponding verification subproblem. #SMT vars denotes the number of free real variables in each SMT verification query. The NN has

153

stored parameters, with

4

independent trained quantities. NN times cover the complete verification process; Total sums times only. UNSAT denotes a passed verification check.

Figure 8: Simulation results for the flexible link manipulator. The figure shows (a) the trajectory in configuration space

(\theta_{1},\theta_{2},y_{\mathrm{tip}})

, where the trajectory (blue) starts at the green marker and ends at the red marker, remaining within the safe region (

b(x)\geq 0

, green surface) and below the safety limit (red plane). (b) The manipulator trajectory in workspace, where the end-effector path (yellow) remains below the safety limit

y_{\mathrm{max}}=1.8\,\mathrm{m}

(red dashed); the snapshots indicate the manipulator configuration at selected times. (c) Evolution of the barrier function along the trajectory (with

b(x_{0})=1.800

and with a minimum

b(x(t))=0.2320

), confirming that

b(x(t))\geq 0\,\forall\,t

Explore similar work

Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations
May 8, 2026Jun Zhang, Haibo Zhang, Chun Liu +2Neural Network Verification Control Barrier Functions
School of Mechatronic Engineering and Automation, Shanghai University, Shanghai, China · Beijing Institute of Control Engineering, Beijing, China · School of Mechatronic Engineering and Automation, Shanghai2026 University, Shanghai, China +1
Distributed Predictive Control Barrier Functions: Towards Scalable Safety Certification in Modular Multi-Agent Systems
Mar 31, 2026Jonas Ohnemus, Alexandre Didier, Ahmed Aboudonia +2Safety-Critical Control Control Barrier Functions
Institute for Dynamic Systems and Control, ETH Zurich, 8092 Zurich, Switzerland · University of California Berkeley, 94720 CA, USA
Least Restrictive Hyperplane Control Barrier Functions
Oct 21, 2025Mattias Trende, Petter ÖgrenSafety-Critical Control Control Barrier Functions
The authors are with the Robotics, Perception and Learning Lab., School of Electrical Engineering and Computer Science, Royal Institute of Technology (KTH), SE-100 44 Stockholm, Sweden

May 8, 2026J/K move · Enter open · S save

Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations

Jun Zhang, Haibo Zhang, Chun Liu, Xiaofan Wang+1

School of Mechatronic Engineering and Automation, Shanghai University, Shanghai, China · Beijing Institute of Control Engineering, Beijing, China · School of Mechatronic Engineering and Automation, Shanghai2026 University, Shanghai, China+1

Neural Network Verification Control Barrier Functions

Open paper AskPDF arXiv

Formal verification of neural control barrier functions (NCBFs) remains challenging, especially for neural networks with nonlinear activations like

\tanh

. Existing CROWN-based methods rely on conservative linear relaxations for Jacobian bounds, limiting scalability. We propose LightCROWN, which computes tighter Jacobian bounds by exploiting the analytical properties of activation functions. Experiments on nonlinear control systems including the inverted pendulum, Dubins car, and planar quadrotor demonstrate that LightCROWN improves verification success rates up to 100%, while enhancing speed and scalability. Our approach provides a generalizable improvement for CROWN-based frameworks, enabling more efficient verification of complex NCBFs. The code can be found at github.com/Autonomous-Systems-and-Control-Lab/verify-neural-CBF.

Abstract

Explore similar work

Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations

Distributed Predictive Control Barrier Functions: Towards Scalable Safety Certification in Modular Multi-Agent Systems

Least Restrictive Hyperplane Control Barrier Functions