Pith. sign in

REVIEW 3 major objections 5 minor 38 references

KaPilot claims that a documentation-grounded, multi-agent LLM pipeline can generate Kani specifications for most unsafe Rust functions, reporting 88.9% success on a 54-function benchmark and 57.4% of outputs semantically equivalent to or st

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 06:13 UTC pith:22GIY4WN

load-bearing objection KaPilot is a workmanlike, honestly-evaluated LLM pipeline for Kani spec generation; the 88.9% pass rate is weaker than it looks, and the number to watch is 57.4% genuinely good specs. the 3 major comments →

arxiv 2607.21957 v1 pith:22GIY4WN submitted 2026-07-24 cs.SE cs.CR

KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification

Minghua Wang , Yuxi Ling , Mingzhi Gao , Yuwei Liu , Lin Huang This is my paper
classification cs.SE cs.CR
keywords unsafe RustKaniLLM specification generationmemory safetybounded model checkingmulti-agent LLM pipelineformal verificationfunction contracts
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.

This paper tries to show that writing formal memory-safety specifications for unsafe Rust—traditionally a manual, expert-only task—can be largely automated by a multi-agent LLM pipeline called KaPilot. The key bet is that the safety-relevant facts live in the function's documentation, not its implementation, so the pipeline deliberately hides the source code from the spec-writing agent and instead feeds it a distilled list of documented safety requirements. Those requirements guide a generate–precheck–verify loop in which an LLM drafts Kani contracts, a second agent checks them against the requirement list, and Kani (a bounded model checker for Rust) either confirms them or returns counterexamples. A final shuffle-and-implication step recombines preconditions, postconditions, and loop invariants across verified candidates to pick the weakest-precondition/strongest-postcondition combination. On 54 functions with human-written ground truth, KaPilot reports 88.9% generation success and 57.4% of outputs semantically equivalent to or stronger than the ground truth, roughly 15 and 26 percentage points better on those two metrics than a code-centric baseline.

Core claim

The paper's central claim is that grounding specification generation in documentation-derived safety requirements—rather than in source code—lets LLMs produce Kani contracts for unsafe Rust that are both verifiable and semantically faithful. The authors argue that safety properties are usually hidden in natural-language docs, while code-centric generation inherits implementation flaws. They demonstrate this through KaPilot: SafetyReq extracts atomic, traceable safety requirements from docs; SpecGenerate writes contracts without seeing the implementation; SpecPrecheck filters weak or incomplete drafts; SpecVerify runs Kani with vacuity checks; and shuffle-and-implication selects the best veri

What carries the argument

The load-bearing machinery is the documentation-grounded safety-requirement list plus the shuffle-and-implication selection strategy. The safety-requirement list is a concise, atomic, source-traceable inventory of every memory-safety and panic constraint mentioned in the function's docs and cross-references; it converts unstructured prose into a stable target that SpecGenerate must satisfy. The shuffle-and-implication strategy takes the set of verified candidate specifications (each a precondition, postcondition, and loop invariant), ranks preconditions from weakest to strongest and postconditions from strongest to weakest, and uses Kani to test combinations—including conjoined loop invarian

Load-bearing premise

The whole pipeline assumes the function's documentation—Safety and Panics sections plus cross-references—contains every safety-relevant constraint; if a required property is missing from the docs, the generated specification can pass Kani and still miss a real memory-safety violation.

What would settle it

Take a set of unsafe Rust functions whose documentation has a known safety-relevant omission (for example, a missing Panics condition or an unwritten in-bounds requirement), run the full pipeline, and check whether the generated specification both passes Kani and fails to prove the omitted property—if it does, the documentation-completeness assumption is violated and the claimed 88.9% success rate would drop on that set.

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

If this is right

  • If correct, unsafe-Rust memory-safety verification can scale beyond hand-written specs, since documentation already exists for most public functions.
  • Deliberately withholding source code from the spec generator reduces the risk of inheriting implementation bugs in preconditions and postconditions.
  • The vacuity check (appending a deliberately false ensures clause) gives an automated way to catch contradictory preconditions that would otherwise pass verification vacuously.
  • The shuffle-and-implication selection can recover a correct contract from a set of individually imperfect candidates, removing the need to restart generation from scratch.
  • The documented pipeline transfers to other contract-based verifiers beyond Kani, as long as they support preconditions, postconditions, and loop invariants.

