REVIEW 1 major objections 5 minor 2 cited by
Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK
T0 review · 1 major / 5 minor · reviewed 2026-08-08 · deepseek-v4-flash
Pith's one-line read The paper establishes that a language model, when checked and corrected by a theorem prover, can supply the formal annotations that make SPARK programs verifiable: GPT-4o solved 36 of 71 (50.7%) benchmark cases.
desk verdict A useful proof-of-concept for LLM-generated SPARK annotations, but the 50.7% success rate is an upper bound because the eval never checks that the LLM preserved the original program's behavior. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing mechanism is a generate-and-check loop: Marmaragan embeds the SPARK package specification, body, and optionally GNATprove's formatted medium messages into an LLM prompt, asks for the body with pragmas restored, then compiles and runs GNATprove on the result. If verification fails, the medium messages from that attempt are injected into the next prompt, and the tool can draw on several parallel initial solutions and several retries; a chain-of-thought variant asks the model to explain the problem first. The identity that carries the argument is the loop: the theorem prover's feedback supplies the grounding that the LLM's stochastic output otherwise lacks.
What would settle it
A concrete test: for each of the 36 solved benchmark cases, compare the executable statements of Marmaragan's output against the original verified program. If any executable statement differs (beyond pragmas and the allowed wrapping if/for constructs), then a 'correct' solution has changed program behavior, and the definition of correctness as GNATprove-clean does not establish that the annotations are correct for the original program.
Extended reading notes
Core claim
On the paper's own terms, the central claim is that Marmaragan, a Python prototype that asks GPT-4o to regenerate pragma statements in existing SPARK 2014 programs, can complete formal verification for a substantial share of realistic cases. It defines success strictly as GNATprove reporting no errors and no unresolved proof obligations (mediums) on the modified program. Across five benchmark schemata built from 16 programs under different annotation-removal patterns, 36 of 71 cases (50.7%) met this bar, and the best parameter settings (n=6, r=1 and n=4, r=2) each solved 24 cases, with a reproduction run reaching 25 and 26. The paper also highlights that 16 of 36 Argu-repository cases were solved even though that code was published after the model's training cutoff, arguing the model is not memorizing the benchmark.
Load-bearing premise
The load-bearing premise is that a program counts as correctly annotated whenever GNATprove finishes with no errors or mediums, without any check that the LLM preserved the original code's behavior.
Editorial extensions
If this is right
- SPARK editors could offer real-time annotation suggestions: the paper explicitly frames Marmaragan as the prototype backend for such an assistant.
- Mixing initial parallel attempts with retries (n=6, r=1 and n=4, r=2) beats either alone, so a deployed tool should budget for both.
- Assert generation is more reliable than loop-invariant generation, so near-term tooling can target assertion completion while keeping human review for invariants.
- Success on the Argu programs—published after the model's training cutoff—supports the claim that the method can produce annotations for code the model has not seen, not just re-emit remembered examples.
- The approach extends naturally to generating pre- and postconditions for lower-level functions, the future-work direction the paper proposes.
Reading between the lines
- The paper's correctness metric is verification success, not semantic equivalence; a stricter evaluation that diffs executable code or runs differential tests could lower the reported 50.7%, and would make the claim testable.
- The 16 of 36 success rate on the post-cutoff Argu programs is a cleaner estimate of genuine generalization than the overall rate, since the other programs may overlap with training data.
- The same retry-with-checker-feedback loop should transfer to other deductive verification tools, provided they emit counterexamples or unresolved proof obligations; that transferability is not tested here.
- A practical hybrid workflow is suggested: the human writes high-level pre- and postconditions, the LLM proposes lower-level contracts and loop invariants, and the prover checks the combination—this would lower the expertise barrier for adopting formal methods.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper presents Marmaragan, a Python/LangChain tool that asks an LLM (GPT-4o) to generate missing SPARK 2014 annotations—such as pragma Loop_Invariant, pragma Loop_Variant, and pragma Assert—for existing Ada/SPARK programs, and then invokes GNATprove to check whether the resulting program runs free of errors and 'medium' diagnostic messages. The authors construct 71 benchmark tasks from 16 previously verified SPARK programs by removing pragmas according to five schemas, and they report that Marmaragan solves 36 of 71 cases (50.7%) across several parameter combinations. The paper also includes a contamination-control subset built from the first author's Argu repository, reproducibility reruns of the two most successful experiments, and a chain-of-thought prompting variant. The central claim is that LLMs can generate correct SPARK annotations often enough to establish a foundation for combining LLM-based code generation with formal verification.
Significance. The paper makes a useful proof-of-concept contribution if its central number is trustworthy. Its evaluation design is non-circular in an important respect: success is judged by an external verifier, GNATprove, rather than by the LLM itself, and the Argu subset addresses data-leakage concerns by using programs published after the model's training cutoff. The comparison of N-Solutions and Retries also provides practical engineering information for similar tools. The main limitation, discussed below, is that the success metric does not verify whether the LLM preserved the original program's executable behavior, and the small benchmark limits how much can be concluded about general performance. As a proof of concept, the idea is relevant to the intersection of LLM-based code generation and formal verification.
major comments (1)
- [§4.2; §6.1; Listing 2; Tables 1–2] The headline result—that Marmaragan generated 'correct annotations' for 36/71 (50.7%) benchmark cases—is defined entirely by GNATprove returning no errors and no mediums (§4.2, §6.1). This definition is valid only if the LLM output preserves the original program's executable behavior, because the prompt in Listing 2 instructs the model not to modify code, but compliance is never checked. Section 4.2 explicitly states that manual analysis of the generated solutions is infeasible, and no automated diff, artifact, or per-solution report is provided. GNATprove proves consistency with the specified contracts; it does not prove that the modified program is behaviorally equivalent to the original program. An LLM that deletes a loop, weakens an expression, or guards code with a control structure can remove proof obligations while changing functionality, and even a small number of such cases would materially inflate the reported 36/71 figure. Since the benchmark is built from already verified programs, an automated check that the generated .adb differs from the original only by pragma statements and the permitted 'for'/'if' wrappers is straightforward in principle; please add such a check and report the success rate restricted to code-preserving solutions.
minor comments (5)
- [§5.5] The reproducibility reruns are reported only as aggregate totals (25/71 and 26/71); because the LLM sampling is stochastic, it would be informative to know whether the same programs were solved across runs, for example through a per-task contingency table.
- [§6.2] The parameter-efficiency conclusions are stated without uncertainty quantification; with only 71 tasks, differences such as 24/71 versus 20/71 between experimental conditions may not be statistically meaningful, so a confidence interval or per-task comparison would strengthen the interpretation.
- [§3.1; §3.4.6; §1; §6.2; §2.3] There are several typos and leftover thesis-language artifacts, including 'Maramaragan' in Section 3.1, 'graeater' in Section 3.4.6, 'throughly' in Section 1, 'demi-nishing' in Section 6.2, and 'this thesis' in Section 2.3; a careful copyedit is needed.
- [§5.4] The footnote about the reliability of OpenAI's published training-data information is appropriate; the same caveat should be reflected in the main text so that the Argu contamination control is not overstated.
- [§3.1] The text refers to 'Marmaragan [GitHub]' but does not provide a URL or an artifact appendix; providing the benchmark programs, generated outputs, and the diff-checking script would substantially improve reproducibility.
Circularity Check
No significant circularity: the success metric is set by the external GNATprove verifier, and the only self-related element (the Argu repository) is used as an anti-contamination control.
full rationale
This paper is an empirical benchmarking study rather than a chain of mathematical derivations, and its central quantity—the 50.7% success rate—is measured against GNATprove, an external verification tool whose proof obligations are not determined by Marmaragan's outputs. No parameter is fitted to the benchmark and then renamed as a prediction; the definition of a correct solution as one that runs free of errors and mediums is an explicit operationalization adopted because, as the paper states in Section 4.2, 'a manual analysis is also not feasible, given the number of benchmark programs and the total number of solutions generated.' This is a stated limitation of the evaluation, not a circular reduction. The only self-related element is the first author's Argu repository, which the paper selects specifically because it was 'first published after the cutoff dates for the training of GPT-4 and GPT-4o,' making it a deliberate contamination-control measure that strengthens the evaluation. The concern that GNATprove acceptance does not by itself prove preservation of original program functionality is a validity threat to the strength of the claim, but it is not circularity: the paper's reported figure is explicitly a measure of GNATprove error/medium-free completion, and it does not purport to derive functional equivalence from that metric. The derivation chain is therefore self-contained with respect to its stated evaluation criterion.
Assumptions & free parameters
assumptions (3)
- domain assumption GNATprove is a sound verifier: absence of errors and mediums implies the program satisfies its SPARK annotations.
- domain assumption The original programs are already verified, so at least one correct annotation set exists for each benchmark task.
- domain assumption The LLM follows the prompt instruction not to modify program functionality.
Cite this review
Pith. "Pith review of Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK." pith.science (2026). https://pith.science/paper/XO5MOLYX
@misc{pith2026250207728,
author = {Pith},
title = {Pith review of: Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK},
year = {2026},
howpublished = {\url{https://pith.science/paper/XO5MOLYX}},
note = {Machine review of arXiv:2502.07728}
}
read the original abstract
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.
Figures
Figures from the paper (3 more)
Forward citations
Cited by 2 Pith papers
-
The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK
An AI coding agent, judged by the GNATprove verifier, produced a 77.7 kLOC collection of security software with 49,280 machine-checked proof obligations at a claimed 20–40x supervision-cost reduction.
-
Position Paper: Programming Language Techniques for Bridging LLM Code Generation Semantic Gaps
A position paper arguing that PL techniques, especially formal verification and structure-aware representations, should be deeply integrated into LLM code generation.
Reference graph
Works this paper leans on
-
[1]
write newline
" write newline "" before.all 'output.state := FUNCTION fin.entry add.period write newline FUNCTION new.block output.state before.all = 'skip after.block 'output.state := if FUNCTION new.sentence output.state after.block = 'skip output.state before.all = 'skip after.sentence 'output.state := if if FUNCTION not #0 #1 if FUNCTION and 'skip pop #0 if FUNCTIO...
-
[2]
AdaCore (1980). Ada programming language. https://ada-lang.io/
work page 1980
-
[3]
Barnes, J. (2012). High Integrity Software: The SPARK Approach to Safety and Security . Addison-Wesley
work page 2012
-
[4]
Blanchette, J. C., Kaliszyk, C., Paulson, L. C., and Urban, J. (2016). Hammering towards QED . Journal of Formalized Reasoning , 9(1):101–148
work page 2016
-
[5]
Brosgol, B. M. (2019). How to succeed in the software business while giving away the source code: The AdaCore experience. IEEE Software , 36(6):17--22
work page 2019
-
[6]
Chapman, R., Dross, C., Matthews, S., and Moy, Y. (2024). Co-developing programs and their proof of correctness. Commun. ACM , 67(3):84–94
work page 2024
-
[7]
Chapman, R. and Schanda, F. (2014). Are we there yet? 20 years of industrial theorem proving with SPARK . In Klein, G. and Gamboa, R., editors, Interactive Theorem Proving , pages 17--26, Cham. Springer International Publishing
work page 2014
-
[8]
Chase, H. (2022). LangChain Python Library . https://github.com/langchain-ai/langchain
work page 2022
Show all 26 references
-
[9]
Cramer, M. (2023). argu. https://github.com/marcoscramer/argu
2023
-
[10]
Dross, C., Efstathopoulos, P., Lesens, D., Mentr, D., and Moy, Y. (2014). Rail, space, security: Three case studies for SPARK 2014
2014
-
[11]
and Paskevich, A
Filli \^a tre, J.-C. and Paskevich, A. (2013). Why3 --- where programs meet provers. In Felleisen, M. and Gardner, P., editors, Programming Languages and Systems , pages 125--128, Berlin, Heidelberg. Springer Berlin Heidelberg
2013
-
[12]
Filliâtre, J.-C. (2011). Deductive software verification. International Journal on Software Tools for Technology Transfer , 13:397--403
2011
-
[13]
N., Ringer, T., and Brun, Y
First, E., Rabe, M. N., Ringer, T., and Brun, Y. (2023). Baldur: Whole-proof generation and repair with large language models
2023
-
[14]
Hoare, C. A. R. (1969). An Axiomatic Basis for Computer Programming . Communications of the ACM
1969
-
[15]
W., Schuurmans, D., Bosma, M., Ichter, B., Xia, F., Chi, E., Le, Q., and Zhou, D
Jason Wei, X. W., Schuurmans, D., Bosma, M., Ichter, B., Xia, F., Chi, E., Le, Q., and Zhou, D. (2023). Chain-of-thought prompting elicits reasoning in large language models
2023
-
[16]
Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóźdź, T., Miłoś, P., Wu, Y., and Jamnik, M
Jiang, A. Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóźdź, T., Miłoś, P., Wu, Y., and Jamnik, M. (2023a). Thor: Wielding hammers to integrate language models and automated theorem provers. Journal of Formal Methods
2023
-
[17]
Q., Welleck, S., Zhou, J
Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., and Lample, G. (2023b). Draft, sketch, and prove: Guiding formal theorem provers with informal proofs
2023
-
[18]
S., Reid, M., Matsuo, Y., and Iwasawa, Y
Kojima, T., Gu, S. S., Reid, M., Matsuo, Y., and Iwasawa, Y. (2023). Large language models are zero-shot reasoners
2023
-
[19]
Mikolov, T., Chen, K., Corrado, G., and Dean, J. (2013). Efficient estimation of word representations in vector space
2013
-
[20]
Q., Zhou, J
Mikuła, M., Tworkowski, S., Antoniak, S., Piotrowski, B., Jiang, A. Q., Zhou, J. P., Szegedy, C., Łukasz Kuciński, Miłoś, P., and Wu, Y. (2024). Magnushammer: A transformer-based approach to premise selection
2024
-
[21]
Moi, Y. (2013). SPARK 2014 rationale. Ada User Journal , 34(4):243--254
2013
-
[22]
Moy, Y., Ledinot, E., Delseny, H., Wiels, V., and Monate, B. (2013). Testing or formal verification: DO-178C alternatives and industrial experience. IEEE Software , 30(3):50--57
2013
-
[23]
Paulson, L. (2012). Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Schmidt, R. A., Schulz, S., and Konev, B., editors, PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning , ...
2012
-
[24]
Paulson, L. C. (1994). Isabelle: A generic theorem prover
1994
-
[25]
Pennington, J., Socher, R., and Manning, C. D. (2014). Glove: Global vectors for word representation. Conference on Empirical Methods in Natural Language Processing (EMNLP) , pages 1532--1543
2014
-
[26]
N., Kaiser, L., and Polosukhin, I
Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A. N., Kaiser, L., and Polosukhin, I. (2017). Attention is all you need. Advances in Neural Information Processing Systems (NeurIPS) , pages 5998--6008
2017
Reviewed August 8, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.