LLM-Driven Rust Formal Verification at Scale: KaPilot & KVerus

Recent critical vulnerabilities in PHP, Node.js, GitLab, and Nginx highlight the growing threat landscape where AI accelerates vulnerability discovery and exploitation. Formal verification offers mathematical guarantees that code meets safety specifications, but historically remained confined to academia and safety-critical domains like aerospace due to high expertise barriers and long verification cycles.

Meanwhile, AI has achieved breakthroughs in automated theorem proving. OpenAI's release of 700+ mathematical manuscripts with Lean formal proofs signals readiness for large-scale formal reasoning. Since software formal verification is closely related to mathematical verification, the convergence of AI capabilities and verification needs suggests a tipping point for industrial adoption.

KaPilot: Automating Memory Safety Verification for Unsafe Rust

Rust's ownership and borrowing model eliminates many memory bugs at compile time, but Unsafe Rust — required for hardware access, FFI, and performance — bypasses these checks. KaPilot addresses this by orchestrating five specialized agents atop Kani, a model-checking-based verifier (rooted in Turing Award-winning model checking technology) that excels at verifying Unsafe Rust memory safety.

SafetyReq Agent extracts structured safety requirements from code documentation, avoiding specification errors from buggy code.

HarnGen Agent generates Kani verification harnesses via static analysis.

SpecGenerate Agent produces formal specifications (contracts, loop invariants).

SpecPrecheck Agent validates that specifications cover safety requirements and constraints are sufficient.

SpecVerify Agent runs Kani; on failure, errors feed back to SpecGenerate for iterative repair.

A Shuffle-and-Implication strategy combines multiple verified candidates into stronger specifications. KaPilot's paper won the Distinguished Artifact Award at ISSTA 2026 . The skills version is open-source at https://github.com/ant-research/KaPilot-skills.

In the Amazon Rust Standard Library Verification Challenge (https://github.com/model-checking/verify-rust-std), KaPilot completed all 29 bounty challenges within one week, with 16 PRs submitted.

KVerus: Scaling Functional Correctness Verification with Verus

Memory safety alone is insufficient when logic errors exist. Verus uses deductive verification with SMT solvers, allowing Rust-like syntax for specifications and proofs, and handles loops/recursion via induction. The team applied Verus to Asterinas (星绽) OS , a Rust-from-scratch kernel with a Framekernel architecture concentrating Unsafe Rust in a small ostd layer (~15k LOC). Verifying ostd (the VOSTD project) requires proving functional correctness of memory management.

KVerus introduces a four-phase pipeline with a dynamic knowledge base:

Preprocess : analyzes cross-file dependencies, extracts types, specs, and lemmas.

Comprehend : understands project lemmas and aligns verification knowledge with the current Verus version.

Prove : retrieves relevant code/lemmas, uses LLM to generate candidate proofs, invokes Verus.

Refine : iteratively repairs proofs using error feedback and accumulated knowledge until verification passes or attempt limit reached.

Published at ASE 2026 . KVerus evolved into composable Skills (https://github.com/asterinas/KVerus) covering proof generation, code migration, spec generation, quality review, and proof minimization.

Measured Impact on VOSTD

Overall ostd verification progress exceeds 30% ; 274 API entry points fully verified.

In the last month, ~60% of merged PRs were AI-assisted; nearly all new proof code and ~70% of spec code generated by KVerus.

Proof-to-code bloat ratio improved from 1:7.9 to 1:6.1 via automated proof minimization, reducing maintenance overhead.

AI-assisted PRs are tracked under the AI-assist label in the VOSTD repository (https://github.com/asterinas/vostd/pulls?q=is%3Apr+is%3Amerged+label%3AAI-assist).

Broader Landscape and Timing

Beyond Kani/Verus, interactive theorem provers (Lean, Rocq) with AI backends (e.g., Aeneas) are advancing rapidly. Anthropic (Oct 2024) reported using Claude to formally verify 123 open-source libraries at the RISC-V assembly level, covering 239 entry points, generating ~180 million lines of Rocq proofs, and uncovering hundreds of long-standing bugs.

Formal verification is not a silver bullet — it only proves specifications hold under given assumptions — but it establishes trust boundaries. With AI making vulnerability discovery easier and formal verification finally becoming cheap and fast enough for scale, the article argues that now is the optimal moment for formal verification to move from theory into widespread industrial practice .

References

HarnessLLM: Rust Verification Harness Generation with Large Language Models, DOI: https://doi.org/10.1145/3744916.377312

KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification, DOI: https://doi.org/10.1145/3832239

KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code, DOI: https://doi.org/10.1145/3832783.3834503

StarVerus: LLM-Powered Multi-Agent Collaboration for Industrial Rust Code Verification Automation, DOI: https://doi.org/10.1145/3770855.3818485

Beyond Benchmarks: A Case Study of LLM-Generated Verus Specification Failures on Asterinas Vostd, DOI: https://doi.org/10.1145/3832783.3834504

Zhang et al., Survey of Formal Verification Methods for Rust, Journal of Software, 2024

Tooling list: https://arewesafetycriticalyet.org/tooling/tools-list

Verify Rust Std challenge: https://github.com/model-checking/verify-rust-std

Kani model checker: https://github.com/model-checking/kani

Verus verifier: https://github.com/verus-lang/verus

Aeneas: https://github.com/AeneasVerif/aeneas