Paper deep dive

Certified Program Synthesis with a Multi-Modal Verifier

Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, Ilya Sergey

Year: 2026Venue: arXiv preprintArea: cs.SEType: PreprintEmbeddings: 77

Intelligence

Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 98%

Last extracted: 4/27/2026, 12:40:46 AM

Summary

The paper introduces LeetProof, an agentic pipeline for certified program synthesis (vericoding) that utilizes a multi-modal verifier called Velvet. Velvet is embedded in the Lean theorem prover and combines dynamic validation (property-based testing), automated SMT-based proofs, and interactive proof scripting. LeetProof addresses two main challenges in vericoding: the fragmentation of verifiers and the difficulty of generating high-quality formal specifications. The pipeline operates in three stages: specification synthesis (using randomized property-based testing to detect specification defects), program and invariant synthesis, and final proof construction. The authors demonstrate that LeetProof achieves a higher rate of fully certified solutions compared to single-mode baselines and successfully uncovers defects in existing benchmarks like VERINA and CLEVER.

Entities (8)

Clever · benchmark · 100%Dafny · auto-active-verifier · 100%Lean · theorem-prover · 100%LeetProof · agentic-pipeline · 100%Loom · framework · 100%Rocq · interactive-prover · 100%Velvet · multi-modal-verifier · 100%Verina · benchmark · 100%

Relation Signals (4)

LeetProof → evaluateson → Verina

confidence 100% · We evaluate LeetProof on an extensive benchmark suite... VERINA and CLEVER.

LeetProof → isbuilton → Velvet

confidence 100% · LeetProof, an agentic pipeline built on Velvet

Velvet → isbuilton → Loom

confidence 100% · Velvet is built on Loom, a general framework for foundational multi-modal verification in Lean.

Velvet → isembeddedin → Lean

confidence 100% · Velvet, a multi-modal verifier embedded in Lean

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Certified program synthesis (aka vericoding) is the process of automatically generating a program, its formal specification, and a machine-checkable proof of their alignment from a natural-language description. Two challenges make vericoding difficult. First, specifications synthesised from natural language are often either too weak to be meaningful or too strong to be implementable, yet existing approaches lack systematic means to detect such defects. Second, the landscape of program verifiers is fragmented: each tool supports a particular reasoning mode -- auto-active (e.g., Dafny, Verus) or interactive (e.g., Coq, Lean) -- with its own trade-off between automation and expressivity. This forces every synthesis methodology to be tailored to a single verification paradigm, limiting the class of tasks it can handle effectively. We overcome both challenges by structuring the certified synthesis workflow around a multi-modal verifier -- a single tool combining dynamic validation, automated proofs, and interactive proof scripting in one foundational framework. We realise this idea in LeetProof, an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean. Multi-modality enables LeetProof to validate generated specifications via randomised property-based testing before any code is synthesised, decompose the synthesis task into sub-problems guided by verification conditions, and delegate residual proof obligations to frontier AI provers specialised for Lean. We evaluate LeetProof on benchmarks derived from prior work on certified synthesis. Our specification validation uncovers defects in existing reference benchmarks, and LeetProof's staged pipeline achieves a significantly higher rate of fully certified solutions than a single-mode baseline at the same budget -- consistently across two frontier LLM backends.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

76,302 characters extracted from source content.

Expand or collapse full text

