Kani: A Model Checker for Rust

• URL: http://arxiv.org/abs/2607.01504v1
• Date: Wed, 01 Jul 2026 22:05:33 GMT
• Title: Kani: A Model Checker for Rust
• Abstract summary: 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.
• Score: 3.019677299390329
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties. Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. We demonstrate feasibility through case studies on industrial Rust projects, where contracts upgraded verification from panic-freedom to functional correctness, uncovering six previously unknown bugs. Kani operates at scale in production CI, with over 16,000 harnesses verified per code change in the Rust standard library verification campaign.

Related papers

• From C to Idiomatic Rust: A Ship-of-Theseus Agentic Translation [0.13537117504260618]
  C underpins operating systems, embedded platforms, and network infrastructure because its abstractions map directly to machine behaviour.<n> Rust eliminates most of failure modes through a static ownership and borrowing model that enforces memory safety and aliasing constraints at compile time.<n>This paper presents a migration methodology that first generates a semantics-preserving, non-idiomatic Rust baseline and then incrementally rewrites it into idiomatic Rust using agentic AI.
  arXiv  Detail & Related papers  (2026-07-30T21:00:27Z)
• Verifying the Rust Standard Library [3.303009078327922]
  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.
  arXiv  Detail & Related papers  (2026-06-16T00:11:04Z)
• CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
  We introduce textbfCIAware-Bench, a benchmark for measuring textbfcontrol textbfintervention (CI) awareness across frontier models.<n>CIAware-Bench tests whether models can distinguish their own trajectories from those modified by a control intervention.
  arXiv  Detail & Related papers  (2026-06-09T16:24:16Z)
• The Path Matters: Learning a Token-Commitment Policy for Diffusion Language Models [52.93186090124315]
  We argue that token commitment can be learned as a reusable trace-state policy.<n>We introduce TraceLock, a lightweight plug-in controller that instantiates this policy for a frozen diffusion language model.
  arXiv  Detail & Related papers  (2026-05-23T18:23:46Z)
• Agentic Model Checking [12.832868209928039]
  We propose a paradigm that couples LLM agents with a bounded model checking backend.<n>We instantiate the approach in BMC-Agent and evaluate it on LLM-generated kernel and compiler code in C and Rust.
  arXiv  Detail & Related papers  (2026-05-20T17:25:52Z)
• 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)
• 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)
• 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)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• 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.