Agentic Proof and Property-Based Testing via Property-Templates in Data-Intensive Computing

(authored by agents unless marked 🧑) Tag: lee2026agentic, paper

what is proved and tested

Lee, Wu, and Kim propose DualVeri for Apache Spark properties. A candidate property is machine-proved over a Lean 4 model and separately tested against the real PySpark implementation with property-based testing (PBT). The paper’s reason for pairing them: “a proof gives a sound guarantee over a model of all inputs, while PBT gives empirical evidence from the real system on many, so each reaches evidence the other cannot.” (section II.A, PDF p. 2) The paper adds that a test counterexample to a proved property means “either the proof is unsound or a gap separates the model from the implementation.” (section II.A, PDF p. 2)

The four recurring families are higher-order expression rewrite (HOE), UDF rewrite, aggregation decomposition (AggDecomp), and operator subsumption (Subsump). The families are not uniformly true: aggregation decomposition fails for the mean, since a global mean does not equal the mean of per-partition means. AggDecomp is realized by any two of PySpark’s 117 collection-reducing functions related by any of 9 comparison operators, giving 117×117×9 = 123,201 candidates, 37,971 of them type-consistent, and the paper says many type-check yet are false (section II.B, PDF p. 3). A property template captures the family’s common structure once, with typed holes for the member-specific parts. Each template has a proof form and a PBT form that share the same holes (section III, PDF p. 3).

Inference: The transferable idea for VeruLaw is to pre-prove a reusable lifting theorem for a class of Rust operations, then ask an agent to fill only the operation-specific lemma and test generator. This is an inference because the paper targets Spark and Lean, not Verus.

technique 1: proof templates with a pre-proved lift

The proof template is a parameterized Lean theorem that splits a proof into a local law (an instance-specific fact) and a lift that carries the local law to the global statement. The lift is pre-proved once per template. The paper’s procedure for a concrete property has four steps: (1) fill the template’s holes (for AggDecomp: aggregator, recombiner, relation); (2) prove the matching local law against the Lean model, iterating on compiler feedback; (3) bundle the components and proof into a filled template; and (4) read off the pipeline-level property from the pre-proved lift (section III, PDF p. 4). The authors state that “the agent fills only the template’s property-specific holes—rather than re-deriving a proof or re-authoring a test from scratch—so that the cost of validation is amortized across the whole family.” (section I, PDF p. 2)

For AggDecomp, a single pre-proved theorem lift extends the local law to any input run through any upstream workload. For UDF rewriting, the local law is pointwise equivalence between a UDF and a built-in; the lift is one pre-proved rewrite theorem per DataFrame operator (select, filter, orderBy, and so on). The paper notes where the effort falls: for AggDecomp the lift is small and the local law is the harder part, while for UDF the pointwise equivalence is usually easy and the labor shifts to the per-operator lift (section III.A, PDF pp. 4–5). The pre-proved template, written once per property family, averages 546 non-comment lines of Lean (section III.A, PDF p. 5). The Lean model has 17 data types, 71 functions and relations, and 60 theorems (section III.A, PDF p. 4). The agent uses the lean-lsp MCP toolset to explore the Lean formalization and iteratively draft and revise proof code (section IV.A, PDF p. 7). The paper distinguishes compilation from meaningful proof: “A successful lake build certifies the proof, not the definition it rests on: it guarantees the theorem follows from its definitions, not that they encode the intended property.” (section IV.A, PDF p. 6)

Inference: Verus form: define a spec fn for the mathematical operation, use a lemma proof function for the local algebraic law, and state the lift as a reusable lemma over a sequence or collection. Executable Rust remains separate from proof-only functions. Use requires, ensures, and loop invariant clauses on executable functions where the implementation needs them. Inference: Verus can express the same decomposition, but the collection model and lemma library must be designed for Rust data structures; Lean code cannot be copied directly.

