PaperlayerView exact revision on arXiv

Source-linked AI summary

Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification

Andrada-Livia Antoneac, Dorel Lucanu, Dragoş Teodor Gavriluţ

arXiv:2609.34886v1cs.AIcs.PLcs.SE

TL;DR

Formal verification of DLLs is difficult because their forward and backward references must remain consistent, and weak specifications can rely on unverified assumptions. This paper studies LLM-assisted verification across related Rust implementations and develops a reusable, soundness-first skill. Its case study identifies specification quality as a key difficulty and shows the skill addresses some challenges.

  • Problem

    The paper asks whether an AI model can efficiently verify structurally related Rust implementations against a shared specification and whether that process can be made reusable.

    Source: §1 · p. 1

  • Method

    The paper progressively investigates DLL verification and packages domain knowledge with a soundness-first workflow in a reusable skill for LLM agents.

    Source: §4.2 · p. 13, §5 · p. 16

  • Results

    The case study identifies specification quality as a key verification difficulty: weakened specifications can be masked by assume statements and axiomatic lemmas based on unverified trusted functions.

    Source: §5 · p. 16

  • Takeaways & Limitations

    The skill addresses some of the challenges behind weak specifications, and the paper presents its design and interaction with different agents as its main contribution.

    Source: §5 · p. 16

    The skill still needs systematic generation of missing lemmas to replace assume stubs and post-mutation staging that re-establishes invariants.

    Source: §4.5 · p. 16

Abstract

from arXiv · show

LLM-assisted Verus verification is a less tedious method to verify Rust implementations, but paired with self-referential structures, e.g., Doubly Linked Lists (DLLs)—notoriously difficult to formalise for verification—it becomes a substantially more demanding verification task. Moreover, a specification weakness can arise when verification relies on unproven or invalidated assumptions, such as axiomatic lemmas and assume statements. We investigate whether LLM agents can synthesize strong DLL specifications while minimizing these trusted base. The analysis follows three different approaches: manual verification, property-specific verification, and a defined skill for the specific case of DLLs and certain properties of this type of data structure. The skill encodes domain knowledge and a task-decomposition strategy. We show that an LLM agent equipped with a carefully designed verification skill can generate strong, low-trust specifications for DLLs in Verus.

1 Introduction

The paper asks whether LLM agents can verify related Rust implementations against a shared specification and whether the process can become reusable. It presents initial steps toward formal verification of DLL implementations and a verification skill built from the challenges encountered.

1 Introduction

  • Verifying multiple implementations against one abstract specification tests whether LLM-assisted verification can handle a shared proof structure alongside implementation-specific requirements.Source: §1 · p. 1
  • The paper asks whether an AI model can efficiently verify structurally related Rust implementations against a shared formal specification and whether the process can be codified as a reusable methodology.Source: §1 · p. 1
  • DLL correctness is difficult to verify because forward and backward references must remain mutually consistent, and prior work compared eleven implementations without formally verifying their functional correctness.The prior study evaluated execution time, memory footprint, and three safety vulnerabilities; this paper aims to add formal verification.Source: §1 · p. 1
  • The work reports a systematization of verification challenges, principles for designing an AI-agent verification skill, and implementation of a skill based on those principles.Source: §1 · pp. 1–2

2 Background

The background distinguishes Rust verification approaches and prior LLM-assisted proof systems from this paper’s interactive, specification-focused study. It also describes the shared DLL abstraction and its mutually dependent operation contracts.

2.1 Formal Verification in Rust

  • Deductive verifiers such as Verus construct mathematical proofs across possible inputs, while model checkers explore reachable states and translation-based tools verify translated representations.The cited examples include Kani, Verus, Creusot, and Aeneas.Source: §2.1 · p. 2

2.2 AI-Assisted Verification

  • Prior LLM-assisted systems commonly automate proof engineering; AutoVerus [3] uses staged generation, refinement, and debugging, while VeriStruct targets full Verus data-structure modules.The present work instead uses interactive exploration to progressively strengthen specifications and minimize assumptions and axiomatic lemmas in related DLL implementations.Source: §2.2 · pp. 2–3

