Formal Verification of Control Lyapunov-Barrier Functions for Safe Stabilization with Bounded Controls

TL;DR

This paper addresses safe stabilization of nonlinear control-affine systems under bounded inputs by constructing a single smooth control Lyapunov-barrier function (CLBF) that certifies both asymptotic stability and safety. It derives verifiable, SMT-ready conditions for strict compatibility between a control barrier function (CBF) and a control Lyapunov function (CLF) under ball and box input bounds, employing Farkas' lemmas to reformulate quantifier structures. A provably correct patching scheme combines a CBF and a CLF into a CLBF $W$, with a smooth bump and a log-sum-exp surrogate for the safe set, enabling explicit safe stabilizing controllers via universal formulas. Numerical examples demonstrate the approach on two nonlinear systems, showing reduced conservatism relative to SOS-based compatible CBF-CLF designs and validating the formal guarantees via $\,\delta$-complete SMT verification with $dReal$.

Abstract

We present verifiable conditions for synthesizing a single smooth Lyapunov function that certifies both asymptotic stability and safety under bounded controls. These sufficient conditions ensure the strict compatibility of a control barrier function (CBF) and a control Lyapunov function (CLF) on the exact safe set certified by the barrier. An explicit smooth control Lyapunov-barrier function (CLBF) is then constructed via a patching formula that is provably correct by design. Two examples illustrate the computational procedure, showing that the proposed approach is less conservative than sum-of-squares (SOS)-based compatible CBF-CLF designs.

Figures (4)

• Figure 1: Formally verified smooth CLBF constructed by patching a strictly compatible CBF-CLF pair for Example \ref{['ex:2d_toy_verified']}. The green dash-dotted curve marks the verified safe stabilization region under bounded inputs $u \in [-1,1]$, shown relative to the unsafe region (light red). For comparison, the dotted and dashed red curves indicate the largest verified regions from the SOS-based compatible CBF-CLF approach dai2024verification and a quadratic CLF, respectively.
• Figure 2: Simulated trajectories, control inputs, and corresponding barrier function evaluations for Example \ref{['ex:2d_toy_verified']}. All trajectories converge, control input bounds are satisfied, and the barrier function values stay below the safety threshold of 1.
• Figure 3: A formally verified CLBF for Example \ref{['ex:3d_power']} subject to input constraint $\mathcal{U}=[-2,2]^2$. The green dash-dot curve represents the formally verified safe stabilization region, relative to the unsafe region (shaded in light red). For comparison, the best reported SOS CBF-CLF result dai2024verificationv1 is shown in dotted red.
• Figure 4: Simulated trajectories, control inputs, and corresponding barrier function evaluations for Example \ref{['ex:3d_power']}. All trajectories converge, control input bounds are satisfied, and the barrier function values stay below the safety threshold of 1.

Theorems & Definitions (11)

• Proposition 1
• proof
• Definition 1: quartz2025converse
• Proposition 2
• Lemma 1: Farkas' Lemma
• Lemma 2: Second-Order Conic Farkas' Lemma
• Proposition 3
• proof
• Example IV.1
• Example IV.2