{"ID":2842383,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.10510","arxiv_id":"2511.10510","title":"Formal Verification of Control Lyapunov-Barrier Functions for Safe Stabilization with Bounded Controls","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.","short_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 cert...","url_abs":"https://arxiv.org/abs/2511.10510","url_pdf":"https://arxiv.org/pdf/2511.10510v1","authors":"[\"Jun Liu\"]","published":"2025-11-13T17:14:54Z","proceeding":"eess.SY","tasks":"[\"eess.SY\",\"math.OC\"]","methods":"[]","has_code":false}