Pith. sign in

REVIEW 2 major objections 5 minor 33 references

RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation

T0 review · 2 major / 5 minor · reviewed 2026-08-08 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read RagVerus claims retrieval of cross-module context lifts LLM proof pass rates by 27% on repository-level Verus tasks.

desk verdict RepoVBench is a genuinely useful new benchmark, but the reported RAG gains may be inflated by retrieval of the target's own verified proof, so the empirical claims need an author response before they can be trusted. read the letter →

arxiv 2502.05344 v1 pith:24KG7AMF submitted 2025-02-07 cs.SE cs.AI

Sicheng Zhong , Jiading Zhu , Yifang Tian , Xujie Si This is my paper · ORCID
classification cs.SEcs.AI
keywords retrieval-augmentedgenerationprogramverificationVerusRustproofsynthesisrepository-levelbenchmarkLLMpremiseretrieval
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that the bottleneck for LLM-based formal verification is not proof generation but context selection: in multi-module Rust code verified with Verus, a proof often depends on function signatures and invariants defined in other files. RagVerus addresses this by retrieving few-shot examples and dependency-relevant functions from a vector index built over code and informalized summaries, then feeding that context to a proof-generation agent with verifier feedback. To measure the approach, the authors build RepoVBench, the first repository-level Verus benchmark, derived from the VeriSMo security module and consisting of 383 proof-completion tasks (52 dependency-free, 331 dependency-heavy). On RepoVBench, RagVerus solves 75 of 383 tasks versus 59 for the AutoVerus refinement baseline—a 27% relative improvement—and on the function-level VerusBench it triples the success rate of direct generation at a five-sample budget.

What carries the argument

The central mechanism is the retrieval module, split into few-shot example retrieval and dependency retrieval. Few-shot retrieval indexes both raw Rust code and informalized natural-language summaries of function behavior, then returns the most semantically similar verified example proofs so the model inherits in-distribution proof style; dependency retrieval uses FAISS nearest-neighbor search on the same embeddings to surface function signatures that may serve as premises. The paper sketches two further dependency methods—finetuned projection matching and compiler-derived dependency graphs—but leaves both untested in the evaluation. Context assembled from these retrievals is fed to a proof-generation agent, and Verus compiler feedback drives iterative refinement.

What would settle it

Re-run the RepoVBench complex tasks with dependency retrieval replaced by a compiler-derived dependency graph. If that deterministic method does not match or exceed the 52-task success counted for embedding-based retrieval, then semantic similarity is doing the work; if it does, the paper's 27% gain may simply reflect dependency coverage rather than learned similarity.

Watch

Extended reading notes

Core claim

The paper's central claim is that augmenting an LLM proof generator with retrieval from the target repository—rather than presenting the target function in isolation—is what enables progress on repository-level verification. The RagVerus pipeline statically mines function signatures, module dependencies, and verification metadata; indexes code and informalized summaries as embeddings; retrieves the top-k similar verified examples and candidate premise signatures; and then lets a generic agent such as AutoVerus synthesize proof annotations, with Verus compiler errors fed back for repair. On RepoVBench, this context-aware setup reaches 75 successful tasks (19.6%) versus 59 (15.4%) for refinement without retrieval, and on VerusBench it reaches 84 successes (60.4%) at five samples compared to 25 (18.0%) for direct generation. The paper also establishes RepoVBench as a reusable evaluation set: 383 tasks filtered so the Verus compiler cannot solve them without manually written proof bodies.

Load-bearing premise

The load-bearing premise is that embedding similarity between a target function and other functions reliably identifies the proof-relevant premises; if similar code is not the same as premise-relevant code in larger or differently structured repositories, the reported 27% gain may not transfer.

Editorial extensions

