Pith. sign in

REVIEW 2 cited by

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

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2502.07728 v1 pith:XO5MOLYX submitted 2025-02-11 cs.SE cs.AI

Marcos Cramer , Lucian McIntyre This is my paper
classification cs.SEcs.AI
keywords codesparkverificationannotationsformalsoftwarebenchmarkcapabilities
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
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.

Discussion (0). Sign in to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK

    cs.SE 2026-07 conditional novelty 6.0 of 10

    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.

  2. Position Paper: Programming Language Techniques for Bridging LLM Code Generation Semantic Gaps

    cs.SE 2025-07 unverdicted novelty 2.0 of 10

    A position paper arguing that PL techniques, especially formal verification and structure-aware representations, should be deeply integrated into LLM code generation.

Pith tools