  This paper presents, in a unified fashion, deterministic as well as
statistical Lagrangian-verification techniques. They formally quantify the
behavioral robustness of any time-continuous process, formulated as a
continuous-depth model. To this end, we review LRT-NG, SLR, and GoTube,
algorithms for constructing a tight reachtube, that is, an over-approximation
of the set of states reachable within a given time-horizon, and provide
guarantees for the reachtube bounds. We compare the usage of the variational
equations, associated to the system equations, the mean value theorem, and the
Lipschitz constants, in achieving deterministic and statistical guarantees. In
LRT-NG, the Lipschitz constant is used as a bloating factor of the initial
perturbation, to compute the radius of an ellipsoid in an optimal metric, which
over-approximates the set of reachable states. In SLR and GoTube, we get
statistical guarantees, by using the Lipschitz constants to compute local balls
around samples. These are needed to calculate the probability of having found
an upper bound, of the true maximum perturbation at every timestep. Our
experiments demonstrate the superior performance of Lagrangian techniques, when
compared to LRT, Flow*, and CAPD, and illustrate their use in the robustness
analysis of various continuous-depth models.
