Lipschitz Optimization for Formal Verification of Homographies

The adoption of vision neural networks in regulated industries requires formal robustness guarantees, especially in safety-critical domains such as healthcare, aerospace, and autonomous vehicles. However, current approaches are confined to incomplete statistical verification, or robustness to $\ell_p$-norm or affine transforms which represent a limited subset of perturbations to the image formation process.In this paper, we present a formal verification approach when the capturing camera undergoes 3D motion perturbations. We first establish a closed-form mapping from camera pose to pixel values. By analyzing the continuity properties of the resulting homographies, we show that recent work on Lipschitz optimization and piecewise continuity can be extended to derive tight linear bounds on perturbed pixel values. While our formulae are grounded in the vision-based landing problem, they generalize to other scenes with predominantly planar features (e.g., augmented reality, traffic signs). This enables formal verification against a broad class of projective geometry transformations, without requiring simulation or complex modeling of image formation.We first validate our implementation, and show up to 89\% speedup and 7\% tighter bounds than the latest work. We then evaluate our method on established benchmarks from the VNN Competition, and highlight key model vulnerabilities to 3D transforms. Finally, we perform the first formal verification of a vision-based landing system under 3D perturbations, addressing a key challenge in the regulatory certification of learned models for real-world systems. The data and code used for this paper are publicly available.