Here is a video where we are testing our Coq verified altitude limiter with some aggressive flying close to the height boundary. First, I try flying up to the altitude boundary while flying aggressively to the right. Then, with throttle pushed all the way up, I try various motions in other directions, including so-called yaw (essentially pivoting). As you can see, the altitude limiter keeps engaging (since the throttle is all the way up), and it keeps the quadcopter within the appropriate bounds, while allowing control in other dimensions.