Certified Program Synthesis with a Multi-Modal Verifier Yueyang Feng ∗ National University of Singapore Singapore yueyangfeng@u.nus.edu Dipesh Kafle ∗ National University of Singapore Singapore dipesh@u.nus.edu Vladimir Gladshtein National University of Singapore Singapore vovaglad@u.nus.edu Vitaly Kurin Neapolis University Pafos Cyprus v.kurin@nup.ac.cy George Pîrlea National University of Singapore Singapore gpirlea@u.nus.edu Qiyuan Zhao National University of Singapore Singapore zhaoqiyuan@u.nus.edu Peter Müller ETH Zürich Switzerland peter.mueller@inf.ethz.ch Ilya Sergey National University of Singapore Singapore ilya@nus.edu.sg Abstract Certified program synthesis(a.k.a. vericoding) is the process of au- tomatically generating a program, its formal specification, and a machine-checkable proof of program/specification alignment from a task description given in a natural language. Two key challenges make vericoding difficult. First, specifications synthesised from nat- ural language descriptions are often either too weak to be mean- ingful or too strong to be implementable, yet existing approaches lack systematic means to detect and correct such defects. Second, the landscape of program verifiers used to validate the results is fragmented: each tool supports a particular reasoning mode—auto- active(e.g.,Dafny,Verus) orinteractive(e.g.,Rocq,Lean)—with its own trade-off between automation and expressivity. This forces every synthesis methodology to be tailored to a single verification paradigm, limiting the class of tasks it can handle effectively. We propose to overcome both challenges by structuring the cer- tified synthesis workflow in stages around amulti-modal verifier— a single tool that combines dynamic validation, automated proofs, and interactive proof scripting within one foundational framework. We realise this idea inLeetProof, a new agentic pipeline built on Velvet, a multi-modal program verifier embedded in theLeantheo- rem prover. Multi-modality enablesLeetProofto validate gener- ated specifications via randomisedproperty-based testingbefore any code is synthesised, decompose the synthesis task into sub- problems guided by verification conditions, and delegate residual proof obligations to frontier AI provers specialised forLean. We evaluateLeetProofon an extensive benchmark suite derived from prior work on certified synthesis. Our specification validation un- covers defects in existing reference benchmarks, andLeetProof’s staged pipeline achieves a significantly higher rate of fully certified solutions than a single-mode baseline at the same fixed budget— consistently across two different frontier LLM backends. 1 Introduction Certified program synthesis, orvericoding[8], is the task of produc- ing, from a description in a natural language, a program together with a formal specification and a machine-checkable proof that the ∗ Joint first authors. program meets it. This is inherently difficult because it weaves to- gether two problems that are hard in isolation—(a) translating an informal intent into a precise formal specification and (b) proving that a synthesised implementation satisfies it—and each feeds back into the other: a faulty specification dooms even a correct program, while an inadequate proof strategy leaves a correct specification unverified. Recent advances in LLM-based code generation have made vericoding feasible by enabling models to produce formal specifications and proof scripts [9,25,41,58,65], whileprogram verifiersserve as trustworthy oracles that check the results. The landscape of modern program verifiers broadly splits into two families.Auto-activeverifiers, such asDafny[32],Viper[45], Verus[ 28], and F ★ [ 9], ask the programmer to annotate code with pre/postconditions, assertions, and loop invariants, which an SMT solver [6,13] then checks automatically.Interactiveprovers, such asRocq[55] andLean[14] instead require the user to construct proofs, step by step, usingproof scripts, offering full expressivity at the cost of greatly increased manual effort. A growing body of work has tackled vericoding for each indi- vidual verifier and paradigm. On the auto-active side, LLM-based approaches have been developed forDafny[4,5,35,41,43,58], Verus[2,10,65], and F ★ [9]. On the interactive side, analogous ef- forts targetLean[57] andRocq[25,36,61]. Dedicated benchmarks have accompanied each line of work:DafnyBench[ 35] forDafny, andVERINA[67],CLEVER[60], andVeriBench[40] forLean. This fragmentation of the verifier landscape, and of the veri- coding efforts built atop it, is not merely an inconvenience. Be- cause each approach is built around the idioms of a single verifier, the resulting workflows, prompting strategies, and feedback loops are deeply entangled with tool-specific details, making it difficult to distil reusable principles that transfer across different verifiers or LLM backends. Moreover,validatingformal program specifica- tions in most of these pipelines is typically limited to human in- spection [ 8,37,41,67], with no systematic way to detect whether a generated specification is too weak (admitting incorrect imple- mentations) or too strong (ruling out every correct one). 1 arXiv:2604.16584v1 [cs.SE] 17 Apr 2026 Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey The specification-quality problem is not hypothetical. During this work, we discovered that roughly 10% of the reference spec- ifications in two state-of-the-art benchmarks,VERINA[67] and CLEVER[60], are defective—they either under-constrain or incor- rectly express the intended properties of the expected output (more on that inSec. 5). This reinforces the need for automated specifica- tion quality checks as a component of any vericoding pipeline. In this work, we propose to address both the tool-fragmentation and the specification-quality problems by designing the vericod- ing workflow around amulti-modal verifier—a single tool that sup- ports dynamic validation (testing), automated verification (SMT), and interactive proof scripting within onefoundationalframework— one whose reasoning principles are themselves mechanically veri- fied, rather than trusted axioms. Traditionalsingle-modeapproaches commit to one paradigm: auto-active tools such asDafny[ 32] offer fast SMT-backed feedback but cannot express proofs outside the solver’s reach, while interactive provers such asLeanare more ex- pressive but provide less automation. A multi-modal verifier com- bines both, letting the pipeline choose the most effective mode at each step: automation dispatches routine obligations, interactive mode handles harder cases, and testing serves as a fast oracle. We implement this idea on top ofVelvet[ 19], a new verifier for imperative programs embedded as a library inLean.Velvetis built onLoom[18], a general framework for foundational multi-modal verification inLean. It integrates SMT-based automation [42,53] with interactiveLeanproofs and supportsQuickCheck-style [ 11, 20,29] property-based testing (PBT) of programs, specifications, and loop invariants. SinceVelvetprograms are ordinaryLeanpro- grams, the entireLeanecosystem—type checker, automation tac- tics, and theMathliblibrary [38]—is available at every stage, and tricky verification goals can be delegated to frontier AI provers [1]. Working with a foundational yet executable language (i.e.,Lean) also lets us address the specification-quality problem. Lahiri [27] proposedsymbolic specification testing: using specifications and an SMT-based verifier to prove that concrete tests do not fail, without executing code. While effective forDafny, purely symbolic check- ing becomes prohibitively expensive inLean, where SMT covers a smaller fraction of proof obligations. What turned out to work sur- prisingly well israndomised specification testing—using property- based testing [ 20] to validate specifications against test cases in- stead of formal proofs. PBT is fast, requires no proof engineering, and catches the same class of defects at a fraction of the cost. A specification that fails is rejectedbeforeany code synthesis, catch- ing under-specification early and cheaply. Combining multi-modal verification with randomised specifica- tion testing, we presentLeetProof: an AI-assisted agentic pipeline for end-to-end vericoding that decomposes synthesis into indepen- dently validatedstages—specification generation, program/invari- ant synthesis, and last-mile proof construction. This structure maps onto a well-studied agentic architecture [ 66,68], in which indepen- dent AI systems work in tandem with deterministic symbolic tools, allowing the pipeline to be composed modularly and optimised for costs by fine-tuning its specific components. It was only by experi- menting with different modes at each stage that we identified PBT as the most cost-effective approach for specification validation— illustrating the benefit of the staged, multi-modal design. 1defcountDivisors(n:N):N:= 2((List.range(n+1)).filter 3(fund=>d>0∧n%d=0)).length 4 5defisPrime(n:N):Prop:=n>1∧countDivisorsn=2 6 7methodIsNonPrime(n:N)return(result:Bool) 8ensuresresult=true↔¬isPrimen 9do 10ifn≤1thenreturntrue 11letmuti:N:=2 12letmutret:Bool:=false 13whilei*i≤n 14invariant¬ret↔∀d,2≤d∧d<i→n%d≠0 15invarianti≥2∧(i-1)*(i-1)≤n 16do 17ifn%i=0thenret:=true 18i:=i+1 19returnret Fig. 1: AVelvetmethod for checking non-primality. Contributions.This work makes the following contributions: •LeetProof: the first agentic pipeline for end-to-end vericoding built around a foundational multi-modal verifier, combining test- ing, automated SMT-based proofs, and AI-assisted interactive proof scripting in a unified, staged synthesis pipeline (Sec. 3). •A newtesting infrastructureforLean-based vericoding (Sec. 4): type class-based output mutation for specification completeness checking, bounded enumeration for existential quantifiers in ver- ification conditions, and a meta-programmed harness for ran- domised testing of synthesised programs and invariants. •An evaluation ofLeetProofspecification inference(Sec. 5) demon- strating that our PBT-based specification generator achieves 97.4% semantic accuracy on theVERINAbenchmark [67], while ran- domised specification testing uncovers defects in∼10% of two published benchmark suites:VERINAandCLEVER[60]. •A new benchmark of 50 imperative-styleLeetCodeproblems with complexity annotations, and an evaluation ofLeetProof synthesis pipeline( Sec. 6) showing that:(a) the multi-modalLeet- Proofpipeline produces significantly more fully certified solu- tions than a single-modeLeanbaseline at the same fixed budget (Sec. 6.2);(b) all partially verifiedVelvetsolutions are discharge- able with additional interactive effort, confirming the correct- ness of the synthesised artefacts (Sec. 6.3); and(c) these gains are consistent across different frontier LLM backends (Sec. 6.4). 2 Background We start by briefly introducing the two systems thatLeetProof builds on: theLeantheorem prover and theVelvetverifier. 2.1 Lean Lean[ 12] is an open-source theorem prover and dependently typed programming language. Its expressive type system allows users to state and prove theorems (including statements about purefunc- tionalprograms) interactively usingproof scripts.Lean’s mathe- matical libraryMathlib[ 38] contains over 210,000 formalised the- orems, making it one of the most extensive such libraries in any proof assistant. This rich ecosystem has madeLeanthe platform of choice for major AI-assisted mathematical reasoning efforts, in- cludingAlphaProof[ 23], which achieved silver-medal performance 2 Certified Program Synthesis with a Multi-Modal Verifier Given an arraynums, returntrueif the array was originally sorted in non-decreasing order, then rotated some number of positions (including zero). Otherwise, returnfalse. There may be duplicates in the original array. An arrayArotated byx positions results in an arrayBof the same length such thatB[i]==A[(i+x)%A.length]for every valid indexi. (a) LeetCode problem 1752 statement in plain English 1-- A "drop" is a strict decrease from an element to 2-- its cyclic successor. 3defisDrop(nums:ArrayInt)(i:Nat):Prop:= 4nums.size>0∧i<nums.size∧ 5nums[(i+1)%nums.size]!<nums[i]! 6 7-- A sorted-and-rotated array has at most one cyclic drop. 8defrotSortedProp(nums:ArrayInt):Prop:= 9nums.size≤1∨ 10 (∀ij:Nat,isDropnumsi→isDropnumsj→i=j) 11 12-- No extra assumptions are needed for this problem. 13defprecondition(nums:ArrayInt):Prop:=True 14 15-- The returned boolean should exactly decide "rotSortedProp" 16defpostcondition(nums:ArrayInt)(result:Bool):= 17result=true↔rotSortedPropnums (b) Lean specification: auxiliary functions and pre/postconditions 1-- One of the residual goals to prove interactively 2theoremgoal_2 3(nums:ArrayInt) 4(i_2:Nat) 5(invariant_inv_bounds:i_2≤nums.size) 6-- other invariants are omitted for brevity 7(if_pos:k∈Finset.rangei_2|nums[(k+1)%nums.size]! 8<nums[k]!.card≤1) 9(done_1:nums.size≤i_2) 10:postconditionnumstrue:=bysorry 11 12prove_correctCheckSortedAndRotatedby 13loom_solve<;>... 14exact(goal_2...) (d) Proof script and an example extracted residual goal 1methodCheckSortedAndRotated(nums:ArrayInt) 2return(result:Bool) 3requirepreconditionnums 4ensurespostconditionnumsresult 5do 6letn:=nums.size 7ifn≤1thenreturntrue 8else 9letmutdrops:Nat:=0 10letmuti:Nat:=0 11whilei<n 12-- The loop index stays within bounds. ̈ 13invariant"inv_bounds"(i≤n) 14-- The array size used in the loop is fixed. 15invariant"inv_n_def"(n=nums.size) 16-- Modulo indexing is safe because n > 0. 17invariant"inv_n_pos"(n>0) 18-- drops counts the cyclic decreases 19invariant"inv_drops_count" 20(drops=(Finset.filter 21(funk:Nat=>nums[(k+1)%n]!<nums[k]!) 22(Finset.rangei)).card) 23decreasingn-i 24do 25leta:=nums[i]! 26letb:=nums[(i+1)%n]! 27ifb<athendrops:=drops+1 28i:=i+1 29return(drops≤1) 30 31 #guard(CheckSortedAndRotated#[4,1,2,3]).extract≠ 32velvet_plausible_testCheckSortedAndRotatedÆ (c) Executable Velvet implementation and tests Fig. 2:LeetProofpipeline: from the task description in a natural language to formally specified and verifiedVelvetcode. at the 2024 International Mathematical Olympiad (IMO), andAris- totle[1], which reached gold-medal level at the 2025 IMO. Beyond mathematics,Leanalso serves as ameta-verifier: its hygienic macro system and metaprogramming facilities [49] allow users to embed domain-specific reasoning frameworks as libraries. 2.2 Velvet Velvet[ 19] is a Hoare-style [22] program verifier forimperative programs, embedded as a library inLeanviaLoomframework [18]. Programs inVelvetare annotated with pre/postconditions and loop invariants, andLoomgenerates verification conditions (VCs) whose validity implies program correctness. BecauseLoomis itself for- malised inLean, this implication is a machine-checked theorem— makingVelvetafoundationalverifier that needs not be trusted. Fig. 1shows a completeVelvetexample: a method that decides whether a natural number isnotprime. The specification relies on two auxiliaryLeandefinitions, countDivisorsandisPrime(lines 1– 5). These are ordinaryLeanfunctions that use list filtering and quantification; they are executable but would be inefficient to run on large inputs. This is a deliberate design choice: specifications in VelvetareLeanpropositions andneed notbe executable. The imperative methodIsNonPrime(lines 7–19) comes with the postcondition (ensuresclause at line 8), which states that its Boolean result corresponds exactly to¬isPrimen. The loop (lines 13–18) carries two invariants:retis false iff no divisor of푛has been found in[2,푖), and푖≥2with(푖−1) 2 ≤푛.Velvetprograms are ordinary Leanprograms (with monadically encoded effects [ 59]): one can execute,e.g., #eval(IsNonPrime42).runto test the method. TheVelvetcommand prove_correcttriggers VC generation. For this example, it produces 15 verification conditions—plainLean theorems that together imply correctness of IsNonPrimew.r.t.the ascribed specification. Of these, 14 are discharged fully automati- cally with the help of SMT-based automation (vialean-auto[53]) andLeantactics such as grind[30] andaesop[34]. The single re- maining VC requires aninteractiveproof: it is the number-theoretic fact stating that a number is prime if and only if it has no divisors 3 Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey Task description in natural language LLM drafts specification Type checking LLM reviews specification PBT Hoare-style specification Revise Revise Revise Hoare-style specification LLM drafts program Build + test case assertion + PBT LLM reviews program Velvetprogram (no invariants) Revise Revise Velvetprogram (no invariants) LLM drafts invariants Build + PBT (test invariants) Check VCs (SMT + PBT) LLM reviews invariants Velvetprogram + loop invariants Revise Revise Revise Fig. 3: PartialLeetProofpipeline: specification generation (top), program synthesis (middle), and invariant inference (bottom). Solid blue arrows show artefacts flowing between stages; dashed red arrows show revision loops within each stage. between 2 and its integer square root. This proof can be written manually inLeanor delegated to an AI prover such asAristotle. 3 A Tour ofLeetProof LeetProoftakes a programming task in natural language and pro- duces a verifiedVelvetprogram with a machine-checkable correct- ness proof inLean. The task is decomposed into three stages: speci- fication ( Sec. 3.1), program synthesis (Sec. 3.2), and proof (Sec. 3.3); each producing a validated intermediate artefact.Fig. 2illustrates the pipeline onLeetCodeproblem 1752: 1 the natural language state- ment (Fig. 2a) becomes a formal specification (Fig. 2b), then aVelvet implementation (Fig. 2c), and finally a correctness proof (Fig. 2d). 3.1 Specification Synthesis The first stage translates a natural-language problem description into a formalLeanspecification (Fig. 2b). The LLM also generates several concrete test cases alongside the specification; these serve both as validation inputs and as human-readable documentation for the formal definitions. Since every subsequent stage—program synthesis, invariant inference, and correctness proof—depends on this specification, ensuring its quality is crucial. An LLM-generated specification can go wrong in several ways: it may fail to type- check, admit trivially correct implementations by being too weak, impose constraints that no implementation can satisfy by being too strong, or simply misinterpret the problem. Our pipeline addresses these risks in steps, as shown in the top row of Fig. 3. The process begins with an LLM proposing a draft specification together with∼10 test cases (some derived from the problem state- ment, some are synthesised). The draft must type-check inLean; an 1 https://leetcode.com/problems/check-if-array-is-sorted-and-rotated/ LLM judge then reviews it for common issues. If either check fails, the LLM revises the draft. To gain further confidence, we apply our new take onrandomised specification testingusingLean’sPlausible PBT library [29]. For each test case,LeetProofprogrammatically generates three checks: (a) the test input satisfies theprecondition, filtering irrelevant inputs; (b) the intended input/output pair satis- fies thepostcondition, catching specs that reject correct answers; and (c) no alternative output satisfies the postconditionfor the same input, ruling out under-specification [4,27]. Fig. 4illustrates this on our running example. The specification defines aprecondition( ̈) requiring the array size to exceed 1, and apostcondition(≠) stating thatresult=trueimpliesthe array is sorted-and-rotated. A test case (Æ) is generated alongside. Each PBT check is aLeandefinition typed asProp—syntactically iden- tical to a theorem. Normally this requires a deductive proof; how- ever, the tacticplausible'(a non-failing variant ofLean’sPlausi- bletactic [29]) instead searches for counterexamples by generating random inputs. If a counterexample is found, the check fails and the spec or test case is flagged. If none is found, plausible'silently admits the goal (i.e., inserts asorry), letting the pipeline proceed. This is safe in terms of verification because these checks are vali- dation guards, not part of the final correctness certificate. In this example, checksØand∞both pass: the input # [1,2,3] satisfies the precondition (size3>1), and the expected outputtrue satisfies the postcondition. However, the uniqueness check±fails: PBT findsresult=falseas a counterexample. Because the post- condition uses an implication (→rather than↔), setting resultto falsemakes itvacuously true—so the specification admits a degen- erate implementation that always returns false. This is exactly the class of under-specification that randomised testing is designed to 4 Certified Program Synthesis with a Multi-Modal Verifier 1defprecondition(nums:ArrayInt):Prop:= ̈ 2nums.size>1-- not the final one, too restrictive 3≠ 4defpostcondition(nums:ArrayInt)(result:Bool):= 5result=true→rotSortedPropnums 6Æ 7deftest1_nums:ArrayInt:=#[1,2,3] 8deftest1_Expected:Bool:=true 9 10defprecondition_test1:preconditiontest1_nums:=Ø 11bysimp;plausible' 12 13defpostcondition_test1:∞ 14postconditiontest1_numstest1_Expected:=by 15simp;plausible' 16 17 -- counterexample to uniqueness: result = false± 18defuniqueness_test1(result:Bool): 19result≠test1_Expected→ 20¬postconditiontest1_numsresult:=by 21simp;plausible' Fig.4:PBTchecksforgeneratedspecificationsandtestcases. catch. Beyond filtering, the generated tests serve as human-readable documentation for the formal specification: a user can inspect the accepted concrete input/output pairs to understand what the spec means without reading the formalLeandefinitions, closing an im- portant gap between the informal task description and the rigorous specification used in subsequent stages. An alternative issymbolic specification testing[ 27], whichprovesthat each test passes under the specification via an SMT-based verifier. We experimented with this and found it ineffective inLean: even simple proof obligations were expensive to construct, making PBT the clear winner in cost. 3.2 Program and Invariant Synthesis Velvetis anintrinsicprogram verifier: correctness proofs rely on program-level annotations—most importantly,loop invariants—that drive the verification condition (VC) generation covered in Sec. 3.3. Consequently, this stage couples two sub-tasks: synthesising the program code and inferring its loop invariants. Code generation.Given a validated specification from Stage 1, the LLM generates a candidateVelvetprogram (middle row ofFig. 3). For our running example, the result is shown inFig. 2c. Because Velvetprograms are ordinaryLeanprograms, they can be tested immediately:≠shows a concrete test case assertion (viaLean’s #guardcommand), andÆinvokes PBT via a helper macro. PBT checks the program against both the specification and concrete test cases by running it on random inputs satisfying the precondition and verifying the postcondition holds. Any failure is fed back to the LLM for revision. An LLM judge additionally reviews the out- put for common issues (e.g., producing pure functionalLeancode rather than imperativeVelvetcode, which would bypass invariant inference and defeat the purpose of multi-modal verification). Invariant inference.Loop invariant inference—finding inductive properties that hold at every iteration and are strong enough to im- ply the postcondition—is a notoriously difficult problem, closely intertwined with the specification inference and program correct- ness proof [ 4,17,43]. In auto-active verifiers likeDafny, candidate invariants can be checked cheaply via SMT. InLean, SMT covers 1invariant"inv_drops_count" 2(drops=<(Finset.filter 3(funk:Nat=>nums[(k+1)%n]!<nums[k]!) 4(Finset.rangei)).card) Fig. 5: Incorrect invariant caught by PBT. a smaller fraction of obligations (though it remains effective for linear arithmetic), so we again exploit multi-modality. The invariant inference loop (bottom row ofFig. 3) proceeds as follows. The LLM proposes candidate invariants ( ̈inFig. 2c). LeetProofthen triggers VC generation viaLoomand attempts to discharge the resulting VCs with automated tactics. For VCs that remain, PBT searches for counterexamples. If a counterexample is found—or if the LLM, inspecting the remaining VCs, judges one to be unprovable given the current invariants—the feedback is prop- agated back and the LLM revises its invariants. Fig. 5illustrates this: replacing=with<in theinv_drops_count invariant causes PBT to immediately produce a counterexample: [velvet_plausible_test] FAIL: invariant "inv_drops_count" doesn't hold↩→ nums = #[-18, 10, -13, 11, 8, 17, 13, -19, 15, -1, -27, -25] The buggy invariant claimsdropsisstrictly lessthan the number of cyclic decreases seen so far. For this input, the two quantities are equal at some iteration, violating the strict inequality. Thedecreasingclause (line 23 ofFig. 2c) specifies atermination measurefor the loop, which is also inferred by LLM at this stage and formally verified in the subsequent proof synthesis stage. This clause is optional:Velvetsupports bothpartial correctness(the post- condition holdsifthe program terminates) andtotal correctness (the program terminates and satisfies its postcondition) [ 18]. The choice can be configured per task in the vericoding pipeline. Guarantees at the end of this stage.PBT can refute incorrect in- variants but cannot prove that the surviving ones are inductive or sufficiently strong. The goal of this stage is thereforehigh-confidence invariants: candidates that pass all automated checks (PBT, SMT, LLM review) without yet having been formally proved correct. This leaves room for incompleteness—an invariant may turn out to be too weak during the proof stage—but in practice, the combination of PBT filtering and LLM-based VC assessment produces invari- ants that rarely need revision (cf. Sec. 6). A program that passes all checks is forwarded to the next stage for the final formal proof. 3.3 Proof Synthesis and Residual Obligations Once aVelvetprogram with high-confidence invariants is ready, the prove_correctcommand triggers VC generation viaLoom. Each VC is an ordinaryLeantheorem, which means we can dispatch it usinganymethod available in theLeanecosystem—a key advan- tage of working inside a foundational proof assistant. LeetProoffirst attempts to close every VC automatically using a combination of SMT-based tactics [ 42,53] and built-inLeantactics such asgrind[30] andaesop[34]. For our running example, this step discharges 14 out of 18 VCs, leaving 4residual obligations. A residual obligation is a VC that automation cannot close. In the listing, these appear asLeantheorems with sorryplacehold- ers (Fig. 2d), which are then plugged into theprove_correctblock. 5 Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey The goalgoal_2inFig. 2dis one such obligation: it requires show- ing that the loop’s postcondition follows from the invariants at termination—a general mathematical fact that SMT cannot discharge. To close residual obligations,LeetProofemploys an LLM-based agent inspired by the decomposition technique ofHilbert[63]. The prover agent has access toMathlib[38] search, can register auxil- iary lemmas, and can decompose a goal into smaller sub-goals that it attempts recursively. For particularly hard obligations,LeetProof can delegate to specialised AI provers such asAristotle[ 1]. The agent operates autonomously within a fixed token budget. In principle, the PBT-based checks from earlier stages (specifica- tion validation, invariant inference) could be all replaced by a loop over AI-assisted interactive proof attempts. We experimented with this alternative and found it impractical: even for simple tasks, the token and time costs of attempting formal proofs vastly exceeded those of PBT, which provides the same filtering effect at a fraction of the cost. This confirms our design choice of reserving interactive proving for the final stage, where it is strictly necessary. 4LeetProofTesting Infrastructure This section details the PBT machinery that underpins the pipeline stages described in Sec. 3: generating specification tests, handling existential quantifiers in statements, testing programs and invari- ants, and the role ofLeanmeta-programming. All PBT checks in LeetProofare built onPlausible[ 29], a property-based testing frame- work forLean4 that integrates with the tactic system. Given a the- orem statement,Plausiblegenerates random inputs and attempts to refute the theorem by finding counterexamples. 4.1 Handling Existential Quantification PBT fundamentally struggles with existential quantification. Uni- versally quantified properties can be tested bysamplinginputs and checking the predicate, but negating an existential postcondition requires showing thatnowitness exists—which in general entails reasoning over the entire domain. This pattern is pervasive in ver- ification conditions for array programs. For example, to test (∀푖, 푖< arr.size→arr[푖] ≥0) →sum(arr) ≥0, one must handle the logically equivalent form (∃푖, 푖< arr.size∧arr[푖]<0)∨sum(arr) ≥0. (The equivalence follows from rewriting the implication퐴→퐵as ¬퐴∨퐵and pushing the negation through the universal quantifier.) Plausiblecannot test the existential disjunct directly, since refuting it would require enumerating the entire domain of푖. We exploit a structural property of the verification conditions that arise in practice: existential variables typically admit finite bounds inferable from the theorem structure. In the example above, the constraint푖< arr.sizebounds the existential variable푖, so the disjunct can be checked by enumerating푖∈ [0, arr.size). We extendPlausiblewith a lightweight heuristic that extracts subex- pressions appearing in inequality constraints as candidate bounds for existential variables and usesLeantactics (e.g., grind,omega) to discharge the resulting bound obligations—i.e., to prove that the candidate expression is indeed an upper bound, which is necessary for the enumeration to be sound. When bounds can be established, existential quantification reduces to bounded enumeration during testing. While this does not solve the challenge of testing arbitrary existential quantifiers, it covers the common patterns that arise in program verification and is effective in practice. 4.2 Testing Specifications Sec. 3.1described the three PBT checks—pre/postcondition sound- ness, and output uniqueness—thatLeetProofgenerates for each test case. Here we formalise the underlying definitions. Let퐼de- note a set of inputs, let휓(푖)be the precondition, and let휑(푖,표)be the postcondition. For an input푖∈퐼, let b 푂(푖)denote the set of in- tended outputs. A postcondition휑(푖,표)ispreciseon퐼if it satisfies: (1)Soundness: all intended outputs are accepted,i.e.,∀푖∈퐼,∀표∈ b 푂(푖), 휑(푖,표). A violation means the spec is too strong. (2)Completeness: all unintended outputs are rejected,i.e.,∀푖∈ 퐼,∀표∉ b 푂(푖),¬휑(푖,표). A violation means the spec is too weak. During spec generation, the LLM produces concrete test cases along- side the spec. Each test case consists of an input푖together with a representative intended outputb표∈ b 푂(푖). To validate soundness, for each test case(푖,b표),Plausiblechecks (a) the input satisfies the precondition and (b) the input/output pair satisfies the postcondi- tion. Failure in either check indicates a flaw in either the generated specification or the tests; the failing check and counterexample are fed back to the LLM, which revises the spec (cf. Sec. 3.1). Testing completeness is more challenging, because it requires checking thatnounintended output satisfies the postcondition— a universal statement over an unbounded output domain. How- ever, for many algorithmic problems (e.g., typicalLeetCodetasks), the intended output is deterministic: b 푂(푖)=b표. Under this as- sumption, completeness simplifies to verifying theuniquenessof the intended output, yielding the testable form∀표≠b표,¬휑(푖,표). Checking completeness thus becomes a search for a spurious out- put표≠b표that erroneously satisfies휑. In practice, spurious out- puts often share structure with the intended one. We therefore first sample candidate outputs randomly, then apply small mutations tob표, checking viaPlausiblewhether any candidate inadvertently satisfies휑. The mutations are type-directed: Booleans are flipped; numeric types ( Nat,Int,Char) are perturbed by a small additive delta (withIntadditionally supporting negation); pairs훼×훽have one component mutated (or, when훼=훽, swapped); collections ( Array훼,List훼,String) undergo element-level mutation, random deletion, or random insertion. All mutations are implemented viaLeantype classes—a mecha- nism for expressing constrained polymorphism, similar toHaskell’s type classes orRust’s traits [31]. A type classMutatable훼declares a single operationmutate:훼→Gen훼, whereGenisPlausible’s randomised generation monad. The operation takes a value and re- turns a “nearby” variant, enabling corpus-guided fuzzing on top of Plausible. Concrete instances provide the implementation for each base type listed above. Composite types such as multi-dimensional arrays are supported automatically through recursive instance res- olution: the instance for Array훼delegates element-level mutations to theMutatable훼instance, which in turn may recurse further. 4.3 Testing Programs and Invariants We adapt PBT to test both synthesised programs and their loop invariants, as outlined inSec. 3.2, by transforming aVelvetmethod 6 Certified Program Synthesis with a Multi-Modal Verifier 1methodCheckSortedAndRotatedTesting 2do 3nums←sample(Array Int)satisfyingprecondition 4letn:=nums.size 5ifn≤1thenreturntrue 6else 7letmutdrops:Nat:=0 8letmuti:Nat:=0 9ifnot(plausible_test"inv_bounds")then 10throwError"inv_bounds failed at entry" 11-- (other invariants checked similarly) 12whilei<ndo 13leta:=nums[i]! 14letb:=nums[(i+1)%n]! 15ifb<athendrops:=drops+1 16i:=i+1 17ifnot(plausible_test"inv_bounds")then 18throwError"inv_bounds not preserved" 19-- other invariants are checked similarly 20letresult:Bool:=drops≤1 21ifnot(plausible_test"post")then 22throwError"postcondition failed" Fig. 6: A testing procedure forCheckSortedAndRotated into a testing harness that interleaves execution with checks done at runtime.Fig. 6illustrates the result for our running example. The harness has three noteworthy components (highlighted in Fig. 6). First, the input is sampled randomly subject to the precon- dition (line 3):Plausiblegenerates candidate arrays and retains only those satisfyingprecondition. Second, each loop invariant is checked both at loop entry (lines 9–11) and after every itera- tion (lines 17–19). A failure pinpoints the exact invariant and the concrete input that violates it, giving the LLM targeted feedback for revision. Third, the postcondition is checked on the final result (lines 21–22), catching implementations that compute an incorrect answer despite maintaining all invariants. 4.4 UsingLeanMeta-Programming The testing harness ofFig. 6must inspect a method’s structure to instrument each invariant, so it cannot be an ordinary func- tion. We implement it viaLean’s meta-programming facilities [49], which manipulate program components during compilation.Vel- vetis shallowly embedded inLean: a method is a monadic com- putation in VelvetM[18], modelling mutable state and imperative control flow. We enrich it with two monad transformers [33] for failure reporting and randomised input generation: defVelvetTestingM:=ExceptTString(StateTStdGenVelvetM) Here,ExceptTStringadds the ability to abort with an error mes- sage (used when a check fails), andStateTStdGenthreads a pseudo- random generator through the computation (used byPlausiblefor sampling). Duringelaboration—the phase in whichLeanresolves implicit arguments, synthesises type class instances, and type-checks terms—our metaprogramming code embeds every VelvetMoper- ation intoVelvetTestingM(via the standard monad transformer lift) and replaces each invariant annotation with an inlinedPlau- siblecheck. The result is exposed as thevelvet_plausible_test command (cf.Fig. 2c), which runs property-based tests onVelvet methods and reports any violations and counterexamples. 5 Specification Inference Evaluation Specification quality is the bedrock of the vericoding pipeline: a flawed spec renders every subsequent stage vacuous. We evaluate how faithfully LLM-generated specifications capture problem in- tent and whether PBT can serve as a quality oracle, which isa pri- orinot obvious, since specs are logical formulas whose counterex- amples may be hard to find by random sampling. We test against theVERINAbenchmark [67]; the results are surprising—both in accuracy and in what PBT reveals about existing benchmarks. 5.1 Assessing Specification Accuracy RQ1: How well do the specifications generated byLeetProof capture the intent of the natural language description? To answer this question, we need a benchmark with ground-truth specifications against which we can compare. We chooseVERINA, the largest availableLean-based vericoding benchmark to date [ 67], which pairs 189 natural-language problem descriptions with man- ually curated formal specs. We excluded one problem (basic_104) from our experiment because its reference specification relies on a custom data structure that prevents automated comparison. For each of the remaining 188 problems, we run our specifica- tion generator ( Sec. 3.1) to produce a candidate(pre gen ,post gen ) and compare it against the reference(pre ref ,post ref ). We assess se- mantic accuracy via formal equivalence checking inLean: (i) the preconditions are equivalent,pre gen ↔pre ref , and (i) under the precondition the postconditions agree,pre gen → (post gen ↔post ref ). We discharge these obligations usingAristotleAI prover [1], which was freely available at the time of submission, though high demand for the system led to long waiting times. When equivalence cannot be established, we manually inspect the specifications to categorise the discrepancy. The 188 problems break down as follows: (1)Equivalent (150):generated specifications are logically equiva- lent to the reference ones. (2)Reference issues (16):inconsistencies between the benchmark’s reference postconditions and the intended semantics (cf.Sec. 5.2). (3)Precondition variations (14):preconditions differ slightly (e.g., admitting broader input sets) but remain valid semantic exten- sions. These do not affect correctness of synthesised programs. (4)Ambiguous language (3):vague descriptions admit multiple in- terpretations, leading to divergent but defensible specifications. (5)Over-restrictive postconditions (2):our postconditions impose unstated constraints to ensure determinism (e.g., a tie-breaking rule not mandated by the problem). While stricter than neces- sary, these specs are still sound and lead to correct, if slightly constrained, implementations. (6)Incorrect specifications (3):the specifications generated byLeet- Proofare semantically inconsistent with the problem: incor- rect preconditions (2) and an incorrect postcondition (1). Categories (1)-(4) are correct or defensible specifications (169/188, 89.9%). The over-restrictive cases (5) stem from a preference for de- terministic specifications; while stricter than necessary, they are still sound. Only category (6) represents genuine errors: our ap- proach deviates from the intended semantics in just 5/188 instances (2.6%)—lower than the inconsistency rate of the human-written 7 Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey Tab. 1: Specification issues discovered in published benchmark suites for vericoding inLean. Benchmark Issue type# Instances VERINA[67] Underspecified postcondition12 adv.8, adv.47, adv.71, bas.22, bas.34, bas.37, bas.46, bas.77, bas.84, bas.95, bas.97, bas.103 Incorrect postcondition4 adv.10, adv.12, adv.13, bas.79 CLEVER[60] Underspecified postcondition16 P7, P24, P27, P29, P30, P44, P49, P68, P69, P79, P84, P88, P89, P96, P156, P161 Implementation issue1 P9 Possible incorrect specification 1 P94 benchmark itself (16/188, or 8.5%, category (2),cf.Sec. 5.2). The PBT techniques fromSec. 4.2played a critical role: PBT caught er- rors in two specifications that had already passed the LLM judge, reducing incorrect specifications from 7 (3.7%) to 5 (2.6%). It also uncovered one case where the generated test cases did not satisfy the stated preconditions despite passing the judge. The three incorrect specs (category 6) are allover-constraining output in some edge cases: a spurious frequency bound, and an input bound mistakenly imposed on the output. Because the gen- erated test cases happen to satisfy these constraints, PBT cannot detect them—a fundamental limitation of testing-based validation. Answer to RQ1.LeetProof’s specification generator matches the intent of the natural-language description in 97.4% of cases. PBT filtering caught 2 of the 7 errors that pass the LLM judge. 5.2 Specification Defects in Benchmarks Beyond evaluating our own specifications, we applied specification- level PBT to the reference specs of bothVERINAandCLEVER[60]. For each benchmark problem, we run the three PBT checks of Sec. 4.2—precondition soundness, postcondition soundness, and out- put uniqueness—using the test cases provided by the benchmarks. Without any LLM assistance, this process uncovered 13 issues inVERINAand 18 inCLEVERwithin one day on a single Apple M4 MacBook Pro (14-core CPU, 24 GB RAM). Specification-level PBT is dramatically more cost-effective than LLM-based equiva- lence checking inLean: the 13VERINAissues require only 9 min- utes of PBT, whereasAristotle-based equivalence checking takes approximately 8 hours (both are run with GPT-5.2 at a USD $1 bud- get per problem, though most problems consume less than $0.2). In total, we identify 16 issues inVERINA(out of 189 specifica- tions, 8.5%) with the help ofAristotle, and 18 inCLEVER(out of 161 specifications, 11.2%) purely via PBT, summarised in Tab. 1. Al- though our primary focus was testing specs, sampling inputs and executing reference implementations can also surface implemen- tation bugs (e.g., problem P9 inCLEVER). We reported all findings to the benchmark authors. TheVERINAauthors acknowledged and addressed 15; the remaining one is under review. TheCLEVERau- thors acknowledged the 18 issues but have not yet released fixes. 6 Certified Program Synthesis Evaluation We now present our evaluation of theLeetProofsynthesis pipeline on a new benchmark of imperative-style problems ( Sec. 6.1), com- paring the multi-modalLeetProofpipeline against a single-mode Leanbaseline ( Sec. 6.2), assessing the provability of residual obliga- tions ( Sec. 6.3), and testing robustness across different LLMs (Sec. 6.4). 6.1 Benchmark Selection ExistingLeanbenchmarks (VERINA[67],CLEVER[60]) favour functional patterns (e.g., recursive list traversals), omit complex- ity constraints, and risk training-data contamination due to long public availability. We therefore construct a benchmark of 50Leet- Codeproblems targeting imperative algorithms (two-pointer, slid- ing window, random index access). We manually selected 15 prob- lems during development; 35 more were sampled using Claude Opus 4.6 requiring: simple input types, no complex data structures, deterministic specifications, a mix of classical and recent problems, and easy-to-medium difficulty. For each problem, Claude suggested a target time complexity based on input constraints; we manually verified all annotations and applied minor simplifications where needed. Below, we report results on all 50 problems, distinguishing the development and evaluation sets where relevant (e.g., Fig. 7). 6.2 Multi-Modal vs. Single-Mode Synthesis One might expect that handing a formal specification to a fron- tier LLM and asking it to produce executableLean—without stag- ing through an imperative DSL or inferring invariants—would suf- fice. We call thissingle-mode synthesis: the LLM directly produces aLeandefinition with its proof, verified solely by the type checker. DoesLeetProof’s staged pipeline offer a measurable advantage? RQ2: Does theLeetProofpipeline produce more certified so- lutions than a single-modeLeanbaseline at the same cost? Setup.We compare the fullLeetProofpipeline (Velvetcode+in- variants+multi-modal proof) against a single-modeLeanbaseline in which the LLM directly synthesisesLeanprograms verified by the same prover. Both configurations use the same LLM (GPT-5.2) and the same specifications produced inSec. 5; the USD $5-per- problem budget covers only code synthesis and proving, excluding specification generation (which is identical for both). Fig. 7shows the results; the development set (15 problems, top part) and evalu- ation set (35 problems, bottom part) are visually distinguished. Results.For each problem we record one of three outcomes.Fully proven:the pipeline synthesises an implementation (with loop in- variants forVelvet) and produces a complete machine-checked cor- rectness proof. Overall,Velvetfully proves 28/50 problems, signifi- cantly outperforming single-modeLeanwith 17/50. (Development: 5/15 vs. 1/15; Evaluation: 23/35 vs. 16/35.)Partially proven:an im- plementation is synthesised but the proof is incomplete—some ver- ification conditions remain open after GPT-5.2 exhausts its budget. In Sec. 6.3we further attempt to discharge these residual obliga- tions withAristotle; here we report both sub-categories together. 8 Certified Program Synthesis with a Multi-Modal Verifier Lean baseline 50 problems (15 dev + 35 eval) Velvet pipeline 50 problems (15 dev + 35 eval) Fully provenPartially proven (Aristotle succeeds)Partially proven (Aristotle fails)Synthesis failure Fig. 7: Synthesis results for single-modeLeanandVelvet. Velvetyields 18 partially proven cases, while single-modeLeanpro- duces 30. (Development: 7 vs. 13; Evaluation: 11 vs. 17.)Synthesis failure:no implementation passes the pipeline’s checks.Velvetfails on 4 problems, compared to 3 for single-modeLean. (Development: 3 vs. 1; Evaluation: 1 vs. 2.) We attribute the higher failure rate of Velvetto the stricter validation imposed by invariant checking. Overlap analysis.Tab. 2breaks down the per-problem overlap. For example, the entry in the first row, second column indicates that 13 problems are fully proven byVelvetbut only partially proven byLean. WhileVelvetoutperformsLeanoverall, it does not uni- formly dominate: 4 problems are fully proven byLeanbut only par- tially proven byVelvet. A representative example isLeetCode917 (“reverse only the English letters in a character sequence”). The idiomatic functional recursive implementation inLeannaturally handles skipping non-letter characters, whereas the imperative two- pointer implementation inVelvetrequires maintaining a complex invariant, significantly complicating the proof. Depending on the problem, one style may yield a more concise implementation whose correctness is easier to establish. SinceVelvetis itself embedded in Lean, users can freely fall back to single-mode synthesis. Answer to RQ2.At the same USD $5 budget, the multi-modal LeetProofpipeline produces 44% more fully certified solutions on the evaluation set (23 vs. 16) and 65% more overall (28 vs. 17) com- pared to the single-modeLeanbaseline using GPT-5.2. The advan- tage stems from staging: invariant inference and PBT filtering re- solve issues early, leaving the prover with fewer obligations. 6.3 Last-Mile Interactive Proof Effort The “partially proven” category in Fig. 7contains programs whose proofs are incomplete: some verification conditions remain open after GPT-5.2 exhausts its $5 budget. A failed proof does not neces- sarily mean the program is wrong: it may simply need more prov- ing effort (perhaps, by a human prover). We therefore ask whether LeetProofindeed produces correct programs in these cases. RQ3: Are partially provenLeetProof-synthesised programs actually correct,i.e., can their remaining verification condi- tions be discharged with additional proof effort, and does the multi-modal decomposition make them easier to close? To answer this, we attempted to close remaining verification con- ditions usingAristotle[1], a more powerful AI prover. ForVelvet, all 18 partially proven programs are fully discharged byAristotle. This confirms that theLeetProofpipeline synthesises correct im- plementations and invariants in every case; the incomplete proofs reflect budget limitations, not errors in the synthesised artefacts. Tab. 2: Overlap betweenVelvetand single-modeLean. Velvet/Lean Fully proven Partial / Aristotleok Partial / Aristotlefail Synthesis failure Total Fully proven13131128 Partial (Aristotleok)494118 Partial (Aristotlefail)00000 Synthesis failure01214 Total17237350 For single-modeLean,Aristotlesuccessfully discharges 23 of the 30 partial solutions but fails on the remaining 7. Notably, 1 of these problems is fully solved byVelvet, and for the other six the cor- respondingVelvetverification conditions are fully discharged by Aristotle. This suggests that the staged pipeline generates proof obligations that are structurally easier to close. Answer to RQ3.Every partially provenVelvetprogram from our benchmark suite is provably correct: theAristotleprover success- fully closes all residual obligations. The single-modeLeanbaseline leaves seven programs whose VCs resist evenAristotle, whereas the equivalentVelvetVCs are discharged, confirming that multi- modal decomposition yields more tractable proof obligations. 6.4 Robustness to LLM Choice RQ4: Are the advantages of synthesis with a multi-modal ver- ifier over the single-mode one we discussed in RQ2 consistent across different frontier LLM backends? We randomly sample 25 problems from our benchmark suite and replicate the experiment using Claude Opus 4.6 in place of GPT-5.2, keeping all other settings identical. Fig. 8(left) confirms thatVel- vetoutperforms single-modeLeanunder both backends: 28/50 vs. 17/50 for GPT-5.2, and 10/25 vs. 7/25 for Opus 4.6. The lower abso- lute numbers for Opus 4.6 reflect its higher per-token cost, which leaves less room within the fixed $5 budget.Fig. 8(right) shows the overlap of fully proven sets. Under GPT-5.2, 13 problems are solved by both pipelines, 4 only by single-modeLean, and 15 only byVelvet. Under Opus 4.6, the split is 5/2/5. Changing the backend affects which individual problems are solved but does not change the overall ranking:Velvetremains the stronger pipeline. Answer to RQ4.The results are qualitatively consistent across LLMs: theVelvet-based multi-modal pipeline yields more fully proven solutions than single-modeLeanunder both GPT-5.2 and Claude Opus 4.6, even though the margin narrows on the Opus subset. 7 Threats to Validity Benchmark scale and selection.Our benchmark comprises 50 al- gorithmicLeetCodeproblems (Sec. 6.1), which do not cover all soft- ware classes (e.g., concurrent or I/O-heavy systems). Of these, 15 informed pipeline design, though no hyperparameters were tuned on them. To mitigate selection bias, we additionally test our spec- ification inference against two external suites (VERINA,CLEVER) and observe consistent results across LLMs, suggesting structural rather than dataset-specific advantages. Fixed budget and LLM evolution.The RQ2 comparison ( Sec. 6.2) uses a fixed $5 budget per problem. At substantially higher budgets 9 Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey LeanVelvet 0 5 10 15 20 25 30 35 40 45 50 Problems 17 33 n=50 28 22 n=50 GPT-5.2 LeanVelvet Problems 7 18 n=25 10 15 n=25 Claude Opus 4.6 Fully provenNot proven 41315 Lean only Both Velvet only Lean fully proven 17 problems Velvet fully proven 28 problems GPT-5.2 50 problems 255 Lean only Both Velvet only Lean fully proven 7 problems Velvet fully proven 10 problems Claude Opus 4.6 25 problems Fig. 8: LLM robustness. Left: fully proven vs. failure for single-modeLeanandVelvet. Right: overlap of fully proven problems. single-mode synthesis might close the gap; conversely, at lower budgets the gap may widen. As frontier models improve, single- mode approaches will also get stronger. However, multi-modality reduces cost by letting cheap validation modes (testing, SMT) filter candidates before expensive interactive proving is invoked—a cost- reduction principle that holds regardless of model capability. Implementation and external dependencies.Although the staged decomposition of vericoding is a conceptual contribution not tied to any particular tool, our implementation relies onVelvet,Lean, andAristotle. The RQ3 claim that all partialVelvetproofs are dis- chargeable ( Sec. 6.3) depends onAristotle’s current capabilities. PortingLeetProofto another multi-modal verifier would require engineering effort, but the pipeline architecture transfers directly. 8 Related Work AI-assisted vericoding.A growing body of work uses LLMs to generate verified code for specific verifiers: auto-active approaches targetDafny[4,5,35,41,43,58],Verus[2,10,65], and F ★ [9], while interactive-side efforts focus onLean[57] andRocq[25,36,61]. Several of these systems employ staged pipelines. Misuet al.[ 41] first generate a specification, then synthesise a verifiedDafnymethod; Clover [58] generates code, docstrings, and annotations separately before cross-validating them;ATLAS[4] uses an explicit two-stage spec-then-implementation loop; andLaurel[43] decomposes in- variant inference from proof search inDafny. However, all these pipelines rely on asingle verification mode(SMT) throughout every stage, leaving no fallback when the solver times out or cannot han- dle a particular obligation.LeetProofdiffers by building on a multi- modal verifier, matching each stage to the most cost-effective rea- soning mode: PBT for specification validation, SMT + PBT for in- variant inference, and interactive proofs for last-mile obligations. The reusable insight is thismode-aware decomposition, rather than a prompting strategy tied to one tool’s annotation language. The most closely related agentic effort isAutoRocq[ 62], which uses an LLM agent with an iterative feedback loop to generate tac- tic proofs inRocq. However,AutoRocqaddresses only theproof generationsub-problem: specifications and loop invariants are pro- duced externally (e.g., byFrama-Cverifier [ 26]). Mukherjeeet al.[44] use an LLM in a feedback loop withVST[3] to synthesise verified C programs, but start from a formal specifi- cation rather than natural language and target a single verification mode:Rocqproofs in Separation Logic [46,54]. By contrast,Leet- Proofis an end-to-end pipeline covering the full vericoding task from natural language to certified code, using multi-modal verifica- tion to match each sub-task to the most effective reasoning mode. Non-LLM certified program synthesis.Before LLMs, several sys- tems produced programs with machine-checkable correctness proofs using deductive synthesis or verified compilation.Fiat[15] syn- thesises correct-by-construction implementations of abstract data types inRocqvia tactic-driven stepwise refinement.Rupicola[51] compiles idiomaticRocqfunctions to efficient imperative code, pre- serving correctness through the compilation pipeline. The work by Watanabeet al.[64] certifies the output of a separation logic-based program synthesiser [52] in a post-hoc way by translating deduc- tive derivations intoRocqproofs. More recently, Goldsteinet al.[21] used deductive synthesis inLeanto produce certified constrained random generators for property-based testing [ 11]. These approaches require the specification to be written manually in the verifier’s logic;LeetProofcomplements them by using LLMs to bridge the gap from natural language to formal specifications. Specification quality and validation.Ensuring generated speci- fications are neither too weak nor too strong is a recurring chal- lenge. Existing approaches rely on manual tagging [41], user stud- ies [37], LLM-as-judge with manual inspection [8], design disci- plines such as non-computable specifications [60], or multi-stage evaluators mixing theorem proving with testing [67]. Notably,VE- RINA[67] also uses PBT (viaLean’sPlausiblelibrary [29]) to check spec soundness and completeness, but as afallbackwhen theo- rem proving is inconclusive and only for retrospective benchmark evaluation—not as an online filter during synthesis. Moreover,VE- RINAcompares generated specs againstground-truthreference specs, whereas our checks require only test cases and the generated spec itself.ATLAS[ 4] attempts a similar uniqueness check by gener- atingDafnylemmas that derive a contradiction from alternative outputs, but reports that this often exceeds SMT capabilities. Us- ing randomised testing to validate formal specs has a long his- tory [ 7,24,48]; however, these works target hand-written specs in stand-alone proof assistants, not LLM-generated specs inside a syn- thesis pipeline. Lahiri [ 27] proposessymbolic specification testing, checking LLM-generatedDafnyspecs against concrete input/out- puts via theDafnyverifier. Our approach builds on these ideas but (1) uses PBT as theprimarymethod and as a filtering stage 10 Certified Program Synthesis with a Multi-Modal Verifier in the synthesis pipeline (not a fallback or post-hoc evaluation), (2) replaces SMT-based checking with randomised testing, which we found more cost-effective inLean, and (3) includes a uniqueness check that PBT handles naturally but SMT often cannot. Multi-modal verifiers.K[56] derives multiple reasoning modes (execution, model checking, deductive verification) from a single semantics but lacks interactive proofs.Ivy[39,47] andVeil[50] combine SMT verification with model checking and manual proofs, but target distributed systems.Velvet[19], whichLeetProofbuilds on, unifies SMT automation, interactiveLeanproofs, and PBT— making all three modes available to an LLM-driven pipeline. To our knowledge, no prior multi-modal verifier has been used for implemting end-to-end LLM-assisted certified synthesis. 9 Conclusion We have presentedLeetProof, an agentic pipeline for certified pro- gram synthesis that leverages multi-modal verification—combining testing, SMT-based automation, and interactive proof scripting—to decompose vericoding into stages, each matched to the most ef- fective reasoning mode. Our evaluation shows that this decompo- sition yields more fully certified solutions than single-mode base- lines at the same cost, while randomised specification testing catches defects that existing benchmarks miss. While a sufficiently power- ful AI prover could in principle subsume every stage, our results demonstrate that reserving interactive proving for the final stage— and delegating earlier filtering to cheaper modes such as PBT and SMT—reduces costs by orders of magnitude without sacrificing cor- rectness. Multi-modality is thus not merely a convenience but a practical necessity: principled composition of complementary rea- soning modes within a foundational framework provides a robust foundation for future vericoding systems. Data Availability Statement.An artefact containing the imple- mentation ofLeetProof, the benchmark suite of 50LeetCodeprob- lems, and the evaluation harness for reproducing the results from Sec. 5andSec. 6is publicly available [16]. References [1]Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladimir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, and Lawrence Wu. 2025. Aristotle: IMO-level Automated Theorem Proving.CoRRabs/2510.01346 (2025). https://doi.org/10.48550/ARXIV.2510.01346 [2]Pranjal Aggarwal, Bryan Parno, and Sean Welleck. 2025. AlphaVerus: Bootstrap- ping Formally Verified Code Generation through Self-Improving Translation and Treefinement. InICML (Proceedings of Machine Learning Research). PMLR / OpenReview.net. https://proceedings.mlr.press/v267/aggarwal25a.html [3]Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014.Program Logics for Certified Compilers. Cambridge University Press. [4]Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Soonho Kong, and Sean B. Holden. 2025. ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis.CoRRabs/2512.10173 (2025).https://doi.org/10.48550/ARXIV. 2512.10173arXiv:2512.10173 [5]Debangshu Banerjee, Olivier Bouissou, and Stefan Zetzsche. 2026. DafnyPro: LLM-Assisted Automated Verification for Dafny Programs.CoRR abs/2601.05385 (2026). https://doi.org/10.48550/ARXIV.2601.05385 [6]Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lach- nitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. InTACAS (LNCS, Vol. 13243). Springer, 415–442.https://doi.org/ 10.1007/978-3-030-99524-9_24 [7]Lukas Bulwahn. 2012. The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof. InCPP (LNCS). Springer, 92–108.https: //doi.org/10.1007/978-3-642-35308-6_10 [8]Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, Lacramioara Astefanoaei, Ionel Emilian Chiosa, Jure Kukovec, Alok Singh, Oliver Butterley, Adem Bizid, Quinn Dougherty, Miranda Zhao, Max Tan, and Max Tegmark. 2025. A Bench- mark for Vericoding: Formally Verified Program Synthesis.CoRRabs/2509.22908 (2025).https://doi.org/10.48550/ARXIV.2509.22908 [9]Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fa- tima, Shuvendu K. Lahiri, and Nikhil Swamy. 2025. Towards Neural Synthe- sis for SMT-Assisted Proof-Oriented Programming. InICSE. IEEE, 1755–1767. https://doi.org/10.1109/ICSE55347.2025.00002 [10]Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shu- vendu K Lahiri, Tao Xie, and Lidong Zhou. 2025. Automated Proof Gener- ation for Rust Code via Self-Evolution.CoRRabs/2410.15756 (2025).https: //doi.org/10.48550/ARXIV.2410.15756ICLR 2025. [11]Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for ran- dom testing of Haskell programs. InICFP. ACM, 268–279.https://doi.org/10. 1145/351240.351266 [12]Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. InCADE (LNCS, Vol. 12699). Springer, 625–635. https://doi.org/10.1007/978-3-030-79876-5_37 [13]Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. InTACAS (LNCS, Vol. 4963). Springer, 337–340. https://doi.org/10.1007/ 978-3-540-78800-3_24 [14]Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). InCADE (LNCS, Vol. 9195). Springer, 378–388.https://doi.org/10.1007/978-3- 319-21401-6_26 [15]Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. 2015. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. InPOPL. ACM, 689–700. https://doi.org/10.1145/2676726.2677006 [16]Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey. 2026.LeetProof: Artefact. Zenodo. https://doi.org/10.5281/zenodo.19624966Includes implementation, benchmarks, and evaluation harness. [17]Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an Annotation Assistant for ESC/Java. InFME (LNCS, Vol. 2021). Springer, 500–517. https: //doi.org/10.1007/3-540-45251-6_29 [18]Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey. 2026. Foundational Multi-Modal Program Verifiers.Proc. ACM Program. Lang. 10, POPL (2026), 1–28. https://doi.org/10.1145/3776719 [19]Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey. 2026. Velvet: A Multi-Modal Verifier for Effectful Programs. InDafny Work- shop.https://verse-lab.org/papers/velvet-dafny26.pdfCode available athttps: //github.com/verse-lab/velvet . [20]Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head. 2024. Property-Based Testing in Practice. InICSE. ACM, 187:1– 187:13. https://doi.org/10.1145/3597503.3639581 [21]Harrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati, Leonidas Lam- propoulos, and Benjamin C. Pierce. 2025. The Search for Constrained Random Generators.CoRRabs/2511.12253 (2025). https://doi.org/10.48550/ARXIV.2511. 12253 arXiv:2511.12253 [22]C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming.Commun. ACM12, 10 (1969), 576–580. https://doi.org/10.1145/363235.363259 [23]Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z. Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Ma- soom, Ottavia Bertolli, Tom Zahavy, Amol Mandhane, Jessica Yung, Iuliya Be- loshapka, Borja Ibarz, Vivek Veeriah, Lei Yu, Oliver Nash, Paul Lezeau, Salva- tore Mercuri, Calle Sönne, Bhavik Mehta, Alex Davies, Daniel Zheng, Fabian Pedregosa, Yin Li, Ingrid von Glehn, Mark Rowland, Samuel Albanie, Ameya Vel- ingker, Simon Schmitt, Edward Lockhart, Edward Hughes, Henryk Michalewski, Nicolas Sonnerat, Demis Hassabis, Pushmeet Kohli, and David Silver. 2026. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature651, 8106 (March 2026), 607–613. https://doi.org/10.1038/s41586-025- 09833-y [24]John Hughes. 2011. Specification based testing with QuickCheck:tutorial talk. InFMCAD. FMCAD Inc., 17.http://dl.acm.org/citation.cfm?id=2157659 [25]Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, and Emily First. 2024. Cobblestone: A Divide-and-Conquer Approach for Au- tomating Formal Verification.CoRRabs/2410.19940 (2024). arXiv:2410.19940 http://arxiv.org/abs/2410.19940 [26]Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2015. Frama-C: A software analysis perspective.Formal Aspects 11 Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey Comput.27, 3, 573–609.https://doi.org/10.1007/S00165-014-0326-7 [27]Shuvendu K. Lahiri. 2024. Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. InFMCAD. IEEE, 142–147.https://doi.org/ 10.34727/2024/isbn.978-3-85448-065-5_19 [28]Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Haw- blitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024. Verus: A Practical Foundation for Systems Verification. InSOSP. ACM, 438–454.https: //doi.org/10.1145/3694715.3695952 [29]leanprover-community. 2025. Plausible: A property testing framework for Lean 4.https://github.com/leanprover-community/plausible. [30]leanprover-community. 2026. Lean Language Reference: The grind tactic.https: //lean-lang.org/doc/reference/latest/The--grind--tactic/. [31]leanprover-community. 2026. Lean Language Reference: Type Classes.https: //lean-lang.org/doc/reference/latest/Type-Classes/. [32]K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. InLPAR (LNCS, Vol. 6355). Springer, 348–370.https://doi.org/10. 1007/978-3-642-17511-4_20 [33]Sheng Liang, Paul Hudak, and Mark P. Jones. 1995. Monad Transformers and Modular Interpreters. InPOPL. ACM Press, 333–343.https://doi.org/10.1145/ 199448.199528 [34]Jannis Limperg and Asta Halkjær From. 2023. Aesop: White-Box Best-First Proof Search for Lean. InCPP. ACM, 253–266.https://doi.org/10.1145/3573105. 3575671 [35]Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. 2025. DafnyBench: A Benchmark for Formal Software Verifica- tion.Trans. Mach. Learn. Res.2025 (2025).https://openreview.net/forum?id= yBgTVWccIx [36]Minghai Lu, Benjamin Delaware, and Tianyi Zhang. 2024. Proof Automation with Large Language Models. (2024), 1509–1520.https://doi.org/10.1145/ 3691620.3695521 [37]Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. SpecGen: Auto- mated Generation of Formal Program Specifications via Large Language Models. InICSE. IEEE, 16–28. https://doi.org/10.1109/ICSE55347.2025.00129 [38]The mathlib Community. 2020. The Lean mathematical library. InCPP. ACM, 367–381. https://doi.org/10.1145/3372885.3373824https://github.com/ leanprover-community/mathlib4. [39]Kenneth L. McMillan and Oded Padon. 2020. Ivy: A Multi-modal Verification Tool for Distributed Algorithms. InCAV (LNCS, Vol. 12225). Springer, 190–202. https://doi.org/10.1007/978-3-030-53291-8_12 [40]Brando Miranda, Zhanke Zhou, Allen Nie, Elyas Obbad, Leni Aniva, Kai Frons- dal, Weston Kirk, Dilara Soylu, Andrea Yu, Ying Li, and Sanmi Koyejo. 2025. VeriBench: End-to-End Formal Verification Benchmark for AI Code Generation in Lean 4. (2025). https://openreview.net/forum?id=rWkGFmnSNl [41]Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024. To- wards AI-Assisted Synthesis of Verified Dafny Methods.Proc. ACM Softw. Eng. 1, FSE (2024), 812–835.https://doi.org/10.1145/3643763 [42]Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark W. Barrett. 2025. lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. In CAV (LNCS, Vol. 15933). Springer, 197–212. https://doi.org/10.1007/978-3-031- 98682-6_11 [43]Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou. 2025. Laurel: Unblocking Automated Verification with Large Language Models.Proc. ACM Program. Lang.9, OOPSLA1 (2025). https://doi. org/10.1145/3720499 [44]Prasita Mukherjee, Minghai Lu, and Benjamin Delaware. 2025. LLM-Assisted Synthesis of High-Assurance C Programs. InASE. IEEE, 3108.https://doi.org/ 10.1109/ASE63991.2025.00255 [45]Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. InVMCAI (LNCS, Vol. 9583). Springer, 41–62.https://doi.org/10.1007/978-3-662-49122-5_2 [46]Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. InCSL (LNCS, Vol. 2142). Springer, 1–19.https://doi.org/10.1007/3-540-44802-0_1 [47]Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: safety verification by interactive generalization. InPLDI. ACM, 614–630. https://doi.org/10.1145/2908080.2908118 [48]Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. 2015. Foundational Property-Based Testing. InITP (LNCS, Vol. 9236). Springer, 325–343.https://doi.org/10.1007/978-3-319-22102- 1_22 [49]Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Bövinga, Jannis Limperg, Siddhartha Gadgil, and Siddharth Bhat. 2024. Metapro- gramming in Lean 4. Available athttps://leanprover-community.github.io/ lean4-metaprogramming-book/ . [50]George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey. 2025. Veil: A Framework for Automated and Interactive Verification of Transition Systems. InCAV (LNCS, Vol. 15933). Springer, 26–41.https: //doi.org/10.1007/978-3-031-98682-6_2 [51]Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, and Adam Chlipala. 2022. Relational Compilation for Performance-Critical Applications. InPLDI. ACM, 918–932. https://doi.org/10.1145/3519939.3523706 [52]Nadia Polikarpova and Ilya Sergey. 2019. Structuring the Synthesis of Heap- Manipulating Programs.PACMPL3, POPL (2019), 72:1–72:30.https://doi.org/ 10.1145/3290385 [53]Yicheng Qian, Joshua Clune, Clark W. Barrett, and Jeremy Avigad. 2025. Lean- Auto: An Interface Between Lean 4 and Automated Theorem Provers. InCAV (LNCS, Vol. 15933). Springer, 175–196.https://doi.org/10.1007/978-3-031-98682- 6_10 [54]John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. InLICS. IEEE Computer Society, 55–74.https://doi.org/10.1109/LICS. 2002.1029817 [55]Rocq Development Team. 2025. The Rocq Prover.https://rocq-prover.org. Ver- sion 9.0.0, released March 12, 2025. [56]Grigore Rosu. 2017.K: A Semantic Framework for Programming Languages and Formal Analysis Tools. InDependable Software Systems Engineering. NATO Science for Peace and Security Series - D: Information and Communication Secu- rity, Vol. 50. IOS Press, 186–206.https://doi.org/10.3233/978-1-61499-810-5-186 [57]Peiyang Song, Kaiyu Yang, and Anima Anandkumar. 2025. Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean. (2025), 144–169. https://proceedings.mlr.press/v288/song25a.html [58]Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. 2024. Clover: Closed- Loop Verifiable Code Generation.CoRRabs/2310.17807 (2024).https://doi.org/ 10.48550/ARXIV.2310.17807SAIV 2024. [59]Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat- Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella- Béguelin. 2016. Dependent types and multi-monadic effects in F*. InPOPL. ACM, 256–270. https://doi.org/10.1145/2837614.2837655 [60]Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzsche, Greg Durrett, Yisong Yue, and Swarat Chaudhuri. 2025. CLEVER: A Curated Benchmark for Formally Verified Code Generation.CoRR abs/2505.13938 (2025). https://doi.org/10.48550/ARXIV.2505.13938NeurIPS 2025 Datasets and Benchmarks. [61]Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez- Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, and Emily First. 2024. Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification. arXiv preprint arXiv:2412.14063(2024). https://arxiv.org/abs/2412.14063 [62]Haoxin Tu, Huan Zhao, Yahui Song, Mehtab Zafar, Ruijie Meng, and Abhik Roy- choudhury. 2025. Agentic Program Verification.CoRRabs/2511.17330 (2025). https://doi.org/10.48550/ARXIV.2511.17330arXiv:2511.17330 [63]Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, and Ke Ye. 2025. Hilbert: Recursively Building Formal Proofs with Informal Reason- ing.CoRRabs/2509.22819 (2025). https://doi.org/10.48550/ARXIV.2509.22819 arXiv:2509.22819 [64]Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, and Ilya Sergey. 2021. Certifying the Synthesis of Heap-Manipulating Programs. Proc. ACM Program. Lang.5, ICFP (2021), 1–29.https://doi.org/10.1145/3473589 [65]Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu. 2025. AutoVerus: Automated Proof Generation for Rust Code.Proc. ACM Program. Lang.9, OOPSLA2 (2025). https://doi.org/ 10.1145/3763174 [66]John Yang, Carlos E Jimenez, Alexander Wettig, Kilian Lieret, Shunyu Yao, Karthik R Narasimhan, and Ofir Press. 2024. SWE-agent: Agent-Computer Inter- faces Enable Automated Software Engineering. InNeurIPS. https://openreview. net/forum?id=mXpq6ut8J3 [67]Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song. 2025. VERINA: Benchmarking Verifiable Code Generation.CoRR abs/2505.23135 (2025). https://doi.org/10.48550/ARXIV.2505.23135ICLR 2026. [68]Yuntong Zhang, Haifeng Ruan, Zhiyu Fan, and Abhik Roychoudhury. 2024. Au- toCodeRover: Autonomous Program Improvement. InISSTA. ACM, 1592–1604. https://doi.org/10.1145/3650212.3680384 12

Instant research discovery