Authors:  Rance W Cleaveland1, Grant Whitman2 and Brent Kensington2

JSA-Vol. 4 (2025),

1 University of Maryland, College Park, College Park, MD, United States.

2 University of Western Australia, Perth, WA, Australia.

* Correspondence: mailto.rance@cs.umd.edu

Received: 1 December 2024; Accepted: 5 April 2025; Published: 20 June 2025.

Abstract: Artificial intelligence and machine learning components are increasingly deployed in industrial software systems, ranging from autonomous vehicles and cloud infrastructures to financial platforms and safety-critical cyber-physical systems. While formal methods have demonstrated significant success in verifying conventional software and hardware systems, their applicability to learning-enabled components remains limited. The inherent uncertainty, adaptivity, and high-dimensional nature of machine learning models pose fundamental challenges to classical verification techniques. This paper presents a comprehensive research study on the formal verification of AI-based and learning-enabled industrial systems. We analyze the limitations of existing formal methods when applied to machine learning models, review emerging verification frameworks for neural networks, and examine integration strategies for combining formal verification with industrial development pipelines. Furthermore, we propose a unified research framework that integrates design-time verification, runtime monitoring, and uncertainty-aware assurance for AI-enabled systems. The paper identifies open challenges and outlines concrete research directions aimed at bridging the gap between formal methods and modern industrial artificial intelligence.

Keywords: Formal methods, Artificial intelligence, Machine learning, Software verification, Industrial systems