Pith. sign in

REVIEW 2 major objections 5 minor 66 references

HarnessLLM claims that an LLM-driven pipeline can turn a Rust codebase's existing test suite into verification harnesses automatically — extracting 294 scenarios from 9 real-world crates with 94.66 percent precision, generating a harness fo

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-01 05:35 UTC pith:FGOL4VRL

load-bearing objection Useful and concrete LLM pipeline for Kani harness generation with real bug findings, but the preservation metric is weaker—and the arithmetic looser—than the headline claims. the 2 major comments →

arxiv 2607.22161 v1 pith:FGOL4VRL submitted 2026-07-24 cs.SE cs.CR

HarnessLLM: Rust Verification Harness Generation with Large Language Models

Minghua Wang , Yuwei Liu , Lin Huang This is my paper
classification cs.SE cs.CR
keywords Rust verificationverification harness generationlarge language modelsbounded model checkingKanicalling scenario extractionnondeterministic input generationmemory safety
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The paper tries to establish that verification harnesses for Rust — the glue code that lets bounded model checkers like Kani explore a function's behavior — can be generated automatically by large language models, provided the harnesses are derived from the codebase's own test suite rather than written from scratch. The workflow isolates each distinct calling scenario from a test, promotes its constants to parameters so they can be replaced by nondeterministic symbolic inputs, constructs those inputs by walking a type-dependency graph, and then compiles the harness in a loop with Kani, feeding errors back to the LLM. On nine real-world crates the authors report extracting 294 scenarios from 494 tests with 94.66% precision, generating a compiling harness for every one (100% success, averaging 145 seconds), where the existing Autoharness tool managed only 41%; the resulting harnesses uncovered six real memory-safety bugs in a PDF-parsing crate, five already fixed. The authors flag a limitation: the trace-based preservation check instruments only surface Rust functions, so macro-generated code can escape observation.

Core claim

HarnessLLM is presented as the first automated workflow that uses LLMs to generate Rust verification harnesses directly from a codebase's existing test suite, and the claim is that this makes bounded-model-checking of real-world Rust practical. The core discovery is that a test's assertions, together with their data dependencies, can be lifted into 'scenario functions' — with literal constants promoted to parameters — and that feeding those functions nondeterministic arguments, built by recursively composing public type constructors, yields harnesses Kani can compile and check. On nine real-world crates the workflow reports 94.66% precision in extracting 294 scenarios from 494 tests, a 100%

What carries the argument

The scenario function is the load-bearing object: each assert in a test becomes a separate function containing only the statements that feed it, then constants are promoted to parameters so the inputs can later be made nondeterministic. Around that object, two mechanisms carry the argument. First, a type-dependency graph whose nodes are public constructors — including pub structs, pub enums, and trait implementations — is traversed topologically to emit Chain-of-Thought instructions that tell the LLM, section by section, how to construct each nondeterministic argument from Kani primitives; this fits the prompt in the context window and avoids fabricated types. Second, an iterative compile lo

Load-bearing premise

The load-bearing premise is that matching execution traces — logged function entries — between the original test and the extracted scenario function is enough to prove the calling scenario was preserved; the paper itself concedes that instrumentation covers only surface Rust functions and can miss macro-generated code, so identical traces do not guarantee identical semantics.

What would settle it

A direct check: take a function with a known memory-safety bug, run HarnessLLM to get its harness, then mutate the extracted scenario function so a branch condition changes while the logged function-entry trace stays identical; if the harness no longer detects the known bug, the preservation oracle is too weak. A complementary field check: run the pipeline on a crate whose behavior depends heavily on macro-generated code — the authors acknowledge this case is missed — and see whether the reported preservation precision and bug-detection rate degrade.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Harness generation for Kani can be automated end-to-end for real-world Rust crates: 294 of 294 scenarios produced a compiling harness, averaging 145 seconds each, with near-100% success even when the test suite is sparse.
  • The bottleneck Autoharness hits — nondeterministic construction of user-defined and trait-based types — is the part the dependency-graph and CoT instructions solve, closing a 59-point coverage gap.
  • The generated harnesses are practically useful for bug finding: 6 real memory-safety bugs were detected in a PDF-parsing crate, 5 already fixed, including an out-of-bounds access triggered by a nondeterministic slice length.
  • Both design choices are individually load-bearing: removing the CoT nondet-construction guidance cuts first-pass success by 23.1%, and removing the protected error-fix prompt cuts it by 18.7%.
  • Scenario coverage is inherited from the existing test suite; sparse tests reduce the number of distinct scenarios but do not reduce the harness-generation success rate.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Because scenario coverage is inherited from the test suite, the method's practical ceiling is the quality and density of a project's tests; a natural extension — hinted at by the authors' sparse-test experiment — is to pre-augment test suites (e.g., with LLM-generated unit tests or fuzzer drivers) before extraction.
  • The trace-equality oracle is a cheap, reusable proxy for semantic preservation in any LLM code-transformation setting, but its documented blind spot (macro-generated code invisible to surface instrumentation) suggests a concrete testable upgrade: instrument at the MIR or LLVM IR level and re-measure the reported 94.66% precision.
  • The dependency-graph-to-CoT recipe is separable from harness generation: any tool that must build an arbitrary value of a complex type — fuzz drivers, symbolic-execution seeds, API-misuse testers — could reuse this component.
  • A stress test that would sharpen the claims: run the pipeline on trait-heavy or macro-heavy crates, and on crates with only one or two tests per function, where the current dataset of well-tested libraries is least representative.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 5 minor

