Turing Award Laureate: Model Checking Not Viable for AI Systems

By Harry Wu, 21st Century Business Herald, SFC

Model Checking cannot verify the entire AI system or its key components as a "model" and write and verify specifications for it, such as "never harm humans" or "maintain fairness," because Model Checking relies on the idea that I have a mathematical model of the behavior and system,” said Joseph Sifakis, 2007 A.M. Turing Award Laureate and Founder of the Verimag laboratory, at the 2025 Sustainability Global Leaders Conference held from October 16th to 18th in Shanghai.

“For AI systems, we cannot extract mathematical models, which are neural networks imitating the neural networks of our brain. And we don't have the models,” he added. “We don't know how to apply Model Checking techniques to AI system.”

Sifakis is a principal co-inventor of Model Checking , an algorithmic technique for verifying computing systems. His work transformed this approach from a theoretical technique to a highly effective technology that enables hardware and software engineers to find errors efficiently in complex systems.

Model Checking has resulted in increased assurance that systems perform as intended by designers, and has had a major impact on designers and manufacturers of software and semiconductor chips, who face a technology explosion where products of unprecedented complexity have to operate as expected. Sifakis's work enabled these industries to shorten time to market and greatly increase product integrity.