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

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

scope and result

KaPilot is a five-agent pipeline for generating Kani contracts for unsafe Rust from documentation and lightweight code metadata. The paper targets memory safety and panic conditions, rather than functional correctness inferred from implementation. Its central design is to make documentation-derived safety requirements the specification target, then generate, precheck, verify, and select contracts. The authors evaluate 54 functions with expert ground truth (GoldSet) and 70 unsafe functions without ground truth (ULSet), using Kani 0.62.0 and GPT-5, DeepSeek-v3.2, and Claude-Sonnet-4. The paper says: “The process begins with lightweight program analysis and proof harness generation.” (abstract, p. 1)

The pipeline has SafetyReq, HarnGen, SpecGenerate, SpecPrecheck, and SpecVerify agents. HarnGen creates a symbolic-input Kani harness; SafetyReq converts documentation into atomic requirements; SpecGenerate writes #[kani::requires], #[kani::ensures], and loop-invariant annotations; SpecPrecheck checks coverage and strength; SpecVerify runs Kani and returns contextual failures. Several candidates are generated, then a shuffle-and-implication procedure combines the weakest usable precondition, strongest usable postcondition, and compatible invariants.

technique 1: extract traceable safety requirements from documentation

Use this when unsafe behavior is documented in Safety, Panics, or cross-referenced API text and the implementation may hide or omit the actual assumptions. The paper’s example is offset_from_unsigned: its local documentation says the distance is non-negative and may link to offset_from, where same-allocation, in-bounds, size-multiple, and isize-overflow conditions are stated. KaPilot deliberately does not ask the model to infer these only from code.

Steps:

1. restrict source material to the target function’s Safety and Panics sections and relevant cross-references
2. ask SafetyReq to produce one sentence per memory-safety or panic property
3. map every variable to a target parameter, return value, or generic
4. append provenance in <src>-<sec>: <original documentation> form
5. reject duplicate, implying, contradictory, out-of-scope, or incomplete lists
6. score the list by the harmonic mean of rule scores; feed per-rule feedback back for up to three iterations

The six rules are scope, atomicity, variable reference, source traceability, exclusivity, and completeness. The paper states: “Each requirement must consist of a single sentence describing exactly one safety property in a precise and concise manner.” (Sec. 3.3, p. 6) It also states: “There must be no duplicates between requirements, no logical implications between two requirements, and no contradictions between two requirements.” (Sec. 3.3, p. 6)

Verus form (inference). Put each requirement into explicit requires predicates and, where appropriate, ensures predicates or loop invariants. Preserve the source citation as a comment or an external requirement record. Kani’s kani::mem::same_allocation, can_dereference, and can_write have no direct one-to-one Verus equivalent; in Verus one would use pointer models, validity predicates, ownership/borrow facts, or a trusted specification for an unsafe primitive. The source-to-contract traceability process carries over unchanged. The bounded Kani harness does not carry over as a complete proof of unbounded Rust behavior.

Evidence. In the offset case study, four requirements capture byte-size overflow, allocation derivation, in-bounds range, and address-space wraparound (Fig. 6, pp. 16–17). KaPilot’s contract includes kani::mem::same_allocation; the code-centric AutoSpec variant misses that condition and fails Kani. This is a concrete demonstration of documentation-first extraction, but the paper’s quality labels on GoldSet still required human review.

technique 2: generate a harness and metadata without exposing implementation to contract generation

Use this before generation for functions with arbitrary inputs, generic types, traits, or non-primitive parameters. Lightweight analysis records the signature, visibility, trait bounds, implemented traits, call graph, description, and public helper methods in a shared knowledge database. HarnGen uses AutoHarness first, then an LLM fills missing declarations when AutoHarness cannot construct a valid harness. The harness initializes parameters with Kani values such as kani::any() and invokes the target as the proof entry point.

Steps:

1. statically extract the target signature and type relationships
2. enumerate public methods that could express safety predicates
3. call AutoHarness
4. for failures, ask HarnGen to fill in missing parameter declarations
5. check that the target is actually invoked in the harness; the metadata goes to the shared knowledge database

