# NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing

arXiv: https://arxiv.org/abs/2203.15841 · HTML: https://mlsanity.com/paper/2203.15841/

## Key facts

- Cited by 19 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 28 references that are in the map.
- First posted on arXiv 29 Mar 2022.

## Builds on (most cited first, 10 of 10)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI](https://mlsanity.com/paper/2005.07173/) (2020)
- [Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks](https://mlsanity.com/paper/2111.09293/) (2021)
- [Bounding the Complexity of Formally Verifying Neural Networks: A Geometric Approach](https://mlsanity.com/paper/2012.11761/) (2020)
- [Safe-by-Repair: A Convex Optimization Approach for Repairing Unsafe Two-Level Lattice Neural Network Controllers](https://mlsanity.com/paper/2104.02788/) (2021)
- [Provably Correct Training of Neural Network Controllers Using Reachability Analysis](https://mlsanity.com/paper/2102.10806/) (2021)

## Built on by (most cited first, 19 of 19)

- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [How Safe Am I Given What I See? Calibrated Prediction of Safety Chances for Image-Controlled Autonomy](https://mlsanity.com/paper/2308.12252/) (2023)
- [Discovering Closed-Loop Failures of Vision-Based Controllers via Reachability Analysis](https://mlsanity.com/paper/2211.02736/) (2022)
- [DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation](https://mlsanity.com/paper/2305.13508/) (2023)
- [Bridging Dimensions: Confident Reachability for High-Dimensional Controllers](https://mlsanity.com/paper/2311.04843/) (2023)
- [Certifying Robustness of Learning-Based Keypoint Detection and Pose Estimation Methods](https://mlsanity.com/paper/2408.00117/) (2024)
- [Scenario-based Compositional Verification of Autonomous Systems with Neural Perception](https://mlsanity.com/paper/2504.20942/) (2025)
- [Learning Ensembles of Vision-based Safety Control Filters](https://mlsanity.com/paper/2412.02029/) (2024)
- [Deterministic World Models for Closed-loop Reachability Analysis of End-to-End Vision-based Control](https://mlsanity.com/paper/2512.08991/) (2025)
- [Assumption Generation for the Verification of Learning-Enabled Autonomous Systems](https://mlsanity.com/paper/2305.18372/) (2023)
- [Refining Perception Contracts: Case Studies in Vision-based Safe Auto-landing](https://mlsanity.com/paper/2311.08652/) (2023)
- [Pre-Trained Vision Models as Perception Backbones for Safety Filters in Autonomous Driving](https://mlsanity.com/paper/2410.22585/) (2024)
- [How Safe Will I Be Given What I Saw? Calibrated Prediction of Safety Chances for Image-Controlled Autonomy](https://mlsanity.com/paper/2508.09346/) (2025)
- [Certifying Safety in Reinforcement Learning under Adversarial Perturbation Attacks](https://mlsanity.com/paper/2212.14115/) (2022)
- [Efficient Reachability Analysis for Convolutional Neural Networks Using Hybrid Zonotopes](https://mlsanity.com/paper/2503.10840/) (2025)
- [Verification of Visual Controllers via Compositional Geometric Transformations](https://mlsanity.com/paper/2507.04523/) (2025)
- [Perception with Guarantees: Certified Pose Estimation via Reachability Analysis](https://mlsanity.com/paper/2602.10032/) (2026)
- [From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications](https://mlsanity.com/paper/2603.05604/) (2026)
- [Stochastic World Models for Verifying Vision-Based Neural Feedback Systems](https://mlsanity.com/paper/2609.38120/) (2026)

## Abstract (arXiv)

In this paper, we consider the problem of formally verifying a Neural Network (NN) based autonomous landing system. In such a system, a NN controller processes images from a camera to guide the aircraft while approaching the runway. A central challenge for the safety and liveness verification of vision-based closed-loop systems is the lack of mathematical models that captures the relation between the system states (e.g., position of the aircraft) and the images processed by the vision-based NN controller. Another challenge is the limited abilities of state-of-the-art NN model checkers. Such model checkers can reason only about simple input-output robustness properties of neural networks. This limitation creates a gap between the NN model checker abilities and the need to verify a closed-loop system while considering the aircraft dynamics, the perception components, and the NN controller. To this end, this paper presents NNLander-VeriF, a framework to verify vision-based NN controllers used for autonomous landing. NNLander-VeriF addresses the challenges above by exploiting geometric models of perspective cameras to obtain a mathematical model that captures the relation between the aircraft states and the inputs to the NN controller. By converting this model into a NN (with manually assigned weights) and composing it with the NN controller, one can capture the relation between aircraft states and control actions using one augmented NN. Such an augmented NN model leads to a natural encoding of the closed-loop verification into several NN robustness queries, which state-of-the-art NN model checkers can handle. Finally, we evaluate our framework to formally verify the properties of a trained NN and we show its efficiency.