Air traffic control is a vast, distributed operation that requires the efficient and safe coordination of approximately 45,000 commercial airline flights per day in the United States. Safely managing this volume of traffic requires extensive human coordination combined with sophisticated algorithmic planning. Unfortunately, despite multiple overlapping safety layers, serious safety incidents occur at an alarming frequency. The proposed research combines artificial intelligence with formal methods to improve the safety, reliability, and efficiency of air traffic management. Using a combination of voice recognition, predictive models, and safety checks, the project aims to help detect problems before they occur, such as a misunderstanding causing a future runway incursion or a weather-driven delay that cascades across multiple airports. Beyond air traffic control, the developed framework can enhance other cyber-physical systems that combine human coordination with intelligent automation, improving the safety of firefighting operations, strengthening the resilience of the power grid to adverse events, and advancing national security by preventing human error in military operations. This research aims to advance the theory and application of cyber-physical systems (CPS) by improving the safety and resilience of air traffic management. The project investigates a multi-layered approach that integrates formal verification, robust speech understanding, and data-driven disruption analysis. At the airport level, compositional hybrid automata and signal temporal logic (STL) will be used for predictive monitoring of aircraft trajectories and controller-issued commands, enabling early detection of safety violations. At the interface layer, robust machine learning models will extract semantic intent from noisy, domain-specific voice data to support online reasoning and decision-making. At the regional level, scheduling algorithms will be analyzed under operational uncertainty, using formal sensitivity analysis and probabilistic post-mortem inference to identify failure modes and propose mitigation strategies. While focused on air traffic control, the general methods developed are applicable to a wide range of CPS domains that involve human-in-the-loop operation and algorithmic oversight in distributed safety-critical settings. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.