Mathematical Proof Meets Machine Learning: NASA Team Formally Verifies AI Runway Advisor

Every day at major airports, controllers make a decision that quietly shapes the safety and efficiency of the entire national airspace: which runways should arriving and departing aircraft use. The choice depends on wind speed and direction, traffic load, visibility, and the geometry of the airfield itself. Now, a team at NASA’s Ames Research Center has taken an unusual step toward trusting artificial intelligence with that decision. Rather than simply testing their machine learning tool with more data, they subjected it to formal verification, a mathematical technique borrowed from computer science that can prove, rather than merely suggest, whether a system behaves safely. The results, published in Frontiers in Aerospace Engineering, show that their Runway Configuration Assistance (RCA) tool satisfied strict wind safety criteria in 94 percent of predictions under realistic conditions, and about 70 percent under deliberately harsh, worst-case winds.

The RCA tool is the product of a line of research the group has developed over several years. At its core is an approach called offline model-free reinforcement learning, specifically an algorithm known as Conservative Q-Learning. In conventional reinforcement learning, an agent learns by trial and error, interacting with its environment and adjusting its strategy based on rewards. That is fine for games, but unthinkable for an airport, where early mistakes during learning could put aircraft at risk. Offline reinforcement learning sidesteps the problem entirely: the algorithm never touches the live operational environment. Instead, it learns a near-optimal policy purely from historical records that capture the full state of the airport surface, the human decisions that were actually made, and the resulting traffic flow. The trained model then acts as a decision-support system, recommending runway configurations to controllers rather than replacing them.

But learning from history raises its own question: how do you know the trained model will not recommend something dangerous when it encounters conditions it has never seen? This is where formal verification enters the picture. Model-checking, the specific technique the team employed, is an automated method for determining whether a mathematical model of a system satisfies a specified property. It has long been used to verify software, hardware, communication protocols, and security systems. The specifications are written in temporal logic, a formal language for expressing statements about how properties evolve over time. The team chose Computation Tree Logic, or CTL, a branching-time logic that can reason not just about a single sequence of events but about trees of possible future paths, which makes it well suited to reasoning about how wind conditions might unfold.

The safety criteria being verified are not abstract. Aviation regulators, including the Federal Aviation Administration and the International Civil Aviation Organization, prescribe hard limits on the wind components an aircraft may tolerate during takeoff and landing. Under FAA Order 8400.9, the maximum crosswind component on a dry runway is 25 knots, dropping to 15 knots on wet or contaminated surfaces, while the maximum tailwind component is 10 knots regardless of surface condition, and as low as 3 knots on shorter contaminated runways. A contaminated runway, one covered with standing water, ice, snow, or slush, degrades braking, which is why the limits tighten. For reference, a Boeing 737-300 on a dry runway has manufacturer limits of 29 knots of crosswind and 10 knots of tailwind. The verification framework encodes these thresholds as logical properties and checks whether the RCA tool’s recommendations, given a particular wind speed and direction, keep the crosswind and tailwind components within bounds.

To translate a wind forecast into something a model checker can process, the researchers defined a wind state as a specific combination of active runways. For an airport with multiple runways, an indicator function determines whether each runway is operational under given wind conditions; all wind conditions that produce identical indicator values across every runway collapse into a single state. Transitions between states represent changes in wind speed and direction over time, not changes to the physical runways themselves. A path in the CTL sense is therefore a trajectory of wind states across a day or simulation interval, with the RCA tool making a configuration choice at every step. The team checked two temporal properties: EF, which asks whether there exists at least one path along which the safety criteria hold, and EG, the stricter property, which demands that the criteria be satisfied at every time step along every path. The distinction matters. A static check might confirm that a configuration is safe under one wind condition; the temporal check confirms that the tool never drifts into an unsafe recommendation as conditions shift hour by hour.

The verification was carried out with the NuSMV model-checking tool, chosen for its native support of CTL, while simulations and policy inference ran in Python using NumPy and Pandas, with historical wind transitions modeled through custom probabilistic transition matrices. The team tested the framework at three major US airports with very different geometries: Charlotte Douglas International Airport (CLT), Denver International Airport (DEN), and Dallas-Fort Worth International Airport (DFW). CLT operates primarily two configurations, a north flow used about 61 percent of the time and a south flow used the rest, while DEN and DFW each juggle more than ten distinct configurations whose historical usage ranges from dominant flows down to rare combinations used less than one percent of the time.

