neural-theorem-proving-verification

name

neural-theorem-proving-verification

description

Generate formal proofs for program verification conditions (VCs) in Isabelle, Lean 4, and Rocq. Translates C/WhyML code obligations into proof assistant syntax and synthesizes tactic-based proofs. Use when: 'prove this verification condition', 'generate Isabelle proof for this invariant', 'verify this C function formally', 'translate this VC to Lean', 'help me prove this loop invariant', 'synthesize a Rocq proof for this postcondition'.

Neural Theorem Proving for Verification Conditions

This skill enables Claude to generate formal proofs for verification conditions (VCs) arising from program verification. Following the NTP4VC methodology (ICLR 2026), it applies neural theorem proving to the hardest bottleneck in software verification: proving the logical obligations that automated theorem provers (ATPs) like Sledgehammer or CoqHammer cannot discharge. Claude translates VCs from Why3/Frama-C pipelines into Isabelle, Lean 4, or Rocq tactic proofs, using structured proof decomposition rather than whole-proof generation.

When to Use

• When a user has a verification condition from Frama-C, Why3, or another deductive verification tool and needs a proof in Isabelle, Lean 4, or Rocq
• When a user needs to prove a loop invariant, precondition, postcondition, or memory safety obligation for annotated C code
• When Sledgehammer, CoqHammer, or auto-level tactics fail on a VC and the user needs a manual tactic proof
• When a user wants to translate a Why3-generated VC into a different interactive theorem prover (ITP) language
• When a user is building a verification pipeline and needs help structuring VC proof obligations from ACSL-annotated C or WhyML specifications
• When a user asks to formally verify properties of data structures, sorting algorithms, or kernel-level code (e.g., linked lists, binary search, memory allocators)

Key Technique

Verification Conditions are logical formulas generated by tools like Why3 from annotated source code. When you write a C function with ACSL annotations (preconditions via requires, postconditions via ensures, loop invariants via loop invariant), Frama-C and Why3 decompose correctness into individual proof obligations. Each VC encodes one specific claim: "if the precondition holds and the loop invariant held before this iteration, then the invariant holds after the iteration" or "array access index is within bounds." ATPs handle many VCs automatically, but real-world projects (Linux kernel, Contiki-OS) produce VCs that ATPs cannot solve -- these are the targets.

The NTP4VC pipeline works as follows: Why3's VC generator produces an XML AST representation of each obligation. A translation layer (approximately 2,400 expert-written rewriting rules) maps these ASTs into Isabelle, Lean 4, or Rocq syntax. This handles prefix/infix conversions, if-then-else desugaring, match-case translation, and semantic rewrites (e.g., integer operations to natural number operations preferred by ITPs). The resulting ITP file contains the VC as a lemma or theorem statement with all necessary type definitions and previously-proved lemmas in scope.

Critical finding from NTP4VC: Tactic-based step-by-step proofs dramatically outperform whole-proof-term generation. The most effective approach is to decompose VCs into subgoals using structural tactics (intro, cases, simp, omega) before applying domain-specific automation. Error analysis shows three dominant failure modes: syntactic errors (24%+ of Isabelle attempts), semantic confusion with repetitive meaningless tactics (64%+ of some model outputs), and hallucinated tactics that do not exist in the target ITP. Avoiding these failure modes is the primary skill.

Step-by-Step Workflow

1. Identify the VC structure. Parse the verification condition to determine: (a) what quantified variables exist, (b) what hypotheses are assumed, (c) what the goal statement is. Separate preconditions from the proof obligation itself. Identify whether the VC concerns arithmetic bounds, pointer validity, functional correctness, or invariant preservation.

2. Choose the target ITP and set up the proof environment. Determine whether the user needs Isabelle (.thy), Lean 4 (.lean), or Rocq (.v). Set up the theory/import header with required libraries:

   • Isabelle: theory VCProof imports Main with relevant Int, List, or Array theories
   • Lean 4: import Mathlib.Tactic plus domain-specific imports
   • Rocq: Require Import Lia ZArith List as baseline

