# Towards Formal Verification of LLM-Generated Code from Natural Language Prompts

arXiv: https://arxiv.org/abs/2507.13290 · HTML: https://mlsanity.com/paper/2507.13290/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 63 references that are in the map.
- First posted on arXiv 17 Jul 2025.

## Builds on (most cited first, 29 of 29)

- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [BigCodeBench: Benchmarking Code Generation with Diverse Function Calls and Complex Instructions](https://mlsanity.com/paper/2406.15877/) (2024)
- [StarCoder 2 and The Stack v2: The Next Generation](https://mlsanity.com/paper/2402.19173/) (2024)
- [CodeT: Code Generation with Generated Tests](https://mlsanity.com/paper/2207.10397/) (2022)
- [Grounded Copilot: How Programmers Interact with Code-Generating Models](https://mlsanity.com/paper/2206.15000/) (2022)
- [Do Users Write More Insecure Code with AI Assistants?](https://mlsanity.com/paper/2211.03622/) (2022)
- [Granite Code Models: A Family of Open Foundation Models for Code Intelligence](https://mlsanity.com/paper/2405.04324/) (2024)
- [CodeBERTScore: Evaluating Code Generation with Pretrained Models of Code](https://mlsanity.com/paper/2302.05527/) (2023)
- [LLM Hallucinations in Practical Code Generation: Phenomena, Mechanism, and Mitigation](https://mlsanity.com/paper/2409.20550/) (2024)
- [Studying the effect of AI Code Generators on Supporting Novice Learners in Introductory Programming](https://mlsanity.com/paper/2302.07427/) (2023)
- [SynCode: LLM Generation with Grammar Augmentation](https://mlsanity.com/paper/2403.01632/) (2024)
- [A Survey on LLM-based Code Generation for Low-Resource and Domain-Specific Programming Languages](https://mlsanity.com/paper/2410.03981/) (2024)
- [SelfCodeAlign: Self-Alignment for Code Generation](https://mlsanity.com/paper/2410.24198/) (2024)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [What's Wrong with Your Code Generated by Large Language Models? An Extensive Study](https://mlsanity.com/paper/2407.06153/) (2024)
- ["What It Wants Me To Say": Bridging the Abstraction Gap Between End-User Programmers and Code-Generating Large Language Models](https://mlsanity.com/paper/2304.06597/) (2023)
- [On the Effectiveness of Large Language Models in Domain-Specific Code Generation](https://mlsanity.com/paper/2312.01639/) (2023)
- [Type-Constrained Code Generation with Language Models](https://mlsanity.com/paper/2504.09246/) (2025)
- [Policy Filtration for RLHF to Mitigate Noise in Reward Models](https://mlsanity.com/paper/2409.06957/) (2024)
- [A Survey and Classification of Controlled Natural Languages](https://mlsanity.com/paper/1507.01701/) (2015)
- [CodeMMLU: A Multi-Task Benchmark for Assessing Code Understanding & Reasoning Capabilities of CodeLLMs](https://mlsanity.com/paper/2410.01999/) (2024)
- [RLSF: Fine-tuning LLMs via Symbolic Feedback](https://mlsanity.com/paper/2405.16661/) (2024)
- [InverseCoder: Self-improving Instruction-Tuned Code LLMs with Inverse-Instruct](https://mlsanity.com/paper/2407.05700/) (2024)
- [PhotoScout: Synthesis-Powered Multi-Modal Image Search](https://mlsanity.com/paper/2401.10464/) (2024)

## Built on by (most cited first, 8 of 8)

- [PatchWorld: Gradient-Free Optimization of Executable World Models for Agent Environments](https://mlsanity.com/paper/2605.30880/) (2026)
- [SLMFix: Leveraging Small Language Models for Domain Specific Language Error Fixing with Reinforcement Learning](https://mlsanity.com/paper/2511.19422/) (2025)
- [EvoUndo: Recoverability-Constrained Self-Evolution for LLM Agent Harnesses](https://mlsanity.com/paper/2608.28363/) (2026)
- [Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic](https://mlsanity.com/paper/2602.18607/) (2026)
- [Uplifted Attackers, Human Defenders: The Cyber Offense-Defense Balance for Trailing-Edge Organizations](https://mlsanity.com/paper/2508.15808/) (2025)
- [LLMs + Security = Trouble](https://mlsanity.com/paper/2602.08422/) (2026)
- [Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study](https://mlsanity.com/paper/2604.14867/) (2026)
- [Model-Driven Requirements Configuration with Three-Valued Uncertainty Scoring](https://mlsanity.com/paper/2607.26220/) (2026)

## Abstract (arXiv)

In the past few years LLMs have emerged as a tool that can aid programmers by taking natural language descriptions and generating code based on it. However, the reliability of LLM code generation and current validation techniques for it are far from strong enough to be used for mission-critical or safety-critical applications. In this work we explore ways to offer formal guarantees of correctness to LLM generated code; such guarantees could improve the quality of general AI Code Assistants and support their use for critical applications. To address this challenge we propose to incorporate a Formal Query Language that can represent a user's intent in a formally defined but natural language-like manner that a user can confirm matches their intent. We then have a formal specification of the user intent which we can use to verify that LLM-generated code matches the user's intent. We implement these ideas in our system, Astrogator, for the Ansible programming language, widely used for system administration, including for critical systems. The system includes an intuitive formal query language, a calculus for representing the behavior of Ansible programs, and a symbolic interpreter and a unification algorithm which together are used for the verification. A key innovation in Astrogator is the use of a Knowledge Base to capture system-specific implementation dependencies that greatly reduce the need for system knowledge in expressing formal queries. On a benchmark suite of 21 code-generation tasks, our verifier is able to verify correct code in 83% of cases and identify incorrect code in 92%.