2.3 Doubly Linked Lists

  • The DLL study uses a trait-based abstract specification independent of memory representation, with eight operations and informal input/output/return contracts.The next and prec contracts are mutually recursive, so correctness cannot be established for either operation in isolation; the full list implementation must be verified as a whole.Source: §2.3 · pp. 3–4

3 A Progressive Verification Case Study

The case study progresses from manual verification to property-specific verification and Claude-assisted specification generation, then catalogs the tool, DLL, and interaction challenges that complicate machine-checked proofs. Claude’s final specification reduces assumptions from 75 to 11, but the remaining assumptions concern the chain-to-sequence bridge.

3.1 First Experiment - Manual Verification

  • The manual index-based DLL exercise used weak contracts and local assumptions, leaving reachability preservation and list-view updates among the informal obligations.Index-based mutations required manual synchronization with the abstract list view.Source: §3.1 · p. 5

3.2 Second Experiment - Property-Specific Verification

  • The property-specific experiment strengthened invariants around chain validity, but still relied on many assumptions and explicit axiomatic lemmas.The remaining gaps were attributed to the index-based memory model’s demands on Rust ownership and Verus’s SMT encoding.Source: §3.2 · pp. 5–6

3.3 Claude-Assisted Scenario

  • 45 verified, 0 errors, and 11 assumes remained after four phases reduced assumptions from 75; the remaining 11 concern the chain-to-sequence bridge.The bridge connects exact-hop-count chain_n to the abstract list_view() sequence index; the agent also required prolonged reasoning and manual prompting.Source: §3.3 · p. 6

3.4.1 Challenges Raised by Using Verus in the Verification of Rust Implemementations

  • Verus proof work faced trigger-sensitive SMT reasoning, ghost-state sequencing, mutable-reference framing, proof-block placement, recursive-function opacity, and resource limits.Raw-pointer support also remained incomplete because pointer validity, aliasing, and layout annotations add overhead and interact with ghost infrastructure.Source: §3.4.1 · pp. 7–8

3.4.2 Challenges Raised by the Specification and Verification of DLLs Implemented in Rust

  • DLL verification requires global chain invariants and memory-model-specific ghost infrastructure, while the abstract specification leaves deletion’s memory recovery unconstrained.The eleven implementations use different workarounds for self-reference, and the three memory-model groups require distinct ghost infrastructure.Source: §3.4.2 · pp. 8–9

3.4.3 Combined Challenges Raised by the Verification of DLLs Using Verus

  • Global invariants compound trigger management: overly specific triggers can leave conjuncts uninstantiated without a trigger diagnostic.Distinguishing non-implication from non-instantiation requires inspecting quantifier-instantiation logs.Source: §3.4.3 · p. 9
  • Mutating a self-referential DLL requires ghost snapshots and proof blocks for intermediate states because old(self) denotes only the function-entry state.Specification gaps also interact with snapshot ordering, while mutually recursive chain specifications require separate lemma libraries for both directions.Source: §3.4.3 · pp. 9–10
  • Inductive chain reasoning needs both bounded reachability and an exact-count predicate such as chain_n.Reachability alone is insufficient for the termination argument in inductive chain lemmas.Source: §3.4.3 · p. 10

4 Towards a Verification Skill for DLLs

The skill packages DLL-specific knowledge and a staged workflow to guide an LLM agent through Verus specification generation. Its design emphasizes traceable, sound specifications and separates analysis, mapping, generation, verification, and debugging.

4 Towards a Verification Skill for DLLs

  • The skill is an on-demand package of knowledge and procedural guidance intended to turn a general-purpose agent into a specialist for a specific task.Its design separates analysis, mapping, generation, verification, and debugging to support clarity and repeatability.Source: §4 · p. 10, §4.1 · pp. 10–11

