Elamur Research⌕
☰
home / papers / 2024 / AutoVerus: Automated Proof Generation for Rust Code

AutoVerus: Automated Proof Generation for Rust Code

Paper · 2024 · Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu et al.

Summary

Using LLMs to produce machine-checkable correctness proofs still lags far behind using them to write code. Little earlier work targets programs in a mainstream language. AutoVerus tackles this for Rust programs checked by Verus, an SMT-based verifier. Verus specifications and proof annotations use Rust syntax, but the tool is young and has few public examples to learn from. The system avoids fine-tuning and retrieval. It relies on an existing model (GPT-4o) and builds Verus experts' strategies into a network of LLM agents. The agents work in three stages that mirror how a human builds a proof:

  • drafting initial loop invariants,
  • refining them with generic checks for typical omissions,
  • repairing the proof step by step from Verus error messages.

Agents sample many diverse candidates at high temperature. Verus and Lynette, a custom AST-level analyzer, then discard invalid or "cheating" candidates, rank the remaining ones and merge useful fragments. On Verus-Bench, a new suite of 150 non-trivial tasks, AutoVerus proves over 90% of tasks, often very quickly. This is a practical step toward formally verified Rust code written with AI help.

Key points

  • Verus-Bench: 150 proof tasks drawn from code-generation and verification sources (MBPP, Diffy, Clover, Misc). Only the 38 Diffy tasks are mainly about loop invariants. For example, 43 of the 78 MBPP tasks also need asserts, lemmas or other annotations.
  • Results: AutoVerus produced correct proofs for more than 90% of tasks. Over half were solved in under 30 seconds or with at most 3 LLM calls.
  • Debugging stage: about 10 specialized agents, each targeting one major class of Verus verification error (e.g., an unsatisfied post-condition, or an invariant that fails before the loop).
  • Filtering: Lynette, built on the Verus parser, rejects candidates that alter the specification or the code under proof, or that insert assume. Verus feedback is used to rank and combine partial proofs.
  • Publication and artifact: Proc. ACM Program. Lang. (OOPSLA2, 2025). Code and artifact are available at microsoft/verus-proof-synthesis.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🏢MicrosoftRedmond · United States404 works · 163,863 citations🎓Columbia UniversityNew York · United States263 works · 57,820 citations🎓University of Illinois Urbana-ChampaignUrbana · United States228 works · 74,590 citations🎓University of TorontoToronto · Canada121 works · 179,944 citations🏢Microsoft Research AsiaBeijing · China86 works · 61,617 citations🎓University of ChicagoChicago · United States54 works · 50,989 citations🎓University of California, IrvineIrvine · United States45 works · 36,639 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksInformation Systems · 1,888 worksSoftware · 150 works

Cite

Cite as Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou and Shan Lu. 2024. AutoVerus: Automated Proof Generation for Rust Code. arXiv:2409.13082.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1145/3763174 · arXiv 2409.13082

@misc{yang2024autoverus,
  title = {{AutoVerus: Automated Proof Generation for Rust Code}},
  author = {Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou and Shan Lu},
  year = {2024},
  doi = {10.1145/3763174},
  eprint = {2409.13082},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1145/3763174}
}

References