Where Pith is reading between the lines

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

  • Editorial inference: the pipeline's ceiling is documentation quality—if a required safety property is missing from the docs, the generated spec can pass Kani yet miss a real memory-safety violation; the authors acknowledge this dependence but do not quantify how much it bounds the headline success rates.
  • A testable extension would be to run the pipeline on deliberately underdocumented functions and check whether the generated spec admits undefined behavior that Kani would catch with a stronger spec; if so, documentation completeness is the binding constraint.
  • Because the spec-writing agent never sees the implementation, the intermediate safety-requirement lists double as auditable natural-language artifacts that human reviewers or other tools could consume independently.
  • The shuffle-and-implication idea is not limited to LLMs: any pool of verified-but-incomplete Hoare-triple candidates could be recombined by implication checking to recover a stronger overall contract.

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

3 major / 5 minor

Summary. The paper presents KaPilot, a multi-agent LLM pipeline that automatically generates Kani specifications (preconditions, postconditions, loop invariants) for unsafe Rust functions. The pipeline extracts safety requirements from documentation via SafetyReq, generates candidate specifications via SpecGenerate, refines them through a generate–precheck–verify loop involving SpecPrecheck and SpecVerify, and finally selects the best candidate using a shuffle-and-implication strategy. The evaluation covers 54 unsafe Rust functions with ground truth (GoldSet) and 70 without (ULSet), reporting 88.9% and 71.4% Kani-pass rates respectively, with 57.4% of GoldSet specifications judged semantically equivalent to or stronger than ground truth, and reporting improvements over an AutoSpec baseline adapted to Kani. The central claim is that documentation-grounded multi-agent LLM pipelines can automate most unsafe-Rust specification writing well enough to be practically useful.

Significance. If the results hold, KaPilot is a meaningful step forward: it demonstrates that an LLM-based multi-agent pipeline can produce non-vacuous, Kani-verifiable contracts for a nontrivial set of standard-library unsafe functions, with ablations isolating the contribution of each agent and inter-rater agreement supporting the qualitative labels. The use of an external ground-truth source (verify-rust-std), the verifier anchor (Kani), and the public artifact are clear strengths. However, the significance is bounded by two caveats that the paper itself partly discloses: Kani pass is a bounded-verification result and does not certify memory safety independently of the documentation-derived requirements, and the ULSet success rates are pass rates rather than quality rates. These caveats do not eliminate the practical value, but they must be reflected in the central claims.

major comments (3)
  1. [§3.3–§3.4 and §5] The central validity of the results is conditional on documentation completeness. SafetyReq is constrained to the Safety/Panics sections plus cross-references, and SpecGenerate is deliberately withheld from the source code (§3.4). Kani pass only proves that the implementation satisfies the generated specification; it does not prove that the specification entails the intended memory-safety properties. If a constraint is missing or ambiguous in the documentation, neither SafetyReq nor SpecPrecheck can recover it, and Kani will still pass. The paper concedes this in §5 ('Poor documentation may lead to missing or underspecified constraints') and attributes the higher ULSet failure rate in §4.1 to lower-quality descriptions. The headline 88.9% and 57.4% rates therefore describe generation of verifiable specifications of documented requirements, not verified memory-safety coverage. An independ
  2. [§3.7, Algorithm 1] The shuffle-and-implication algorithm as printed does not implement the exhaustive search the text claims. The inner loop over postconditions exits with j=M and Q empty, and j is not reset in the outer loop; therefore only the first selected weakest precondition is ever paired with postconditions, and later preconditions are never combined with any Q. The statement that the two-layer loop covers all combinations whenever M≥|SP| is therefore false. The selection criteria at lines 4 and 8 are also not the standard weakest-precondition/strongest-postcondition definitions: the disjunction (p_m⇒p_k)∨(p_k⇏p_m) is satisfied by incomparable predicates and does not identify a unique weakest element. Please correct the pseudocode or specify the actual search procedure, and confirm that the implementation matches the corrected version.
  3. [§4.1, Table 3; Abstract] The term 'specification generation success' conflates Kani-verifiability with specification quality. On ULSet there is no ground truth and no good/bad classification, so the 71.4% pass rate is not evidence that the specifications are correct. On GoldSet, good/bad labels come from the two co-authors' blind review; the reported Cohen's κ (0.81–0.95) demonstrates inter-rater consistency, not validity against an independent oracle. Because Table 3 counts bad specifications as Pass (e.g., 17 bad for GPT-5), the 88.9% is a bounded-verifiability rate: Kani pass is subject to unwind and harness bounds (§5), not a safety proof. The abstract and conclusion should use qualified wording (e.g., 'Kani-verifiable' and 'manually judged good or better'), and the paper should state the bounded nature in the headline results.