If this is right

  • Because five-sample RagVerus surpasses the 125-sample original baseline on VerusBench, retrieval buys sample efficiency rather than merely final accuracy.
  • RepoVBench gives future work a stable 383-task evaluation with a 52/331 simple/complex split, so repository-level methods can be compared on dependency handling.
  • The 331-task complex subset remains largely unsolved (under 16% for the best RAG setup), implying retrieval and generation both need further progress before repository-level verification is practical.
  • The safety metric—implementation lines unaltered—shows RAG helps prove the original code rather than rewriting it, since safe counts stay comparable across settings.
  • Retrieval from the same repository gives the largest jump on dependency-free tasks (from 13.5% to 44.2% success), indicating in-distribution examples carry most of the benefit.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the embedding-similarity premise fails on repositories with different idioms, the 27% gain may not transfer; the compiler-derived dependency graph the paper sketches is the natural untested control.
  • The same retrieve-then-generate pipeline should apply to specification inference and code generation in Verus, since the framework's generation stage is agnostic to the task.
  • The informalization index outperformed the code index on Diffy tasks, so natural-language summaries may carry semantic cues that raw code misses; RepoVBench, where only the code index was evaluated, is a ready testbed for that hypothesis.
  • RepoVBench's filtering of auto-solvable tasks means it measures proof-completion difficulty rather than raw verification difficulty, so future expansions should preserve that filter to keep comparisons meaningful.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper proposes RagVerus, a retrieval-augmented generation framework for automating Verus proof synthesis in multi-module Rust repositories, and introduces RepoVBench, a repository-level benchmark built from the VeriSMo project. The framework retrieves few-shot examples and dependency-related premises from a codebase and feeds them into an LLM-based proof-generation pipeline. Evaluations report a 27% relative improvement over an AutoVerus refinement baseline on RepoVBench and roughly a tripling of proof pass rates on the function-level VerusBench under constrained sampling budgets. The paper also describes several retrieval strategies, but only embedding-based retrieval is evaluated.

Significance. If the reported results hold, the paper would make a useful contribution by demonstrating that retrieval-augmented context selection can materially improve LLM-based proof synthesis at the repository level, and by providing a benchmark (RepoVBench) that captures cross-module dependencies. The use of an external verifier (Verus) as the success criterion is a strength, and the authors honestly acknowledge some limitations, such as the single-project benchmark and the simplification of masking one function at a time. However, the empirical claims rest on a single unreleased dataset and an underspecified retrieval pipeline, and the possibility that the target's ground-truth proof is included in the retrieved few-shot examples is not explicitly ruled out. The lack of released code, data, seed reporting, and variance statistics makes the headline numbers difficult to assess independently.

major comments (2)
  1. [3.2 and 5.2] The paper must explicitly rule out a retrieval leak of the ground-truth proof. Section 3.2 states that 'the embeddings are built only with unverified files, but during retrieval, the corresponding verified files are also retrieved, forming input-output pairs as few-shot examples.' For a RepoVBench task, the query is the masked (unverified) function, and its verified counterpart contains the exact proof lines that the model is asked to synthesize. The ID filter described in Section 3.2 excludes only 'the input document itself.' If the input document is the masked function and the index is at function granularity, the exclusion may suffice; but if the query is a different object than the indexed document (e.g., a whole file or module, or if the index contains both unverified and verified documents), the verified target could be retrieved. The paper does not specify the document granularity or confirm that the query's verified counterpart is excluded by construction. Because the reported gains on Simple tasks (21 vs. 4) and the 27% relative improvement could largely be explained by copying a retrieved ground-truth proof, this issue is load-bearing. The authors should clarify the exact retrieval index construction for RepoVBench, state whether the target's verified file is ever in the candidate pool, and, if necessary, rerun the experiments with an explicit exclusion of the target's verified document.
  2. [Appendix B / Reproducibility] The paper does not release the RepoVBench dataset, the task-creation scripts, the retrieval index, or the exact prompts used. For a paper whose main contributions include a new benchmark and a framework, this is a major reproducibility gap. The authors should commit to releasing the benchmark construction pipeline, the embedding index configuration, and the evaluation code, ideally before publication.
