CoChat
Sign Up
PreprintCited by 1Logic, programming, and type systemsSoftware Engineering ResearchSoftware Testing and Debugging Techniques

Can LLMs Enable Verification in Mainstream Programming?

Open access
Shefer, Aleksandr, Engel, Igor, Alekseev, Stanislav, Berezun, Daniil, Verbitskaia, Ekaterina, Podkopaev, Anton·2025·arXiv
DOI 10.48550/arxiv.2503.14183arXiv 2503.14183
Open this paper in CoChat — free accountOpen PDF

Abstract

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.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.2503.14183

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Verus enforces strict implementation-level constraints (e.g., ownership, fixed-width integers), and expressing these constraints requires a verbose and strict syntax that creates a syntax barrier.

    “Verus, by contrast, enforces strict implementation-level constraints (e.g., ownership, fixed-width integers).Expressing these constraints requires a verbose and strict syntax that-compounded by the scarcity of Verus training data (Chen et al., 2024;Shefer et al., 2025)-creates a syntax barrier.”

    From AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms (2026) · cites this paper as Shefer et al., 2025

    Section 3.1 (p. 11) says Verus code generation frequently encounters type errors because of its complex type system and the different types permitted in code and invariants. The Evaluation (p. 9) also records syntax errors and notes that Verus has less training code available than Dafny. These passages support a barrier for LLM-generated Verus code, but do not establish ownership constraints or describe Verus syntax as verbose and strict. (LLM, conf=0.84)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

No references could be resolved yet.

Research works printed but not linked: 30

  1. [1]1. Pranjal Aggarwal, Bryan Parno, and Sean Welleck. Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement. arXiv preprint arXiv:2412.06176 , 2024. · arXiv
  2. [2]2. Dirk Beyer, Thomas A Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Path invariants. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation , pages 300-309, 2007.
  3. [3]3. Marat Boshernitsan, Roongko Doong, and Alberto Savoia. From daikon to agitator: lessons and challenges in building a commercial tool for developer testing. In Proceedings of the 2006 international symposium on Software testing and analysis , pages 169-180, 2006.
  4. [4]4. Franck Cassez, Joanne Fuller, and Aditya Asgaonkar. Formal verification of the ethereum 2.0 beacon chain. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages 167-182. Springer, 2022.
  5. [5]5. Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, and Nikhil Swamy. Towards neural synthesis for smtassisted proof-oriented programming. arXiv preprint arXiv:2405.01787 , 2024. · arXiv
  6. [6]6. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 , 2021. · arXiv
  7. [7]7. Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, et al. Automated proof generation for rust code via self-evolution. arXiv preprint arXiv:2410.15756 , 2024. · arXiv
  8. [8]8. Isil Dillig, Thomas Dillig, Boyang Li, and Ken McMillan. Inductive invariant generation via abductive inference. Acm Sigplan Notices , 48(10):443-456, 2013.
  9. [9]9. Marco Eilers and Peter Müller. Nagini: a static verifier for python. In Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I 30 , pages 596-603. Springer, 2018.
  10. [10]10. Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K Lahiri. Can large language models transform natural language intent into formal method postconditions? Proceedings of the ACM on Software Engineering , 1(FSE):18891912, 2024.
  11. [11]11. Michael D Ernst, Jeff H Perkins, Philip J Guo, Stephen McCamant, Carlos Pacheco, Matthew S Tschantz, and Chen Xiao. The daikon system for dynamic detection of likely invariants. Science of computer programming , 69(1-3):35-45, 2007.
  12. [12]12. Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948 , 2025. · arXiv
  13. [13]13. Hong Hu, Zheng Leong Chua, Sendroiu Adrian, Prateek Saxena, and Zhenkai Liang. Automatic generation of { Data-Oriented } exploits. In 24th USENIX Security Symposium (USENIX Security 15) , pages 177-192, 2015.
  14. [14]14. Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948 , 2023. · arXiv
  15. [15]15. Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps. Non-linear reasoning for invariant synthesis. Proceedings of the ACM on Programming Languages , 2(POPL):1-33, 2017.
  16. [16]16. Herb Krasner. The cost of poor software quality in the us: A 2022 report. Proc. Consortium Inf. Softw. QualityTM (CISQTM) , 2022.
  17. [17]17. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying rust programs using linear ghost types. Proceedings of the ACM on Programming Languages , 7(OOPSLA1):286-315, 2023.
  18. [18]18. Ton Chanh Le, Guolong Zheng, and ThanhVu Nguyen. Sling: using dynamic analysis to infer program invariants in separation logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation , pages 788-801, 2019.
  19. [20]20. Hong Lu, Jiacheng Gui, Chengyi Wang, and Hao Huang. A novel data-driven approach for generating verified loop invariants. In 2020 International Symposium on Theoretical Aspects of Software Engineering (TASE) , pages 9-16. IEEE, 2020.
  20. [21]21. Md Rakib Hossain Misu, Cristina V Lopes, Iris Ma, and James Noble. Towards aiassisted synthesis of verified dafny methods. Proceedings of the ACM on Software Engineering , 1(FSE):812-835, 2024.
  21. [22]22. Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou. Laurel: Generating dafny assertions using large language models. arXiv preprint arXiv:2405.16792 , 2024. · arXiv
  22. [23]23. Peter Müller, Malte Schwerhoff, and Alexander J Summers. Viper: A verification infrastructure for permission-based reasoning. In Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings 17 , pages 41-62. Springer, 2016.
  23. [25]25. Gabriel Poesia, Chloe Loughridge, and Nada Amin. dafny-annotator: Ai-assisted verification of dafny programs. arXiv preprint arXiv:2411.15143 , 2024. · arXiv
  24. [26]26. Daniel Riley and Grigory Fedyukovich. Multi-phase invariant synthesis. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering , pages 607-619, 2022.
  25. [27]27. Álvaro F Silva, Alexandra Mendes, and João F Ferreira. Leveraging large language models to boost dafny's developers productivity. In Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE) , pages 138-142, 2024.
  26. [29]29. Akhilesh Srikanth, Burak Sahin, and William R Harris. Complexity verification using guided theorem enumeration. ACM SIGPLAN Notices , 52(1):639-652, 2017.
  27. [30]30. Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. Clover: Closed-loop verifiable code generation. In International Symposium on AI Verification , pages 134-155. Springer, 2024.
  28. [31]31. Jianan Yao, Ziqiao Zhou, Weiteng Chen, and Weidong Cui. Leveraging large language models for automated proof synthesis in rust. arXiv preprint arXiv:2311.03739 , 2023. · arXiv
  29. [32]32. David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin. Higher-order specifications for deductive synthesis of programs with pointers. In 38th European Conference on Object-Oriented Programming (ECOOP 2024) . Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2024.
  30. [33]33. Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. Hacl*: A verified modern cryptographic library. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security , pages 1789-1806, 2017.

Cited by

Sorted by citations

Authors
Shefer, A., Engel, I., Alekseev, S., Berezun, D., Verbitskaia, E., & Podkopaev, A.
ORCID
Podkopaev, Anton
Venue
arXiv
Publisher
arXiv
Published
2025
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.2503.14183
arXiv
2503.14183
OpenAlex
W6891941702
Cited by
0
References
0
Type
posted content
Language
en
Open access
Licence
creativecommons.org/licenses/by/4.0/legalcode
Locations
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University) (cc-by)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Information Systems › Software Engineering Research
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
Keywords
large language models, formal verification, Dafny, Verus, HumanEval, Python, correctness guarantees, formal methods adoption

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review