The paper warns that AutoHarness cannot handle complex parameters, missing trait implementations, or user-defined types directly (Sec. 3.2.2, p. 6). Verus form (inference): write a proof fn or verified wrapper with explicit requires assumptions and symbolic or ghost values; use trait bounds and abstract views instead of Kani’s bounded nondeterministic arrays. Harness construction remains a separate engineering step. A generated harness only proves the paths and bounds represented by its assumptions.

technique 3: generate Kani contracts from requirements, metadata, API knowledge, and few-shot examples

SpecGenerate receives the requirement list, metadata, Kani primitive documentation, similar verified examples, and feedback from previous attempts. Critically, KaPilot excludes target source code: “We exclude the source code of the target function, because we believe that the actual implementation would interfere with LLMs’ understanding of safety properties.” (Sec. 3.4, p. 7) The intended separation (the paper’s motivation C1, not a measured result) is to keep a defective implementation from becoming its own contract.

Steps:

1. retrieve similar function/specification pairs from the shared database
2. prompt for all preconditions, postconditions, and loop invariants needed by the requirement list
3. use Kani forms such as #[kani::requires(...)], #[kani::ensures(...)], #[kani::loop_invariant(...)], kani::mem predicates, and #[kani::modifies(...)]
4. feed the last precheck or verification feedback into the next generation
5. store every candidate that eventually verifies for later few-shot retrieval

Verus form (inference). The analogous prompt should emit requires, ensures, invariant, spec fn, proof fn, and appropriate ghost views. Verus has stronger ownership and mathematical-sequence idioms, while Kani contracts can directly call memory predicates and bounded-model-checking APIs. The documentation-first and implementation-blind choice is portable as a workflow rule, but source exclusion can make functional postconditions impossible when documentation is incomplete.

technique 4: semantic precheck before invoking the verifier

SpecPrecheck is a lightweight filter, not a sound proof. It first checks that every extracted requirement is covered. It then assigns a score from 1 to 10 for precondition strength and postcondition adequacy, rejecting overly restrictive preconditions and weak postconditions. Scores below six receive targeted feedback; the loop runs for at most five iterations.

A Verus adaptation (inference) can use an LLM or static review to flag missing clauses before expensive SMT calls, but the final decision must remain Verus verification and semantic review. The paper expressly says: “SpecPrecheck is designed as a lightweight semantic-based specification checker rather than a sound verifier.” (Sec. 3.5, p. 8) Treat its score as triage only.

technique 5: contextual verifier feedback and a mechanical vacuity check

SpecVerify runs Kani and classifies syntax errors, counterexample failures, and vacuous successes. For a failure it sends the model the counterexample, passing and failing harnesses, and a failure-specific repair rule. For example, an assigns violation triggers a correction of #[kani::modifies(...)].

To detect a contract such as #[kani::requires(false)], it appends #[kani::ensures(|_| false)]. If the original contract verifies but the appended false postcondition also verifies, the assumptions were unreachable and the contract is vacuous. In the as_flattened case, an initial T::IS_ZST && ... precondition excluded all non-ZST cases; the check led SpecGenerate to regenerate the corrected !T::IS_ZST || ... form (Fig. 8, p. 18).

Verus form (inference). Add a deliberately impossible postcondition or an equivalent reachability assertion in a temporary verification harness, run Verus, and require the temporary check to fail. This catches contradictory requires, although the exact Kani interpolation behavior is tool-specific. Preserve counterexamples and diagnostics as repair context, then rerun the verifier.

technique 6: shuffle candidates by logical implication

Use this when independently generated candidates have useful but mismatched clauses. Suppose candidate one has weaker P and weaker Q', while candidate two has stronger P' and stronger Q; the desired contract may be {P} C {Q} even though no single candidate contains it. KaPilot extracts all preconditions and postconditions, chooses a weakest precondition and strongest postcondition under implication, and verifies their combinations. For loops it tests the invariant from the weakest-precondition candidate, the invariant from the strongest-postcondition candidate, and their conjunction.

