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

arXiv: https://arxiv.org/abs/2607.09072 · HTML: https://mlsanity.com/paper/2607.09072/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 7 of its 31 references that are in the map.
- First posted on arXiv 10 Jul 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 7 of 7)

- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [Agentic Property-Based Testing: Finding Bugs Across the Python Ecosystem](https://mlsanity.com/paper/2510.09907/) (2025)
- [Lemmanaid: Neuro-Symbolic Lemma Conjecturing](https://mlsanity.com/paper/2504.04942/) (2025)
- [SITA: A Framework for Structure-to-Instance Theorem Autoformalization](https://mlsanity.com/paper/2511.10356/) (2025)
- [Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning](https://mlsanity.com/paper/2604.19459/) (2026)
- [Detecting Optimization Bugs in Database Engines via Non-Optimizing Reference Engine Construction](https://mlsanity.com/paper/2007.08292/) (2020)

## Abstract (arXiv)

As the cost of code generation becomes cheaper with AI, the new bottleneck in software engineering has shifted to intent specification and validation. Overcoming this durability crisis of AI-driven coding requires more than traditional fuzzing: each candidate property must be proven correct over a model and shown to hold on the real implementation, making formal proof and systematic property-based testing (PBT) complementary. However, validating properties this way at scale requires solving two subproblems: verifying candidate properties and operationalizing PBT without AI hallucination. We hypothesize that recurring property patterns, cast as property templates--abstract, parameterized forms with holes--address both at once. This paper investigates recurring property patterns in Apache Spark. In data-intensive scalable computing systems, correctness properties arise from the principles of data partition, computation decomposition, and dataflow computation. For instance, aggregation decomposition relates a global function executed on the entire dataset to a local function followed by a recombiner. We design an agentic, dual-track validation framework that uses property templates to formally verify correctness in the Lean 4 theorem prover and instantiate PBT templates as executable PySpark tests. Our evaluation shows that property templates increase agentic proof engineering success by up to 2.6x (1.6x on average) and reduce proof hallucinations by 59%. Template-guided PBT synthesis reduces intent misalignments from 22 to 1 and cuts synthesis cost by up to 5.7x (3.8x on average). Template-guided synthesis further exceeds a state-of-the-art Spark fuzzer and approaches unguided LLM-based PBT on code coverage. Finally, comparing the two tracks is informative: when a proof succeeds yet a PBT finds a counterexample, the mismatch identifies a gap between the formal model and implementation.