CoChat
Sign Up
PreprintCited by 4Logic, programming, and type systemsSoftware Testing and Debugging TechniquesFormal Methods in Verification

Automated Proof Generation for Rust Code via Self-Evolution

Open access
Chen, Tianyu, Lu, Shuai, Lu, Shan, Gong, Yeyun, Yang, Chenyuan, Li, Xuheng, Misu, Md Rakib Hossain, Yu, Hao +6 more·2024·arXiv
DOI 10.48550/arxiv.2410.15756arXiv 2410.15756
Open this paper in CoChat — free accountOpen PDF

Abstract

Ensuring correctness is crucial for code generation. Formal verification offers a definitive assurance of correctness, but demands substantial human effort in proof construction and hence raises a pressing need for automation. The primary obstacle lies in the severe lack of data-there is much fewer proofs than code snippets for Large Language Models (LLMs) to train upon. In this paper, we introduce SAFE, a framework that overcomes the lack of human-written proofs to enable automated proof generation of Rust code. SAFE establishes a self-evolving cycle where data synthesis and fine-tuning collaborate to enhance the model capability, leveraging the definitive power of a symbolic verifier in telling correct proofs from incorrect ones. SAFE also re-purposes the large number of synthesized incorrect proofs to train the self-debugging capability of the fine-tuned models, empowering them to fix incorrect proofs based on the verifier's feedback. SAFE demonstrates superior efficiency and precision compared to GPT-4o. Through tens of thousands of synthesized proofs and the self-debugging mechanism, we improve the capability of open-source models, initially unacquainted with formal verification, to automatically write proofs for Rust code. This advancement leads to a significant improvement in performance, achieving a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.

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.2410.15756

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?

  • SAFE++ proposes translating an existing Rust dataset to Verus and training generation and refinement models on the collected data.

    “Second, the concurrent work SAFE++ (Chen et al., 2024) proposes translating an existing Rust dataset to Verus and training generation and refinement models on the collected data.”

    From AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (2024) · cites this paper as Chen et al., 2024

    The Introduction and §4.1 say the paper translates programs from existing datasets into Verus-compatible Rust and uses the resulting data for training. Section 3.3 describes joint training for proof generation and self-debugging, rather than separate generation and refinement models. The paper calls the framework SAFE and its self-debugging variant SAFE+, not SAFE++. (LLM, conf=0.87)

    Experimental — accuracy not yet measured

  • The translation process in Chen et al. (2024) was initialized with over a month of continuous generation from GPT-4.

    “However, the translation process in Chen et al. (2024) was initialized with over a month of continuous generation from GPT-4.”

    From AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (2024) · cites this paper as Chen et al. (2024)

    Section 3.1 says GPT-4o was used to translate Rust code into Verus-compatible code. Section 3.3 attributes one whole month of non-stop GPT-4o invocations to bootstrapping proof synthesis, not translation. The source also says one month, rather than over a month. (LLM, conf=0.88)

    Experimental — accuracy not yet measured

  • 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 Chen et al., 2024

    Section 3.1 says Verus does not support all Rust features and requires code to be adapted to Verus-compatible syntax; Section 2.1 says nontrivial proofs often need annotations. The Introduction also documents a scarcity of Verus specifications and proofs. Our copy does not establish that ownership constraints or verbose syntax create the claimed syntax barrier. (LLM, conf=0.84)

    Experimental — accuracy not yet measured

  • Treefinement leads to substantial gains over vanilla refinement strategies that resemble those used in concurrent work.

    “We show that Treefinement leads to substantial gains over vanilla refinement strategies that resemble those used in concurrent work (Yang et al., 2024;Chen et al., 2024).”

    From AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (2024) · cites this paper as Chen et al., 2024

  • Unlike prior work that requires LLMs to fill proof annotations in existing code and specifications, AlphaVerus evaluates models on generating both the code and the corresponding proofs given only the specifications.

    “Unlike prior work that requires LLMs to fill proof annotations in existing code and specifications (Loughridge et al., 2024;Yang et al., 2024;Chen et al., 2024), we evaluate our models on this challenging task of generating both the code and the corresponding proofs given only the specifications.”

    From AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (2024) · cites this paper as Chen et al., 2024

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: 40

  1. Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al. Program synthesis with large language models. arXiv preprint arXiv:2108.07732, 2021. · arXiv
  2. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Al- bert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. arXiv preprint arXiv:2310.10631, 2023. · arXiv
  3. Dirk Beyer. Software verification: 10th comparative evaluation. In Proceedings of Tools and Algo- rithms for the Construction and Analysis of Systems: 27th International Conference, pp. 401-422, 2021.
  4. Saikat Chakraborty, Shuvendu K Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, and Nikhil Swamy. Ranking LLM-generated loop invariants for program verification. arXiv preprint arXiv:2310.09342, 2023. · arXiv
  5. Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, and Nikhil Swamy. Towards neural synthesis for smt-assisted proof-oriented program- ming. arXiv preprint arXiv:2405.01787, 2024. · arXiv
  6. Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. Teaching large language models to self-debug. arXiv preprint arXiv:2304.05128, 2023. · arXiv
  7. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proceedings of Inter- national conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340, 2008.
  8. Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The LLaMa 3 herd of models. arXiv preprint arXiv:2407.21783, 2024. · arXiv
  9. Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K Lahiri. Can large language models transform natural language intent into formal method postconditions? In Proceedings of the ACM International Conference on the Foundations of Software Engineering, pp. 1889-1912, 2024.
  10. Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1229- 1241, 2023.
  11. Cormac Flanagan and K Rustan M Leino. Houdini, an annotation assistant for ESC/Java. In Pro- ceedings of the International Symposium of Formal Methods Europe, pp. 500-517, 2001.
  12. Kelsey R Fulton, Anna Chan, Daniel Votipka, Michael Hicks, and Michelle L Mazurek. Benefits and drawbacks of adopting a secure programming language: Rust as a case study. In Proceedings of Seventeenth Symposium on Usable Privacy and Security, pp. 597-616, 2021.
  13. Caglar Gulcehre, Tom Le Paine, Srivatsan Srinivasan, Ksenia Konyushkova, Lotte Weerts, Abhishek Sharma, Aditya Siddhant, Alex Ahern, Miaosen Wang, Chenjie Gu, et al. Reinforced self-training (rest) for language modeling. arXiv preprint arXiv:2308.08998, 2023. · arXiv
  14. Daya Guo, Qihao Zhu, Dejian Yang, Zhenda Xie, Kai Dong, Wentao Zhang, Guanting Chen, Xiao Bi, Y Wu, YK Li, et al. DeepSeek-Coder: When the large language model meets programming- the rise of code intelligence. arXiv preprint arXiv:2401.14196, 2024. · arXiv
  15. Henry Hsu and Peter A Lachenbruch. Paired t test. Wiley StatsRef: statistics reference online, 2014.
  16. 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
  17. Shuvendu K Lahiri. Evaluating LLM-driven User-Intent Formalization for Verification-Aware Lan- guages. arXiv preprint arXiv:2406.09757, 2024. · arXiv
  18. Shuvendu K Lahiri, Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, Madanlal Musuvathi, Piali Choudhury, Curtis von Veh, Jeevana Priya Inala, Chenglong Wang, et al. Inter- active code generation via test-driven user-intent formalization. arXiv preprint arXiv:2208.05950, 2022. · arXiv
  19. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon How- ell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying rust programs using linear ghost types. In Proceedings of the Annual Conference on Object-Oriented Programming Systems, Languages, and Applications, pp. 286-315, 2023.
  20. K Rustan M Leino. Dafny: An automatic program verifier for functional correctness. In Proceedings of the International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 348-370, 2010.
  21. Chang Liu, Xiwei Wu, Yuan Feng, Qinxiang Cao, and Junchi Yan. Towards general loop invari- ant generation via coordinating symbolic execution and large language models. arXiv preprint arXiv:2311.10483, 2023. · arXiv
  22. Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. DafnyBench: A benchmark for formal software verification. arXiv preprint arXiv:2406.08467, 2024. · arXiv
  23. Anton Lozhkov, Raymond Li, Loubna Ben Allal, Federico Cassano, Joel Lamy-Poirier, Nouamane Tazi, Ao Tang, Dmytro Pykhtar, Jiawei Liu, Yuxiang Wei, et al. Starcoder 2 and the stack v2: The next generation. arXiv preprint arXiv:2402.19173, 2024. · arXiv
  24. Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. Specgen: Automated generation of formal program specifications via large language models. arXiv preprint arXiv:2401.08807, 2024. · arXiv
  25. Md Rakib Hossain Misu, Cristina V Lopes, Iris Ma, and James Noble. Towards AI-assisted synthesis of verified Dafny methods. Proceedings of the ACM International Conference on the Foundations of Software Engineering, pp. 812-835, 2024.
  26. Theo X Olausson, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao, and Armando Solar- Lezama. Is self-repair a silver bullet for code generation? In Proceedings of the Twelfth In- ternational Conference on Learning Representations, 2023.
  27. Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. Can large language models reason about program invariants? In Proceedings of the International Conference on Machine Learning, pp. 27496-27520, 2023.
  28. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022. · arXiv
  29. Ruchir Puri, David S Kung, Geert Janssen, Wei Zhang, Giacomo Domeniconi, Vladimir Zolotov, Julian Dolby, Jie Chen, Mihir Choudhury, Lindsey Decker, et al. CodeNet: A large-scale ai for code dataset for learning a diversity of coding tasks. arXiv preprint arXiv:2105.12655, 2021. · arXiv
  30. Elijah Rivera, Samuel Mergendahl, Howard Shrobe, Hamed Okhravi, and Nathan Burow. Keeping safe Rust safe with Galeed. In Proceedings of the 37th Annual Computer Security Applications Conference, pp. 824-836, 2021.
  31. Baptiste Roziere, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Tal Remez, Jérémy Rapin, et al. Code Llama: Open foundation models for code. arXiv preprint arXiv:2308.12950, 2023. · arXiv
  32. Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. Clover: Closed-loop verifiable code generation. In Proceedings of the International Symposium on AI Verification, pp. 134-155, 2024a.
  33. Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, et al. Anvil: Verifying liveness of cluster manage- ment controllers. In Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation, pp. 649-666, 2024b.
  34. Nikhil Swamy, Cȃtȃlin Hrit ¸cu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, et al. De- pendent types and multi-monadic effects in F. In Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, pp. 256-270, 2016.
  35. Zhengwei Tao, Ting-En Lin, Xiancai Chen, Hangyu Li, Yuchuan Wu, Yongbin Li, Zhi Jin, Fei Huang, Dacheng Tao, and Jingren Zhou. A survey on self-evolution of large language models. arXiv preprint arXiv:2404.14387, 2024. · arXiv
  36. Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, et al. AutoVerus: Automated proof generation for rust code. arXiv preprint arXiv:2409.13082, 2024a. · arXiv
  37. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. LeanDojo: Theorem proving with retrieval- augmented language models. Advances in Neural Information Processing Systems, 36, 2024b.
  38. 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
  39. Lichen Zhang, Shuai Lu, and Nan Duan. Selene: Pioneering automated proof in software verifica- tion. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics, pp. 1776-1789, 2024.
  40. Ziqiao Zhou, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui, et al. {VeriSMo}: A verified security module for confidential {VMs}. In Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation, pp. 599-614, 2024.

Cited by

Sorted by citations

Authors
Chen, T., Lu, S., Lu, S., Gong, Y., Yang, C., Li, X., Misu, M. R. H., Yu, H., Duan, N., Cheng, P., Yang, F., Lahiri, S. K., Xie, T., & Zhou, L.
Affiliations
  • Peking University (CN)
  • Microsoft (United States) (US)
  • University of Illinois Urbana-Champaign (US)
  • Columbia University (US)
ORCID
Venue
arXiv
Publisher
arXiv
Published
2024
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.2410.15756
arXiv
2410.15756
OpenAlex
W4404088940
Cited by
1
References
0
Citations by year
2025: 1
Type
posted content
Language
en
Open access
Licence
Locations
  • arXiv (Cornell University) (submittedVersion, cc-by)
  • arXiv (Cornell University) (cc-by)
Funders
  • National Natural Science Foundation of China (92464301)
  • Peking University
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
Keywords
proof automation, formal verification, large language models, self-evolution, data synthesis, SAFE framework

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