55 references, 18 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers. 2019. Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang. 3, OOPSLA (2019), 147:1–147:30. https://doi.org/10.1145/ 3360573 find
  2. Jacob Austin, Augustus Odena, Maxwell I. Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie J. Cai, Michael Terry, Quoc V. Le, and Charles Sutton. 2021. Program Synthesis with Large Language Models. CoRR abs/2108.07732 (2021). https://arxiv.org/abs/2108.07732 ↗
  3. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, U…
  4. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. 1999. The Coq proof assistant reference manual. INRIA, version 6, 11 (1999). https://hal.science/inria-00069919 ↗
  5. Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri, and Nikhil Swamy. 2024. Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming. CoRR abs/2405.01787 (2024). https://doi.org/10.48550/ARXIV.2405.01787 ↗
  6. Supratik Chakraborty, Ashutosh Gupta, and Divyesh Unadkat. 2021. Diffy: Inductive Reasoning of Array Programs Using Difference Invariants. In Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II (Lecture Notes in Computer Scienc… — [doi:10.1007/978-3-030-81688-9_42](https://doi.org/10.1007/978-3-030-81688-9_42) find
  7. 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. 2021. Evaluating large language models trained on code. CoRR abs/2107.03374 (2021). https://arxiv.org/abs/2107.03374 ↗
  8. Xiangdong Chen, Zhaofeng Li, Lukas Mesicek, Vikram Narayanan, and Anton Burtsev. 2023. Atmosphere: Towards Practical Verified Kernels in Rust. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification, KISV 2023, Koblenz, Germany, 23 October 2023. ACM, 9–17. https://doi.org/10.… — [doi:10.1145/3625275.3625401](https://doi.org/10.1145/3625275.3625401) find
  9. Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings (Lecture Notes in Computer Science, Vol. 12699), André Platzer and…
  10. Yinlin Deng, Chunqiu Steven Xia, Haoran Peng, Chenyuan Yang, and Lingming Zhang. 2023. Large Language Models Are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023,… — [doi:10.1145/3597926.3598067](https://doi.org/10.1145/3597926.3598067) find
  11. Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In Formal Methods and Software Engineering - 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, October 24-27, 2022, Proceedings (Lec… — [doi:10.1007/978-3-031-17244-1_6](https://doi.org/10.1007/978-3-031-17244-1_6) find
  12. ETAPS. 2024. 10th Competition on Software Verification (SV-COMP 2021). https://sv-comp.sosy-lab.org/2021/. [Online], [Accessed: 2024-09-01]. ↗
  13. Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, and Nikhil Swamy. 2024. 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers. CoRR abs/2404.10362 (2024). https://doi.org/10.48550/ ARXIV.2404.10362 — [arXiv:2404.10362](https://arxiv.org/abs/2404.10362) find
  14. Emily First and Yuriy Brun. 2022. Diversity-Driven Automated Formal Verification. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022. ACM, 1–13. https://doi.org/10. 1145/3510003.3510138 find
  15. Emily First, Yuriy Brun, and Arjun Guha. 2020. TacTok: semantics-aware proof synthesis. Proc. ACM Program. Lang. 4, OOPSLA (2020), 231:1–231:31. https://doi.org/10.1145/3428299 — [doi:10.1145/3428299](https://doi.org/10.1145/3428299) ↗
  16. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. 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, ESEC/FSE 2023, San Francisco,…
  17. Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an Annotation Assistant for ESC/Java. In FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings (Lecture Notes in Computer Science, Vol. 20… — [doi:10.1007/3-540-45251-6_29](https://doi.org/10.1007/3-540-45251-6_29) find
  18. Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. 2024. RefinedRust: A Type System for High-Assurance Verification of Rust Programs. Proc. ACM Program. Lang. 8, PLDI (2024), 1115–1139. https://doi.org/10.1145/3656422 — [doi:10.1145/3656422](https://doi.org/10.1145/3656422) ↗
  19. Son Ho and Jonathan Protzenko. 2022. Aeneas: Rust verification by functional translation. Proc. ACM Program. Lang. 6, ICFP (2022), 711–741. https://doi.org/10.1145/3547647 ↗
  20. Rijul Jain, Shraddha Barke, Gabriel Ebner, Md Rakib Hossain Misu, Shan Lu, and Sarah Fakhoury. 2025. What’s in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus. arXiv preprint arXiv:2508.02733 (2025). — [arXiv:2508.02733](https://arxiv.org/abs/2508.02733) find
  21. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In Advances in Neural Information Processing Systems 35: Annual Conference on N…
  22. Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018. RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2, POPL (2018), 66:1–66:34. https://doi.org/10.1145/3158154 ↗
  23. Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. 2023. Finding Inductive Loop Invariants using Large Language Models. CoRR abs/2311.07948 (2023). https://doi.org/10.48550/ARXIV.2311.07948 — [doi:10.48550/arxiv.2311.07948](https://doi.org/10.48550/arxiv.2311.07948) ↗
  24. Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024. Verus: A Practical Foundation for Systems Verification. In Proceedings of the 30th… find
  25. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. Proc. ACM Program. Lang. 7, OOPSLA1 (2023), 286–315. https://doi.org/10.1145/3586037 — [doi:10.1145/3586037](https://doi.org/10.1145/3586037) ↗
  26. Hayley LeBlanc, Jacob R Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, and Vijay Chidambaram. 2025. PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection. OSDI (to appear) (2025). find
  27. K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (Lecture Notes in Computer Science, Vol.… — [doi:10.1007/978-3-642-17511-4_20](https://doi.org/10.1007/978-3-642-17511-4_20) find
  28. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. 2024. A Survey on Deep Learning for Theorem Proving. CoRR abs/2404.09939 (2024). https://doi.org/10.48550/ARXIV.2404.09939 ↗
  29. Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. 2023. Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation. In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing System…
  30. Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. 2024. DafnyBench: A Benchmark for Formal Software Verification. CoRR abs/2406.08467 (2024). https://doi.org/10.48550/ARXIV.2406.08467 ↗
  31. Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. 2022. RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. In PLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA,… — [doi:10.1145/3519939.3523704](https://doi.org/10.1145/3519939.3523704) find
  32. Microsoft. 2024. Storage systems with verified correctness properties. https://github.com/microsoft/verified-storage. [Online], [Accessed: 2024-09-01]. ↗
  33. Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024. Towards AI-Assisted Synthesis of Verified Dafny Methods. Proc. ACM Softw. Eng. 1, FSE (2024), 812–835. https://doi.org/10.1145/3643763 ↗
  34. Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou. 2024. Laurel: Generating Dafny Assertions Using Large Language Models. CoRR abs/2405.16792 (2024). https://doi.org/10.48550/ ARXIV.2405.16792 — [arXiv:2405.16792](https://arxiv.org/abs/2405.16792) find
  35. Office of the National Cyber Director. 2024. BACK TO THE BUILDING BLOCKS: A PATH TOWARD SECURE AND MEASURABLE SOFTWARE. https://www.whitehouse.gov/wp-content/uploads/2024/02/Final-ONCD-Technical-Report.pdf ↗
  36. Lawrence C. Paulson. 1994. Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow). Lecture Notes in Computer Science, Vol. 828. Springer. https://doi.org/10.1007/BFB0030541 — [doi:10.1007/bfb0030541](https://doi.org/10.1007/bfb0030541) ↗
  37. Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. CoRR abs/2009.03393 (2020). https://arxiv.org/abs/2009.03393 ↗
  38. MIT Technology Review. 2023. How Rust went from a side project to the world’s most-loved programming language. https://www.technologyreview.com/2023/02/14/1067869/rust-worlds-fastest-growing-programming-language/. [Online], [Accessed: 2024-09-01]. ↗
  39. Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. 2020. Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, MAPL@PLDI 2020, London, UK, June 15, 2020. ACM, 1–10. https://…
  40. Stackoverflow. 2024. "2024 Developer Survey: AI tools at development process; Challenges with AI at work". https://survey.stackoverflow.co/2024/ai/. [Online], [Accessed: 2025-03-01]. ↗
  41. Stackoverflow. 2024. "Rust continues to be the most-admired programming language". https://survey.stackoverflow.co/ 2024/technology. [Online], [Accessed: 2024-09-01]. ↗
  42. Chuyue Sun, Ying Sheng, Oded Padon, and Clark W. Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation. In AI Verification - First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22-23, 2024, Proceedings (Lecture Notes in Computer Science, Vol. 14846). Springer, 134–155. https…
  43. Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. 2024. Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2… find
  44. Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. 2016. Dependent types and multi-monadic effects in F. In Proceeding… — [doi:10.1145/2837614.2837655](https://doi.org/10.1145/2837614.2837655) find
  45. The Kani Team. 2024. How Open Source Projects are Using Kani to Write Better Software in Rust \| AWS Open Source Blog. https://aws.amazon.com/blogs/opensource/how-open-source-projects-are-using-kani-to-write-better-software-in-rust/. [Online], [Accessed: 2024-09-01]. ↗
  46. Runchu Tian, Yining Ye, Yujia Qin, Xin Cong, Yankai Lin, Yinxu Pan, Yesai Wu, Haotian Hui, Weichuan Liu, Zhiyuan Liu, and Maosong Sun. 2024. DebugBench: Evaluating Debugging Capability of Large Language Models. (2024), 4173–4198. https://aclanthology.org/2024.findings-acl.247 ↗
  47. Verus. [n. d.]. Verus Tutorial and Reference. https://verus-lang.github.io/verus/guide/. ↗
  48. Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. 2024. LEGO-Prover: Neural Theorem Proving with Growing Libraries. In The Twelfth International Conference on Learning Representations, ICLR 20…
  49. Haoze Wu, Clark W. Barrett, and Nina Narodytska. 2024. Lemur: Integrating Large Language Models in Automated Program Verification. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net. https://openreview.net/forum?id=Q3YaCghZ… ↗
  50. Chunqiu Steven Xia and Lingming Zhang. 2023. Keep the Conversation Going: Fixing 162 out of 337 bugs for $0.42 each using ChatGPT. CoRR abs/2304.00385 (2023). https://doi.org/10.48550/ARXIV.2304.00385 — [doi:10.48550/arxiv.2304.00385](https://doi.org/10.48550/arxiv.2304.00385) ↗
  51. Chenyuan Yang, Yinlin Deng, Runyu Lu, Jiayi Yao, Jiawei Liu, Reyhaneh Jabbarvand, and Lingming Zhang. 2024. Whitefox: White-box compiler fuzzing empowered by large language models. Proceedings of the ACM on Programming Languages 8, OOPSLA2 (2024), 709–735. find
  52. Chenyuan Yang, Zijie Zhao, and Lingming Zhang. 2025. Kernelgpt: Enhanced kernel fuzzing via large language models. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2. 560–573. find
  53. Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Interacting with Proof Assistants. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA (Proceedings of Machine Learning Research, Vol. 97). PMLR, 6984–6994. http:…
  54. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. 2023. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Infor…
  55. Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, and Weidong Cui. 2024. VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024. USENIX Association, 599–614.… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/yang-2024-autoverus-automated-proof-generation-rust/