Formal Verification for AI-Assisted Code Changes in Regulated Environments
Main Article Content
Abstract
Use of AI in code generation is able to make software creation faster, and yet due to lack of controls, the possibility of making severe compliance and reliability issues increases in regulated and safety-critical fields like finance and medicine. We describe, in this paper, a proof-carrying pipeline incorporating proofs presented by Large Language Model (LLM) advice into static analysis, symbolic execution, bounded Model checking, and policy execution mechanisms to certify changes to code before it is merged. The system will block unsafe pattern automatically, generation of auditor friendly evidence packages, and fits with Continuous Integration/Continuous Deployment (CI/CD) worklifes so that the impacts on developer velocity are minimal.
We measure the method of the two production-scale repositories, one one in fintech and another one in healthcare, in terms of defect reduction, verification efficiency and the effect on audit preparation. The outcome denotes that the relative decrease in incident of defects after the merge was reduced by 73-78% and the success rate that is evaluated by the verification is markedly elevated when put to the test in a solitary mode. The preparation time of audits was decreased by more than 69%, and gift boxes of proofs were prepared in a structured manner and machine-defensible, therefore, decreasing manual review processes. Prompt refinement using the reinforcement learning also enhanced the throughput in verification by minimizing the number of repetitive re-verifications involved.
The results show how AI-based development could be secure and meet standards with the integration of thorough formal verification. Through the use of generative AI techniques and technologies, the outlined pipeline solves the two-fold problem of pushing the development speed, and maintaining correctness and regulatory compliance and provides a scalable template of how high-stakes software engineering can be done in the era of generative AI.
Article Details
Section
How to Cite
References
[1] Li, Y., Meng, R., & Duck, G. J. (2025, April 2). Large Language Model powered Symbolic Execution. arXiv.org. https://arxiv.org/abs/2505.13452
[2] Cotroneo, D., Foggia, A., Improta, C., Liguori, P., & Natella, R. (2024). Automating the correctness assessment of AI-generated code for security contexts. Journal of Systems and Software, 216, 112113. https://doi.org/10.1016/j.jss.2024.112113
[3] Charalambous, Y., Tihanyi, N., Jain, R., Sun, Y., Ferrag, M. A., & Cordeiro, L. C. (2023). A new era in software security: towards Self-Healing software via large language models and formal verification. arXiv (Cornell University). https://doi.org/10.48550/arxiv.2305.14752
[4] Rao, B., Eiers, W., & Lipizzi, C. (2025, April 23). Neural theorem proving: Generating and structuring proofs for formal verification. arXiv.org. https://arxiv.org/abs/2504.17017
[5] Miranda, B., Zhou, Z., Nie, A., Obbad, E., Aniva, L., Fronsdal, K., Kirk, W., Soylu, D., Yu, A., Li, Y., & Koyejo, S. (n.d.). VeriBench: End-to-End Formal Verification Benchmark for AI code Generation in Lean 4.
OpenReview. https://openreview.net/forum?id=rWkGFmnSNl
[6] Grimm, T., Lettnin, D., & Hübner, M. (2018). A survey on Formal Verification Techniques for Safety-Critical Systems-on-Chip. Electronics, 7(6), 81. https://doi.org/10.3390/electronics7060081
[7] Sapkota, R., Roumeliotis, K. I., Cornell University, Department of Biological and Environmental Engineering, USA, University of the Peloponnese, Department of Informatics and Telecommunications, Tripoli, Greece, & rs2672@cornell.edu, mk2684@cornell.edu. (2025). Vibe Coding vs. Agentic Coding: Fundamentals and Practical Implications of Agentic AI. https://arxiv.org/pdf/2505.19443v1
[8] Tihanyi, N., Bisztray, T., Jain, R., Ferrag, M. A., Cordeiro, L. C., & Mavroeidis, V. (2023). The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification. The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification. https://doi.org/10.1145/3617555.3617874
[9] Böhme, M., Bodden, E., Bultan, T., Cadar, C., Liu, Y., & Scanniello, G. (2024). Software Security Analysis in 2030 and Beyond: A Research Roadmap. ACM Transactions on Software Engineering and Methodology. https://doi.org/10.1145/3708533
[10] Jha, M., Wan, J., Zhang, H., & Chen, D. (2025). PREFACE - a reinforcement learning framework for code verification via LLM Prompt Repair. Proceedings of the Great Lakes Symposium on VLSI 2022, 547–