4.2 A First Version of the Skill

  • The workflow analyzes inputs, maps the abstract specification to Verus, generates contracts and helper specifications, adds loop or recursion invariants, verifies properties, debugs failures, and reports discrepancies.When classified as axiom-boundary, it marks executable functions external_body and focuses on precise contracts and consistency lemmas.Source: §4.2 · pp. 12–13
  • The skill abstracts node identity and membership from storage, letting specifications focus on global DLL properties across diverse memory models.This addresses the need to rebuild ghost infrastructure for each implementation.Source: §4.2 · p. 13

4.1 Principles Guiding the Skill Design

  • Every invariant clause must trace to an abstract requirement, while specifications must not be weakened to accommodate verifier convenience or implementation bugs.The skill also requires reporting real bugs or specification mismatches with a counterexample, violated requirement, and suggested fix.Source: §4.1 · p. 11, §4.2 · p. 13

4.3 Current Results and Resolutions

  • The current skill is not final, and its evaluation requires users to inspect generated Verus code against the workflow and check whether its specifications satisfy the criteria.Table 5 examples include index-based runs I1–I4, plus Standard DLL and SlotMap DLL tests; I2 and I3 use the same implementation and agent but different prompts.Source: §4.3 · p. 13, Table 5 · p. 14

4.4 Specifications’ Evaluation Criteria

  • The evaluation criteria compare agents’ workflow choices across soundness boundaries, specification alignment, order precision, generality, allocator modeling, and proof ergonomics.Specification alignment distinguishes direct, witness-based, traversal-derived, and axiomatic reachability approaches.Source: §4.4 · p. 14

6. SlotMap with Claude 4.6 High

Table 6 presents per-specification evaluation criteria; the discussion identifies strengths and remaining gaps that guide skill development and specification fine-tuning.

4.5 Shortcomings Yet to Be Addressed

  • The evaluation’s strengths and shortcomings guide specification refinement; proposed skill improvements include systematic lemma coverage, post-mutation proof staging, and stronger ordering witnesses.Post-mutation staging would add ghost snapshots after state changes and local lemmas to re-assert invariants.Source: §4.5 · pp. 15–16
  • I1 and I2 define chain validity through reachability, but I1 relies on many assumptions and I2 lacks a positional witness for fine-grained order guarantees.I2 uses lemmas for fuel monotonicity, frame conditions, and reachability chaining, and includes allocator correctness in its state invariant.Source: §4.5 · p. 16
  • I3 achieves full verification and high-precision ordering postconditions with a ghost order sequence, but is less faithful to the concrete implementation.It strengthens the invariant and proves that it implies reachability.Source: §4.5 · p. 16
  • I4 leaves link, a mutation-critical function, as an external_body, so its proof is incomplete in a central part of list construction.Source: §4.5 · p. 16
  • STD specifies chain shape with a ghost address chain but axiomatizes pointer-touching operations, leaving concrete-code verification unable to expose implementation bugs.It also cannot justify allocator freshness beyond trust assumptions.Source: §4.5 · p. 16
  • The SlotMap specification supports bidirectional link-consistency lemmas while retaining a chain witness, despite its opaque backend.It provides a stronger abstract model than the pointer case.Source: §4.5 · p. 16

5 Conclusions

The conclusion identifies specification quality and trusted assumptions as central challenges in Verus verification of DLLs. It presents a reusable, soundness-first skill as a first version, with broader verification and further workflow improvements left for future work.

5 Conclusions

  • The case study finds that weak specifications can be masked by assume statements and axiomatic lemmas based on unverified trusted functions.The skill addresses some challenges that lead to this situation.Source: §5 · p. 16
  • The reusable skill packages domain knowledge and a soundness-first workflow to help a general-purpose agent produce DLL specifications with an explicit, minimal trusted base.Source: §5 · p. 16
  • The skill is a first version; future work includes replacing assume stubs with systematic lemmas, post-mutation proof staging, and stronger ordering witnesses.Source: §5 · p. 17
  • The longer-term goal is to verify all eleven implementations against one shared specification, while accommodating different agents and proof strategies.The paper describes that evaluation as extensive and representative of an actual skill and Verus assessment.Source: §5 · p. 17
Loading 2609.34886v1…