CoChat
Sign Up
PreprintCited by 20Logic, programming, and type systemsSoftware Testing and Debugging TechniquesSoftware Engineering Research

AutoVerus: Automated Proof Generation for Rust Code

Open access
Yang, Chenyuan, Li, Xuheng, Misu, Md Rakib Hossain, Yao, Jianan, Cui, Weidong, Gong, Yeyun, Hawblitzel, Chris, Lahiri, Shuvendu +5 more·2024·arXiv
DOI 10.48550/arxiv.2409.13082arXiv 2409.13082

Preprint — published as 10.1145/3763174 · Paper page

Open this paper in CoChat — free accountOpen PDF

Abstract

Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AutoVerus. AutoVerus uses LLMs to automatically generate correctness proof for Rust code. AutoVerus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AutoVerus consists of a network of LLM agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AutoVerus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.

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

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?

  • Existing baseline methods for proof annotations in Verus lack contamination analysis.

    “Notably, existing baseline methods for proof annotations in Verus (Yang et al., 2024;Chen et al., 2024) lack such contamination analysis.”

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

    The paper does not lack contamination analysis: its “General threats to validity” section explicitly considers whether the LLM had seen benchmark tasks in training data. It examines the public availability of Verus proofs and the baseline LLM’s performance on potentially leaked tutorial tasks. The analysis is qualitative, but it directly contradicts the claim that none was conducted. (LLM, conf=0.87)

    Checked by a reasoning model — may be wrong.

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

  • AutoVerus prompts GPT-4 with a pipeline of hand-engineered prompts tailored to specific errors and programs.

    “First, AutoVerus (Yang et al., 2024) prompts GPT-4 with a pipeline of hand-engineered prompts tailored to specific er-rors and programs.”

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

  • MBPP-verified contains 78 programs from the original MBPP dataset.

    “In particular, MBPP -verified is sourced from (Yang et al., 2024;Misu et al., 2024) and contains 78 programs from the original MBPP dataset (Austin et al., 2021).”

    From AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (2024) · cites this paper as Yang 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 Yang 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: 49

  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 · DOI
  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 · arXiv
  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, USA (Proceedings of Machine Learning Research, Vol. 97). PMLR, 454-463. http://proceedings.mlr.press/v97/bansal19a.html
  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 · DOI
  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 Science, Vol. 12760), Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, 911-935. https://doi.org/10.1007/978-3-030-81688-9_42 · DOI
  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 · arXiv
  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.1145/3625275.3625401 · DOI
  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 Geoff Sutcliffe (Eds.). Springer, 625-635. https://doi.org/10.1007/978-3-030-79876-5_37 · DOI · Paper page
  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, Seattle, WA, USA, July 17-21, 2023. ACM, 423-435. https://doi.org/10.1145/3597926.3598067 · DOI · Paper page
  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 (Lecture Notes in Computer Science, Vol. 13478). Springer, 90-105. https://doi.org/10.1007/978-3-031-17244-1_6 · DOI
  12. 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 · DOI
  13. 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 · DOI
  14. 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
  15. 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, CA, USA, December 3-9, 2023. ACM, 1229-1241. https://doi.org/10.1145/3611643.3616243 · DOI · Paper page
  16. 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. 2021), José Nuno Oliveira and Pamela Zave (Eds.). Springer, 500-517. https://doi.org/10.1007/3-540-45251-6_29 · DOI
  17. 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
  18. 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 · DOI
  19. 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
  20. 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 Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 -December 9, 2022. http://papers.nips.cc/paper_files/ paper/2022/hash/377c25312668e48f2e531e2f2c422483-Abstract-Conference.html
  21. 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 · DOI
  22. 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 · Paper page
  23. 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 Symposium on Operating Systems Principles, SOSP 2024, Hilton Austin, Texas, USA, November 4-6, 2024. ACM. https://sigops.org/s/conferences/sosp/2024/accepted.html
  24. 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
  25. Hayley LeBlanc, Jacob R Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, and Vijay Chi- dambaram. 2025. PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection. OSDI (to appear) (2025).
  26. 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. 6355), Edmund M. Clarke and Andrei Voronkov (Eds.). Springer, 348-370. https://doi.org/10.1007/978-3-642-17511-4_20 · DOI · Paper page
  27. 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 · DOI
  28. 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 Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 -16, 2023. http://papers.nips.cc/paper_files/paper/2023/hash/43e9d647ccd3e4b7b5baab53f0368686- Abstract-Conference.html
  29. 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 · DOI · Paper page
  30. 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, USA, June 13 -17, 2022. ACM, 841-856. https: //doi.org/10.1145/3519939.3523704 · DOI
  31. 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 · DOI · Paper page
  32. 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 · DOI
  33. 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
  34. Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. CoRR abs/2009.03393 (2020). https://arxiv.org/abs/2009.03393 · arXiv
  35. 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://doi.org/10.1145/3394450.3397466 · DOI
  36. 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://doi.org/10.1007/978-3-031-65112-0_7 · DOI · Paper page
  37. 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 2024, Santa Clara, CA, USA, July 10-12, 2024. USENIX Association, 649-666. https://www.usenix.org/conference/osdi24/presentation/sun-xudong
  38. 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 Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 -22, 2016,
  39. Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 256-270. https://doi.org/10.1145/2837614.2837655 · DOI
  40. 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
  41. 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 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net. https://openreview.net/forum?id=3f5PALef5B
  42. 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=Q3YaCghZNt
  43. each using ChatGPT. CoRR abs/2304.00385 (2023). https://doi.org/10.48550/ARXIV.2304.00385 · DOI
  44. Chenyuan Yang. 2025. Artifact of "AutoVerus: Automated Proof Generation for Rust Code" in OOPSLA 2025. https: //doi.org/10.5281/zenodo.16891950 · DOI
  45. 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.
  46. 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.
  47. 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://proceedings.mlr.press/v97/yang19a.html
  48. 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 Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 -16, 2023. http://papers.nips.cc/paper_files/paper/2023/hash/ 4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_and_Benchmarks.html
  49. 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. https://www.usenix.org/conference/ osdi24/presentation/

Cited by

Sorted by citations

Authors
Yang, C., Li, X., Misu, M. R. H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J. R., Lu, S., Yang, F., Zhou, Z., & Lu, S.
Affiliations
  • University of Illinois Urbana-Champaign (US)
  • Columbia University (US)
  • University of California, Irvine (US)
  • University of Toronto (CA)
  • Microsoft (United States) (US)
  • Microsoft Research Asia (China) (CN)
ORCID
Venue
arXiv
Publisher
arXiv
Published
2024
Volume
9
Issue
OOPSLA2
Pages
3454-3482
ISSN
2475-1421 (ISSN-L)
DOI
10.48550/arxiv.2409.13082
arXiv
2409.13082
OpenAlex
W4415007625
Cited by
20
References
0
Citations by year
2026: 15 · 2025: 5
FWCI
8.09
Type
journal article
Language
en
Open access
Licence
Locations
  • Proceedings of the ACM on Programming Languages (publishedVersion, cc-by)
  • arXiv (Cornell University) (submittedVersion, cc-by)
  • arXiv (Cornell University) (cc-by)
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 › Information Systems › Software Engineering Research
Keywords
proof automation, Rust, Verus, large language models, program verification, multi-agent systems, correctness proofs, benchmark suite

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