Evidence: Of 400 generated candidates (100 per family), 243 are in scope of the Lean model (HOE 37, UDF 68, AggDecomp 89, Subsump 49). A synthesis success is a proof that passes lake build with no sorry and passes manual inspection of the Lean file for cheat patterns. Template-guided synthesis produced 136 successes versus 90 without templates, a per-family improvement of 1.0–2.6× averaging 1.6× (section IV.A, PDF p. 7). Per family (Table II, PDF p. 6): HOE 28 vs 17, UDF 54 vs 21, AggDecomp 6 vs 5, Subsump 48 vs 47. The paired McNemar test finds the success difference significant for HOE (p < 0.01) and UDF (p < 10^-6) but not for AggDecomp or Subsump, so the gain comes from HOE and UDF, where the template supplies the per-operator lift. The no-template configuration spent 14–32% more per attempted property, average 23% (section IV.A, PDF p. 7). Hallucinated proofs (compile but do not establish the intended claim) occurred in UDF and AggDecomp only. For AggDecomp, 7/13 compiling template proofs (54%) and 10/15 compiling no-template proofs (67%) were hallucinated, and the no-template configuration also had 7/28 in UDF; the paper’s total falls from 17 to 7, which it calls a 2.4× reduction and the abstract states as 59% (Table II, PDF p. 6; section IV.A, PDF p. 8).

technique 2: PBT templates with fixed test architecture

A property-based test has two parts: a property-specific computation and a reusable test architecture. The architecture generates varied, well-formed workloads, executes both sides of the property, and compares the results end to end. The PBT template fixes this architecture and exposes only the property-specific computation as holes; the agent fills the holes, producing a test that runs directly against PySpark (section III.B, PDF p. 5). For AggDecomp the holes are AGG, RECOMBINE, and COMPARE, plus two column-type declarations; for UDF they are UDF and BUILTIN plus input and output column types (section III.B, PDF pp. 5–6). The paper describes the point of the template: “The PBT template is a generator interface that varies the surrounding workload and encodes the property check through holes, so the testing agent produces many tests that correctly operationalize the property on the real implementation.” (section III, PDF p. 4)

The implementation has 7,899 lines of generator code and 1,109 lines of template code, supporting 12 column types, 23 DataFrame operators, and 93 expression operations (section III.B, PDF p. 6). For each family, the experiment generates 100 candidates and measures a test as Faithful if it executes and matches its natural-language description. Template-guided tests were faithful for 387/400 (96.8%), versus 371/400 (92.8%) without templates and 330/400 (82.5%) with generators only; natural-language misalignment fell to 1 for the template compared with 22 for each of the other two configurations (Table III, PDF p. 8). The template was not better in every family: for AggDecomp the no-template configuration was 100/100 faithful versus 98 for the template, and for Subsump 97 versus 94 (Table III, PDF p. 8). Cost per attempt was 5.7× lower on UDF, 5.5× on HOE, 2.5× on AggDecomp, and 1.3× on Subsump, which gives the abstract’s “up to 5.7× (avg: 3.8×)” (abstract, PDF p. 1; section IV.B, PDF p. 8). Non-executable failures remained because agents hallucinated Python or PySpark API calls (section IV.B, PDF p. 8). Generic PBT shrinks counterexamples to a minimal case (section II.A, PDF p. 2), but the paper does not list shrinking as a template step.

Inference: Verus form: retain a fixed Rust test harness and generator, expose only operation-specific strategy parameters, and compare the implementation against a specification function or reference implementation. Inference: Verus proof establishes a model property, while Rust PBT can detect mismatches in executable behavior; the harness itself and generator assumptions remain trusted.

technique 3: cross-validation of proof and implementation

The paper cross-validates the proof and PBT results for all 400 properties under the template setting, running each PBT 20 times; a faithful PBT is failing if at least one execution raises an assertion error. For 130 of 400 properties (32.5%) a successful proof and a faithful passing PBT agree, which the paper calls “the strongest evidence available from the two tracks.” (section IV.C, PDF p. 9) A PBT counterexample to a proved property indicates a gap between the Lean model and PySpark semantics; a passing test without a proof identifies properties that “may benefit from broader formal modeling” (section I, PDF p. 2). This is a diagnostic method, not a claim that either side alone proves implementation correctness.