minor comments (5)
  1. [§3.3] The sentence 'or encoded implicitly as behavioural constraints rather than explicitly stated in Safety or Panics sections' appears twice in almost identical form; remove the duplicate.
  2. [§4.2, Table 6] The 'Surpass' row is hard to interpret because the percentages are given with mixed signs and no explicit baseline; specify for each column whether the delta is relative to AutoSpec's count and what 'Surpass' means.
  3. [§4.4, Case Study 2] The text says 'Fig. 6 shows the safety requirement list' but the referenced listing appears to be Fig. 8; check the cross-reference.
  4. [§4.1, Table 5] The model name is given as 'Claude-4-Sonnet' in the text and 'Claude-Sonnet-4' in the table; standardize the spelling.
  5. [§5] The heading 'Why comparing with AutoSpec' is ungrammatical; 'Why We Compare with AutoSpec' is clearer.

Circularity Check

0 steps flagged

No central circularity: external Kani and verify-rust-std ground truth anchor the claims; residual limitation is documentation completeness, not circularity.

full rationale

KaPilot's derivation chain is: docs -> SafetyReq list -> SpecGenerate -> SpecPrecheck -> SpecVerify (Kani) -> candidate set -> shuffle-and-implication -> final spec. The headline empirical claims are anchored externally rather than by construction. The 88.9% GoldSet and 71.4% ULSet success rates are Kani-verifiability results, and Kani is an independent bounded model checker. The 57.4% 'equivalent-or-stronger' rate is determined by manual comparison against human-written verify-rust-std ground truth ([11]), with reported inter-rater agreement (Cohen's kappa 0.81-0.95), not against KaPilot's own SafetyReq output. SpecPrecheck does check coverage and strength relative to the SafetyReq list, so it would not independently catch a systematic LLM misreading of documentation; however, this is a quality-assurance limitation, and the paper explicitly concedes it in Sec. 5: 'Poor documentation may lead to missing or underspecified constraints.' That is a threat-to-validity assumption, not a by-construction equivalence. The shuffle-and-implication strategy selects weakest preconditions/strongest postconditions and re-verifies the combined candidate in Kani, so the selection is not accepted merely by definition. The only self-citations ([32] artifact, [33] UnsafeCop related work) appear in data-availability/related-work context and are not load-bearing; no uniqueness theorem or ansatz is imported from the authors' prior work. No specific prediction is fitted to the data it claims to predict. Residual circularity is therefore minor and non-central.

Axiom & Free-Parameter Ledger

4 free parameters · 6 axioms · 0 invented entities

The central claims rest on engineering hyperparameters (thresholds, iteration limits, unwind bounds), on the soundness of Kani's bounded checking, and on documentation completeness. No free physical constants or fitted scientific parameters are involved; the free parameters listed are hand-set system thresholds that affect reported success rates.

