Formal verification of tilt estimation using the Rocq prover

Abstract

The safe operation of a humanoid robot critically relies on accurate estimation of its vertical orientation, or ``tilt''. This requires a variety of mathematical tools, including three-dimensional geometry and differential equations. To formally verify tilt estimation, we develop a library for stability analysis in the Rocq prover. We start by formalizing a theory of ordinary differential equations. We provide a formalization of the (local) Cauchy-Lipschitz (a.k.a. Picard-Lindelof) theorem for existence and uniqueness, taking advantage of the library support for quotients provided by the Mathematical Components library. We extend this formalization with a variant for global existence and continuous dependence on initial conditions. Building on these foundations, we develop a theory of Lyapunov stability that is compatible with an existing formalization of LaSalle's invariance principle. We also extend an existing library for the statics of robot manipulators to support dynamical systems. Finally, we apply these libraries to the verification of a state-of-the-art tilt estimation developed for a humanoid robot.