The Symbiosis of Formal Methods and Artificial Intelligence
Source abstract
Abstract
Formal methods are software engineering approaches with a rigorous mathematical basis that can help ensure the correctness of software systems, especially where safety or security is critical. Artificial Intelligence (AI) has developed very rapidly in the area of Generative AI (GenAI), where questions can be answered with increasingly impressive but potentially unreliable and variable results. This paper surveys research in integrating the two approaches in a synergistic manner. Traditionally, such explorations have required significant manual efforts in searching for and evaluating existing research. However, most relevant publications are now accessible online, and AI tools are increasingly good at answering research questions with more and more reliability. This paper takes the approach of using GenAI to evaluate research questions on combining formal methods and AI-related techniques. The paper assesses the usefulness and validity of these results. With recent improvements in AI search tools, the approach is now a useful aid to researchers, significantly reducing the time needed to survey existing research, while always needing human checking by an expert. In addition, the combination of formal methods and AI approaches looks to be an interesting and beneficial research area with potential industrial-scale applications in the future. This paper does not claim to be an exhaustive systematic review, but rather demonstrates an AI-assisted search process to aid in literature surveys within a fast-moving research area.
Source: crossref · Quality: baseline
Research context
OpenAlex topics: Software Engineering Techniques and Practices · Software Testing and Debugging Techniques · Software Engineering Research
SciVX discovery tags are terminology-based. OpenAlex topics are source-provided classifications.
Affiliations
School of Computer Science and Digital Technologies, London South Bank University, London SE1 0AA, UK
Centre for Research and Innovation in Software Engineering (RISE), Southwest University, Chongqing 400715, China
Software Engineering Institute, East China Normal University, Shanghai 200062, China
References (74)
Show source-provided references
1. A Specifier’s Introduction to Formal Methods10.1109/2.58215 ↗
2. Formal methods: Practice and experience10.1145/1592434.1592436 ↗
3. Turing, A.M. (1949). Checking a Large Routine. Report of a Conference on High Speed Automatic Calculating Machines, Cambridge University Mathematical Laboratory. Available online: https://turingarchive.kings.cam.ac.uk/checking-large-routine.
4. An Early Program Proof by Alan Turing10.1109/MAHC.1984.10017 ↗
5. Computing Machinery and Intelligence10.1093/mind/LIX.236.433 ↗
6. Google (2026, February 25). Google Scholar Labs. Available online: https://scholar.google.com/scholar_labs/search.
7. Formal Methods: Whence and Whither?10.1007/978-3-032-24494-9_2 ↗
8. The Z Notation: Whence the Cause and Whither the Course?10.1007/978-3-319-29628-9_3 ↗
9. Scharts, S.T. (1967). Assigning meaning to programs. Symposia in Applied Mathematics, American Mathematical Society. Mathematical Aspects of Computer Science.
10. An axiomatic basis for computer programming10.1145/363235.363259 ↗
11. Hoare, C.A.R., and He, J. (1998). Unifying Theories of Programming, Prentice Hall.10.1007/BFb0002714 ↗
12. Beth, E.W. (1962). Formal Methods: An Introduction to Symbolic Logic and to the Study of Effective Operations in Arithmetic and Logic, D. Reidel Publishing Company.
13. Strachey, C. (2025, March 02). The Strachey’s Philosophy. Department of Computer Science, University of Oxford. Available online: https://www.cs.ox.ac.uk/activities/concurrency/courses/stracheys.html.
14. Seven myths of formal methods10.1109/52.57887 ↗
15. Seven more myths of formal methods10.1109/52.391826 ↗
16. Ten commandments of formal methods10.1109/2.375178 ↗
17. Hinchey, M.G., and Bowen, J.P. (1995). Applications of Formal Methods. Prentice Hall, Series in Computer Science, Prentice Hall.
18. Hinchey, M.G., and Bowen, J.P. (1999). Industrial-Strength Formal Methods in Practice, FACIT.10.1007/978-1-4471-0523-7 ↗
19. Frappier, M., and Habrias, H. (2001). Software Specification Methods: An Overview Using a Case Study, FACIT.10.1007/978-1-4471-0701-9 ↗
20. Boulanger, J.-L. (2012). Formal Methods: Industrial Use from Model to the Code, Wiley.10.1002/9781118561829 ↗
21. Gnesi, S., and Margaria, T. (2012). Formal Methods for Industrial Critical Systems: A Survey of Applications, Wiley.10.1002/9781118459898 ↗
22. Safety-critical systems, formal methods and standards10.1049/sej.1993.0025 ↗
23. From Logic to Programming10.1007/978-981-96-4656-2_2 ↗
24. Lessons from applying the systematic literature review process within the software engineering domain10.1016/j.jss.2006.07.009 ↗
25. Developing search strategies for detecting relevant experiments10.1007/s10664-008-9091-7 ↗
26. Petersen, K., Feldt, R., Mujtaba, S., and Mattsson, M. (2008). Systematic mapping studies in software engineering. EASE’08: Proceedings of the 12th International Conference on Evaluation and Assessment in Software Engineering, ACM Digital Library.10.14236/ewic/EASE2008.8 ↗
27. Guidelines for conducting systematic mapping studies in software10.1016/j.infsof.2015.03.007 ↗
28. A coefficient of agreement for nominal scales10.1177/001316446002000104 ↗
29. The Lean Theorem Prover (System Description)10.1007/978-3-319-21401-6_26 ↗
30. Ramsay, A. (1988). Formal Methods in Artificial Intelligence, Cambridge University Press.
31. Krichen, M., Mihoub, A., Alzahrani, M.Y., Adoni, W.Y.H., and Nahhal, T. (2022). Are formal methods applicable to machine learning and Artificial Intelligence?. 2022 2nd International Conference of Smart Systems and Emerging Technologies (SMARTTECH), IEEE.10.1109/SMARTTECH54121.2022.00025 ↗
32. A promising path towards autoformalization and General Artificial Intelligence
33. Computer theorem proving and Artificial Intelligence10.1007/978-94-009-2356-0_5 ↗
34. Whitehead, A.N., and Russell, B. (1910–1913). Principia Mathematica, Cambridge University Press.
35. Automatic B-model repair using model checking and machine learning10.1007/s10515-019-00264-4 ↗
36. Abrial, J.-R. (1996). The B-Book: Assigning Programs to Meanings, Cambridge University Press.10.1017/CBO9780511624162 ↗
37. Sun, X., Khedr, H., and Shoukry, Y. (2019). Formal verification of neural network controlled autonomous systems. 22nd ACM International Conference on Hybrid Systems: Computation and Control, ACM Digital Library.10.1145/3302504.3311802 ↗
38. Zhang, Y., Cai, Y., Zuo, X., Luan, X., Wang, K., Hou, Z., Zhang, Y., Wei, Z., Sun, M., and Sun, J. (2024). The fusion of Large Language Models and formal methods for trustworthy AI agents: A roadmap. arXiv.
39. MLFMF: Data sets for machine learning for mathematical formalization10.52202/075280-2207 ↗
40. Machine learning methods in statistical model checking and system design–Tutorial10.1007/978-3-319-23820-3_23 ↗
41. Machine learning and formal concept analysis
42. Jha, S., Jha, S.K., Lincoln, P., Bastian, N.D., Velasquez, A., and Neema, S. (2023). Dehallucinating Large Language Models using formal methods guided iterative prompting. 2023 IEEE International Conference on Assured Autonomy (ICAA), IEEE.10.1109/ICAA58325.2023.00029 ↗
43. Polu, S., and Sutskever, I. (2020). Generative language modeling for automated theorem proving. arXiv.
44. Lin, Y., Tang, S., Lyu, B., Wu, J., Lin, H., Yang, K., Li, J., Xia, M., Chen, D., and Arora, S. (2025). Goedel-Prover: A frontier model for open-source automated theorem proving. arXiv.
45. Lin, Y., Tang, S., Lyu, B., Yang, Z., Chung, J.H., Zhao, H., Jiang, L., Geng, Y., Ge, J., and Sun, J. (2025). Goedel-Prover-V2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv.
46. Xin, H., Ren, Z., Song, J., Shao, Z., Zhao, W., Wang, H., Liu, B., Zhang, L., Lu, X., and Du, Q. (2024). DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. arXiv.
47. Xin, H., Guo, D., Shao, Z., Ren, Z., Zhu, Q., Liu, B., Ruan, C., Li, W., and Liang, X. (2024). DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data. arXiv.
48. Verification of image-based neural network controllers using generative models
49. Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M.D., Sung, F., Vinyes, M., Ying, Z., and Zhu, Z. (2025). Kimina-Prover preview: Towards large formal reasoning models with reinforcement learning. arXiv.
50. Carreira-Munich, T., Paz-Marcolla, V., and Castro, R. (2024). DEVS Copilot: Towards Generative AI-Assisted Formal Simulation Modeling based on Large Language Models. 2024 Winter Simulation Conference (WSC), IEEE.10.1109/WSC63780.2024.10838994 ↗
51. Tihanyi, N., Charalambous, Y., Jain, R., Ferrag, M.A., and Cordeiro, L.C. (2025). A new era in software security: Towards self-healing software via Large Language Models and formal verification. 2025 IEEE/ACM International Conference on Automation of Software Test (AST), IEEE.10.1109/AST66626.2025.00020 ↗
52. Bounded Model Checking Using Satisfiability Solving10.1023/A:1011276507260 ↗
53. Tihanyi, N., Bisztray, T., Jain, R., Ferrag, M.A., Cordeiro, L.C., and Mavroeidis, V. (2023). The FormAI dataset: Generative AI in software security through the lens of formal verification. PROMISE 2023: Proceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering, ACM Digital Library.10.1145/3617555.3617874 ↗
54. Lu, M., Delaware, B., and Zhang, T. (2024). Proof automation with Large Language Models. ASE’24: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, IEEE/ACM Digital Library.10.1145/3691620.3695521 ↗
55. Autoformalization with Large Language Models
56. Nipkow, T., Wenzel, M., and Paulson, L.C. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Springer. LNCS.10.1007/3-540-45949-9 ↗
57. Shminke, B. (2023). Applications of AI to Study of Finite Algebraic Structures and Automated Theorem Proving. [Ph.D. Thesis, Université Côte d’Azur].
58. Specify what? Enhancing neural specification synthesis by symbolic methods
59. Kumar, A., and Gadde, D.N. (2024). Generative AI augmented induction-based formal verification. 2024 IEEE 37th International System-on-Chip Conference (SOCC), IEEE.10.1109/SOCC62300.2024.10737803 ↗
60. Weng, K., Du, L., Li, S., Lu, W., Sun, H., Liu, H., and Zhang, T. (2025). Autoformalization in the Era of Large Language Models: A Survey. arXiv.
61. Tihanyi, N., Bisztray, T., Ferrag, M.A., Cherif, B., Dubniczky, R.A., Jain, R., and Cordeiro, L.C. (2025). Vulnerability detection: From formal verification to Large Language Models and hybrid approaches: A comprehensive overview. arXiv.10.1007/978-3-031-99447-0_3 ↗
62. Nowroozi, E., Taheri, R., and Cordeiro, L. (2026). Vulnerability detection: From formal verification to Large Language Models and hybrid approaches: A comprehensive overview. Adversarial Example Detection and Mitigation Using Machine Learning, Springer. Chapter 3.10.1007/978-3-031-99447-0 ↗
63. Langville, A.N., and Meyer, C.D. (2006). Google’s PageRank and Beyond: The Science of Search Engine Rankings, Princeton University Press.10.1515/9781400830329 ↗
64. Detecting hallucinations in large language models using semantic entropy10.1038/s41586-024-07421-0 ↗
65. Avigad, J. (2026, June 02). Mathematics in the Age of AI. LMS/BCS-FACS Seminar, London Mathematical Society. Available online: https://www.lms.ac.uk/events/lms-bcs-facs-seminar-jeremy-avigad.
66. Tao, T. (2026, June 02). The Potential for AI in Science and Mathematics. Oxford Mathematics Public Lectures, Science Museum, London. Available online: https://www.maths.ox.ac.uk/node/68243.
67. George, R.J., Huang, S., Song, P., and An kumar, A. (2025). LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction. arXiv.
68. Lu, J., Emond, K., Yang, K., Chaudhuri, S., Sun, W., and Chen, W. (2025). Lean Finder: Semantic Search for Mathlib That Understands User Intents. arXiv.
69. Cress, L. (2026, June 02). ‘Vibe Coding’ Named Word of the Year by Collins Dictionary. BBC News, BBC. Available online: https://www.bbc.co.uk/news/articles/cpd2y053nleo.
70. Fawzy, A., Tahir, A., and Blincoe, K. (2025). Vibe Coding in Practice: Motivations, Challenges, and a Future Outlook—A Grey Literature Review. arXiv.10.1145/3786583.3786866 ↗
71. Mathematical discoveries from program search and large language models10.1038/s41586-023-06924-6 ↗
72. Nature Editorial (2026). Mathematicians are developing rules for AI use—Other fields should follow. Nature, 654, 571.10.1038/d41586-026-01881-2 ↗
73. Will AI spark a scientific renaissance—Or a diffuse monoculture?10.1038/d41586-026-01954-2 ↗
74. Shao, Z., Luo, Y., Lu, C., Ren, Z.Z., Hu, J., Ye, T., Gou, Z., Ma, S., and Zhang, X. (2025). DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning. arXiv.