  We study the problem of verification and synthesis of robust control barrier
functions (CBF) for control-affine polynomial systems with bounded additive
uncertainty and convex polynomial constraints on the control. We first
formulate robust CBF verification and synthesis as multilevel polynomial
optimization problems (POP), where verification optimizes -- in three levels --
the uncertainty, control, and state, while synthesis additionally optimizes the
parameter of a chosen parametric CBF candidate. We then show that, by invoking
the KKT conditions of the inner optimizations over uncertainty and control, the
verification problem can be simplified as a single-level POP and the synthesis
problem reduces to a min-max POP. This reduction leads to multilevel
semidefinite relaxations. For the verification problem, we apply Lasserre's
hierarchy of moment relaxations. For the synthesis problem, we draw connections
to existing relaxation techniques for robust min-max POP, which first use
sum-of-squares programming to find increasingly tight polynomial lower bounds
to the unknown value function of the verification POP, and then call Lasserre's
hierarchy again to maximize the lower bounds. Both semidefinite relaxations
guarantee asymptotic global convergence to optimality. We provide an in-depth
study of our framework on the controlled Van der Pol Oscillator, both with and
without additive uncertainty.