3. Translate the VC into a formal statement. Convert the logical formula into the target ITP's syntax. Apply rewriting rules: map Why3 integer division to ITP-native div, convert array access notation, handle bitvector operations for kernel code. Preserve all quantifier structure exactly.

4. Decompose the proof into subgoals. Use structural tactics first:

   • Introduce universally quantified variables and hypotheses (intros, intro, fix)
   • Case-split on disjunctions or conditional expressions (cases, split, destruct)
   • Simplify with definitional unfolding (simp, unfold, simpl)

5. Apply arithmetic automation to leaf goals. For integer/natural number arithmetic subgoals, use the strongest available automation:

   • Isabelle: sledgehammer first, then arith, linarith, auto
   • Lean 4: omega, linarith, norm_num, simp [*]
   • Rocq: lia, omega, ring, auto with zarith

Concrete Examples

Example 1: Loop invariant preservation for binary search

User: "I have this Why3 VC from a binary search. Prove it in Lean 4."

-- VC: If 0 <= lo <= hi <= arr.size and arr is sorted,
-- then after mid = (lo + hi) / 2 and lo' = mid + 1,
-- we have 0 <= lo' <= hi <= arr.size

Approach:

1. Identify this as an arithmetic bounds VC with integer division
2. Set up Lean 4 with import Mathlib.Tactic
3. Formalize and prove with omega after introducing hypotheses

Output:

import Mathlib.Tactic

