Computing Control Lyapunov-Barrier Functions:
Softmax Relaxation and Smooth Patching with Formal Guarantees
October 02, 2025
Abstract
We present a computational framework for synthesizing a single smooth Lyapunov function that certifies both asymptotic stability and safety. We show that the existence of a strictly compatible pair of control barrier and control Lyapunov functions (CBF-CLF) guarantees the existence of such a function on the exact safe set certified by the barrier. To maximize the certifiable safe domain while retaining differentiability, we employ a log-sum-exp (softmax) relaxation of the nonsmooth maximum barrier, together with a counterexample-guided refinement that inserts half-space cuts until a strict barrier condition is verifiable. We then patch the softmax barrier with a CLF via an explicit smooth bump construction, which is always feasible under the strict compatibility condition. All conditions are formally verified using a satisfiability modulo theories (SMT) solver, enabled by a reformulation of Farkas’ lemma for encoding strict compatibility. On benchmark systems, including a power converter, we show that the certified safe stabilization regions obtained with the proposed approach are often less conservative than those achieved by state-of-the-art sum-of-squares (SOS) compatible CBF-CLF designs.
Safety; Stability; Formal verification; Control Lyapunov function; Control barrier function; Smooth patching.
1 Introduction↩︎
In many control applications, stability alone is no longer sufficient; formal safety guarantees are equally necessary. Feedback controllers must not only stabilize the system but also enforce state constraints, a requirement that is especially critical in domains such as autonomous vehicles, industrial processes, and robotics, where safe operation is essential for real-world deployment.
Control Lyapunov functions (CLFs) provide a classical framework for stabilizing nonlinear systems, with necessary and sufficient conditions for their existence established in [1] and later exploited to derive a universal control law for control-affine nonlinear systems [2]. Similarly, control barrier functions (CBFs) [3]–[5] enforce safety by constraining the Lie derivative of a barrier function, but they alone do not guarantee stability. This gap has motivated increasing interest in safe stabilization and reach-avoid formulations that combine safety with stability or reachability, as studied in works such as [6]–[14].
A widely used strategy is to couple CBFs and CLFs within an optimization-based framework. For control-affine systems, this is typically formulated as a quadratic program (QP) [4], [15], which can be solved efficiently and deployed online, for instance through model predictive control (MPC) [16]. The main challenge lies in guaranteeing compatibility between the two functions so that the optimization remains feasible. When compatibility is absent, stability is often relaxed and treated as a soft constraint [4], [11], [13]. A further limitation is that such optimization-based formulations may introduce undesired dynamics such as additional equilibrium points [13], and the provable region of attraction, if any, is often considerably smaller than the certified safe region.
An alternative approach is to merge a CLF and a CBF into a single control Lyapunov-barrier function (CLBF) [6]. Once such a function is available, Sontag’s universal formula [2] (or QP with guaranteed feasibility) can be applied to construct a safe stabilizing controller. While conceptually appealing, the drawback—as highlighted in [17], [18] and further discussed in [7], [8]—is that the CLBF conditions of [6] generally fail to hold unless stringent assumptions on the safe set are satisfied. The difficulty stems from topological obstructions: a system with state constraints, whether imposed explicitly by safety requirements or implicitly by limited controllability, may not admit a continuous stabilizing feedback. We refer the reader to the expository work [19] for a discussion on the necessity of discontinuous feedback in nonlinear stabilization.
Converse Lyapunov theorems for safety [20] and for stability under safety constraints [7] are useful for theoretically understanding when a single Lyapunov function can certify both stability and safety. The work in [20] provided a characterization of robust safety using Lyapunov functions. In [7], a general theoretical framework was established that connects Lyapunov and barrier functions through converse results, ensuring stability together with safety and accommodating reach-avoid-stay specifications. This framework has also been extended to cover hybrid systems [21] and stochastic systems [22]. Building on [7], the recent work [8] broadened the scope by deriving necessary conditions for the existence of CLBFs and for the compatibility of CBF-CLF pairs. Complementary to these results, the converse Lyapunov theorem developed in [14] shows that a strictly compatible pair of control Lyapunov and control barrier functions exists if and only if there is a single smooth Lyapunov function that simultaneously certifies asymptotic stability and safety.
Inspired by the work above, and in particular [14], the present paper develops a computational framework to unify strictly compatible CBFs and CLFs into a single CLBF for safe stabilization. Our first motivation is to enlarge the safe stabilization region compared with current approaches based on compatible CBF-CLF pairs [11], [23]. To this end, we propose a natural log-sum-exp (softmax) relaxation of a maximum barrier function, obtained from sublevel safety constraints, as a candidate CBF. Surprisingly, this simple choice often yields barrier functions that are formally verifiable. When verification fails, we introduce a counterexample-guided synthesis procedure that iteratively inserts half-space cuts until a verifiable barrier is obtained. We find that this significantly extends the safe stabilization region achieved by existing CBF-CLF synthesis methods [11], [23], as it does not restrict barrier functions to a fixed template and instead allows them to adapt to the geometry of the safe set. We then search for a compatible CLF and prove theoretically that, under a strict compatibility condition, it is always possible to patch the compatible CBF-CLF pair into a single smooth CLBF. In contrast to methods that require compatibility over larger domains, our approach only imposes strict compatibility on the boundary of the safe set, making the search for compatible CLFs more tractable. Through a series of benchmark examples, we demonstrate that the proposed method outperforms alternative approaches, including sum-of-squares (SOS) synthesis of compatible CBF-CLF pairs.
2 Preliminaries and problem formulation↩︎
2.1 System description↩︎
Consider a nonlinear system in control-affine form \[\label{eq:sys} \dot{x} = f(x) + g(x)u,\tag{1}\] where \(f:\,\mathbb{R}^n \to \mathbb{R}^n\) and \(g:\,\mathbb{R}^n \to \mathbb{R}^{n \times m}\) with \(f(0)=0\). We aim to design a state-feedback controller \(u = \kappa(x)\), where \(\kappa:\,\mathbb{R}^n \to \mathbb{R}^m\) and \(\kappa(0)=0\), such that the origin remains an equilibrium point of the closed-loop system \[\label{eq:clsys} \dot{x} = f(x) + g(x)\kappa(x),\tag{2}\] and solutions of (2 ) satisfy additional properties. In this paper, we focus on asymptotic stabilization under state constraints.
Given a control input \(u:[0,\infty) \to \mathbb{R}^m\) and functions \(f\) and \(g\) satisfying mild conditions, for example \(u\) is locally essentially bounded and \(f\), \(g\) are locally Lipschitz, system (1 ) admits a unique solution \(\phi(t; x, u)\) on its maximal interval of existence. Here, \(\phi(t; x, u)\) denotes the unique trajectory of (2 ) starting from \(x(0)=x\) under the control input \(u\). We call an input signal admissible if a solution exists for it.
2.2 Safety constraints↩︎
Consider multiple state constraints of the form \[\label{eq:constraint} \mathcal{C}_i = \left\{ x \in \mathbb{R}^n \mid h_i(x) \le 1 \right\}, \quad i = 1, \ldots, N,\tag{3}\] where each \(h_i:,\mathbb{R}^n \to \mathbb{R}\) is continuously differentiable. We assume that the safe set is defined as the intersection of the sets above: \[\label{eq:safe95set} \mathcal{C}_{\text{safe}}=\bigcap_{i=1}^N\mathcal{C}_i.\tag{4}\] Equivalently, the safe set can be written as \[\label{eq:hmax} \mathcal{C}_{\text{safe}} = \left\{ x \in \mathbb{R}^n \mid h_{\max}(x) \le 1 \right\},\tag{5}\] where \(h_{\max}(x) := \max_{1 \le i \le N} h_i(x)\). Note that \(h_{\max}\) is generally not continuously differentiable.
Safety is enforced by requiring that solutions of the closed-loop system (2 ) remain in the set \(\mathcal{C}_{\text{safe}}\) whenever they start in \(\mathcal{C}_{\text{safe}}\). Additionally, we impose asymptotic stability. Assuming that the origin lies in the interior of \(\mathcal{C}_{\text{safe}}\), we seek a feedback controller \(u = \kappa(x)\) such that the origin is asymptotically stable for the closed-loop system (2 ), and solutions starting in \(\mathcal{C}_{\text{safe}}\) remain in \(\mathcal{C}_{\text{safe}}\) and converge to the origin as \(t \to \infty\).
This is not always possible unless the set \(\mathcal{C}_{\text{safe}}\) is a controlled forward invariant set for (1 ) and is contained within the domain of null controllability of (1 ).
Definition 1. A set \(\mathcal{C} \subseteq\mathbb{R}^n\) is called controlled forward invariant for system (1 ) if for every \(x \in \mathcal{C}\) there exists an admissible control input \(u\) such that \(\phi(t; x, u)\) is defined for all \(t \ge 0\) and satisfies \(\phi(t; x, u) \in \mathcal{C}\) for all \(t \ge 0\).
Definition 2. The domain of null controllability for (1 ) is defined as \[\mathcal{D} := \left\{ x \in \mathbb{R}^n \,\middle|\, \exists\, u \text{ such that } \phi(t; x, u) \to 0 \text{ as } t \to \infty \right\}.\]
2.3 Problem formulation↩︎
We seek to find a tight under-approximation of \(\mathcal{C}_{\text{safe}}\), denoted by \(\mathcal{C}\), that is represented as the 1-sublevel set of a continuously differentiable function \(W:\,\mathbb{R}^n\rightarrow\mathbb{R}\), i.e., \[\label{eq:set95C} \mathcal{C}=\left\{x\in\mathcal{\mathbb{R}}^n \mid W(x)\le 1\right\}\tag{6}\] Furthermore, we require that \(W\) serves as a control Lyapunov function for (1 ) on \(\mathcal{C}\); that is, \(W\) is positive definite and \[\inf_{u \in \mathbb{R}^m} [L_f W(x) + L_g W(x)u] < 0, \quad \forall x \in \mathcal{C} \setminus \{0\},\] where \(L_f W = \nabla W^\top f\) and \(L_g W = \nabla W^\top g\). As a result, standard results from nonlinear control (e.g., Sontag’s universal formula [2]) apply directly to \(W\) to obtain a safe, stabilizing controllerone of the main benefits of having a single smooth Lyapunov function. These results ensure we can construct a feedback controller that is continuous everywhere except possibly at the origin.
Remark 1. We take a unifying approach that employs a single Lyapunov function to certify both safety and stability, in contrast to the common approach of using a separate barrier function and a Lyapunov function [4]. It has been shown in the literature that, under mild assumptions, this can be done without loss of generality; see, for example, [7], [8], [14], [20] for characterizations of safety and stability using converse Lyapunov functions. In this work, we focus on demonstrating the computational feasibility and benefits of unifying barrier and Lyapunov functions. Despite being merely a control Lyapunov function, \(W\) is also referred to as a control Lyapunov-barrier function (CLBF) to emphasize its dual role in simultaneously certifying stability and safety, in line with recent work on unified Lyapunov-barrier certificates [6]–[8], [14].
3 Softmax relaxation of the safe set↩︎
Often, one of the objectives of a safe stabilizing controller is to maximize the safe domain of attraction, namely the set of initial conditions that converge to the origin while remaining in the safe set \(\mathcal{C}_{\text{safe}}\). A natural choice is to design a barrier function whose \(1\)-sublevel set coincides with \(\mathcal{C}_{\text{safe}}\). Indeed, \(h_{\max}\) in (5 ) provides an exact characterization of \(\mathcal{C}_{\text{safe}}\) via its \(1\)-sublevel set. A potential drawback of using \(h_{\max}\) directly, however, is that it is generally not differentiable.
3.1 Softmax relaxation of the safe set↩︎
We approximate \(h_{\max}\) by the smooth log-sum-exp with temperature \(\tau>0\): \[\label{eq:softmax} h_{\mathrm{sm}}(x;\tau)\;:=\;\frac{1}{\tau}\,\log\!\Big(\sum_{i=1}^N e^{\tau\,h_i(x)}\Big).\tag{7}\] We have the following well-known property of \(h_{\mathrm{sm}}\). The proof is elementary, but we include it for completeness.
Proposition 1. For all \(x \in \mathbb{R}^n\), \[h_{\max}(x) \;\le\; h_{\mathrm{sm}}(x;\tau) \;\le\; h_{\max}(x) + \frac{\log N}{\tau}.\]
Proof. Fix \(x\in\mathbb{R}^n\). Let \(a_i := h_i(x)\) for \(i=1,\dots,N\) and \(a_{\max} := \max_i a_i\). Then \[\sum_{i=1}^N e^{\tau a_i} \;\ge\; e^{\tau a_{\max}}, \qquad \sum_{i=1}^N e^{\tau a_i} \;\le\; N e^{\tau a_{\max}},\] since \(e^{\tau a_i} \le e^{\tau a_{\max}}\) for all \(i\). Taking logarithms and dividing by \(\tau>0\) gives \[a_{\max} \;\le\; \frac{1}{\tau}\log\!\Bigl(\sum_{i=1}^N e^{\tau a_i}\Bigr) \;\le\; a_{\max} + \frac{\log N}{\tau},\] which is precisely the desired inequality. ◻
An immediate consequence of Proposition 1 is that \[\{h_{\mathrm{sm}}\le 1\}\subseteq\{h_{\max}\le 1\}=\mathcal{C}_{\text{safe}}.\] In other words, the 1-sublevel set of \(h_{\mathrm{sm}}\) gives a guaranteed under-approximation of the safe set, and, as \(\tau\to\infty\), \(h_{\mathrm{sm}}\to h_{\max}\) uniformly on compact sets.
3.2 Control barrier condition↩︎
Consider a continuously differentiable function \(h: \mathbb{R}^n \rightarrow \mathbb{R}\). Denote \[\begin{align} \mathcal{C} & = \left\{ x \in \mathbb{R}^n \mid h(x) \le 1 \right\}, \label{safe-set}\\ \partial \mathcal{C} & = \left\{ x \in \mathbb{R}^n \mid h(x) = 1 \right\}. \end{align}\tag{8}\] We rely on the following strict barrier condition on \(h\) to ensure controlled invariance of the set \(\mathcal{C}\).
Definition 3. We say that \(h\) is a strict control barrier function on \(\mathcal{C}\) if, for every \(x\in \partial \mathcal{C}\), there exists \(u\in\mathbb{R}^m\) such that \[\label{eq:cbf} \inf_{u \in \mathbb{R}^m} [L_f h(x) + L_g h(x) u] < 0.\qquad{(1)}\]
Example 1. We consider the following toy example taken from [23] to illustrate the construction of a near-maximal smooth barrier function and its verification.
3.2.0.1 System dynamics
Let \(x = (x_1,x_2)^\top\) and consider the control-affine system (1 ) with \[f(x) = \begin{bmatrix} 0 \\ -\sin x_1 \end{bmatrix}, \quad g(x) = \begin{bmatrix} 1 \\ -1 \end{bmatrix},\] and domain \([-\pi,\pi] \times [-3,4]\).
3.2.0.2 Hard constraints
The safe set is defined by \[h_1(x) := -\sin x_1 - \cos x_1 - x_2 \;\le 1,\] together with box constraints encoding the domain: \[h_{2j}(x) := 1 + x_j - \bar x_j \le 1, \qquad h_{2j+1}(x) := 1 - x_j + \underline x_j \le 1,\] for \(j=1,2,\) where \(\underline x_j\) and \(\bar x_j\) denote the lower and upper bounds of the \(j\)th coordinate.
3.2.0.3 Verified smooth barrier
Let \(h_1,\dots,h_N\) (\(N=5\)) be all constraints above. We construct a smooth log-sum-exp* approximation \(h_{\mathrm{sm}}(x;\tau)\) as defined in ( 7 ). For a wide range of \(\tau\) values, we can formally verify (details to provide in Section 5) the strict barrier condition (?? ). Fig. 1 depicts formally verified \(h_{\mathrm{sm}}(x;\tau)\) for \(\tau=1.5\) and \(\tau=4.5\). It clearly shows that increasing \(\tau\) leads to a closer approximation of the exact safe set boundary. As a comparison, we also depict a state-of-the-art approach that synthesizes compatible Lyapunov and barrier functions using sum-of-squares (SOS) as a comparison. Of course, at the moment, we have only discussed the barrier condition. With the results to be presented in Section 4, we will be able to produce a formally verified single smooth Lyapunov-barrier function that achieves the exact same safe stabilization region enclosed by the softmax barrier.*
![Figure 1: Smooth barrier function h_{\mathrm{sm}}(x) (left) and its 1-level set (right). As a comparison, the best verified safe controllable region obtained using SOS CBF-CLF is shown in dotted red. It can be seen that the softmax relaxation barrier outperforms the SOS approach [23]. Data for comparisons in this and subsequent examples were extracted from published figures using the WebPlotDigitizer tool [24].](ex_softmax_tau_4.5.png "fig:")
3.3 Counterexample-guided refinement↩︎
While in many cases, as we shall see in Section 6, the softmax relaxation barriers readily satisfy the strict barrier condition, there are scenarios in which this is not the case. We present a counterexample-guided refinement procedure that iteratively adds new half-space constraints to the softmax approximation until the barrier condition becomes verifiable.
3.3.0.1 Construction of half-space cuts
Suppose that \(h_{\mathrm{sm}}(x;\tau)\) fails the barrier condition at some counterexample \(x^\ast\in\partial \mathcal{C}\) provided by the verifier. Let \[n := \frac{\nabla h_{\mathrm{sm}}(x^\ast;\tau)}{\|\nabla h_{\mathrm{sm}}(x^\ast;\tau)\|}\] denote the outward unit normal of the current softmax level set at \(x^\ast\). To exclude this point, we generate a new half-space \[\label{eq:new-halfspace} h_{\mathrm{new}}(x) := n_{\mathrm{new}}^\top x - b_{\mathrm{new}} + 1, \qquad h_{\mathrm{new}}(x) \le 1,\tag{9}\] where \(n_{\mathrm{new}}\) is a slight rotation of \(n\): \[n_{\mathrm{new}} := n\cos\theta + r\sin\theta, \qquad r \perp n,\;\|r\|=1,\] with a small angle \(\theta > 0\). The plane is shifted inward by a small margin \(\varepsilon>0\), \(b_{\mathrm{new}} := n_{\mathrm{new}}^\top x^\ast - \varepsilon,\) so that \(x^\ast\) lies strictly outside the updated safe set. The refined constraint set is then \[\{h_1(x)\le 1,\dots,h_N(x)\le 1,h_{\mathrm{new}}(x)\le 1\},\] and a new softmax \(h_{\mathrm{sm}}(x;\tau)\) is built from this set.
3.3.0.2 Algorithm
The procedure repeats this step until either the barrier condition is verified or a maximum number of cuts is reached. This is summarized in Algorithm 2.
Example 2. We consider the nonlinear control-affine system (1 ), taken from [25], with \[f(x)=\begin{bmatrix} 0 \\ -x_1 + x_1^3/6 \end{bmatrix}, \quad g(x)=\begin{bmatrix} 1 \\ -1 \end{bmatrix},\] and domain \([-4.5,4.5]^2\). The unsafe set is given by the single half-space \(h_1(x):= -2 - x_1 - x_2 \le 1\), together with the box constraints defining the domain. We construct a softmax relaxation \(h_{\mathrm{sm}}(x;\tau)\) with \(\tau=3.0\). Direct verification of the control barrier condition on \(h_{\mathrm{sm}}=1\) fails, but applying the counterexample-guided refinement procedure from Algorithm 2 adds a sequence of half-space cuts. Upon termination, the refined softmax barrier is formally verified, and its \(1\)-sublevel set provides a guaranteed controlled invariant subset of the original safe set. Fig. 3 depicts the verified refined softmax barrier for this example.
![Figure 3: Smooth barrier function h_{\mathrm{sm}}(x) (left) and its 1-level set (right) obtained by softmax relaxation and counterexample-guided refinement (Algorithm 2. As a comparison, the best verified safe controllable region obtained using SOS CBF-CLF is shown in dotted red. The softmax relaxation barrier outperforms the SOS approach [25].](ex_2d_nonlinear_tau_3.0.png "fig:")
4 Strict compatibility implies smooth patching↩︎
In the previous section, we demonstrated that the softmax relaxation can yield a significantly less conservative barrier for safety. To ensure safe stabilization, however, we must combine it with a Lyapunov function for stabilization, posed as the main problem in Section 2.3. We address this issue in the present section. The theoretical foundation is a converse Lyapunov theorem for joint safety and stability recently proved in [14]. Our focus here is on efficient and verifiable computation. The proposed approach uses smooth patching with formal guarantees and relies on satisfiability modulo theories (SMT) verification and an analytical formula to patch strictly compatible control barrier and Lyapunov functions. We present this as the main result of the paper.
4.1 Strictly compatible CBF and CLF↩︎
Consider a candidate CBF \(h:\,\mathbb{R}^n\rightarrow\mathbb{R}\) and a candidate CLF \(V:\,\mathbb{R}^n\rightarrow\mathbb{R}\). We assume that both \(h\) and \(V\) are continuously differentiable, \(V\) is positive definite, and the set \(\mathcal{C}\) defined by (8 ) contains the origin in its interior.
Definition 4. We say that \(h\) and \(V\) are strictly compatible if the following conditions hold:
For every \(x \in \mathcal{C} \setminus \{0\}\), there exists \(u\in\mathbb{R}^m\) such that \[\label{eq:CLFV} L_f V(x) + L_g V(x) u < 0.\qquad{(2)}\]
For every \(x \in \partial \mathcal{C}\), there exists \(u\in\mathbb{R}^m\) such that \[\label{eq:CLFBoundary} L_f V(x) + L_g V(x) u < 0,\qquad{(3)}\] and \[\label{eq:CBF} L_f h(x)+L_g h(x) u < 0.\qquad{(4)}\]
Remark 2. We impose the strict form of inequality ?? to ensure robust invariance of \(\partial\mathcal{C}\). This is essential for it to be verifiable by \(\delta\)-complete SMT solvers such as dReal [26]. We also relax the compatibility conditions, see, e.g., [12], [13], [23], to hold only on the boundary of the set \(\mathcal{C}\).
4.2 Smooth patching with guarantees↩︎
We establish the following result on patching a strictly compatible CBF and CLF pair to form a single smooth Lyapunov-barrier function (CLBF).
Theorem 1. Let \(h\) and \(V\) be strictly compatible as defined in Definition 4. Suppose that the set \(\mathcal{C}\) is compact. Then there exists a continuously differentiable function \(W:\,\mathbb{R}^n\rightarrow\mathbb{R}\) with the following properties:
\(\mathcal{C}=\left\{x\in\mathcal{\mathbb{R}}^n \mid W(x)\le 1\right\}\).
For every \(x \in \mathcal{C} \setminus \{0\}\), there exists \(u\in\mathbb{R}^m\) such that \[\label{eq:CLFW} L_f W(x) + L_g W(x) u < 0.\qquad{(5)}\]
Proof. Fix \(\varepsilon \in (0,1)\) and define the inner boundary band \[\partial\mathcal{C}_{\varepsilon}^{-} := \{x : 1-\varepsilon \le h(x) \le 1\}.\] By strict compatibility and compactness of \(\mathcal{C}\), we can choose \(\varepsilon>0\) such that, for every \(x \in \partial\mathcal{C}_{\varepsilon}^{-}\), there exists \(u\) such that both \(L_f V(x) + L_g V(x) u < 0\) and \(L_f h(x) + L_g h(x) u < 0\). We also assume that \(\varepsilon>0\) is sufficiently small such that \(0\not\in \partial\mathcal{C}_{\varepsilon}^{-}\).
Since \(\mathcal{C}\) is compact, we can choose \(\alpha > 0\) such that \(V_2 := \alpha V\) satisfies \[\quad V_2(x) \le 1 \;\forall x \in \mathcal{C}, \qquad V_2(x) \le h(x) \;\forall x \in \partial\mathcal{C}_{\varepsilon}^{-}.\] Indeed, we can simply choose \[\alpha = \frac{1-\varepsilon}{\max_{x\in \mathcal{C}} V(x)}.\]
Define a \(C^1\) bump function supported on the band: \[b(x)= \begin{cases} \exp\!\Bigl(-\dfrac{1}{\varepsilon^2 - (h(x)-1)^2} + \dfrac{1}{\varepsilon^2}\Bigr), & 1-\varepsilon < h(x) < 1,\\[4pt] 1, & h(x) \ge 1,\\ 0, & h(x) \le 1-\varepsilon. \end{cases}\] Now define the patched function \[\label{eq:patched95W} W(x) := (1-b(x)) V_2(x) + b(x) h(x),\tag{10}\] which is \(C^1\) by construction, with gradient \[\label{eq:grad95W} \nabla W = b \nabla h + (1-b)\nabla V_2 + (h - V_2)\nabla b.\tag{11}\]
We verify the following properties of \(W\).
Property (1): Exact safe set. If \(h > 1\), then \(b=1\) and \(W=h > 1\). This implies \(\{W \le 1\} \subseteq\{h \le 1\}\).
If \(h \le 1-\varepsilon\), then \(b=0\) and \(W=V_2 \le 1\). If \(1-\varepsilon<h<1\), then \(0<b<1\) and \(W=(1-b)V_2 + b h \le 1\) since \(V_2 \le 1\) on \(\mathcal{C}\) and \(h \le 1\) in the band. These together imply \(\{h \le 1\} \subseteq\{W \le 1\}\).
Thus \(\{W \le 1\} = \{h \le 1\} = \mathcal{C}\).
Property (2): Strict CLF condition. Following (11 ), we further compute \[\nabla b(x) = \begin{cases} p(x)\,\nabla h(x), & \quad \text{if } 1-\varepsilon < h(x) < 1, \\[6pt] 0, & \quad \text{if } h(x) \ge 1 \text{ or } h(x) \le 1-\varepsilon, \end{cases}\] where \[p(x) = \exp\!\Bigl(-\dfrac{1}{\varepsilon^2 - (h-1)^2} + \dfrac{1}{\varepsilon^2}\Bigr) \frac{2(1-h)}{\bigl(\varepsilon^2-(h-1)^2\bigr)^2}.\] Take \(x \in \mathcal{C} \setminus \{0\}\).
If \(h(x) \le 1-\varepsilon\), then \(b=0\), \(\nabla b=0\), and \(\nabla W = \nabla V_2 = \alpha \nabla V\). The CLF condition (?? ) holds for \(W\) because \(V\) satisfies the CLF condition (?? ).
If \(1-\varepsilon < h(x) \le 1\), then \[\nabla W = \bigl(b+(h - V_2)p\bigr)\nabla h + (1-b)\nabla V_2,\] where \(p\ge 0\) and \(h - V_2 \ge 0\). By strict compatibility of \(h\) and \(V\), for each \(x\), there exists \(u\) such that \(\nabla h^\top (f+gu)<0\) and \(\nabla V_2^\top (f+gu)<0\) simultaneously. This implies \(\nabla W^\top (f+gu)< 0\).
Therefore, for every \(x \in \mathcal{C} \setminus \{0\}\), there exists \(u\) such that \(L_f W(x) + L_g W(x) u < 0\). ◻
The following corollary is a direct application of Theorem 1 and is a well-established result in nonlinear control.
Corollary 1. Under the assumptions of Theorem 1, there exists a feedback controller \(\kappa:\,\mathbb{R}^n\rightarrow\mathbb{R}\) such that the origin is asymptotically stable for the closed-loop system (2 ), and solutions starting in \(\mathcal{C}\) remain in \(\mathcal{C}\) and converge to the origin as \(t \to \infty\). Furthermore, \(\kappa\) can be chosen to be smooth on \(\mathbb{R}^n\setminus\left\{0\right\}\).
Remark 3. If \(V\) satisfies the small control property [2], then so does \(W\) constructed in 10 . Consequently, the feedback law \(\kappa\) in the corollary is continuous at the origin. Moreover, \(\kappa\) can be explicitly constructed using Sontag’s universal stabilization formula [2].
5 SMT verification↩︎
In this section, we discuss formal verification of the strict barrier condition ?? introduced in Section 3 and the strict compatibility between control barrier and Lyapunov conditions defined in Section 4. Once these conditions are verified, the function \(W\) constructed in Theorem 1 is a continuously differentiable CLBF that can be used for safe stabilization.
5.1 Verification of strict CBF↩︎
The strict CBF condition (?? ) is equivalent to \[\label{eq:cbf-verification} (L_g h(x) = 0 \wedge h(x) = 1) \Longrightarrow L_f h(x)<0.\tag{12}\] The barrier function \(h\) constructed using the softmax relaxation (7 ) involves transcendental functions \(\log\) and \(\exp\). Over a compact domain, condition (12 ) can be readily verified by a \(\delta\)-complete SMT solver such as dReal [26].
5.2 Verification of CBF-CLF compatibility↩︎
The strict compatibility conditions proposed in Definition 4 include a CLF condition for \(V\) on \(\mathcal{C}\), which is equivalent to \[\label{eq:clf-verification} (L_g V(x) = 0 \wedge h(x) \le 1) \Longrightarrow L_f V(x)<0.\tag{13}\] Similar to 12 , this can be readily verified using an SMT solver such as dReal [26]. The synthesis of CLFs using SMT solvers and neural networks has been discussed in detail in [27]. We refer the reader to [27] for a detailed discussion of the formal verification of the CLF condition 13 , in particular the treatment of difficulties near the origin when using dReal, which is only \(\delta\)-complete and may return spurious counterexamples in a neighborhood of the origin.
Furthermore, Definition 4 includes a strict compatibility condition ?? –?? between \(V\) and \(h\) on the boundary of \(\mathcal{C}\). Because this condition has the quantifier structure \(\forall x \, \exists u\), it cannot be readily handled by dReal, which supports only quantifier-free or purely universal formulas. We use the following variant of Farkas’ lemma [28] to addresses this issue.
Lemma 1 (Farkas’ Lemma). Let \(A \in \mathbb{R}^{n \times m}\) and \(b \in \mathbb{R}^n\). The system \(A u \le b\), \(u \in \mathbb{R}^m\), has a solution if and only if every nonnegative \(y \in \mathbb{R}^n\) with \(y^\top A = 0^\top \in \mathbb{R}^{1 \times m}\) also satisfies \(y^\top b \ge 0\).
We reformulate Farkas’ Lemma in a strict inequality form and add a normalization to the vector \(y\).
Lemma 2 (Farkas’ Lemma Reformulation). Let \(A \in \mathbb{R}^{n \times m}\) and \(b \in \mathbb{R}^n\). The system \(A u < b\), \(u \in \mathbb{R}^m\), has a solution if and only if every nonnegative \(\lambda \in \mathbb{R}^n\) with \(\lambda^\top A = 0^\top \in \mathbb{R}^{1 \times m}\) and \(\sum_{i=1}^n \lambda_i=1\) also satisfies \(\lambda^\top b > 0\).
Proof. (\(\Rightarrow\)) We have \[\lambda^\top b\;=\;\lambda^\top(b-Au)+\underbrace{\lambda^\top A u}_{=\,0}\;=\;\sum_{i=1}^n \lambda_i\,(b_i-a_i^\top u)\;>\;0,\] because each \(b_i-a_i^\top u>0\) and \(\lambda_i\ge 0\) with \(\sum_{i=1}^n \lambda_i=1\).
(\(\Leftarrow\)) Suppose no \(u\) satisfies \(Au<b\). Then for every \(u\) there exists an index \(i\) such that \(a_i^\top u \ge b_i\). Equivalently, the convex sets \[\{ (Au-b) \in \mathbb{R}^n : u \in \mathbb{R}^m \}, \qquad \mathbb{R}^n_{<0}\] are disjoint. By the separating hyperplane theorem [29], there exists a nonzero vector \(\tilde{\lambda} \in \mathbb{R}^n\) such that \[\tilde{\lambda}^\top(Au-b) \;\ge\; 0\quad \forall u\in\mathbb{R}^m, \qquad \tilde{\lambda}^\top c \;\le\; 0\quad \forall c \in \mathbb{R}^n_{<0}.\] The second condition implies \(\tilde{\lambda} \ge 0\). The first condition implies \(\tilde{\lambda}^\top A=0\) (otherwise one can choose \(u\) in the direction of \(-(\tilde{\lambda}^\top A)\) to violate the inequality), and then \(\tilde{\lambda}^\top b \le 0\). Set \[\lambda = \frac{\tilde{\lambda}}{\sum_{i=1}^n \tilde{\lambda}_i},\] so that \(\lambda \ge 0\), \(\sum_i \lambda_i = 1\), \(\lambda^\top A=0\), and \(\lambda^\top b \le 0\). This contradicts the assumption that all such \(\lambda\) satisfy \(\lambda^\top b > 0\). Therefore, \(\exists u\) with \(Au<b\). ◻
We now state the conditions that we can verify for strict compatibility.
Lemma 3. The strict compatibility condition ?? –?? is equivalent to \[\label{eq:farkas} \begin{align} & ((h(x)=1) \\ & \wedge (\lambda_1 \ge 0 \wedge \lambda_2 \ge 0 \wedge \lambda_1 + \lambda_2=1) \\ & \wedge (\lambda_1 L_g V(x)+\lambda_2 L_g h(x)=0))\\ & \Longrightarrow \lambda_1 L_f V(x) + \lambda_2 L_f h(x) <0. \end{align}\qquad{(6)}\]
Proof. Write \[A(x)\;=\;\begin{bmatrix}L_g V(x)\\[2pt] L_g h(x)\end{bmatrix}\in\mathbb{R}^{2\times m},\; b(x)\;=\;\begin{bmatrix}-L_f V(x)\\[2pt] -L_f h(x)\end{bmatrix}\in\mathbb{R}^{2}.\] Fix any \(x\in \partial \mathcal{C}\) and write \(\lambda=(\lambda_1,\lambda_2)^\top\). Then the strict compatibility is \(\exists u:\;A(x)u<b(x)\) componentwise, and ?? is \[\forall\,\lambda\in\mathbb{R}_{\ge 0}^2,\;\lambda_1+\lambda_2=1,\;\lambda^\top A(x)=0^\top\;:\;\lambda^\top b(x)<0.\] Their equivalence is precisely Lemma 2. ◻
Remark 4. We consider a strict inequality formulation and add a simplex normalization to \(\lambda\) so that (?? ) can be handled by \(\delta\)-complete SMT solvers such as dReal [26], which are effective essentially only for strict inequalities over compact domains.
Remark 5. We verify (12 ), (13 ), and (?? ) sequentially. To enable guaranteed patching of CBF and CLF by Theorem 1 using the explicit formula (10 ), we also do a bisection search to compute \(\varepsilon\in(0,1)\) such that \[\label{eq:farkas-band} \begin{align} & ((1-\varepsilon\le h(x)\le 1) \\ & \wedge (\lambda_1 \ge 0 \wedge \lambda_2 \ge 0 \wedge \lambda_1 + \lambda_2=1) \\ & \wedge (\lambda_1 L_g V(x)+\lambda_2 L_g h(x)=0))\\ & \Longrightarrow \lambda_1 L_f V(x) + \lambda_2 L_f h(x) <0. \end{align}\qquad{(7)}\] is verified. This implies strict compatibility of \(h\) and \(V\) on the band \[\partial\mathcal{C}_{\varepsilon}^{-} := \{x : 1-\varepsilon \le h(x) \le 1\}.\] defined in the proof of Theorem 1. Upon successful verification of these inequalities, the single Lyapunov function \(W\) defined by (10 ) provides both a certificate and a means for computing provably safe, stabilizing controllers. In the next section, we demonstrate that this approach is effective and can provide less conservative safe stabilization regions, compared to alternative approaches.
6 Numerical examples↩︎
We illustrate the effectiveness of the proposed approach with several nonlinear control examples. All computations were performed on a 2020 MacBook Pro with a 2 GHz quad-core Intel Core i5 processor and solved within the toolbox LyZNet [30], supported by dReal [26] as the
verification engine. The code for all examples presented here, as well as additional examples, is available at https://git.uwaterloo.ca/hybrid-systems-lab/lyznet under
examples/patch-clbf.
Example 3. We first revisit Example 1. Upon formally verifying the softmax barrier \(h=h_{\mathrm{sm}}\), defined in (7 ) with \(\tau=4.5\), as a strict barrier function using (12 ), we also formally verify its strict compatibility with a quadratic CLF. The strict barrier condition was certified in less than \(0.01\)s, and strict compatibility in \(0.42\)s. The latter involved a bisection procedure to determine the largest \(\varepsilon\) such that strict compatibility (?? ) holds on the band \(\left\{x : 1-\varepsilon \le h(x) \le 1\right\}\) (capped at \(\varepsilon=0.5\)). The CLF we verify is the quadratic function \(V(x)=x_1^2+2x_2^2\). Figure 4 depicts the patched CLBF and the phase portrait of the closed-loop system under Sontag’s controller [2]. Figure 5 shows 50 simulated trajectories from the set \(\mathcal{C}=\left\{h\le 1\right\}\), along with the evaluation of \(h\) to demonstrate safety. The barrier function \(h\) itself cannot serve as a Lyapunov function on \(\mathcal{C}\), not only because it takes negative values, but also because it has a stationary point at \(x = (0.1294085, 0.94176161)^\top\) (numerically confirmed via gradient descent). Patching it with a quadratic CLF yields a provable CLBF, as demonstrated here.
![Figure 4: A smooth Lyapunov-barrier function patched from a strictly compatible CBF-CLF pair for Example 3. The green dash-dotted line represents the formally verified safe stabilization region, relative to the unsafe region (shaded in light red). For comparison, the best verified safe controllable region obtained using compatible SOS CBF-CLF [23] is shown in dotted red, while the dashed red curve depicts the largest safe stabilization region certified by a quadratic CLF.](2d_toy_clbf_tau=4.5.png "fig:")
Figure 5: Simulated trajectories and corresponding barrier function values for Example 3. All trajectories converge, and the barrier function values remain below the safe threshold of 1..
Example 4. Revisit Example 2. We are able to formally verify strict compatibility of the CBF \(h\) depicted in Fig. 3 with the simple CLF \(V(x) = x_1^2 + x_2^2\). The patched CLBF using (10 ) and Theorem 1 is shown in Fig. 6, along with the phase portrait of the closed-loop system.
![Figure 6: A smooth control Lyapunov-barrier function patched from a strictly compatible CBF-CLF pair for Example 4. The green dash-dotted line represents the formally verified safe stabilization region, relative to the unsafe region (shaded in light red). For comparison, the best verified safe controllable region obtained using compatible SOS CBF-CLF [25] is shown in dotted red, while the dashed red curve depicts the largest safe stabilization region certified by a quadratic CLF.](2d_nonlinear_clbf_tau=3.0.png "fig:")
Example 5. We consider the nonlinear control-affine system (1 ), taken from [25], with \[f(x)=\begin{bmatrix}x_1+x_2\\ -2x_1+3x_2 \end{bmatrix}, \quad g(x)=\begin{bmatrix} 1 & 0 \\ 0 & 1 \end{bmatrix},\] and domain \([-10,10]^2\). The unsafe set is given by the single half-space \(h_1(x):= -2 - x_1 - x_2 \le 1\), together with the box constraints defining the domain. We can verify strict compatibility of the softmax barrier function \(h=h_{\mathrm{sm}}\) (\(\tau=10.0\)) with a quadratic CLF \(V\). The resulting patched CLBF using (10 ) and Theorem 1 is depicted in Fig. 7.
![Figure 7: A smooth control Lyapunov-barrier function patched from a strictly compatible CBF-CLF pair for Example 5. The green dash-dotted line represents the formally verified safe stabilization region, relative to the unsafe region (shaded in light red). For comparison, the best verified safe controllable region obtained using compatible SOS CBF-CLF [25] is shown in dotted red.](2d_linear_clbf_tau=10.0.png "fig:")
Example 6. We consider the case study of a power converter, taken from [31] and also used in [25], which is a nonlinear control-affine system 1 with \[f(x)=\begin{bmatrix} -0.05x_1 - 57.9x_2 + 0.00919x_3\\[2pt] 1710x_1 + 314x_3\\[2pt] -0.271x_1 - 314x_2 \end{bmatrix},\] \[g(x)=\begin{bmatrix} 0.05 - 57.9x_2 & -57.9x_3\\[2pt] 1710 + 1710x_1 & 0\\[2pt] 0 & 1710 + 1710x_1 \end{bmatrix},\] on the domain \([-2,2]^3\). The unsafe set is specified by \[x_1 \le 0.2, \quad x_1 \ge -0.8, \quad (x_2-0.001)^2 + x_3^2 \le 1.2^2,\] together with the box constraints defining the domain. Here, the state vector \(x=(x_1,x_2,x_3)^\top\) corresponds to the measured quantities \((v_{dc},i_d,i_q)^\top\), where \(v_{dc}\) is the DC-link voltage and \(i_d,i_q\) are the direct- and quadrature-axis currents in the synchronous \(dq\)-frame [31]. We construct a softmax barrier function \(h=h_{\mathrm{sm}}\) with \(\tau=3.1\) and verify strict compatibility with a quadratic CLF \(V\) on the boundary band. The strict barrier condition was certified in less than \(0.01\)s, and strict compatibility in \(0.59\)s. The patched CLBF obtained from 10 using Theorem 1 is depicted in Fig. 8.
![Figure 8: A patched control Lyapunov-barrier function for Example 6. 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 [25] is shown in dotted red.](3d_power_converter_softmax_tau=3.1.png "fig:")
7 Conclusions↩︎
We developed a computational framework for constructing a single smooth Lyapunov function that certifies both stability and safety, enabled by softmax barrier relaxations, strict compatibility verification of CBF-CLF pairs, and explicitly defined smooth patching. Formal guarantees were established using \(\delta\)-complete SMT solvers, and the method was demonstrated on benchmark systems and compared with an alternative sum-of-squares approach. Future work will focus on incorporating input constraints and extending the approach with compositional verification techniques to scale to high-dimensional systems.
References↩︎
This research was supported in part by the Natural Sciences and Engineering Research Council of Canada and the Canada Research Chairs program.↩︎
Jun Liu and Maxwell Fitzsimmons are with the Department of Applied Mathematics, University of Waterloo, Waterloo, Ontario N2L 3G1, Canada. Email:
j.liu@uwaterloo.ca (Jun Liu)↩︎