free parameters (4)
  • SafetyReq acceptance threshold = 6 (harmonic-mean rule score)
    Hand-chosen threshold for accepting generated safety-requirement lists; higher/lower changes which requirements are passed to spec generation. §3.3.
  • SpecPrecheck quality threshold = 6 on 1–10 scale
    Hand-chosen cutoff for precheck score; affects how many refinement iterations occur. §3.5.
  • Iteration limits and candidate counts = SafetyReq 3, SpecGenerate–SpecPrecheck 5, SpecVerify 3, shuffle M=2, candidates 2
    Hand-chosen caps on agent loops and candidate counts; these directly bound how much repair occurs and which combinations are tried. §3.3, §3.5, §3.6, §3.7.
  • Kani unwind/harness bounds = e.g., #[kani::unwind(33)], MAX_SIZE=32; bounded unwind when full unwinding is costly
    Bounded-model-checking parameters determine which programs count as 'verified'; a pass is only a proof up to the bound. §2.2, §4.1.
axioms (6)
  • domain assumption Kani's contract checking is a sound formal verification of the checked properties within the given unwind bounds.
    The whole pipeline treats Kani verification success as evidence that the specification is satisfied. §2.2, §3.6.
  • domain assumption Documentation (Safety/Panics sections plus cross-references) contains all safety requirements relevant to the target function.
    SpecGenerate is deliberately given metadata, not source code; SafetyReq is restricted to doc sources. §3.3, §3.4. If false, specs may be incomplete yet labeled good.
  • domain assumption Two co-authors' manual blind labeling reliably distinguishes good from bad specifications relative to ground truth.
    The good/bad categorization that underlies all headline rates is human judgment, not an automated oracle. §4.1, Table 2.
  • domain assumption The adapted AutoSpec baseline faithfully represents the original AutoSpec pipeline.
    AutoSpec was re-implemented/adapted from Frama-C to Kani with prompt and API changes; the comparison depends on this adaptation being fair. §4.2.
  • ad hoc to paper The invariant candidates (i_w, i_s, i_w∧i_s) suffice to find a correct loop invariant.
    The shuffle-and-implication loop tests only these three invariant forms; the paper argues heuristically and admits P'_1 etc. are not actually derived. §3.7.
  • domain assumption LLM outputs (safety req lists, specs, precheck scores) are reliable enough after iterative refinement.
    LLM nondeterminism and hallucination are mitigated by loops but not eliminated. §3.3-§3.6.

pith-pipeline@v1.3.0-alltime-deepseek · 22490 in / 15391 out tokens · 151702 ms · 2026-08-01T06:13:28.407532+00:00 · methodology

0 comments
read the original abstract

Rust's ownership and type system provide strong memory safety guarantees, but unsafe code still presents memory safety risks. Formal verification is crucial for ensuring memory safety, but writing precise specifications for unsafe Rust is challenging and largely manual. Large language models (LLMs) have shown promise in generating formal specifications but are often code-centric, prone to inheriting implementation flaws, and lack systematic quality assessment. In this paper, we present KaPilot, a multi-agent framework for automatically generating specifications to verify unsafe Rust memory safety using Kani. The process begins with lightweight program analysis and proof harness generation. The SafetyReq agent extracts a concise, refined list of safety requirements from the target Rust function's documentation, which guides the SpecGenerate agent in producing initial specifications that specify memory safety concerns. Then, the specifications are iteratively refined through a generate-precheck-verify loop involving SpecGenerate, SpecPrecheck, and SpecVerify agents, which assess quality and feed errors back. By executing this loop multiple times, KaPilot generates a set of candidate specifications. Finally, the shuffle-and-implication strategy is applied to systematically determine the best specification from these candidates. We evaluated KaPilot on 54 unsafe Rust functions with ground truth and 70 without. KaPilot achieved 88.9% and 71.4% specification generation success, respectively, with 57.4% of generated specifications equivalent to or stronger than the ground truth. Compared with AutoSpec, KaPilot produces 14.8% more verifiable specifications and 25.9% more equivalent-or-better specifications.

Figures

Figures reproduced from arXiv: 2607.21957 by Lin Huang, Minghua Wang, Mingzhi Gao, Yuwei Liu, Yuxi Ling.

