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

• URL: http://arxiv.org/abs/2607.21957v1
• Date: Fri, 24 Jul 2026 04:10:12 GMT
• Title: KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
• Abstract summary: Rust's ownership and type system provide strong memory safety guarantees, but unsafe code still presents memory safety risks.<n>KaPilot is a framework for automatically generating specifications to verify unsafe Rust memory safety.<n>Compared with AutoSpec, KaPilot produces 14.8% more verifiable specifications and 25.9% more equivalent-or-better specifications.
• Score: 8.36913747598685
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• HarnessLLM: Rust Verification Harness Generation with Large Language Models [8.14069260667009]
  Rust's ownership model and type system offer strong memory safety guarantees, but unsafe code and runtime panics still present significant risks.<n>Formal verification is essential to ensure memory safety, but developing verification harnesses remains a challenging and manual task.<n>We present HarnessLLM, an automated workflow that leverages large language models to generate verification harnesses for Rust code directly from existing test suites.
  arXiv  Detail & Related papers  (2026-07-24T10:06:52Z)
• HyperSafe: Inference-Time Safety Recovery for Fine-Tuned Language Models [65.08794811632073]
  HyperSafe restores safety behavior by generating a model-specific Safe Side Network for each fine-tuned checkpoint.<n>We evaluate HyperSafe on two model families, Qwen2-7B and LLaMA-3-8B, across multiple safety benchmarks.
  arXiv  Detail & Related papers  (2026-07-13T12:28:43Z)
• 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)
• CHILLGuard: Towards Fine-Grained Chinese LLM Safety Guardrail with Scalable Data Construction and Model-aware Preference Alignment [55.74660714572696]
  Malicious content generated from large language models (LLMs) could pose severe safety risks and ethical concerns.<n>Existing LLM safety guardrails excel in English or multilingual settings, but lack adaptation to Chinese-specific regulatory policies, cultural context and linguistic nuances.<n>We introduce a 5-macro, 31-micro category fine-grained risk taxonomy for Chinese scenarios, and build CHILLGuard: a dedicated Chinese LLM content safety guardrail.
  arXiv  Detail & Related papers  (2026-06-13T16:57:51Z)
• Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
  We present VeriSpecGen, a traceable refinement framework that synthesizes intent-aligned specifications in Lean through requirement-level attribution and localized repair.<n>VeriSpecGen decomposes natural language into atomic requirements and generates requirement-targeted tests with explicit traceability maps.<n>We achieve 86.6% on VERINA SpecGen task using Claude Opus 4.5, improving over baselines by up to 31.8 points across different model families and scales.
  arXiv  Detail & Related papers  (2026-04-12T00:52:27Z)
• SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
  Reasoning language models (RLMs) are increasingly used in programming.<n>Yet, even state-of-the-art RLMs frequently introduce critical security vulnerabilities in generated code.<n>We present SecPI, a fine-tuning pipeline that teaches RLMs to internalize structured security reasoning.
  arXiv  Detail & Related papers  (2026-04-04T04:29:11Z)
• LiteRSan: Lightweight Memory Safety Via Rust-specific Program Analysis and Selective Instrumentation [19.377860990540444]
  Rust is a memory-safe language, and its strong safety guarantees have been attracting widespread adoption.<n>A widely adopted approach for detecting memory safety bugs in Rust is Address Sanitizer (ASan)<n>We present LiteRSan, a novel memory safety sanitizer that addresses the limitations of prior approaches.
  arXiv  Detail & Related papers  (2025-09-19T20:09:20Z)
• 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)
• Is unsafe an Achilles' Heel? A Comprehensive Study of Safety Requirements in Unsafe Rust Programming [4.981203415693332]
  Rust is an emerging, strongly-typed programming language focusing on efficiency and memory safety. Current unsafe API documents in the standard library exhibited variations, including inconsistency and insufficiency. To enhance Rust security, we suggest unsafe API documents to list systematic descriptions of safety requirements for users to follow.
  arXiv  Detail & Related papers  (2023-08-09T08:16:10Z)

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.