Summary. HarnessLLM is a four-phase LLM pipeline for generating Kani verification harnesses for Rust libraries from existing test suites. In code analysis the tool identifies panicking/unsafe functions and candidate test cases; in scenario extraction it prompts an LLM to split tests into single-assert scenario-separated functions, promote constants to parameters, and remove unused parameters, then deduplicates by comparing entry-name execution traces; in synthesis it builds a type-constructor dependency graph and Chain-of-Thought instructions for generating nondet arguments; in compilation it iterates with Kani error feedback, protecting the scenario function and external knowledge snippets from modification. The evaluation reports 94.66% preservation precision over 294 scenarios from 9 crates, 100% syntactic harness-generation success within 10 attempts, 145 s average generation time, a 41% success baseline for Autoharness, and six memory-safety bugs in pdf-rs, five confirmed fixed.

Significance. The practical result — that an LLM-assisted workflow can convert developer-written tests into Kani harnesses and find real memory-safety bugs — is valuable and is partly corroborated by the maintainer fixes for five of the six reported bugs. The paper also provides a useful comparison against Autoharness and across four LLMs, and it decomposes the pipeline in a way that is mostly easy to follow. However, the quantitative precision and component-ablation claims rest on a weak trace-equality oracle and on an internally generated scenario set, respectively, so the headline numbers should be interpreted with caution.

major comments (2)
  1. [§3.3, Fig. 5, §4] The preservation oracle records only function names at entry (`#[logfn::logfn(Pre,Debug,fn)]`). Two runs are judged equal when their callee sequences match, even if the extracted scenario function altered arguments, removed a branch, or changed loop counts. The replay test also uses only the original test's literal constants, so a scenario can be 'preserved' on that input while diverging on the nondet inputs the harness later supplies. Since Table 2's 94.66% precision and Table 3's 294 harnesses rest on this check, the central claim is not fully supported. Please strengthen the oracle (log arguments/returns or use differential testing on additional inputs) or explicitly reframe 'preserved' as 'call-sequence-preserved for the replayed constant input' and show that the bug-finding results are robust under that weaker notion.
  2. [§5.3, RQ2] The ablations (SNG vs FULL, SEF vs FULL) are performed on D_scen, the 294 scenario functions produced by HarnessLLM itself. This makes the component analysis circular for the extraction phase: scenarios that failed preservation were already filtered out. The observed differences in @Pass=0 and #Generations therefore do not measure the components' effect on realistic, unfiltered test-derived scenarios. Please run ablations on an independently constructed scenario set (e.g., all scenario-separated functions before the preservation filter, or a sample of developer-written tests) or clearly state this limitation and argue that D_scen is representative.
minor comments (5)
  1. [§1 / Abstract] Typo: '145 seconds seconds' in the introduction; also 'only generated harnesses for only 41%' repeats 'only'.
  2. [Fig. 2] The example function name 'encode_with_array_marco' appears to be a typo for 'encode_with_array_macro'.
  3. [§6, Coverage] The statement that 'the statement coverage can be guaranteed' is too strong: Kani is a bounded model checker with user-supplied unwind bounds, and nondet arguments do not guarantee coverage of all paths within those bounds. Suggest rephrasing to 'the harnesses can exercise diverse inputs within the specified bounds.'
  4. [Table 3] Clarify that '#Generations' is the total number of synthesis-plus-repair attempts per library, not per harness, since the text later says '46 generation attempts' and '1.4 attempts per valid harness'.
  5. [General] The paper does not include an artifact availability statement or link to the tool, prompts, or datasets, which would aid independent reproduction of the results.

