Formal methods for safety-critical machine learning: a systematic literature review

The integration of Machine Learning (ML) systems into safety-critical domains heightens the need for rigorous safety guarantees. Traditional testing-based verification techniques are insufficient for fully capturing the complex, data-driven, and non-deterministic behaviors of modern ML models. Therefore, applying formal methods-which provide rigorous mathematical guarantees of a system's adherence to specified properties-to ML systems has been of particular interest in recent years.

This work presents a comprehensive Systematic Literature Review of peer-reviewed research from 2020 to mid-2025 on the use of formal methods to enhance ML safety, specifically for safety-critical applications. Articles selected present empirical research applying formal methods to modern machine learning approaches. Application domains as well as gaps, limitations, and challenges in this research area are compiled and presented.

Following a structured protocol, 46 studies were identified across four major digital libraries and classified into eight categories: Reachability and Over-Approximation Techniques, SMT-based Verification and Abstraction/Refinement, MILP/ILP Approaches, Model Checking Approaches, Runtime Verification Approaches, Shielding Techniques, Control Barrier Function Methods, and Risk Verification Methods. The review synthesizes methodological advances, application areas, and comparative strengths over traditional verification, while also presenting bibliometric trends in the literature.

Analysis reveals persistent challenges and gaps, including scalability to large and complex models, integration with training processes, and limited real-world validation. Future research opportunities include developing integrated training-verification loops, scalable verification frameworks, hybrid formal methods, and novel techniques for emerging ML paradigms such as Large Language Models. This work serves both as a state-of-the-art reference and as a roadmap for advancing the safe deployment of ML systems.