The first round of testing was deliberately brutal. Using Monte Carlo simulation, the researchers sampled wind speeds uniformly from zero up to each airport’s maximum observed speed, 30 knots for CLT and 40 knots for DEN and DFW, and wind directions uniformly across the full 360-degree circle, then ran 100,000 trials per airport. This is a worst-case stress test: it floods the model with wind conditions that may never occur at that location. The results were revealing. At CLT, the tool achieved a perfect 100 percent safe-prediction rate with zero tailwind violations and only 4.7 percent crosswind violations. At DEN, the safe rate fell to 70.5 percent, with 15 percent tailwind and 16.7 percent crosswind violations. DFW landed in between at 84.5 percent safe, with 20.3 percent tailwind and 6.2 percent crosswind violations. The tool also showed efficiency, not just safety: when multiple runways were viable, it selected the historically preferred configuration 63 percent of the time at CLT and 74 percent at DFW.

The second round replaced random sampling with realism. The team drew on actual weather data from 2018 and 2019 to build a transition matrix describing how wind conditions realistically evolve hour by hour at each airport. For each of 100 randomly selected days, they picked a random starting wind condition and simulated a full day of wind evolution 100 times, capturing random variation, and evaluated the RCA tool’s recommendation at every step. The improvement was dramatic. Crosswind violations fell from 4.7 percent to 0.4 percent at CLT, from 16.7 percent to 3.7 percent at DEN, and from 6.2 percent to 1.3 percent at DFW. Tailwind violations dropped from 15 percent to 5.8 percent at DEN and from 20.3 percent to 2.6 percent at DFW, while CLT maintained zero tailwind violations in both regimes. Averaged across the three airports, roughly 94 percent of predictions satisfied the safety criteria under realistic conditions, compared with about 70 percent under worst-case sampling.

That gap between the two testing regimes is itself informative. It suggests that a substantial share of the model’s apparent failures under random sampling occur in wind regimes that are physically implausible for the airport in question, while performance under the conditions controllers actually face is considerably stronger. The worst-case scenarios also pinpoint where the tool struggles, and the researchers note that adjusting the RCA tool’s predictions can mitigate those violations, with the violation rate declining over the course of simulated days. The verification framework thus serves a dual purpose: it certifies the tool where it works and localizes the boundary where it does not.

The broader significance lies in the marriage of two disciplines that rarely meet. Machine learning offers adaptability and pattern recognition drawn from data; formal verification offers mathematical guarantees that safety properties hold across entire state spaces, not just on the examples a test set happens to contain. The authors acknowledge that scaling this approach to deep reinforcement learning architectures will require abstractions or symbolic encodings, such as decision trees or binary decision diagrams, to keep the model-checking tractable, and point to neural-symbolic verification techniques like abstraction-refinement as a path forward. For now, the study demonstrates that a learning-based decision-support tool for a safety-critical aviation task can be rigorously audited with the same formal machinery used to verify flight software and protocols. The controllers remain firmly in the loop, applying their expertise to uphold all operational guidelines; the verification simply ensures that when the machine speaks, its advice respects the same hard wind limits that govern every takeoff and landing.

Subject of Research: Formal verification of a machine learning runway configuration tool using CTL model-checking at three major US airports

Article Title: Formal verification of a machine learning tool for runway configuration assistance

Article References: Razzaghi, P., Memarzadeh, M., & Kalyanam, K. (2025). Formal verification of a machine learning tool for runway configuration assistance. Frontiers in Aerospace Engineering, 4, Article 1463425. https://doi.org/10.3389/fpace.2025.1463425

Image Credits: AI Generated

DOI: 10.3389/fpace.2025.1463425

Keywords: formal verification, model-checking, Computation Tree Logic, machine learning, reinforcement learning, runway configuration management, air traffic management, aviation safety, crosswind, tailwind, NuSMV, NASA Ames Research Center