Circularity Check

0 steps flagged

No significant circularity; central claims are supported by external evaluation and upstream-confirmed bug fixes.

full rationale

HarnessLLM's central claims are evaluated on external artifacts: 9 crates.io libraries, Kani/Autoharness comparisons, and 6 memory-safety bugs in pdf-rs, 5 of which were fixed by upstream maintainers. The scenario-preservation rate (94.66%) is an internal measurement defined as matching execution traces after replaying with constants from the original tests; the paper does not present a forward prediction that reduces to that measurement by construction. The RQ2 ablations are run on D_scen, the 294 scenario functions HarnessLLM itself extracted, which limits external independence but is not circular: the ablated prompts are compared on the same scenario functions and the outcomes are not fixed by definition. The acknowledged limitation in §6 that instrumentation 'only instruments functions in surface Rust code, potentially missing those generated by macros' weakens the trace-equality oracle as a semantic ground-truth proxy, but that is a validity/coverage concern, not circularity. No load-bearing argument rests on a self-citation: [49] (UnsafeCop) shares authors but is cited only as related work. The upstream-confirmed bug fixes provide an external success criterion that is independent of HarnessLLM's own outputs, so the central derivation chain is self-contained.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 2 invented entities

The method has no learned parameters fitted to a target result, but it depends on several hand-chosen thresholds and on assumptions about the verification toolchain, the fidelity of the scenario-preservation oracle, and the representativeness of the evaluated crates. The invented entities (scenario functions and nondet constructors) are internal code artifacts without direct external evidence.

free parameters (3)
  • LLM temperature = 0
    Fixed to 0 for determinism in all experiments (Section 4); other temperatures may yield different success rates and the reported numbers are contingent on this choice.
  • Iteration limit for compiler feedback = 10
    The 100% final success rate is measured with a cap of 10 LLM-compiler interactions (Section 4); lower caps would produce lower success rates, as shown in Table 3 (@Pass columns).
  • Unwind/slice bounds = LLM-selected per harness (e.g., SLICE_MAX_LEN=10 in Fig. 11)
    Kani requires explicit bounds for loops and slice lengths. The LLM chooses these bounds without a principled method; the paper discusses this as a challenge (Section 6 'Bound Values'). Different bound choices affect which bugs are reachable and whether Kani terminates.
axioms (5)
  • domain assumption Kani's bounded model checking is sound within the given unwind bounds
    The bug-detection results (Table 4) are interpreted as real memory-safety issues found by Kani; this relies on Kani's semantics as an established verifier (Section 2).
  • domain assumption Execution-trace equality is a sufficient oracle for calling-scenario preservation
    The 94.66% precision figure is computed by comparing logfn traces of the scenario function and the original test (Sections 3.3 and 5.2). No independent validation of this oracle is given.
  • domain assumption The 9 selected crates are representative of real-world Rust codebases
    Selection criteria are not stated beyond 'various categories on crates.io' (Section 5.1); generality to a broader population is assumed.
  • domain assumption The error-fix protocol preserves the scenario function verbatim
    The err-fix prompt (Fig. 9b) instructs the LLM to keep the scenario function unchanged ('No touch!'), but there is no mechanism that verifies the LLM did not silently modify it during repair. A modified scenario function would make the harness invalid.
  • domain assumption MIR-based analysis correctly identifies all functions with unsafe blocks or potential panics
    Section 3.2 describes MIR traversal to find target functions; if this analysis misses functions, the harness coverage is incomplete.
invented entities (2)
  • scenario function no independent evidence
    purpose: An intermediate representation capturing a single API calling scenario with promoted constants as parameters; used to drive harness synthesis.
    A new code artifact introduced by the paper. Its validity is supported only by the paper-internal trace-matching oracle, not by any external benchmark.
  • nondet constructor no independent evidence
    purpose: LLM-generated functions that construct nondeterministic values for complex types via public constructors; used to build harness arguments.
    An implementation artifact whose correctness depends on LLM behavior and is validated only indirectly by Kani compilation success.

pith-pipeline@v1.3.0-alltime-deepseek · 21160 in / 13661 out tokens · 126026 ms · 2026-08-01T05:35:31.933126+00:00 · methodology

0 comments
read the original abstract

