Source-linked AI summary
Can LLMs Enable Verification in Mainstream Programming?
Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev
TL;DR
Formal methods can produce reliable software, but verification remains difficult to adopt in everyday programming, while code-generating LLMs rarely target strong correctness guarantees. This study tests LLM generation of verified code in three systems using HumanEval-derived benchmarks and finds higher synthesis performance in Dafny than Nagini or Verus.
Problem
Formal methods can produce reliable software but have limited everyday adoption, while code-generating LLMs rarely target strong correctness guarantees; verification also requires expertise and specialized languages.
Source: §1 · p. 1Method
Results
Dafny performance was higher than Nagini or Verus; Mode 6 had less than 30% success in Dafny and 15% in Nagini and Verus.
Source: §3 · p. 9Takeaways & Limitations
The demonstrated ability to generate verified code motivates further research in less-explored systems such as Nagini and Verus.
Source: §4 · p. 12The validation compares generated specifications with benchmark ground truth, an approach the authors note may not scale to more complicated tasks.
Source: §2.3 · p. 7
Abstract
from arXiv · showhide
Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini, and Verus). To do so, we use manually curated datasets derived from the state-ofthe-art Python benchmark, HumanEval. We also assess what types of information are sufficient to achieve good-quality results.
1 Introduction
LLMs make code generation widespread, heightening the need to ensure generated code is correct, while formal verification remains difficult to adopt in everyday programming. This study tests LLMs’ ability to generate verified code and investigates how much task information they need.
1 Introduction
- LLMs’ growing use for code generation makes correctness guarantees important because less critical evaluation can allow errors into codebases.The paper presents intermediate verification languages as one way to bridge mainstream programming and formal methods.Source: §1 · pp. 1–2
- Formal verification requires expertise and adds development time, limiting its use outside domains where mistakes have severe consequences.Specialized verification languages can also bring less mature tooling, limited interoperability with mainstream languages, and a steeper learning curve.Source: §1 · p. 1
- The study evaluates LLM-generated verified code in Dafny, Nagini, and Verus, using Dafny as a baseline and HumanEval-derived reference datasets.It also varies how much problem information is exposed to the model.Source: §1 · p. 2
2 Method
The method evaluates LLM-generated code across tasks with different information requirements, then checks both whether generated code verifies and whether it meets the benchmark reference specification.
2 Method
- The evaluation pipeline prepares a task prompt, generates a candidate, uses verifier feedback for refinement, optionally post-processes the code, and validates it against the reference specification.Reference validation checks that generated preconditions are not too weak and postconditions are not too strong.Source: §2 · p. 3
2.4 Benchmarks
- The benchmarks contain manually verified HumanEval-derived programs, with datasets prepared for Dafny, Nagini, and Verus; some original tasks were excluded as unsuitable or unsupported.Dafny and Verus benchmarks were created manually; Nagini conversion required inspection and manual adjustments because it is less expressive than Dafny.Source: §2.1 · p. 4, §2.4 · pp. 7–8
2.1 Task Preparation for Different Modes
- Mode 1 asks the model to complete proofs from given code and specifications, while Modes 2–4 respectively generate specifications from code, implement and prove from a specification, and do so with a text description.Mode 1 removes invariants, assertions, and lemma calls from the target methods.Source: §2.1 · p. 4
- Modes 5 and 6 ask the model to generate an implementation and proof from natural-language specifications and method signatures, with specification functions included only in Mode 5.The functions provide additional context but may make user intent easier to guess.Source: §2.1 · pp. 4, 6
2.2 Interaction with an LLM
- System prompts set the verifier role and output format, while user prompts provide the task, code-structure guidance, examples, and optional tips.Verification errors are fed back for correction up to a limit, and syntax converters address common Nagini mistakes before another model call.Source: §2.2 · p. 6
2.3 Validation
- Additional validation checks that existing code remains unchanged or that generated code and specifications are sufficiently expressive.The approach restricts some language features, adds verification overhead, and compares generated code with benchmark ground truth, which may not scale to more complex tasks.Source: §2.2 · pp. 6–7, §2.3 · p. 7
3 Evaluation
Across the HumanEval evaluation, Dafny outperformed Nagini and Verus, though Nagini verified over half of the programs in the first four modes. The reported error patterns also differed across languages.
3 Evaluation
- The evaluation used Claude 3.5 Sonnet on HumanEval five times, allowing up to five attempts to fix verification issues and counting unique problems verified in at least one run.The authors selected Claude 3.5 Sonnet after it outperformed the other models they tried in quality while remaining manageable in time and cost.Source: §3 · p. 8
- Dafny outperformed Nagini and Verus; Nagini verified over half of the programs in the first four modes, while Verus was the least expressive and newest system.The authors note that Dafny's higher performance was expected given its popularity and the greater amount of available training code.Source: §3 · p. 9
- Mode 6 had the lowest success rates: below 30% for Dafny and 15% for both Nagini and Verus, which the authors attribute to validation requiring ground-truth-matching specifications.The validation step checks that generated specifications match those in the ground truth.Source: §3 · p. 9
- Only a minuscule number of successfully generated programs were unique to systems other than Dafny, suggesting models may draw on Dafny knowledge when using the other systems.Figure 4 shows intersections among programs successfully generated in at least one of five attempts.Source: §3 · p. 9, Figure 4 · p. 10
3.1 Understanding Common Pitfalls
- Timeouts were the most frequent error in Nagini, and the authors report that models rarely resolve them because they provide little information about the underlying proof problem.Timeouts were less common in Dafny and Verus, which are aimed at delivering verification results quickly.Source: §3.1 · p. 11
- Dafny and Nagini most often had incomplete-proof errors, whereas Verus most often had type errors linked to its complex type system and differing code and invariant types.An explicit cast, pos as int, can fix the illustrated Verus type error, but models often fail to supply it.Source: §3.1 · p. 11
4 Conclusion
The study demonstrates that LLMs can generate formally verified code, lowering barriers to formal-methods adoption in mainstream programming. The authors identify further work on less-explored systems, model familiarity, error correction, and human involvement.
4 Conclusion
- The study demonstrates that LLMs can generate formally verified code, lowering barriers to formal-methods adoption in mainstream programming.The authors identify high success in Dafny as motivation for further research on less-explored systems such as Nagini and Verus.Source: §4 · p. 12
- The authors propose fine-tuning for unfamiliar verification systems, which would require larger datasets that may be difficult to collect because little source code is published online.They note synthetic means as one possible way to approach dataset collection.Source: §4 · p. 12
- Specialized error-correction mechanisms, self-improving frameworks, and a balance between automation and human involvement are identified as directions for making verification more accessible.Source: §4 · p. 12