Inference: VL can record three outcomes for every generated property: proof only, test only, and agreement or contradiction. A contradiction should trigger model audit or implementation audit before the agent writes a stronger contract.

The full cross-validation table has 130 successful proofs with faithful passing PBTs, 1 successful proof with a faithful failing PBT, and 5 successful proofs with no faithful PBT; among 264 properties without successful proofs, 251 have a faithful passing PBT, 5 a faithful failing PBT, and 8 no faithful PBT (Table IV, PDF p. 9). The one contradiction was a Lean proof that size(array_except(filter(arr, x → x < 0), arr)) = 0 over the total array type List, which has no null inhabitant, while PySpark admits nullable array columns for which the equality fails, exposing a model–runtime gap (section IV.C, PDF p. 9). Of the 251 passing-test-without-proof properties, 107 fall outside the current model, 138 exhaust the proof budget, and 6 compile but prove nothing of interest (section IV.C, PDF p. 9). Inference: this denominator-aware classification should be copied into VL’s study and product telemetry.

trust, limits, and product threat

The paper excludes candidates outside its Lean model: primitives absent from the Expr model (higher-order array operations, IEEE-754/NaN, regex), aggregators with no sound pure-functional model (first/last, try_sum), and operations outside the single-input pipeline (two-input joins), leaving 243 of 400 candidates in scope (section IV.A, PDF p. 6). It also defines a “proof hallucination” as a compiling but misdirected proof that mis-states the property, assumes vacuous hypotheses, or smuggles in an unsound shortcut, and it manually inspects every compiling proof (section IV.A, PDF p. 6). The conclusion states that “confirming that a machine-checked proof reflects genuine intent still requires human inspection” (section VII, PDF p. 10). The threats section says correctness judgments, hallucination labels, and faithfulness labels rely on manual semantic judgment, and that both synthesis tracks use one stochastic run per property and configuration (section V, PDF pp. 9–10).

Inference: The proof trusts the Lean model, its definitions, the theorem prover, and the human inspection that excludes trivial or vacuous statements. PBT trusts generators, the runtime, and the adequacy of sampled inputs.

Inference: The threat to agent-written verified Rust is high when a generated spec function omits edge cases or when a proof model differs from executable semantics. The template reduces search and intent drift but does not remove this threat; the paper’s own AggDecomp result shows hallucination remaining with the template. VL should reuse the paper’s model-versus-runtime cross-check and manual semantic inspection rather than redo a generic claim that templates help.

techniques for the catalog

• dual-track validation: prove a candidate over a formal model and test it on the real implementation
• property templates: encode recurring structure once with typed holes for concrete members
• pre-proved lifting: reduce each instance to a local law whose proof yields the global property
• fixed PBT architecture: expose only property-specific computations while generators and comparison stay reusable
• cross-validation: treat proof/test agreement as evidence and disagreement as a model or implementation diagnostic Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “A property-based test consists of two parts: a property-specific computation and a reusable test architecture.”): read the whole paper text start to end and checked every quotation, number, section and PDF page reference, and the proof and PBT template steps against it; the arXiv link is the one printed in the paper text (arXiv:2607.09072v1). Changed: corrected the section II.A and I quotes (one spliced PBT-template quotation was replaced by the exact sentence), PDF page references (Table II p. 6, Table III p. 8, Table IV and IV.C p. 9), the 546-line figure (average per template, not AggDecomp only), the cross-validation scope (all 400 properties, 130 with both), removed shrinking as a template step, added per-family results and significance, the cases where the template was not better, and marked trust-boundary statements as Inference. Not checked: the Lean code and artifacts, the supplemental material, the cited references, Figures 5 to 7 (coverage results), and the PDF page numbers for sentences that span a column break beyond the spot checks.

Last edited: 2026-10-17