Rust's ownership model and type system offer strong memory safety guarantees, but unsafe code and runtime panics still present significant risks. Formal verification is essential to ensure memory safety, but developing verification harnesses remains a challenging and manual task. Although large language models (LLMs) have shown strong performance in various code analysis tasks, directly applying them to harness generation often results in inaccurate API invocations, inefficient nondeterministic data generation, and fabricated fixes. In this paper, we present HarnessLLM, an automated workflow that leverages LLMs to generate verification harnesses for Rust code directly from existing test suites. HarnessLLM automatically extracts calling scenarios from test cases, generates nondeterministic arguments based on dependency analysis, and incrementally synthesizes harnesses. It then iteratively refines the harnesses, preserving critical code regions and reporting fabricated types or functions to LLMs for correction. In our evaluation on 9 real-world Rust codebases, HarnessLLM extracted 294 calling scenarios from 494 test cases with 94.66% precision and generated harnesses for all scenarios in an average of 145 seconds each. It outperformed the existing approach, Autoharness, which succeeded on only 41% of those scenarios. Finally, 6 real-world memory safety bugs were detected using the generated harnesses, demonstrating the practical utility of our approach in verification. To our knowledge, this is the first work to use LLMs for generating harnesses aimed at memory safety verification in real-world Rust projects.

Figures

Figures reproduced from arXiv: 2607.22161 by Lin Huang, Minghua Wang, Yuwei Liu.

