Blame for code/docs/research/BUGFINDING_LIT_REVIEW.md

# Finding real software bugs with LLM theorem provers and LLM-driven formal verification: a literature review

Status: L1 review, 2026-10-14. Target application of the `align` prover (Goedel-Prover-V2-8B, strict Lean verifier, 4x A10G).
Vault tag: `leanstral-bugfinding` (hyperresearch, `/apps/development/rlhf/research/notes/`).

## 0. Method, scope and honesty notes

Question: how can LLM theorem provers and LLM-driven formal verification (Lean 4, Dafny, Verus, Coq, Isabelle) be used to find real bugs in software, and which training recipes, benchmarks and evaluation protocols exist?

Procedure (condensed lit-review mode, not a full PRISMA run): the `academic-research-skills:deep-research` skill was loaded, but its 13-agent pipeline needs a subagent tool that this session does not have, so the steps were carried out by hand. About 35 hyperresearch `scholar search` queries (OpenAlex, Crossref, CORE and others) were run, then each primary source was fetched with `hyperresearch fetch` and its text read from the vault note. The numbers below were read from those note bodies, not recalled. Where a number comes from a paper's abstract rather than a table I read, it is cited as "abstract".

What was NOT verified, and why:

| Item | Status |
|---|---|
| Vostd/Asterinas Verus spec-failure case study (doi 10.1145/3832783.3834504) | Publisher bot wall; known only from search metadata. Not used for any number. |
| AutoACSL (2606.20969), HarnessLLM, Safe4U, KaPilot, CheckerBench (2610.07557), SpecMind (2602.20610) | Appeared in searches; not fetched in full. Verification pass: the arXiv ids of AutoACSL, CheckerBench and SpecMind resolve to those titles, and CheckerBench's abstract numbers are used in one table row and in RQ2. The others are not used for numbers. |
| Primary-source check | All 35 arXiv ids in the references were re-fetched from arxiv.org in the verification pass; each resolves to the cited title. Abstract-level numbers in the methods table were compared with the live abstracts; the corrections are listed in the status notes above and inline. |
| Coq and Isabelle | Searches returned almost no LLM bug-finding work in either. The only Coq evidence is Vero's Coq-origin instances and Leanstral's Rocq-to-Lean case study. This is a coverage gap in this review, not evidence that none exists. |
| Several 2026 arXiv ids (26xx.xxxxx) | Fetched from arxiv.org and read as given. The review does not cross-check them against other venues. |
| Rust-Prover paper (2610.03994) | Model names ("Claude Opus 5.5" and others) and costs are the paper's own statements. Single-source. |
| Leanstral 1.5 numbers | From Mistral's own launch post and technical report (vendor claims, not peer reviewed; the report is a PDF on GitHub, `mistralai/LeanstralSafeVerify`, not on arXiv). Verification pass: the blog says "11 pointing to genuine bugs, 5 of them previously unreported"; the technical report (section 4.2) is clearer: 47 flags, 11 genuine, and "since some properties failed because of the same root cause, this corresponded to 5 bugs, which were all previously unreported". This review originally read the blog as 11 bugs, 5 new; that was wrong and is corrected below. Availability: Mistral's own model card (fetched 12 Oct 2026) marks `labs-leanstral-1-5` Deprecated with deprecation date 9/29/2026, which is already past on the review date (14 Oct 2026). A third-party note says 30 Sep. So the hosted API should be treated as unavailable or going away; the Apache-2.0 weights are on Hugging Face. |
| Rust-Prover (2610.03994) versions | arXiv shows v1 and v2. The numbers in the methods table were read from the vault copy (v1). The current abstract (v2) differs: 1259 of 1325 theorems proved in one run under 32 h, median 3.2 min and $1.17 per proof, 70% on the first iteration, 21,413 test cases. Both are given in the table. |
| Venue labels (AutoSpec LNCS 2024, SpecGen ICSE'25, Clover CAV'24, fuzz-driver ISSTA'24) | Not shown in the fetched text or the arXiv comments field. They come from the reviewer's background knowledge and were not re-checked. Venue labels for KNighter (SOSP 2025), VeriSoftBench (COLM 2026), nl2postcond (FSE 2024), SAFE and IRIS (ICLR 2025), CLEVER (NeurIPS 2025 D&B) and VERINA (ICLR 2026) were seen in the fetched text or the arXiv comments. |

Citation convention: arXiv id plus the abstract or the table/section where the figure was read. Section numbers are given only where the fetched text shows them.

## 1. Taxonomy

Axis A is what the LLM produces. Axis B is what counts as a "found bug". The key observation is that *proof* is rarely what finds the bug; a failed proof is only weak evidence. The bug-finding signal comes from one of three different oracles (listed below the table).

| Class | LLM role | Verifier role | What counts as a found bug | Examples |
|---|---|---|---|---|
| S. Spec synthesis | writes pre/post/invariants | checks spec is satisfiable and the code meets it | Spec fails on code (violation), or spec disagrees with docstring | AutoSpec, SpecGen, nl2postcond, NL2Contract |
| C. Consistency checking | writes code, spec, doc; cross-checks | proves spec-code and spec-doc agreement | Mismatch flagged between independent artifacts | Clover |
| P. Property proving / disproving | writes proof of property, or of its negation | kernel/SMT accepts proof | Proof of the negation of a plausible property (a verified counterexample) | Leanstral 1.5 Aeneas pipeline, Vero audit |
| V. Verified code generation | writes code + spec + proof | accepts or rejects | Not bug finding; produces bug-free-by-construction code. Also yields bugs in benchmarks | AlphaVerus, SAFE, VERINA, CLEVER, FVAPPS, DafnyBench, miniCodeProps, VeruSyn |
| R. Counterexample-guided repair | reads counterexamples to fix proofs or specs | produces counterexample | Counterexample to a candidate invariant or proof | ExVerus, Vero audit |
| N. Proof-free baselines | reads code / writes checkers / drivers | static analysis, fuzzer, symbolic execution, concrete replay | Crash, sanitizer hit, confirmed CVE | Big Sleep, IRIS, KNighter, Sailor, LLM fuzz drivers |

Three distinct bug oracles follow from this:

1. A kernel- or SMT-checked disproof (class P). The finding is sound given the spec and the code-to-logic translation.
2. A dynamically reproduced failure (class N, and class S when the postcondition is executable). Sound given the test harness.
3. A cross-artifact inconsistency (class C). No ground truth is needed, but the finding can be a defect in any of the three artifacts.

Every class has an unverified link: the spec is the one component the verifier cannot check against intent (section 5).

## 2. Methods table

Language = target language of the *software*. "Found bug" is the paper's own criterion. All numbers are as reported.

| Method (arXiv / venue) | Language, verifier | What counts as a found bug | Benchmark | Reported numbers (source) |
|---|---|---|---|---|
| AutoSpec (2404.00762, LNCS 2024) | C, Frama-C WP | Not a bug finder; synthesises specs that give a full proof | 4 benchmarks, 251 programs; X509-parser | Verifies 79% of programs, 1.592x over prior work; six X509 functions specified in minutes (abstract, intro) |
| SpecGen (2401.08807, ICSE'25) | Java, OpenJML | Not a bug finder; verifiable specs | SV-COMP Java + 120 hand-built programs | Verifiable specs for 279 of 385 programs; beats Houdini and Daikon (abstract) |
| nl2postcond (2310.01831, FSE'24) | Python/Java, run-time assertions | Postcondition violated by a buggy mutant or a real historical bug | EvalPlus (164 problems), Defects4J | GPT-4 accept@1 0.63-0.77; correct postconditions discriminate up to 81% of buggy programs on average (EvalPlus); on Defects4J the postconditions discriminate 70 buggy methods belonging to 64 known historical bugs, 12.2% of the bugs considered (abstract; intro; conclusion). These are known, already-fixed bugs, so this is discriminative power, not new-bug discovery. Table 2 of the paper is the EvalPlus bug-completeness table, not this result |
| NL2Contract (2510.12702) | Python, software verifier | Contract rejects buggy implementation, accepts reference | HumanEval-derived tasks | LLM verification soundness@1 66.7-81.1%, @5 87.9-88.7%, @10 90.0-93.9%; test-set correctness does not imply verification soundness (contributions section) |
| Clover (2310.17807, CAV'24) | Dafny | Inconsistency among code, docstring, annotations | CloverBench; MBPP-DFY-50 | Up to 87% acceptance of correct instances, zero false positives on adversarial incorrect ones; 6 incorrect programs found in MBPP-DFY-50 (abstract) |
| AlphaVerus (2412.06176) | Rust/Verus | Not a bug finder; verified code | HumanEval-Verus, MBPP-Verus | Table 2, pass@256: GPT-4o 27.1% / 35.9%; Llama-3.1-70B base 11.8% / 26.9%; AlphaVerus exploration 27.1% / 59.1%, plus Treefinement 32.9% / 65.7% |
| SAFE (2410.15756, ICLR'25) | Rust/Verus | Not a bug finder; proofs | VerusBench (human specs), CodeNet-Test | Abstract: 52.52% vs GPT-4o 14.39% on a human-expert benchmark. Intro: DeepSeekCoder reaches 43.17% / 43.83% direct, 79.14% VerusBench with self-debugging, vs GPT-4o 11.51% / 0.28% |
| VeruSyn (2602.04910) | Rust/Verus | Not a bug finder; data | VeruSAGE-Bench (560 of 849 tasks fit the model's context), VerusBench, HumanEval, MBPP | 6.9M synthesized verified programs; Qwen2.5-Coder-32B-Instruct fine-tuned with VeruSyn data scores 39% (Accuracy@100, no debugging) and 49% (Accuracy@600, 5 debugging rounds) on VeruSAGE-Bench, vs 10% / 19% for the raw model, 11% / 15% with AlphaVerus data and 6% / 11% with SAFE data; Claude Sonnet 4.5 scores 46% / 54% on the same table (Table 1, "Total (560)" column) |
| VeruSAGE (2512.18436) | Rust/Verus | Not a bug finder; agentic proofs | VeruSAGE-Bench, 849 tasks from 8 Verus systems | Best LLM-agent combo completes over 80%; over 90% of a set of tasks human experts had not finished (abstract) |
| ExVerus (2603.25810) | Rust/Verus | Counterexample to a failing proof/invariant, used to repair | VerusBench, DafnyBench, LCBench, HumanEval | Outperforms AutoVerus by 60.92% on average on VerusBench (section 4.2; the text does not say whether relative or percentage points); solves about 2x (LCBench) and 1.5x (HumanEval) as many tasks; the two tools are complementary, each solving tasks the other does not (appendix H). AutoVerus was run on a newer Verus than it was built for and is stated to degrade (footnote 3) |
| DafnyBench (2406.08467) | Dafny | Not a bug finder; hint generation | 750+ programs, ~53,000 lines | Best 68%; success falls with required code and hints; "solved" forbids edits to requires/ensures, `{:verify false}` and `assume false` (abstract, intro) |
| dafny-annotator (2411.15143) | Dafny | n/a | DafnyBench test split | Llama-3.1 8B greedy 15.7%; fine-tuned on DafnyBench + DafnySynth 50.6% (abstract) |
| DafnyPro (2601.05385) | Dafny | n/a | Clover, MBPP-Dafny, HumanEval-Dafny, DafnyBench | Sonnet 3.5 + DafnyPro 86% on DafnyBench (+16pp); fine-tuned Qwen 7B/14B 68%/70% (abstract) |
| RLVR in Dafny thesis (2605.30914) | Dafny, Lean | n/a | APPS-derived Dafny, VERINA | GRPO verified reward 2.2% -> 58.1% but with specification hacking; after filtering underspecified tasks, multi-turn RLVR 9.7% -> 31.1% (abstract) |
| FVAPPS (2502.05714) | Lean 4 | n/a | 4715 samples, 1083 curated; 406 theorems of 100 samples evaluated | Sonnet proves 30%, Gemini 18% (abstract) |
| miniCodeProps (2406.11915) | Lean 4 | n/a | 201 specs on lists, nats, trees | SOTA provers do well on easy, fail nearly all medium and hard (abstract) |
| CLEVER (2505.13938, NeurIPS D&B'25) | Lean 4 | n/a | 161 problems, spec-matching + implementation | Few-shot frontier LLMs solve at most 1 of 161 end-to-end (introduction) |
| VERINA (2505.23135, ICLR'26) | Lean 4 | n/a | 189 tasks | Best model o3: 72.6% code, 52.3% spec soundness and completeness, 4.9% proof, one trial per task (abstract) |
| VERINA+ / VeriScale (2605.22368) | Lean 4 | Adversarial implementations used to expose weak specs | VERINA with 83x larger test suites | Sharp score drops on SpecGen and CodeGen tasks vs original VERINA (abstract; magnitude not extracted) |
| WybeCoder (2603.29088) | Lean 4 + SMT, imperative | n/a | Verina and Clever translated to imperative specs | Solves 74% of Verina and 62% of Clever tasks at moderate compute (abstract) |
| AlgoVeri (2602.09464) | Dafny / Verus / Lean | n/a | 77 classical algorithms, identical contracts | Gemini-3 Flash: Dafny 40.3%, Verus 24.7%, Lean 7.8% (abstract) |
| VeriContest (2605.08553) | Rust/Verus | n/a | 946 problems | Best model: NL-to-code 92.18%, spec generation 48.31%, proofs 13.95%, end-to-end 5.29% (abstract) |
| Rust-Prover on VeriContest (2610.03994) | Rust -> Lean 4 | Specs restated and checked against test suites | 1007 problems, 1325 theorems | v1 (vault copy): all 1325 theorems proved by Claude Opus 5.5 in about 35 h, median 3.4 min and $1.20 per proof, 71% accepted at first check, translated Lean programs matched Rust output on 19,555 tests. v2 (current arXiv abstract): 1259 of 1325 in one run under 32 h, median 3.2 min and $1.17, 70% on the first iteration, 21,413 tests; all 1325 proved overall. Note it counts 1007 problems where the VeriContest abstract says 946 (benchmark was apparently extended; not reconciled here) |
| Verus-SpecGym (2605.26457) | Rust/Verus | Spec fails an executed official test or a Codeforces "hack" case | 581 spec-writing tasks | Best model 77.8%, other frontier 51.1-57.8%, open-source 21.5-25.5%; LLM-as-judge misses 26% of failures the executable check catches (abstract) |
| VeriSoftBench (2602.18307, COLM'26) | Lean 4 | n/a | 500 repository-context obligations | Mathlib-tuned provers transfer poorly; success falls with transitive dependency closure (abstract) |
| FVSpec (2606.01008) | Python -> Lean 4 specs | n/a | 7,413 property-based tests scraped; 2,623 (35%) translated to 9,415 Lean specs | Baselines for proof generation (abstract; numbers not extracted) |
| Vero (2608.13522) | Lean 4 repos from Python/Dafny/Verus/Coq | Formal proof that a spec is unsatisfiable or reference code is wrong | 43 multi-module instances | Strongest agent fully solves 27/43; audit mechanism surfaced latent spec and code errors missed by manual review (abstract, intro) |
| Aeneas/Rust-to-Lean experience report (2605.30106) | Rust -> Lean 4 | n/a (proofs of crypto primitives) | Plonky3, RISC Zero | AI provers closed two previously `sorry`-ed bounds; toolchain drift across Lean versions is a stated obstacle (abstract) |
| SymCrypt + Aeneas (2609.15648) | Rust -> Lean 4 | Safety, panic-freedom, functional correctness | 16.7 KLOC Rust | 237 KLOC Lean development; agents write proofs, kernel verifies (abstract) |
| C-to-Lean trust ledger (2609.38237) | C -> Lean 4 | n/a | SQLite, 8,602 functions | 60.7% hole-free, only 24.8% call-closed; found a translation that succeeded with a wrong result (abstract) |
| **Leanstral 1.5** (Mistral blog and technical report PDF, 2 Jul 2026; no arXiv) | Rust -> Lean 4 via Aeneas | Property whose negation the model proves (4 attempts x 30 turns to prove, then negation); triaged by the authors, method not described | 57 Rust repos translated by Aeneas | 47 flags, 11 of them genuine, which are 5 distinct root-cause bugs, all previously unreported on GitHub (tech report section 4.2; the blog's wording "11 genuine bugs, 5 of them previously unreported" is looser). The other 36 flags were properties "too strong (for instance failing because of a state that was unreachable from the public interface) or malformed", no counts given. Example: zigzag `sign` overflow at `u64::MAX` in `datrs/varinteger`. The report's footnote 4 says Claude, given that repository and asked to identify bugs, also caught it |
| Big Sleep (Project Zero blog, Oct 2024) | C, none (agent + debugger) | Exploitable crash reproduced | SQLite recent commits | One real stack buffer underflow in SQLite (Gemini 1.5 Pro agent) found by variant analysis from commit diffs; missed by OSS-Fuzz and SQLite's own testing. The post's own explanation for the miss in the worked example is harness configuration: the OSS-Fuzz harness is not built with the `generate_series` extension enabled. No rate reported (blog) |
| IRIS (2405.17238, ICLR'25) | Java, CodeQL + LLM | Taint path to sink matching a CWE | CWE-Bench-Java, 120 vulnerabilities | CodeQL 27; IRIS+GPT-4 55 (+28); false discovery rate 5pp better; 4 previously unknown vulnerabilities (abstract) |
| KNighter (2503.09002, SOSP'25) | C (Linux kernel), Clang Static Analyzer | Checker warning confirmed by maintainers | Linux kernel | 92 new bugs (average 4.3 years latent); 77 confirmed, 57 fixed, 30 CVEs (abstract) |
| Sailor (2604.06506) | C/C++, symbolic execution + concrete replay | Crash replayed on unmodified source | 10 projects, 6.8M lines | 379 new memory-safety vulnerabilities, 421 confirmed crashes; the strongest of five baselines (agentic detection with Claude Code, full codebase access) found only 12; without static-analysis targeting confirmed vulnerabilities drop 12.2x; without iterative LLM synthesis none are confirmed (abstract) |
| CheckerBench (2610.07557; abstract only, not fetched in full) | 5 language ecosystems, vulnerable and fixed revisions | Checker that fires on the vulnerable revision and not the fixed one | 300 tasks from 297 CVEs, 167 repositories, 85 CWEs | Mean Pass@1 32.30% across 21 model-harness configurations, best 45.33% (abstract). Same pre-fix/post-fix gold label that RQ2 uses |
| LLM fuzz-driver study (2307.12469, ISSTA'24) | C, libFuzzer | Fuzzing coverage and crashes | 86 questions, 30 C projects | 736,430 generated drivers, 0.85 billion tokens ($8,000+ charged), 3.75 CPU-years of fuzzing; LLM drivers on par with industry drivers in fuzzing outcome; "promising but obstacles remain" (abstract) |

## 3. What the evidence says

### 3.1 The only proof-based, LLM-driven, real-codebase bug-finding result is vendor-reported and has a low-precision funnel

Leanstral 1.5 is the sole item in this review where a prover-class model finds previously unknown bugs in real repositories through a prove-or-disprove loop. The funnel (technical report section 4.2, a Mistral PDF; the blog is shorter): Aeneas translates Rust to Lean; the model infers the programmer's intent and writes properties; it gets 4 attempts of 30 turns each to prove a property; if all fail, it tries to prove the negation, and a proved negation flags a potential bug. Reported yield: 57 repositories, 47 flags, 11 flags that genuinely pointed to bugs, and because several flags shared a root cause, 5 distinct bugs, all previously unreported on GitHub.

Two precision figures follow, both my arithmetic from the report's counts. Per flag: 11/47 = 23%. Per distinct bug: 5/47 = 11%, which is the number that matters if a maintainer must triage one report per root cause. The other 36 flags are described qualitatively only: properties that were "too strong (for instance failing because of a state that was unreachable from the public interface) or malformed". So the dominant false-alarm class is an over-strong property, which is the same failure NL2Contract reports for postcondition-only specifications (verifiers flag invalid inputs; adding inferred preconditions reduces false alarms, 2510.12702 abstract). A property gate therefore has an existing, named target: reachability and input-precondition constraints. The report gives no split of the 36 by class, no repository list, and no description of how "genuine" was decided.

The report is candid about two things this review should not overstate. It says a rigorous comparison with testing, fuzzing or simply asking an LLM is future work, and its footnote 4 says Claude, given the `datrs/varinteger` repository and asked for potential bugs, caught the `sign` overflow. The blog's statement that testing and fuzzing "would typically miss" it is therefore the vendor's expectation, not a measured result, and a `u64::MAX` operand is a classic boundary value that fuzzers with interesting-value dictionaries do try. What the disproof adds over an LLM bug report is a kernel-checked witness (`sign core.num.U64.MAX = fail integerOverflow`, proved by `rfl`), not necessarily recall.

### 3.2 Proof is the bottleneck for small and mid-size models, but the bottleneck is moving

On Lean, proof success is low in 2025 benchmarks (VERINA proof 4.9%, CLEVER at most 1/161, miniCodeProps medium and hard nearly all failed, FVAPPS 18-30%). On Verus, VeriContest proof generation is 13.95% for the best model, yet VeruSAGE reports over 80% on system-verification tasks with agents. The Rust-Prover report claims every theorem in VeriContest closes when the specification is restated and proved in Lean with a frontier agent. Taken together, proof search is becoming cheap for frontier agents given an agentic scaffold, and the open problems are specification fidelity (Verus-SpecGym: even best model at 77.8%) and translation fidelity (C-to-Lean ledger: 24.8% call-closed).

### 3.3 Training recipes that exist for provers on code

| Recipe | Mechanism | Reported effect | Risk named by authors |
|---|---|---|---|
| Self-evolving synthesis (SAFE 2410.15756) | Synthesise specs and proofs, verifier filters, fine-tune; reuse failed proofs for self-debugging | 52.52% vs 14.39% GPT-4o (abstract) | Spec quality of synthesised data |
| Cross-language translation + tree search (AlphaVerus 2412.06176) | Dafny-to-Verus translation, Treefinement, critique model filters misaligned specs | Table 2 above | Reward hacking via trivial specs or verifier limitations (intro) |
| Mass synthesis plus agent trajectories (VeruSyn 2602.04910) | 6.9M programs; long-CoT data from agents | 32B model competitive with commercial models at lower cost | Single-source |
| Open-ended synthesis (dafny-annotator 2411.15143) | LLM proposes programs, Dafny validates | 15.7% -> 50.6% for an 8B model | None beyond data scarcity |
| Inference-time scaffolds (DafnyPro 2601.05385) | diff-checker blocks edits to program logic; pruner; hint library | 86% DafnyBench | Models silently alter the base code to pass |
| RLVR with GRPO (2605.30914) | Verifier score as reward, multi-turn | 2.2% -> 58.1% verified reward, then 9.7% -> 31.1% after filtering | Specification hacking before filtering |
| Counterexample-guided repair (ExVerus 2603.25810) | Counterexamples explain proof failure | Large gains over AutoVerus on VerusBench | Weaker on hard tasks needing more invariants |
| Production RL (Leanstral 1.5, blog and technical report) | Mid-training, SFT, CISPO RL; RL mix 50% LeanGym-PR, 20% LeanGym single-theorem, 30% prove-or-disprove multiturn (report section 2.2); the multiturn env asks the model to prove a theorem or its negation, full reward if the proof compiles and passes an axiom check; final check by a SafeVerify fork extended to check negations | PutnamBench 587/672 at 4M-token budget; FLTEval pass@1 21.9 -> 28.9 | Vendor-reported; no ablation of the disprove branch is published; the disprove statements are competition problems, not code properties |

Note on what is and is not covered. Leanstral does train on negation proofs: 30% of its RL mix is a prove-or-disprove environment, and the verifier was extended to check negations. What no retrieved source reports is (a) disproof training on code properties rather than competition statements, (b) a reward shaped for bug yield or for a concrete witness, or (c) an ablation of the disprove branch. An earlier version of this review said no recipe trained on negations at all; that was wrong, and the novelty claim of RQ1 below is narrowed accordingly.

### 3.4 Proof-free baselines set the yield bar

| Baseline | Yield | Cost signal |
|---|---|---|
| KNighter | 92 new Linux kernel bugs, 30 CVEs | One LLM synthesis pass per bug pattern; checkers then run cheaply at scale |
| Sailor | 379 new memory-safety bugs on 6.8M lines; best agentic-LLM baseline (Claude Code, full access) found 12 | Needs a concrete-replay filter; the paper reports that dropping iterative LLM synthesis leaves zero confirmed |
| IRIS | 55/120 vs CodeQL 27/120 on CWE-Bench-Java | Whole-repository taint reasoning |
| Big Sleep | One serious SQLite bug | Variant analysis from a fixed-bug diff; the post attributes the fuzzers' miss in its worked example to a harness that lacked the relevant extension |

These produce more bugs than the prover-based pipeline at the scale reported, and each has an execution- or analysis-based confirmation step. Sailor's baseline row is also the clearest evidence in the corpus that an LLM agent alone, without a verifier or replay stage, finds far fewer bugs at scale (12 versus 379), which supports adding a verification stage but does not compare a prover against fuzzing. A prover pipeline should be compared against them, and, more usefully, composed with them: the Sailor design (static analysis nominates sites; LLM builds the harness; concrete replay validates) is exactly the shape a "prover nominates, execution confirms" pipeline would have.

## 4. Counterexample-guided and cross-check approaches

- ExVerus: produce a counterexample from the failed proof, feed it back, repair. The counterexample is a concrete input violating a candidate invariant. It targets proof repair, but the same artefact is a bug witness when the spec is right.
- Leanstral: failed proof, then proof of the negation. Formal, but the negation's truth depends on the Aeneas model.
- Vero: lets agents prove a spec unsatisfiable or a reference implementation incorrect; this found latent errors that manual review missed. This is a direct precedent for using prover agents to find *benchmark* bugs.
- Clover: three-way consistency (code, docstring, annotations). Zero false positives on adversarial incorrect programs at 87% acceptance, and 6 incorrect programs in a human-written dataset. The number is small, but the protocol gives a no-ground-truth way to test a spec.
- nl2postcond / NL2Contract: docstring to executable postcondition, tested against buggy mutants and real historical bugs (70 buggy methods from 64 known Defects4J bugs; already known and fixed, so this measures discrimination, not discovery). NL2Contract adds the point that matters for precision: postconditions without preconditions make verifiers report false alarms on invalid inputs, and inferred preconditions reduce them (2510.12702 abstract). That is the same failure as Leanstral's "properties that were too strong".
- Verus-SpecGym: executable specs (`exec_spec`) checked against official tests and adversarial "hack" cases. A spec that rejects a valid test output or accepts a hack case is wrong. This is the cheapest oracle found for the weakest link.

## 5. Threats to validity

| Threat | Evidence in the corpus | Mitigation in the literature |
|---|---|---|
| Wrong, weak or vacuous spec | CLEVER designs around specs that "leak implementation logic or allow vacuous solutions"; RLVR thesis: verified reward 2.2% -> 58.1% with specification hacking; Verus-SpecGym: generated specs "omit important input assumptions, accept incorrect outputs, reject valid ones" | Held-out ground-truth specs (CLEVER); test-suite scaling (VeriScale: 83x); adversarial implementations; executable spec checks |
| Spec is right but over-strong, so "disproof" is a false alarm | Leanstral funnel: 11/47 flags genuine, 5 distinct bugs; the rest "too strong" (state unreachable from the public interface) or malformed; NL2Contract: missing preconditions cause false alarms | Human triage (Leanstral); inferred preconditions (NL2Contract); not systematically solved |
| LLM judge of specs is unreliable | Verus-SpecGym: judge misses 26% of failures that the executable check catches | Execution-based evaluators |
| Prover edits the program instead of proving it | DafnyPro Fig. 2, DafnyBench rules forbid `{:verify false}`, `assume false`, edits to requires/ensures | diff-checker; forbidding escape hatches; SafeVerify-style final checks (Leanstral) |
| Verifier unsoundness or toolchain gaps | AlphaVerus names "verifier limitations that cause trivial programs to pass" | Lean kernel check; critique filtering; ceiling tests |
| Translation to the logic is wrong (silent) | C-to-Lean ledger: a translation that "succeeded with an incorrect result"; 24.8% of translated functions are call-closed | Execution check of translated code against tests (Rust-Prover: 19,555 test cases matched in v1, 21,413 in v2) |
| Test-based benchmarks overestimate | VeriScale: larger suites give sharp drops | Larger and adversarial suites |
| "Test-set correct" is not "verification sound" | NL2Contract | Verify, not only test |
| Benchmark errors | Vero audit; Clover found 6 incorrect programs in MBPP-DFY-50 | Prover-assisted audit |
| Data contamination | Not systematically studied in the retrieved corpus | Not covered here; open |
| No comparison to fuzzing on the same targets | Leanstral post has none and its report calls the comparison future work; Big Sleep notes OSS-Fuzz missed its bug, attributing it in the worked example to a harness without the relevant extension | A paired experiment (RQ2) |

Pre-registration implication: any bug-finding claim should report (a) how many flagged findings were human-triaged and by whom, (b) the split of false alarms between wrong spec, wrong translation and intended behaviour, (c) a fuzzing or static-analysis baseline on the same targets with the same budget.

## 6. Gaps a small 8B prover on 4x A10G could fill

Constraints from this repository: Goedel-Prover-V2-8B in bf16 (about 16 GB of weights; one A10G is 23 GB, so KV cache is the limit), Lean pinned at 4.9.0-rc1 with a June 2024 Mathlib (`docs/LEAN_VERIFIER.md`), a strict verifier with measured ceiling (177/178 known-good accepted, 0/61 adversarial accepted), at most 2 Lean workers while the other jobs run. Leanstral 1.5 itself is a 119B-parameter model (6B to 6.5B active): about 238 GB of weights in bf16 and about 119 GB at 8 bits, against 4 x 23 GB = 92 GB of A10G memory, and its Hugging Face card gives `--tensor-parallel-size 4` and a 200k context for larger GPUs. It does not fit this box without aggressive quantisation (about 60 GB at 4 bits, leaving little for a long KV cache; not tested), so it is not a like-for-like local competitor. Its hosted API is deprecated (section 0).

1. **Spec-first yield, not proof strength.** Frontier agents close most proofs given a good spec on the benchmarks that report it (Rust-Prover, VeruSAGE; section 3.2; single-paper evidence for the strongest claim). The unsolved part is the funnel's precision: 23% per flag and 11% per distinct bug. A small model is unlikely to win on proof depth; whether it can make up for that with much higher sample volume is an untested assumption, and RQ1 and RQ2 measure it. The contribution would be a cheap, calibrated property-and-disproof generator with a precision gate.
2. **Disproof on code properties as a trained skill.** Leanstral already trains on negations of competition statements (30% of its RL mix), so the gap is narrower than "no one rewards negation proofs". No retrieved source reports negation training on code properties, a bug-yield reward, a witness requirement, or an ablation of the disprove branch. A Lean verifier that already rejects cheating (the ceiling test) can score "proved `not P`" the same way as "proved `P`"; whether the training signal is useful is what RQ1 tests.
3. **Toolchain mismatch is an open engineering gap, and it is wider than Rust.** Aeneas-based work (2605.30106, 2609.15648) reports Lean toolchain drift as an obstacle, and this repository's verifier is pinned to Lean 4.9.0-rc1 (June 2024 Mathlib). The Lean benchmarks the RQs use are on newer toolchains: FVAPPS states Lean 4.12.0 (2502.05714), VERINA's repository pins Lean and Mathlib v4.18.0 (read from its `lean-toolchain` and `lakefile.lean` on GitHub, not from the paper), VeriScale reports v4.24.0 and Vero v4.29.1. So FVAPPS, VERINA and Vero cannot be checked by the current verifier as is, and "Python-via-FVSpec or FVAPPS-style targets avoid the problem" (an earlier claim here) is false for the pinned toolchain. Each extra toolchain needs its own install and its own ceiling test (known-good accepted, adversarial rejected), and the prover itself may degrade on syntax newer than its training data. Not tested here.
4. **No benchmark of real bugs with a ground-truth oracle in the Lean setting.** Existing Lean benchmarks (FVAPPS, VERINA, CLEVER, miniCodeProps, VeriSoftBench) test proofs of correct code. Bug-finding evaluation exists only as the Leanstral anecdote. A paired benchmark from historical bug-fix commits (property fails on pre-fix, holds on post-fix) would be new. The design is borrowed from KNighter (patch-guided), Big Sleep (variant analysis from a fixed bug) and CheckerBench (vulnerable and fixed revisions with a pinned environment, 2610.07557, abstract only), none of which is in Lean.
5. **Spec validation without an LLM judge.** Executable-spec checks (Verus-SpecGym), adversarial test suites (VeriScale) and three-way consistency (Clover) have not been combined into one gate in front of a prover. A gate that is itself measurable (precision/recall against seeded spec errors) is a small, publishable component.
6. **Compute-matched comparison.** Leanstral's scaling is reported to 4M tokens per attempt (587/672 on PutnamBench at 4M, 44 at 50k). Nobody reports what an 8B model achieves on a bug-finding task at, say, 32k tokens times many samples. The cost-per-genuine-bug is the figure missing from the literature.
7. **Isabelle and Coq.** No evidence retrieved; any claim for those systems needs a separate search.

## 7. Research questions for a publication

Common design elements: all prover arms use the same strict verifier; a finding counts as a bug only if it passes an execution check (an input on which the original code violates the human-agreed intent) or independent human triage by two raters; report Wilson 95% intervals for single proportions and paired bootstrap or exact McNemar intervals for between-arm differences (a Wilson interval does not apply to a paired difference); at most 2 Lean workers and `CUDA_VISIBLE_DEVICES` isolation while other jobs run; no heavy-job lock taken by the experiment unless GPUs are free. Feasibility prerequisites for every RQ: a second Lean toolchain matching the benchmark (section 6, gap 3) with its own ceiling test; training limited to LoRA on bf16 weights, as the repository's plan does (`docs/SOTA_PLAN.md`: L5 is 20-40 on-policy LoRA steps of 32 prompts x 8 rollouts), because full fine-tuning an 8B model with optimizer state does not fit 4 x 23 GB without offload.

### RQ1. Does training on negation proofs raise the yield of genuine bugs per property?

Hypothesis H1 (falsifiable): Starting from the same 8B base, a LoRA RL stage (the repository's L5 is the template) with a reward that gives credit for a kernel-checked proof of either `P` or `not P` (the latter only when `not P` is witnessed by a concrete input that the execution check confirms) yields at least +10 percentage points more genuine bugs found on a fixed bank of properties than the same stage trained prove-only, with precision no more than 5pp lower. H1 is rejected if the 95% paired interval for the recall difference includes 0 or falls below +10pp at its point estimate, or if precision falls by more than 5pp. Novelty note: Leanstral already trains on negation proofs of competition statements (section 3.3); what H1 adds is code properties and the witness requirement. Power: with 300 or more paired items and a discordance rate near 0.3, the paired standard error is about 3pp and the minimum detectable difference at 80% power about 9pp, so 300 items is the floor; with 20-40 LoRA steps an effect this large is an optimistic bet and a null result is a plausible outcome that the design can report.

Experiment: build a seeded-bug corpus by mutating the implementations in VERINA, CLEVER and FVAPPS (the reference specs are the curated ones; mutation operators as in nl2postcond and Clover adversarial categories), keeping only non-equivalent mutants, i.e. mutants that fail at least one of the benchmark's tests (VERINA ships test suites; VeriScale expands them 83x), plus a real-bug subset from RQ2. The property bank is fixed across arms (reference specs and a frozen set of model-written properties), so that "bugs found per 100 properties" compares like with like. Three arms: base model, prove-only RL, prove-or-disprove RL. Metrics: bug recall (negation proved on mutant), false-alarm rate (negation proved on the unmutated program). With curated reference specs this should be 0 when the reference implementation really satisfies its spec, and a nonzero count then points to a benchmark error or a translation error (the Vero audit found such errors in curated benchmarks). With model-written properties it is not 0 even for a sound verifier, because a property can simply be too strong, so report the two cases separately. Also report tokens per finding. Ablate the reward for the witness check to measure reward hacking directly (the DafnyPro and RLVR failure mode).

### RQ2. Does a spec-validation gate raise precision from the reported 23% without destroying recall?

Hypothesis H2: In a Leanstral-style funnel (model writes properties from code, tries a proof, then tries the negation), a gate that keeps only properties that (a) agree across three independently sampled re-derivations from the docstring, (b) pass an executable-spec test on the repository's own test suite and on adversarial cases, and (c) are not trivially true or false under mutation, raises the share of flagged violations that are genuine from the baseline measured for our own ungated funnel (Leanstral reports 11/47 = 23% per flag, 5/47 = 11% per distinct bug, on a different model and on Rust) to at least 50% and at least 20pp above that measured baseline, while keeping at least 80% of the genuine bugs the ungated funnel finds. H2 is rejected if either precision target is missed or recall loss exceeds 20%. Power: retention of 80% is only resolvable with enough ungated findings; with 40 genuine ungated findings the Wilson interval on a retained fraction near 0.8 is roughly +/-12pp, with 15 it is roughly +/-20pp, so plan for at least 40 (which may need well over 100 commits) or declare the recall criterion exploratory.

Experiment: use a pre-fix/post-fix design on 100 or more real bug-fix commits from Python projects with property-based tests (FVSpec corpus, 2606.01008) or Dafny/Verus repositories that have a public fix history. The gold label is "property fails on pre-fix code and holds on post-fix code". Caveat: FVSpec's properties are scraped from current property-based tests, not from fix history, so the commits must be mined separately, and both the pre-fix and post-fix Python must be translated into Lean (FVSpec itself reports modelling Python in Lean as the hard part), which re-introduces the translation-fidelity threat of section 5; check each translation by running it against the repository's tests as Rust-Prover does. Compare against a proof-free baseline given the same token budget (a Big Sleep-style variant-analysis prompt, and a fuzzer using LLM-written drivers as in 2307.12469). Report overlap: how many bugs are found only by the prover pipeline, since the Leanstral post asserts, without measuring it, that boundary bugs like the zigzag overflow are missed by fuzzing (and its own footnote shows an LLM reading the code also finds that one).

### RQ3. Does adding synthesized code-property data to math-prover training transfer, and at what cost to math?

Hypothesis H3: Mixing 20% verifier-filtered code-property data (AlphaVerus/VeruSyn-style synthesis, filtered with the strict verifier and with VeriScale-style adversarial implementations to remove weak specs) into the SFT mixture of Goedel-Prover-V2-8B raises VERINA proof-generation success by at least 5pp (given the 4.9% best-model figure for one trial, the baseline must be measured first, and it needs a Lean 4.18 toolchain) with no more than 3pp regression on miniF2F pass@8 at 16k, measured on the existing P2 baseline (78.7%, 192/244 on miniF2F-test, `docs/SOTA_TARGETS.md`). H3 is rejected if the paired VERINA gain interval includes 0, or if the one-sided 95% paired upper bound on the miniF2F drop exceeds 3pp. The margin was 1pp in the first draft; that is unresolvable here: at 78.7% on 244 problems the binomial standard error is about 2.6pp, and a paired comparison with roughly 12% discordant problems still has a standard error near 2.2pp. Even 3pp needs pooling across seeds or miniF2F valid plus test (488 problems, paired standard error near 1.6pp).

Experiment: three mixtures (0%, 10%, 20% code-property data), matched token budget and schedule, three seeds each (nine LoRA runs), evaluated on VERINA and miniF2F, and miniCodeProps if its Lean version is compatible with an installed toolchain (not checked). CLEVER and VeriSoftBench as held-out checks would each need a further toolchain and are better left to a follow-up. Note that the filtered synthetic data must come from somewhere: AlphaVerus and VeruSyn are Rust/Verus, so their pipelines produce Verus programs, not Lean; a Lean-native synthesis step (as in WybeCoder or the Rust-Prover translation) has to be built and is the largest unbudgeted piece of work. Report pass@1, pass@8 and the unbiased pass@k estimator; decontaminate the synthesised set against all evaluation sets before training.

## 8. Open questions

1. What was the split of Leanstral's 36 non-bug flags (too strong, malformed, translation error, intended behaviour)? The technical report names the first two classes qualitatively and gives no counts; a request to the authors, or a re-run on the same 57 repositories, would fix the baseline for RQ2. The 57 repositories are not listed.
2. Does the Lean 4.9 pin used by the verifier here stay compatible with any Aeneas version, or must a second toolchain be added? Not tested; for VERINA (Lean 4.18), FVAPPS (4.12) and Vero (4.29) a second toolchain is needed regardless.
3. Is a Python or Dafny target a better first domain than Rust, given the toolchain risk and that FVSpec and FVAPPS are already in Lean?
4. Leanstral 1.5 availability: Mistral's own model card marks the API model deprecated as of 9/29/2026 (a third-party note says 30 Sep), so the hosted endpoint should not be planned on. A local baseline is not realistic on 4x A10G: 119B parameters are about 238 GB in bf16 against 92 GB of VRAM (section 6); a 4-bit quantised run is the only candidate and was not tested.
5. Contamination of the 2024-2026 benchmarks with training data was not studied in any retrieved paper.
6. Vostd/Asterinas spec-failure case study (a rare real-world account of LLM spec failures) could not be fetched; worth retrieving through a browser lane.

## 9. References (all fetched into the vault under tag `leanstral-bugfinding` unless marked)

- AutoSpec: arXiv 2404.00762. SpecGen: 2401.08807. nl2postcond: 2310.01831. NL2Contract: 2510.12702.
- Clover: 2310.17807. AlphaVerus: 2412.06176. SAFE: 2410.15756. VeruSyn: 2602.04910. VeruSAGE: 2512.18436. ExVerus: 2603.25810.
- DafnyBench: 2406.08467. dafny-annotator: 2411.15143. DafnyPro: 2601.05385. RLVR/Dafny thesis: 2605.30914.
- FVAPPS: 2502.05714. miniCodeProps: 2406.11915. CLEVER: 2505.13938. VERINA: 2505.23135. VeriScale: 2605.22368. WybeCoder: 2603.29088. AlgoVeri: 2602.09464. VeriContest: 2605.08553. Rust-Prover: 2610.03994. Verus-SpecGym: 2605.26457. VeriSoftBench: 2602.18307. FVSpec: 2606.01008. Vero: 2608.13522.
- Rust-to-Lean pipeline: 2605.30106. SymCrypt/Aeneas: 2609.15648. C-to-Lean trust ledger: 2609.38237.
- IRIS: 2405.17238. KNighter: 2503.09002. Sailor: 2604.06506. LLM fuzz drivers: 2307.12469.
- Leanstral 1.5: Mistral AI, "Leanstral 1.5: Proof Abundance for All", 2 Jul 2026, https://mistral.ai/news/leanstral-1-5/ (vault note `leanstral-15-proof-abundance-for-all`); model card note `mistralaileanstral-15-119b-a6b-hugging-face`; retirement-conflict note `leanstral-15-retires-30-sept-2026-mistral-docs-conflict` (third party).
- Big Sleep: Google Project Zero, "From Naptime to Big Sleep", Oct 2024, https://projectzero.google/2024/10/from-naptime-to-big-sleep.html (vault note `from-naptime-to-big-sleep-using-large-language-models-to-catch-vulnerabilities-i`).
- Not fetched in full: Vostd/Asterinas case study doi 10.1145/3832783.3834504 (no figures used); AutoACSL 2606.20969 and SpecMind 2602.20610 (ids checked, no figures used); CheckerBench 2610.07557 (abstract read on arXiv, figures used only as marked).
- Leanstral technical report: Mistral AI, "Leanstral" technical report, 2 Jul 2026, PDF at https://github.com/mistralai/LeanstralSafeVerify (vault note `in-this-work-we-present-leanstral-a-series-of-generalist-code-agent-models-for`), sections 2.2, 4.2. Mistral model card https://docs.mistral.ai/models/model-cards/leanstral-1-5 (vault note `leanstral-15-mistral-ai-mistral-docs`).