minor comments (5)
  1. [Throughout] There are numerous typos and grammatical errors, for example 'furthur evaluatiosn' in the introduction, 'we identifying' in Section 3.1, 'varifiable' in Section 4.2, and 'overexec' in Section 4.1. A careful proofreading pass is needed.
  2. [Table 2] The 'Overall' row includes both Simple and Complex tasks, but the paper's discussion and Appendix C refer to 'Complex' results computed by subtraction. It would be clearer to show the Complex row explicitly in Table 2.
  3. [4.3 and Appendix C] The BLEU scores in Table 3 are reported only in the appendix, while the main text only mentions the possibility of reporting BLEU. Consider moving the BLEU results into the main evaluation section, or at least referencing Table 3 explicitly in Section 5.2.
  4. [3.2] The three dependency retrieval methods (embedding-based, finetuned projection, dependency graph) are described, but only embedding-based retrieval is evaluated. The paper should make clear in Section 5 that the finetuned projection and dependency graph methods are future work and are not part of the reported results.
  5. [2 and 6] The related work discussion is brief and omits some relevant recent work on retrieval-augmented code generation and verification, such as RepoFusion and similar retrieval-based code models. The authors should expand the comparison to position RepoVBench and RagVerus more precisely.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the empirical claims are checked by an external verifier and the few-shot pool is described as excluding the query's own document.

full rationale

RagVerus is an empirical systems paper whose success criterion is an external checker (the Verus compiler, with safety checked by AutoVerus's Lynette checker), not a quantity fitted from the target outputs. RepoVBench is constructed from the externally developed VeriSMo project by erasing proof lines from verified functions; ground truth is the pre-existing verified code. The retrieval index is described as built from unverified files, and the ID filter excludes 'the input document itself'; verified files are retrieved only as paired outputs of selected examples, so the target's own verified proof is not by construction injected into the prompt. The paper's acknowledged limitations—single-function masking at a time, insufficient premise-pool size, long proofs, and the simplified retrieval setting (§5.2, Appendix C)—are experimental scope limits, not circular steps. Self-citations appear only as background references and do not carry the derivation. Therefore the claimed improvements are not equivalent to their inputs by construction, and no circularity is established.

Assumptions & free parameters 5 free parameters · 5 assumptions · 0 invented entities

The central claims rest on instrumental assumptions about the verification oracle, embedding similarity, and representativeness of the benchmark. No numerical parameters are fitted to the target outcomes; the listed free parameters are experimental choices, such as sampling budgets, temperature, example counts, and embedding model, that affect the reported pass rates. No invented entities are introduced.

free parameters (5)
  • Sampling budget = 5 samples (VerusBench); 3 samples DirectGen/DirectRAG, up to 4 LLM calls Refinement (RepoVBench)
    Success rates depend heavily on how many proof candidates are sampled; the headline 'triples' and 27% relative gains are measured at these specific budgets, not at the 125-invocation budget used in AutoVerus.
  • Few-shot example count = maximum 3
    The framework retains at most three retrieved examples after ranking; no ablation on k is reported, so the effect of this choice on pass rates is unknown.
  • Temperature = 1.0 for stochastic sampling; 0 for greedy baseline
    Temperature controls diversity of sampled proofs and was chosen by the authors; results may shift at other temperatures.
  • Embedding model = OpenAI text-embedding-3-large
    Retrieval quality, and therefore the RAG benefit, depends on this external model; no comparison to other embedders is provided.
  • Retrieved premise count for dependency retrieval = not reported (context-limited maximum)
    Appendix C notes the ground-truth premise pool is larger than the number returned, but the exact cutoff is not specified; this cutoff affects whether proofs can be completed.
assumptions (5)
  • domain assumption Verus compiler and its SMT encoding are a sound and complete oracle for proof correctness.
    The correctness metric treats a Verus compilation pass as ground truth (Section 4.3).
  • domain assumption Semantic embedding similarity between code or informalized summaries is a reliable proxy for proof-relevant premise selection.
    Embedding-based dependency retrieval assumes similar functions can serve as premises (Section 3.2).
  • ad hoc to paper Erasing proof annotations for one function at a time yields tasks representative of repository-level verification.
    Acknowledged simplification in Section 5.2; real repository-level changes may require coordinated edits across many functions.
  • domain assumption GPT-4o with temperature sampling is a representative generator for the conclusions.
    All results use a single model; no other LLMs are tested, so conclusions may not generalize.
  • domain assumption The Lynette checker correctly detects whether implementation lines are unaltered.
    The safety metric relies on this checker from AutoVerus (Section 4.3).

how reviews work

0 comments
Cite this review

Pith. "Pith review of RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation." pith.science (2026). https://pith.science/paper/24KG7AMF

@misc{pith2026250205344,
  author       = {Pith},
  title        = {Pith review of: RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/24KG7AMF}},
  note         = {Machine review of arXiv:2502.05344}
}
read the original abstract

Scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are challenges overlooked by existing function-centric methods. We introduce RagVerus, a framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof synthesis for multi-module repositories, achieving a 27% relative improvement on our novel RepoVBench benchmark -- the first repository-level dataset for Verus with 383 proof completion tasks. RagVerus triples proof pass rates on existing benchmarks under constrained language model budgets, demonstrating a scalable and sample-efficient verification.

Figures

Figures reproduced from arXiv: 2502.05344 by the authors.

Figure 1
Figure 1. Illustration of the RagVerus Framework Pipeline We propose RagVerus, a retrieval-augmented framework for LLM-based program verification, with a special focus on complex Verus projects. The frame￾work modularizes verification task preparation, context retrieval methods, and proof generation models, leveraging repository information and verifier feedback to align domain knowledge. 3.1 The General Pipeline As illustrat… view at source ↗
Figure 2
Figure 2. Illustration of code informalization utility. Dependency Retrieval Dependency retrieval identifies all relevant function signatures within the code repository that should serve as dependent premises for generating proofs for a particular task. A well-chosen premise pool provides essential context, such as file dependencies and variable typing, ensuring accurate and complete proof generation. Understanding premise de… view at source ↗
Figure 3
Figure 3. Examples of code masking and metadata extraction using Verus-adapted tools. (a) an example of an original function and its masked counterpart, where proof annotations are replaced with MASKED_LINE (highlighted in orange); (b) an example of the extracted metadata [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 21 canonical work pages

  1. [1]

    arXiv preprint arXiv:2412.06176 (2024)

    Aggarwal, P., Parno, B., Welleck, S.: Alphaverus: Bootstrapping formally verified code generation through self-improving translation and treefinement. arXiv preprint arXiv:2412.06176 (2024)

    arXiv 2024

  2. [2]

    Advances in neural information processing systems33, 1877–1901 (2020)

    Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J.D., Dhariwal, P., Nee- lakantan, A., Shyam, P., Sastry, G., Askell, A., et al.: Language models are few-shot learners. Advances in neural information processing systems33, 1877–1901 (2020)

    2020

  3. [3]

    arXiv preprint arXiv:2405.01787 (2024)

    Chakraborty, S., Ebner, G., Bhat, S., Fakhoury, S., Fatima, S., Lahiri, S., Swamy, N.: Towards neural synthesis for smt-assisted proof-oriented programming. arXiv preprint arXiv:2405.01787 (2024)

    arXiv 2024

  4. [4]

    arXiv preprint arXiv:2410.15756 (2024)

    Chen, T., Lu, S., Lu, S., Gong, Y., Yang, C., Li, X., Misu, M.R.H., Yu, H., Duan, N., Cheng, P., et al.: Automated proof generation for rust code via self-evolution. arXiv preprint arXiv:2410.15756 (2024)

    arXiv 2024

  5. [5]

    In: International Conference on Computer Aided Verification

    Cho, C., Zhou, Y., Bosamiya, J., Parno, B.: A framework for debugging automated program verification proofs via proof actions. In: International Conference on Computer Aided Verification. pp. 348–361. Springer (2024)

    work page 2024

  6. [6]

    In: International conference on Tools and Algorithms for the Construction and Analysis of Systems

    De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340. Springer (2008)

    2008

  7. [7]

    IEEE Transactions on Big Data7(3), 535–547 (2019)

    Johnson, J., Douze, M., Jégou, H.: Billion-scale similarity search with gpus. IEEE Transactions on Big Data7(3), 535–547 (2019)

    2019

  8. [8]

    arXiv preprint arXiv:2311.07948 (2023)

    Kamath, A., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S.K., Lal, A., Rastogi, A., Roy, S., Sharma, R.: Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948 (2023)

    arXiv 2023

Show all 33 references
  1. [9]

    Formal aspects of computing27(3), 573–609 (2015)

    Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c: A software analysis perspective. Formal aspects of computing27(3), 573–609 (2015)

    2015

  2. [10]

    ACM Transac- tions on Computer Systems (TOCS)32(1), 1–70 (2014)

    Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an os microkernel. ACM Transac- tions on Computer Systems (TOCS)32(1), 1–70 (2014)

    2014

  3. [11]

    In: Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles

    Lattuada, A., Hance, T., Bosamiya, J., Brun, M., Cho, C., LeBlanc, H., Srinivasan, P., Achermann, R., Chajed, T., Hawblitzel, C., et al.: Verus: A practical foundation for systems verification. In: Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles. p...

    2024

  4. [12]

    Proceedings of the ACM on Programming Languages7(OOPSLA1), 286–315 (2023)

    Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., Hawblitzel, C.: Verus: Verifying rust programs using linear ghost types. Proceedings of the ACM on Programming Languages7(OOPSLA1), 286–315 (2023)

    2023

  5. [13]

    In: International conference on logic for programming artificial intelligence and reasoning

    Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: International conference on logic for programming artificial intelligence and reasoning. pp. 348–370. Springer (2010)

    2010

  6. [14]

    Advances in Neural Information Processing Systems 33, 9459–9474 (2020)

    Lewis, P., Perez, E., Piktus, A., Petroni, F., Karpukhin, V., Goyal, N., Küttler, H., Lewis, M., Yih, W.t., Rocktäschel, T., et al.: Retrieval-augmented generation for knowledge-intensive nlp tasks. Advances in Neural Information Processing Systems 33, 9459–9474 (2020)

    2020

  7. [15]

    In: 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23)

    Li, X., Li, X., Qiang, W., Gu, R., Nieh, J.: Spoq: Scaling{Machine-Checkable} systems verification in coq. In: 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23). pp. 851–869 (2023)

    2023

  8. [16]

    In: International Conference on Computer Aided Verification

    Li, Y., Parsert, J., Polgreen, E.: Guiding enumerative program synthesis with large language models. In: International Conference on Computer Aided Verification. pp. 280–301. Springer (2024) 12 S. Zhong et al

    2024

  9. [17]

    arXiv preprint arXiv:2404.09939 (2024)

    Li, Z., Sun, J., Murphy, L., Su, Q., Li, Z., Zhang, X., Yang, K., Si, X.: A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939 (2024)

    2024 arXiv

  10. [18]

    IEEE Transactions on Software Engineering (2024)

    Liao, D., Pan, S., Sun, X., Ren, X., Huang, Q., Xing, Z., Jin, H., Li, Q.: A 3-codgen: A repository-level code generation framework for code reuse with local-aware, global- aware, and third-party-library-aware. IEEE Transactions on Software Engineering (2024)

    2024

  11. [19]

    In: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering

    Liu, J., Chen, Y., Tan, B., Dillig, I., Feng, Y.: Learning contract invariants using reinforcement learning. In: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering. pp. 1–11 (2022)

    2022

  12. [20]

    https://www.llamaindex.ai/, accessed: 2024-11-07

    LlamaIndex: Llamaindex: Build knowledge assistants over your enterprise data. https://www.llamaindex.ai/, accessed: 2024-11-07

    2024

  13. [21]

    Proceedings of the ACM on Software Engineering1(FSE), 812–835 (2024)

    Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards ai-assisted synthesis of verified dafny methods. Proceedings of the ACM on Software Engineering1(FSE), 812–835 (2024)

    2024

  14. [22]

    OpenAI: Hello GPT-4O (2024),https://openai.com/index/hello-gpt-4o/, [Ac- cessed: 2024-11-07]

    2024

  15. [23]

    OpenAI: New embedding models and api updates (2024),https://openai.com/ index/new-embedding-models-and-api-updates/ , accessed: 2025-01-31

    2024

  16. [24]

    In: Proceedings of the 40th International Conference on Machine Learning

    Shrivastava, D., Larochelle, H., Tarlow, D.: Repository-level prompt generation for large language models of code. In: Proceedings of the 40th International Conference on Machine Learning. ICML’23, JMLR.org (2023)

    2023

  17. [25]

    In: Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II 32

    Si, X., Naik, A., Dai, H., Naik, M., Song, L.: Code2inv: A deep learning framework for program verification. In: Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II 32. pp. 151–164. Springer (2020)

    2020

  18. [26]

    In: International Symposium on AI Verification

    Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: Clo sed-loop ver ifiable code generation. In: International Symposium on AI Verification. pp. 134–155. Springer (2024)

    2024

  19. [27]

    In: 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)

    Sun, X., Ma, W., Gu, J.T., Ma, Z., Chajed, T., Howell, J., Lattuada, A., Padon, O., Suresh, L., Szekeres, A., et al.: Anvil: Verifying liveness of cluster manage- ment controllers. In: 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). pp. 649–666 (2024)

    2024

  20. [28]

    In: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering

    Wang, J., Wang, C.: Learning to synthesize relational invariants. In: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering. pp. 1–12 (2022)

    2022

  21. [29]

    In: International Conference on Computer Aided Verification

    Wen, C., Cao, J., Su, J., Xu, Z., Qin, S., He, M., Li, H., Cheung, S.C., Tian, C.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: International Conference on Computer Aided Verification. pp. 302–328. Spri...

    2024

  22. [30]

    arXiv preprint arXiv:2409.13082 (2024)

    Yang, C., Li, X., Misu, M.R.H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J.R., Lu, S., et al.: Autoverus: Automated proof generation for rust code. arXiv preprint arXiv:2409.13082 (2024)

    2024 arXiv

  23. [31]

    Advances in Neural Information Processing Systems36 (2024)

    Yang,K.,Swope,A.,Gu,A.,Chalamala,R.,Song,P.,Yu,S.,Godil,S.,Prenger,R.J., Anandkumar, A.: Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems36 (2024)

    2024

  24. [32]

    arXiv preprint arXiv:2401.07663 (2024)

    Zhang, L., Lu, S., Duan, N.: Selene: Pioneering automated proof in software verification. arXiv preprint arXiv:2401.07663 (2024)

    2024 arXiv

  25. [33]

    In: 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)

    Zhou, Z., Chen, W., Gong, S., Hawblitzel, C., Cui, W., et al.:{VeriSMo}: A verified security module for confidential{VMs}. In: 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). pp. 599–614 (2024) Retrieval Augmented Generation Verifying Rust 13 Ap...

    2024

Pith tools

Reviewed August 8, 2026 · model on record in the stance chip above.