Figure 1
Figure 1. Figure 1: Architecture of HarnessLLM. type constructors for the parameter types and generates nondet data using them. If these constructors require parameters, the pro￾cess is recursively applied until all required types can be built using Kani’s primitives. During this process, a dependency graph is constructed with each node representing a type constructor (tyf) and edges pointing to the constructors for tyf’s par… view at source ↗
Figure 2
Figure 2. Figure 2: An example of HarnessLLM’s workflow. representing identical invocation scenarios, which should be repre￾sented by scen_encode_array. To prevent redundant work in down￾stream harness generation, we deduplicate scenario-separated test functions so that each distinct invocation scenario is represented only once. This is achieved by instrumenting function entry points in the Rust code to trace execution, runni… view at source ↗
Figure 3
Figure 3. Figure 3: Scenario-separated test function generation prompt. [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Prompt chaining for scenario function generation. [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figure 6
Figure 6. Figure 6: Harness synthesis prompt with detailed nondet type [PITH_FULL_IMAGE:figures/full_fig_p005_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The left is the nondet type generation prompt used in [PITH_FULL_IMAGE:figures/full_fig_p005_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Structure of CoT instructions for LLMs to generate [PITH_FULL_IMAGE:figures/full_fig_p006_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Different prompts designed for error fixing. [PITH_FULL_IMAGE:figures/full_fig_p006_9.png] view at source ↗
Figure 11
Figure 11. Figure 11: The harness for the buggy function, along with its [PITH_FULL_IMAGE:figures/full_fig_p008_11.png] view at source ↗
Figure 10
Figure 10. Figure 10: Buggy function with the dataflow highlighted. [PITH_FULL_IMAGE:figures/full_fig_p008_10.png] view at source ↗
Figure 12
Figure 12. Figure 12: Comparison with Autoharness on 𝐷𝑠𝑐𝑒𝑛. The average generation success rate of Autoharness was 41%, while Har￾nessLLM was 100%. 5.5 RQ4: Alternative Models [PITH_FULL_IMAGE:figures/full_fig_p009_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Comparison of LLMs on generation success rate [PITH_FULL_IMAGE:figures/full_fig_p010_13.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

66 extracted references · 9 linked inside Pith

  1. [1]

    Anthropic. 2025. Claude Sonnet 4. https://docs.anthropic.com/en/docs/about- claude/models/overview#model-comparison-table

    2025

  2. [2]

    Vytautas Astrauskas, Aurel Bílý, Jonáš Fiala, Zachary Grannan, Christoph Math- eja, Peter Müller, Federico Poli, and Alexander J. Summers. 2022. The Prusti Project: Formal Verification for Rust. InNASA Formal Methods, Jyotirmoy V. Desh- mukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing, Cham, 88–108

    2022

  3. [3]

    Yechan Bae, Youngsuk Kim, Ammar Askar, Jungwon Lim, and Taesoo Kim. 2021. Rudra: Finding Memory Safety Bugs in Rust at the Ecosystem Scale. InProceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles(Virtual Event, Germany)(SOSP ’21). Association for Computing Machinery, New York, NY, USA, 84–99. doi:10.1145/3477132.3483570

    arXiv 2021

  4. [4]

    Karthikeyan Bhargavan, Maxime Buyse, Lucas Franceschino, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, and Bas Spitters. 2025. hax: Verifying Security-Critical Rust Software using Multiple Provers. Cryptology ePrint Archive, Paper 2025/142. https://eprint.iacr.org/2025/142

    2025

  5. [5]

    Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin...

    2020

  6. [6]

    Twain Byrnes, Yoshiki Takashima, and Limin Jia. 2024. Automatically Enforcing Rust Trait Properties. InVerification, Model Checking, and Abstract Interpreta- tion, Rayna Dimitrova, Ori Lahav, and Sebastian Wolff (Eds.). Springer Nature Switzerland, Cham, 210–223

    2024

  7. [7]

    Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu K Lahiri, Tao Xie, and Lidong Zhou. 2024. Automated Proof Generation for Rust Code via Self-Evolution. arXiv:2410.15756 [cs.SE] https://arxiv.org/abs/2410. 15756

    arXiv 2024

  8. [9]

    The crates.io Team. 2025. The Rust community’s crate registry. https://crates.io Last accessed Nov. 2025

    2025

  9. [10]

    Mohan Cui, Chengjun Chen, Hui Xu, and Yangfan Zhou. 2023. SafeDrop: De- tecting Memory Deallocation Bugs of Rust Programs via Static Data-flow Anal- ysis.ACM Trans. Softw. Eng. Methodol.32, 4, Article 82 (May 2023), 21 pages. doi:10.1145/3542948

    doi:10.1145/3542948 2023

  10. [11]

    Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. InFormal Meth- ods and Software Engineering, Adrian Riesco and Min Zhang (Eds.). Springer International Publishing, Cham, 90–105

    2022

  11. [12]

    Kani Developers. 2025. Autoharness. https://model-checking.github.io/kani/ reference/experimental/autoharness.html

    2025

  12. [13]

    The Mirai developers. 2025. MIRAI: Rust mid-level IR Abstract Interpreter. https://github.com/facebookexperimental/MIRA Last accessed Nov. 2025

    2025

  13. [14]

    The RVT developers

    "The RVT developers". 2025. "Rust Verification Tools". https://project-oak.github. io/rust-verification-tools/about.html Last accessed Nov. 2025

    2025

  14. [15]

    2019.Verification of Rust Generics, Typestates, and Traits (Master’s thesis)

    Matthias Erdin. 2019.Verification of Rust Generics, Typestates, and Traits (Master’s thesis). Master’s thesis. ETH Z¨urich

    2019

  15. [16]

    Andreas Ermedahl, Christer Sandberg, Jan Gustafsson, Stefan Bygde, and Björn Lisper. 2007. Loop Bound Analysis based on a Combination of Program Slicing, Abstract Interpretation, and Invariant Analysis. In7th International Workshop on Worst-Case Execution Time Analysis (WCET’07) (Open Access Series in Informatics (OASIcs), Vol. 6), Christine Rochange (Ed....

    arXiv 2007

  16. [17]

    Sidong Feng and Chunyang Chen. 2024. Prompting Is All You Need: Automated Android Bug Replay with Large Language Models. InProceedings of the IEEE/ACM 46th International Conference on Software Engineering(Lisbon, Portugal)(ICSE ’24). Association for Computing Machinery, New York, NY, USA, Article 67, 13 pages. doi:10.1145/3597503.3608137

    arXiv 2024

  17. [18]

    Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer

  18. [19]

    Son Ho and Jonathan Protzenko. 2022. Aeneas: Rust verification by functional translation.Proc. ACM Program. Lang.6, ICFP, Article 116 (Aug. 2022), 31 pages. doi:10.1145/3547647

    doi:10.1145/3547647 2022

  19. [20]

    I wouldn’t want my unsafe code to run my pacemaker

    Sandra Höltervennhoff, Philip Klostermeyer, Noah Wöhler, Yasemin Acar, and Sascha Fahl. 2023. "I wouldn’t want my unsafe code to run my pacemaker": an interview study on the use, comprehension, and perceived risks of unsafe rust. InProceedings of the 32nd USENIX Conference on Security Symposium(Anaheim, CA, USA)(SEC ’23). USENIX Association, USA, Article ...

    2023

  20. [21]

    Jianfeng Jiang, Hui Xu, and Yangfan Zhou. 2022. RULF: rust library fuzzing via API dependency graph traversal. InProceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering (ASE ’21). IEEE Press, Melbourne, Australia, 581–592. doi:10.1109/ASE51524.2021.9678813

    arXiv 2022

  21. [22]

    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the foundations of the Rust programming language.Proceed- ings of the ACM on Programming Languages2, POPL (2017), 1–34

    2017

  22. [23]

    Lorch, Oded Padon, and Bryan Parno

    Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Haw- blitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024. Verus: A Practical Foundation for Systems Verification. InProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles(Aus...

    arXiv 2024

  23. [24]

    K Rustan M Leino. 2008. This is boogie 2.manuscript KRML178, 131 (2008), 9

    2008

  24. [25]

    Lahiri, and Siddhartha Sen

    Caroline Lemieux, Jeevana Priya Inala, Shuvendu K. Lahiri, and Siddhartha Sen. 2023. CodaMosa: Escaping Coverage Plateaus in Test Generation with Pre-Trained Large Language Models. InProceedings of the 45th International Conference on Software Engineering (ICSE ’23). IEEE Press, Melbourne, Victoria, Australia, 919–931. doi:10.1109/ICSE48619.2023.00085 Con...

    arXiv 2023

  25. [26]

    Zhuohua Li, Jincheng Wang, Mingshen Sun, and John C.S. Lui. 2021. MirChecker: Detecting Bugs in Rust Programs via Static Analysis. InProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security(Virtual Event, Republic of Korea)(CCS ’21). Association for Computing Machinery, New York, NY, USA, 2183–2196. doi:10.1145/3460120.3484541

    arXiv 2021

  26. [27]

    Jinghua Liu, Yi Yang, Kai Chen, and Miaoqian Lin. 2024. Generating API Parame- ter Security Rules with LLM for API Misuse Detection. arXiv:2409.09288v2 [cs.CR] https://arxiv.org/pdf/2409.09288v2

    Pith/arXiv arXiv 2024

  27. [28]

    The logfn developer. 2025. https://crates.io/crates/logfn Last accessed Nov. 2025

    2025

  28. [29]

    Yunlong Lyu, Yuxuan Xie, Peng Chen, and Hao Chen. 2024. Prompt Fuzzing for Fuzz Driver Generation. InProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security(Salt Lake City, UT, USA)(CCS ’24). Association for Computing Machinery, New York, NY, USA, 3793–3807. doi:10. 1145/3658644.3670396

    arXiv 2024

  29. [30]

    Vikram Nitin, Anne Mulhern, Sanjay Arora, and Baishakhi Ray. 2024. Yuga: Automatically Detecting Lifetime Annotation Bugs in the Rust Language.IEEE Trans. Softw. Eng.50, 10 (Oct. 2024), 2602–2613. doi:10.1109/TSE.2024.3447671

    arXiv 2024

  30. [31]

    OpenAI. 2025. GPT-4.1. https://platform.openai.com/docs/models/gpt-4.1

    2025

  31. [32]

    Diatchki, Robert Dockins, Mike Dodds, Joe Hendrix, Tristan Ravich, Patrick Redmond, Ryan Scott, and Aaron Tomb

    Stuart Pernsteiner, Iavor S. Diatchki, Robert Dockins, Mike Dodds, Joe Hendrix, Tristan Ravich, Patrick Redmond, Ryan Scott, and Aaron Tomb. 2024. Crux, a Precise Verifier for Rust and Other Languages. arXiv:2410.18280 [cs.PL] https: //arxiv.org/abs/2410.18280

    Pith/arXiv arXiv 2024

  32. [33]

    The proptest developers. 2025. Proptest. https://github.com/proptest-rs/proptest Last accessed Nov.2025

    2025

  33. [34]

    Boqin Qin, Yilun Chen, Zeming Yu, Linhai Song, and Yiying Zhang. 2020. Under- standing memory and thread safety practices and issues in real-world Rust pro- grams. InProceedings of the 41st ACM SIGPLAN Conference on Programming Lan- guage Design and Implementation(London, UK)(PLDI 2020). Association for Com- puting Machinery, New York, NY, USA, 763–779. d...

    arXiv 2020

  34. [35]

    Zvonimir Rakamarić and Michael Emmi. 2014. SMACK: Decoupling Source Language Details from Verifier Implementations. InComputer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 106–113

    2014

  35. [36]

    Gabriel Ryan, Siddhartha Jain, Mingyue Shang, Shiqi Wang, Xiaofei Ma, Mu- rali Krishna Ramanathan, and Baishakhi Ray. 2024. Code-Aware Prompting: A Study of Coverage-Guided Test Generation in Regression Setting using LLM. Proc. ACM Softw. Eng.1, FSE, Article 43 (July 2024), 21 pages. doi:10.1145/3643769

    doi:10.1145/3643769 2024

  36. [37]

    Elvis Saravia. 2022. Prompt Engineering Guide

    2022

  37. [38]

    Mohammed Latif Siddiq, Joanna Cecilia Da Silva Santos, Ridwanul Hasan Tanvir, Noshin Ulfat, Fahmid Al Rifat, and Vinícius Carvalho Lopes. 2024. Using Large Language Models to Generate JUnit Tests: An Empirical Study. InProceedings of the 28th International Conference on Evaluation and Assessment in Software Engineering(Salerno, Italy)(EASE ’24). Associati...

    arXiv 2024

  38. [39]

    The Tree sitter developer. 2025. https://github.com/tree-sitter/tree-sitter Last accessed Nov. 2025

    2025

  39. [40]

    Yoshiki Takashima. 2023. PropProof: Free Model-Checking Harnesses from PBT. InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering(San Francisco, CA, USA)(ESEC/FSE 2023). Association for Computing Machinery, New York, NY, USA, 1903–1913. doi:10.1145/3611643.3613863

    arXiv 2023

  40. [41]

    Yutian Tang, Zhijie Liu, Zhichao Zhou, and Xiapu Luo. 2024. ChatGPT vs SBST: A Comparative Assessment of Unit Test Suite Generation.IEEE Trans. Softw. Eng. 50, 6 (June 2024), 1340–1359. doi:10.1109/TSE.2024.3382365

    arXiv 2024

  41. [42]

    The DeepSeek Team. 2025. deepseek-chat. https://api-docs.deepseek.com/

    2025

  42. [43]

    The DeepSeek Team. 2025. deepseek-reasoner. https://api-docs.deepseek.com/

    2025

  43. [44]

    2016.Simple Verification of Rust Programs via Functional Purifi- cation (Master’s thesis)

    Sebastian Ullrich. 2016.Simple Verification of Rust Programs via Functional Purifi- cation (Master’s thesis). Master’s thesis. Fakultät für Informatik

    2016

  44. [45]

    Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, and Adrian Samp- son. 2022. Verifying dynamic trait objects in rust. InProceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice (Pittsburgh, Pennsylvania)(ICSE-SEIP ’22). Association for Computing Machinery, New York, NY, USA, 321–330. doi:10.1145/35...

    arXiv 2022

  45. [46]

    Kani Verifier. 2022. Use Kani action in CI. https://github.com/aws/s2n-quic/pull/ 1556

    2022

  46. [47]

    Kani Verifier. 2023. How Kani helped find bugs in Hifitime. https://model- checking.github.io/kani-verifier-blog/2023/03/31/how-kani-helped-find-bugs- in-hifitime.html

    2023

  47. [48]

    Kani Verifier. 2023. Using Kani to Validate Security Boundaries in AWS Fire- cracker. https://model-checking.github.io/kani-verifier-blog/2023/08/31/using- kani-to-validate-security-boundaries-in-aws-firecracker.html

    2023

  48. [49]

    Minghua Wang, Jingling Xue, Lin Huang, Yuan Zi, and Tao Wei. 2025. UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking. InFormal Methods, Andre Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi (Eds.). Springer Nature Switzerland, Cham, 307–324

    2025

  49. [50]

    Zhao, Kelvin Guu, Adams Wei Yu, Brian Lester, Nan Du, Andrew M

    Jason Wei, Maarten Bosma, Vincent Y. Zhao, Kelvin Guu, Adams Wei Yu, Brian Lester, Nan Du, Andrew M. Dai, and Quoc V. Le. 2022. Finetuned Language Models Are Zero-Shot Learners. arXiv:2109.01652 [cs.CL] https://arxiv.org/abs/ 2109.01652

    Pith/arXiv arXiv 2022

  50. [51]

    Chi, Quoc V

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. 2022. Chain-of-thought prompting elicits reasoning in large language models. InProceedings of the 36th International Conference on Neural Information Processing Systems(New Orleans, LA, USA) (NIPS ’22). Curran Associates Inc., Red Hook, NY...

    2022

  51. [52]

    Yifan Wu, Ying Li, and Siyu Yu. 2024. Commit Message Generation via Chat- GPT: How Far Are We?. InProceedings of the 2024 IEEE/ACM First International Conference on AI Foundation Models and Software Engineering(Lisbon, Portugal) (FORGE ’24). Association for Computing Machinery, New York, NY, USA, 124–129. doi:10.1145/3650105.3652300

    arXiv 2024

  52. [53]

    Zhang, and Yong Liu

    Yonghao Wu, Zheng Li, Jie M. Zhang, and Yong Liu. 2024. ConDefects: A Com- plementary Dataset to Address the Data Leakage Concern for LLM-Based Fault Localization and Program Repair. InCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering(Porto de Galinhas, Brazil)(FSE 2024). Association for Computing Ma...

    arXiv 2024

  53. [54]

    Hui Xu, Zhuangbin Chen, Mingshen Sun, Yangfan Zhou, and Michael R. Lyu

  54. [55]

    Hanxiang Xu, Wei Ma, Ting Zhou, Yanjie Zhao, Kai Chen, Qiang Hu, Yang Liu, and Haoyu Wang. 2024. CKGFuzzer: LLM-Based Fuzz Driver Generation Enhanced By Code Knowledge Graph. arXiv:2411.11532 [cs.SE] https://arxiv.org/abs/2411. 11532

    Pith/arXiv arXiv 2024

  55. [56]

    Zhiwu Xu, Bohao Wu, Cheng Wen, Bin Zhang, Shengchao Qin, and Mengda He

  56. [57]

    Chenyuan Yang, Yinlin Deng, Runyu Lu, Jiayi Yao, Jiawei Liu, Reyhaneh Jab- barvand, and Lingming Zhang. 2024. WhiteFox: White-Box Compiler Fuzzing Empowered by Large Language Models.Proc. ACM Program. Lang.8, OOPSLA2, Article 296 (Oct. 2024), 27 pages. doi:10.1145/3689736

    doi:10.1145/3689736 2024

  57. [58]

    Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu

    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. 2025. AutoVerus: Automated Proof Generation for Rust Code. arXiv:2409.13082 [cs.SE] https://arxiv.org/abs/2409.13082

    Pith/arXiv arXiv 2025

  58. [59]

    InProceedings of the IEEE/ACM 46th International Conference on Software Engineering(Lisbon, Portugal)(ICSE ’24)

    RPG: Rust Library Fuzzing with Pool-based Fuzz Target Generation and Generic Support. InProceedings of the IEEE/ACM 46th International Conference on Software Engineering(Lisbon, Portugal)(ICSE ’24). Association for Computing Machinery, New York, NY, USA, Article 124, 13 pages. doi:10.1145/3597503. 3639102

    doi:10.1145/3597503

  59. [60]

    Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. 2023. ReAct: Synergizing Reasoning and Acting in Language Models. arXiv:2210.03629 [cs.CL] https://arxiv.org/abs/2210.03629

    Pith/arXiv arXiv 2023

  60. [61]

    Jiahao Yu, Xingwei Lin, Zheng Yu, and Xinyu Xing. 2024. GPTFUZZER: Red Teaming Large Language Models with Auto-Generated Jailbreak Prompts. arXiv:2309.10253 [cs.AI] https://arxiv.org/abs/2309.10253

    Pith/arXiv arXiv 2024

  61. [62]

    Jianan Yao, Ziqiao Zhou, Weiteng Chen, and Weidong Cui. 2023. Leveraging Large Language Models for Automated Proof Synthesis in Rust. arXiv:2311.03739 [cs.FL] https://arxiv.org/abs/2311.03739

    Pith/arXiv arXiv 2023

  62. [63]

    Sacha Élie Ayoun, Xavier Denis, Petar Maksimović, and Philippa Gardner. 2025. A hybrid approach to semi-automated Rust verification. arXiv:2403.15122 [cs.PL] https://arxiv.org/abs/2403.15122

    Pith/arXiv arXiv 2025

  63. [65]

    Ying Zhang, Peng Li, Yu Ding, Lingxiang Wang, Dan Williams, and Na Meng

  64. [66]

    In Proceedings of the 46th International Conference on Software Engineering: Software Engineering in Practice(Lisbon, Portugal)(ICSE-SEIP ’24)

    Broadly Enabling KLEE to Effortlessly Find Unrecoverable Errors in Rust. In Proceedings of the 46th International Conference on Software Engineering: Software Engineering in Practice(Lisbon, Portugal)(ICSE-SEIP ’24). Association for Com- puting Machinery, New York, NY, USA, 441–451. doi:10.1145/3639477.3639714

    arXiv

  65. [2021]

    Memory-Safety Challenge Considered Solved? An In-Depth Study with All Rust CVEs.ACM Trans. Softw. Eng. Methodol.31, 1, Article 3 (Sept. 2021), 25 pages. doi:10.1145/3466642

    doi:10.1145/3466642 2021

  66. [2024]

    ACM Program

    RefinedRust: A Type System for High-Assurance Verification of Rust Programs.Proc. ACM Program. Lang.8, PLDI, Article 192 (June 2024), 25 pages. doi:10.1145/3656422

    doi:10.1145/3656422 2024