Model-Free Safety-Critical Control for Robotic Systems

The paper’s Theorem 3 constructs the same Lyapunov–barrier function hV(q,ė) = −V(q,ė) + αe h(q) with αe = ((λ−α)k1)/Ch and shows ḣV ≥ −α hV on SV, yielding forward invariance by a CBF-style argument (via Theorem 2) . The candidate solution uses the identical hV and constants, proves ḣV ≥ 0 on the boundary hV=0, and applies a first-exit-time contradiction to establish invariance—an equivalent argument. Minor differences are present in how invariance is certified (global differential inequality vs. boundary condition), but the logic, assumptions, and result coincide with the paper’s proof. The only omissions in the model’s write-up are small: it does not restate the paper’s nonzero-gradient-on-S condition for h and the standard existence/uniqueness assumptions used in the paper’s preliminaries .