Figure 1
Figure 1. Figure 1: An unsafe function from the Rust standard library and its Kani verification [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The pipeline of KaPilot. using Kani primitives (details in Sec. 3.4). Before sending it to Kani to verify, KaPilot performs a precheck in SpecPrecheck to eliminate simple syntax errors and check whether it covers all mentioned safety requirements. If the specification gets a low score, it would be fed back to SpecGenerate for refinement. KaPilot repeats this step till it reaches the maximum iterations or p… view at source ↗
Figure 3
Figure 3. Figure 3: An example of safety requirements extraction in [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Examples of good and bad postconditions: KaPilot-generated (left) vs. ground truth (right) [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Invocation times of KaPilot compo￾nents. Money Costs. Tab. 5 shows the money and token cost on GoldSet and ULSet using different LLM models. At the time of our experiments, the cost per 1 million input (output) tokens is $1.25 ($10) for GPT-5, $0.29 ($1.14) for DeepSeek-v3.2, and $3 ($15) for the Claude-4-Sonnet. DeepSeek-v3.2 incurred the lowest overall cost due to its very low per-token price. Claude-4-S… view at source ↗
Figure 6
Figure 6. Figure 6: offset’s description (left) and SafetyReq-generated safety requirement list (right). #[kani::requires({ let stride = crate::mem::size_of::<T>(); let abs_count = count.unsigned_abs() as usize; abs_count.checked_mul(stride).map_or(false, |bytes| bytes <= isize::MAX as usize) })] #[kani::requires({ let stride = core::mem::size_of::<T>(); if stride == 0 { true } else { let abs = if count >= 0 { count as usize … view at source ↗
Figure 7
Figure 7. Figure 7: Preconditions generated by AutoSpec (left) and [PITH_FULL_IMAGE:figures/full_fig_p017_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Specifications generated for as_flattened based on the safety requirements. The prefixes "-" and "+" denote, respectively, an incorrect precondition generated first and a correct one generated after correction. this new postcondition is incorrectly verified as true, signaling the presence of vacuity. Using this mechanism, KaPilot identifies the flawed precondition and feeds explicit feedback to SpecGenerat… 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

38 extracted references · 4 canonical work pages

  1. [1]

    Pranjal Aggarwal, Bryan Parno, and Sean Welleck. 2024. AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement. arXiv:2412.06176 [cs.LG] https://arxiv.org/abs/2412.06176

    Pith/arXiv arXiv 2024

  2. [2]

    Sacha-Élie Ayoun, Xavier Denis, Petar Maksimović, and Philippa Gardner. 2025. A hybrid approach to semi-automated Rust verification. Proceedings of the ACM on Programming Languages9, PLDI (2025), 970–992. doi:10.5281/zenodo.15183201

    work page doi:10.5281/zenodo.15183201 2025

  3. [3]

    Sarmad Bashir, Alessio Ferrari, Abbas Khan, Per Erik Strandberg, Zulqarnain Haider, Mehrdad Saadatmand, and Markus Bohlin. 2025. Requirements ambiguity detection and explanation with llms: An industrial study. In2025 IEEE International Conference on Software Maintenance and Evolution (ICSME). IEEE, 620–631. doi:10.1109/ICSME64153.2025.00063

    arXiv 2025

  4. [4]

    2026.The Rust Book - Unsafe Rust

    The Rust Book. 2026.The Rust Book - Unsafe Rust. Retrieved Janurary 20, 2026 from https://doc.rust-lang.org/book/ch20-01-unsafe- rust.html

    2026

  5. [5]

    Saikat Chakraborty, Shuvendu Lahiri, Sarah Fakhoury, Akash Lal, Madanlal Musuvathi, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, and Nikhil Swamy. 2023. Ranking llm-generated loop invariants for program verification. InFindings of the Association for Computational Linguistics: EMNLP 2023. 9164–9175. doi:10.18653/v1/2023.findings-emnlp.614

    doi:10.18653/v1/2023.findings-emnlp.614 2023

  6. [6]

    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. 2026. Automated Proof Generation for Rust Code via Self-Evolution. arXiv:2410.15756 [cs.SE] https://arxiv.org/abs/2410.15756

    arXiv 2026

  7. [7]

    Jacob Cohen. 1960. A Coefficient of Agreement for Nominal Scales.Educational and Psychological Measurement20, 1 (1960), 37–46. doi:10.1177/001316446002000104

    doi:10.1177/001316446002000104 1960

  8. [8]

    Jackson, Shaz Qadeer, Sriram K

    Ankush Desai, Vivek Gupta, Ethan K. Jackson, Shaz Qadeer, Sriram K. Rajamani, and Damien Zufferey. 2013. P: safe asynchronous event-driven programming. InACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, W A, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 321–332. doi:10.1145/2491956.2462184

    arXiv 2013

  9. [9]

    Frama-C developers

    "Frama-C developers". 2026. "Frama-C". Retrieved Janurary 20, 2026 from https://frama-c.com/

    2026

  10. [10]

    Kani developers

    "Kani developers". 2026. "Automatic Harness Generation". Retrieved Janurary 20, 2026 from https://model-checking.github.io/kani/ reference/experimental/autoharness.html

    2026

  11. [11]

    Kani developers

    "Kani developers". 2026. "Verify Rust Standard Library Effort". Retrieved Janurary 20, 2026 from https://model-checking.github.io/verify- rust-std

    2026

  12. [12]

    The Coq developers. 2026. The Coq proof assistant. Retrieved Janurary 20, 2026 from https://rocq-prover.org

    2026

  13. [13]

    The RVT developers

    "The RVT developers". 2026. "Rust Verification Tools". Retrieved Janurary 20, 2026 from https://project-oak.github.io/rust-verification- tools/about.html

    2026

  14. [14]

    Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. 2024. Refinedrust: A type system for high-assurance verification of Rust programs.Proceedings of the ACM on Programming Languages8, PLDI (2024), 1115–1139. doi:10.1145/3656422

    doi:10.1145/3656422 2024

  15. [15]

    Arie Gurfinkel, Temesghen Kahsai, and Jorge A Navas. 2015. SeaHorn: A framework for verifying C programs (competition contribution). InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 447–450. doi:10.1007/978-3- 662-46681-0_41

    doi:10.1007/978-3- 2015

  16. [16]

    Mike He, Zhendong Ang, Ankush Desai, and Aarti Gupta. 2025. Ranking Formal Specifications using LLMs. InProceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages. 51–56. doi:10.1145/3759425.3763386

    arXiv 2025

  17. [17]

    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the foundations of the Rust programming language.Proceedings of the ACM on Programming Languages2, POPL (2017), 1–34. https://dl.acm.org/doi/10.1145/3158154

    doi:10.1145/3158154 2017

  18. [18]

    Shuvendu K. Lahiri. 2024. Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. doi:10.34727/2024/ISBN. 978-3-85448-065-5_19

    doi:10.34727/2024/isbn 2024

  19. [19]

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel

  20. [20]

    K Rustan M Leino. 2008. This is boogie 2.manuscript KRML178, 131 (2008), 9. https://www.microsoft.com/en-us/research/wp- content/uploads/2016/12/krml178.pdf

    2008

  21. [21]

    K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. InInternational conference on logic for programming artificial intelligence and reasoning. Springer, 348–370. https://link.springer.com/chapter/10.1007/978-3-642-17511-4_20

    doi:10.1007/978-3-642-17511-4_20 2010

  22. [22]

    Huan Li, Bei Wang, Xing Hu, and Xin Xia. 2025. Safe4U: Identifying Unsound Safe Encapsulations of Unsafe Calls in Rust using LLMs. Proc. ACM Softw. Eng.2, ISSTA (2025), 457–480. doi:10.1145/3728890

    doi:10.1145/3728890 2025

  23. [23]

    Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. In2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE Computer Society, 666–666. https://dl.acm.org/doi/10.1109/ICSE55347.2025.00129

    arXiv 2025

  24. [24]

    Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, and Derek Dreyer. 2022. RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. InProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 841–856. https://dl.acm.org/doi/10.1145/3519939.3523704

    arXiv 2022

  25. [25]

    Md Rakib Hossain Misu, Cristina V Lopes, Iris Ma, and James Noble. 2024. Towards ai-assisted synthesis of verified dafny methods. Proceedings of the ACM on Software Engineering1, FSE (2024), 812–835. https://dl.acm.org/doi/10.1145/3643763

    doi:10.1145/3643763 2024

  26. [26]

    Lahbib Naimi, Abdeslam Jakimi, Rachid Saadane, Abdellah Chehri, et al. 2024. Automating software documentation: Employing llms for precise use case description.Procedia Computer Science246 (2024), 1346–1354. doi:10.1016/j.procs.2024.09.568

    work page doi:10.1016/j.procs.2024.09.568 2024

  27. [27]

    Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. 2023. Can Large Language Models Reason about Program Invariants?. InProceedings of the 40th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 202), Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan ...

    2023

  28. [28]

    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 , Vol. 1, No. 1, Article . Publication date: July 2026. 22 Minghua Wang, Yuxi Ling, Mingzhi Gao, ...

    Pith/arXiv arXiv 2024

  29. [29]

    Zvonimir Rakamarić and Michael Emmi. 2014. SMACK: Decoupling source language details from verifier implementations. InComputer Aided Verification: 26th International Conference, CA V 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26. Springer, 106–113. doi:10.1007/978-3-319-08867-9_7

    work page doi:10.1007/978-3-319-08867-9_7 2014

  30. [30]

    2026.The Rust Reference

    The Rust Reference. 2026.The Rust Reference. Retrieved Janurary 20, 2026 from https://doc.rust-lang.org/reference/behavior-considered- undefined.html

    2026

  31. [31]

    Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, and Adrian Sampson. 2022. Verifying dynamic trait objects in rust. In Proceedings 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/351...

    arXiv 2022

  32. [32]

    Minghua Wang, Yuxi Ling, Mingzhi Gao, Yuwei Liu, and Lin Huang. 2026. KaPilot Artifact. doi:10.6084/m9.figshare.32834699.v3

    work page doi:10.6084/m9.figshare.32834699.v3 2026

  33. [33]

    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. https://link.springer.com/chapter/10.1007/97...

    doi:10.1007/978-3-031-71177-0_19 2025

  34. [34]

    Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. 2024. Enchanting program specification synthesis by large language models using static analysis and program verification. InInternational Conference on Computer Aided Verification. Springer, 302–328. https://doi.org/10.1007/978-3-031-65630-9_16

    doi:10.1007/978-3-031-65630-9_16 2024

  35. [35]

    Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, et al. 2025. Autoverus: Automated proof generation for rust code.Proceedings of the ACM on Programming Languages9, OOPSLA2 (2025), 3454–3482. https://dl.acm.org/doi/abs/10.1145/3763174

    doi:10.1145/3763174 2025

  36. [36]

    Mohammad Amin Zadenoori, Jacek Dąbrowski, Waad Alhoshan, Liping Zhao, and Alessio Ferrari. 2025. Large Language Models (LLMs) for Requirements Engineering (RE): A Systematic Literature Review. arXiv:2509.11446 [cs.SE] https://arxiv.org/abs/2509.11446

    arXiv 2025

  37. [37]

    Ying Zhang, Peng Li, Yu Ding, Lingxiang Wang, Dan Williams, and Na Meng. 2024. Broadly Enabling KLEE to Effortlessly Find Unrecoverable Errors in Rust. InProceedings of the 46th International Conference on Software Engineering: Software Engineering in Practice (Lisbon, Portugal)(ICSE-SEIP ’24). Association for Computing Machinery, New York, NY, USA, 441–4...

    arXiv 2024

  38. [2023]

    https://dl.acm.org/doi/10.1145/3586037

    Verus: Verifying rust programs using linear ghost types.Proceedings of the ACM on Programming Languages7, OOPSLA1 (2023), 286–315. https://dl.acm.org/doi/10.1145/3586037

    doi:10.1145/3586037 2023