The algorithm repeats up to M iterations, removes tested predicates, and falls back to a random candidate if M < |SP|. The paper’s experiment uses two candidates and two iterations. This is an inference-friendly Verus technique: use implication checks and Verus re-verification to combine requires, ensures, and invariants, but do not assume predicate implication implies implementation correctness without a fresh proof.

evidence, denominators, and limits

On GoldSet, GPT-5 gives 31 good, 17 bad, and 6 failures out of 54 (57.41%, 31.48%, 11.11%); DeepSeek gives 28/15/11 (51.85%, 27.78%, 20.37%); Claude gives 34/16/4 (62.96%, 29.63%, 7.41%). On ULSet, pass rates are 50/70 (71.43%), 48/70 (68.57%), and 48/70 (68.57%), but the paper cannot separate good from bad without ground truth. Good means Kani passes and the generated precondition is no stronger and postcondition no weaker than ground truth. Two experts independently labeled GoldSet, with Cohen’s kappa 0.81–0.95, then reconciled disagreements.

Against adapted AutoSpec under GPT-5 and the same 54 GoldSet functions, KaPilot has 31 good versus 17, 17 bad versus 23, and 6 failures versus 14. The paper reports roughly 82% more good specifications and 57% fewer failures, but this is an adaptation of AutoSpec rather than its original implementation.

Ablation is informative: removing SafetyReq yields 6 good versus 31; removing SpecPrecheck yields 12; removing SpecVerify yields 12; removing few-shot examples yields 11; direct prompting yields 8. These are all out of 54. The authors attribute the changes to requirement alignment, semantic filtering, contextual repair, examples, and decomposition, respectively.

What is proved: Kani proves the generated predicates for the bounded harness and unwind settings. What is measured: pass, failure, and manually judged semantic quality. What stays trusted: documentation and cross-reference completeness, LLM requirement extraction, human ground truth, Kani and its compiler/solver, harness representativeness, and the manual good/bad judgment. ULSet’s missing ground truth prevents semantic-quality claims. Full unwinding is used for non-while loops when feasible; loop invariants are limited by Kani support.

The threat to VL is high for automated contract-writing workflows (inference): KaPilot directly automates unsafe-Rust specification generation and uses a stronger anti-vacuity and candidate-selection story than a one-shot model. The threat is lower for Verus-specific functional proofs because Kani’s bounded memory predicates, harnesses, and APIs differ. VL should already adopt requirement extraction with citations, verifier feedback, vacuity tests, and semantic strength checks. It should not redo a direct-prompt baseline as its main contribution. It still needs human-owned intent, unbounded reasoning where required, and explicit review of assumptions.

techniques for the catalog

• documentation-derived safety requirements — extract atomic, source-traceable memory and panic properties before writing contracts
• harness and metadata preparation — build symbolic-input Kani entry points and store type/API context for generation
• implementation-blind contract generation — generate Kani preconditions, postconditions, and invariants from requirements, metadata, API knowledge, and few-shot examples
• semantic precheck — reject uncovered or badly strengthened/weakened contracts before verifier execution
• contextual repair and vacuity testing — feed counterexamples and failure classes back, then append an impossible postcondition to expose unreachable assumptions
• shuffle-and-implication selection — combine weakest preconditions, strongest postconditions, and compatible loop invariants across verified candidates Audited 2026-10-12 against the paper: checked every number (Tab. 3, Tab. 2 kappa range, Tab. 6, Tab. 7, thresholds 6, iteration limits 3, 5 and 2, 2 candidates), the six rules, the pipeline steps, Algorithm 1 and its loop-invariant cases, Figs. 6 to 8 and the three quotations; all numbers match (Tab. 3 prints 27.78% for Claude bad, a typo for 16/54 = 29.63%, and the study has 29.63%). Changed: offset_from conditions listed alignment, which the paper does not state (now in-bounds and size-multiple); HarnGen fills missing parameter declarations, not trait implementations; harness storage claim removed; the implementation-blind benefit marked as motivation not result; vacuity check led to regeneration rather than forcing it; Verus adaptation in technique 4 marked inference. Could not check the code-level claims about Kani and Verus semantics beyond the paper and the Verus notes.

Last edited: 2026-10-13