Verifying the Rust Standard Library

• URL: http://arxiv.org/abs/2606.17374v1
• Date: Tue, 16 Jun 2026 00:11:04 GMT
• Title: Verifying the Rust Standard Library
• Abstract summary: Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code.<n>We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates complementary verification tools into the continuous integration of a verification repository forked from the Rust standard library.
• Score: 3.303009078327922
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic checks under Miri, but lacks static verification. We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates complementary verification tools into the continuous integration of a verification repository forked from the Rust standard library. We analyze the campaign's effectiveness, discuss the practical value of machine-checked proofs for a subset of undefined behaviors (e.g., out-of-bounds access, null and dangling pointer dereferences, and use of uninitialized memory), and frame the remaining obstacles as open challenges for the formal-methods community.

Related papers

• Kani: A Model Checker for Rust [3.019677299390329]
  Kani is an open-source model checker for Rust.<n>It pushes bounded model checking beyond bug-finding to provide correctness guarantees.<n>Kani operates at scale in production CI, with over 16,000 harnesses verified per code change.
  arXiv  Detail & Related papers  (2026-07-01T22:05:33Z)
• The Hidden Signal of Verifier Strictness: Controlling and Improving Step-Wise Verification via Selective Latent Steering [67.8271652641864]
  We study whether verifier strictness can be controlled through hidden-state intervention.<n>VerifySteer exploits latent correctness signals for sample-level routing and selectively intervenes on paragraph boundaries.
  arXiv  Detail & Related papers  (2026-05-20T05:48:16Z)
• Veritas: A Semantically Grounded Agentic Framework for Memory Corruption Vulnerability Detection in Binaries [14.42294978688412]
  We present Veritas, a semantically grounded framework for binary memory corruption vulnerability detection.<n>Veritas combines a static slicer over RetDec-lifted LLVM IR, a dual-view LLM detector, and a multi-agent validator.<n>We implement Veritas as a modular pipeline and evaluate it on a curated benchmark of real-world binary vulnerability cases.
  arXiv  Detail & Related papers  (2026-05-14T17:16:11Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  Safety-aligned large language models (LLMs) are increasingly deployed in real-world pipelines.<n> adversaries can distribute backdoored checkpoints that behave normally under standard evaluation but jailbreak when a hidden trigger is present.<n>Recent post-hoc weight-editing methods offer an efficient approach to injecting such backdoors.
  arXiv  Detail & Related papers  (2026-04-14T06:48:33Z)
• IMMACULATE: A Practical LLM Auditing Framework via Verifiable Computation [49.796717294455796]
  We present IMMACULATE, a practical auditing framework that detects economically motivated deviations.<n>IMMACULATE selectively audits a small fraction of requests using verifiable computation, achieving strong detection guarantees while amortizing cryptographic overhead.
  arXiv  Detail & Related papers  (2026-02-26T07:21:02Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Scalable and Robust LLM Unlearning by Correcting Responses with Retrieved Exclusions [49.55618517046225]
  Language models trained on web-scale corpora risk memorizing and exposing sensitive information.<n>We propose Corrective Unlearning with Retrieved Exclusions (CURE), a novel unlearning framework.<n>CURE verifies model outputs for leakage and revises them into safe responses.
  arXiv  Detail & Related papers  (2025-09-30T09:07:45Z)
• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
  CRUST-Bench is a dataset of 100 C repositories, each paired with manually-written interfaces in safe Rust as well as test cases.<n>We evaluate state-of-the-art large language models (LLMs) on this task and find that safe and idiomatic Rust generation is still a challenging problem.<n>The best performing model, OpenAI o1, is able to solve only 15 tasks in a single-shot setting.
  arXiv  Detail & Related papers  (2025-04-21T17:33:33Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs.
  arXiv  Detail & Related papers  (2024-07-21T07:30:30Z)
• Yuga: Automatically Detecting Lifetime Annotation Bugs in the Rust Language [15.164423552903571]
  Security vulnerabilities have been reported in Rust projects, often attributed to the use of "unsafe" Rust code.<n>These vulnerabilities, in part, arise from incorrect lifetime annotations on function signatures.<n>Existing tools fail to detect these bugs, primarily because such bugs are rare, challenging to detect through dynamic analysis.<n>We devise a novel static analysis tool, Yuga, to detect potential lifetime annotation bugs.
  arXiv  Detail & Related papers  (2023-10-12T17:05:03Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.