theorem binary_search_invariant_preservation
    (lo hi size : Nat)
    (h_lo_nn : 0 ≤ lo)
    (h_lo_hi : lo ≤ hi)
    (h_hi_sz : hi ≤ size)
    (h_lo_lt_hi : lo < hi)  -- loop guard
    (mid : Nat)
    (h_mid : mid = (lo + hi) / 2)
    (lo' : Nat)
    (h_lo' : lo' = mid + 1) :
    0 ≤ lo' ∧ lo' ≤ hi ∧ hi ≤ size := by
  constructor
  · omega
  constructor
  · omega
  · omega

Verify with: lake env lean BinarySearchVC.lean

Example 2: Array access bounds from Frama-C/Why3

User: "Prove this Isabelle VC: accessing buf[i] is safe when 0 <= i and i < length buf."

Approach:

1. Identify as a memory safety VC (array bounds check)
2. Formalize in Isabelle with list-based array modeling
3. Apply auto with list library lemmas

Output:

theory BufAccess
  imports Main
begin

lemma buf_access_safe:
  assumes "0 ≤ i" and "i < length buf"
  shows "i < length buf"
  using assms by simp

lemma buf_access_nth_defined:
  assumes "0 ≤ (i :: nat)" and "i < length buf"
  shows "buf ! i = buf ! i"
  by simp

end

Verify with: isabelle build -d . -b BufAccess

Example 3: Postcondition proof for a swap function in Rocq

User: "I need to prove that after swapping a[i] and a[j], the value at position i equals the old value at j. The VC comes from Frama-C."

Approach:

1. Model array as a function with pointwise update
2. Prove the store/select property: reading index i after storing at i returns the stored value
3. Use Rocq functional array axioms

Output:

Require Import ZArith Lia.

(* Array modeled as Z -> Z with pointwise update *)
Definition store (a : Z -> Z) (idx val : Z) : Z -> Z :=
  fun k => if Z.eq_dec k idx then val else a k.

Theorem swap_postcondition :
  forall (a : Z -> Z) (i j : Z),
    i <> j ->
    let a1 := store a i (a j) in
    let a2 := store a1 j (a i) in
    a2 i = a j.
Proof.
  intros a i j Hneq.
  unfold store. simpl.
  destruct (Z.eq_dec i j) as [Heq | _].
  - contradiction.
  - destruct (Z.eq_dec i i) as [_ | Habs].
    + reflexivity.
    + exfalso. apply Habs. reflexivity.
Qed.

Verify with: coqc SwapVC.v

Best Practices

Do:

• Always decompose VCs into subgoals with intros/cases/split before applying automation. This mirrors how successful proofs are structured and avoids the "repetitive meaningless tactic" failure mode.
• Prefer omega/lia/linarith for linear arithmetic goals -- these are decision procedures that either succeed or definitively fail, giving clear signal.
• Include all necessary hypotheses in the formal statement. VCs from Why3 often carry many preconditions; dropping any one can make the goal unprovable.
• State the exact ITP version. Tactic behavior differs across versions (Lean 4.21 vs 4.10, Rocq 8.20 vs 8.18).

Avoid:

• Never generate a single monolithic tactic like auto or simp as the entire proof for non-trivial VCs. If it were that simple, the ATP would have already solved it.
• Never invent tactic names. Common hallucinations include why3, verify, blast (in Lean), or program_simpl without the right imports. Only use tactics you are certain exist.
• Never use sorry, admit, or Admitted without explicitly telling the user the proof is incomplete. Mark each unfinished subgoal clearly.
• Never assume integer and natural number operations are interchangeable. Why3 uses mathematical integers; ITPs often default to natural numbers. Insert explicit coercions (Int.toNat, Z.of_nat) where types differ.

Error Handling

Error	Cause	Fix
"unknown tactic"	Hallucinated tactic name	Check the tactic exists in the target ITP version; replace with a known equivalent
"type mismatch" in goal	Integer vs natural number confusion	Add explicit type annotations and coercions at the VC formalization step
Tactic succeeds but proof doesn't close	Remaining subgoals after auto/simp	Use · (Lean) or - (Isabelle/Rocq) to focus on remaining goals; decompose further
"timeout" during proof check	Proof search space too large	Replace auto with more directed tactics; provide explicit lemma names to apply
Mismatched parentheses / syntax error	Translation artifacts from AST mapping	Re-check bracket nesting; Isabelle uses ‹ › for fact references, not < >
"sorry is not allowed"	Incomplete proof submitted to strict checker	Identify which subgoal is unsolved; attempt targeted automation or ask user for hints about the domain

Limitations

• Non-linear arithmetic: VCs involving multiplication of variables, modular arithmetic, or bitwise operations are beyond the reach of omega/lia. These require manual lemma construction or specialized tactics (nlinarith in Lean, nia in Rocq), which have low success rates.
• Heap reasoning: VCs about pointer structures (linked lists, trees) require separation logic or custom heap models. Standard ITP tactics do not handle these natively; the user needs a framework like Iris (Rocq/Lean) or AutoCorres (Isabelle).
• Scale: NTP4VC shows even the best models achieve only ~6-18% pass rates on industrial VCs. For genuinely hard VCs (those ATPs already failed on), expect to provide proof sketches that need human refinement rather than complete proofs.
• Library dependence: Proofs often depend on specific Mathlib (Lean), AFP (Isabelle), or Coq-stdlib lemmas. If the user's project uses a different library version or custom theories, generated proofs may not compile without adaptation.
• Why3 translation fidelity: The 2,400-rule translation from Why3 ASTs to ITP syntax is imperfect. Some Why3 constructs (algebraic types with refinements, ghost code) may not map cleanly, requiring manual fixup of the VC statement itself.

Reference

Paper: Neural Theorem Proving for Verification Conditions: A Real-World Benchmark (ICLR 2026) Key takeaway: The NTP4VC benchmark of 600 real-world VCs from Linux/Contiki-OS shows that LLMs achieve 1.5-12% pass@8 rates vs. 18% for Sledgehammer, with tactic-based decomposition and arithmetic decision procedures being the most reliable proof strategy. Focus on structured subgoal decomposition and avoid whole-proof generation.