# Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 24 references that are in the map.
- First posted on arXiv 11 Feb 2025.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Efficient Estimation of Word Representations in Vector Space](https://mlsanity.com/paper/1301.3781/) (2013)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)

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

- [HoarePrompt: Structural Reasoning About Program Correctness in Natural Language](https://mlsanity.com/paper/2503.19599/) (2025)
- [The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK](https://mlsanity.com/paper/2607.14340/) (2026)
- [Can You Check That? The Checkability Boundary for Local LLM Network Automation](https://mlsanity.com/paper/2609.31540/) (2026)
- [Security in LLM-Assisted Coding: A Systematic Literature Review](https://mlsanity.com/paper/2610.15482/) (2026)

## Abstract (arXiv)

Large language models (LLMs) have demonstrated remarkable code generation capabilities, but the correctness of the generated code cannot be inherently trusted. This paper explores the feasibility of using formal software verification, specifically the SPARK framework for Ada, to ensure the reliability of LLM-generated code. We present Marmaragan, a tool that leverages an LLM in order to generate SPARK annotations for existing programs, enabling formal verification of the code. The tool is benchmarked on a curated set of SPARK programs, with annotations selectively removed to test specific capabilities. The performance of Marmaragan with GPT-4o on the benchmark is promising, with correct annotations having been generated for 50.7% of the benchmark cases. The results establish a foundation for future work on combining the power of LLMs with the reliability of formal software verification.