Pipeline Denotational Design: Correct-by-Construction Data Pipelines at Zero Cost
Nikos Karayannidis
cs.DB
Jul 23, 2026 · v1
TL;DR
Pipeline Design Language (PDL), a DSL embedded in Agda and Lean 4, encodes the pipeline algebra so designs carry machine-checked correctness proofs.
Abstract
Pipeline Denotational Design (PDD) is a design-first methodology for building data pipelines that are correct by construction. As AI agents generate pipeline code at scale, the bottleneck shifts from writing to verifying pipelines, and the errors that matter most (grain inconsistencies that silently inflate aggregates) evade schema checks, type checks, and sampled tests. PDD designs pipelines in a semantic domain rather than in code: a design is composed from a typed algebra of operations (the Pipeline Design Algebra, one instantiation) in which every well-typed composition is grain-correct by construction. Resting on grain alone, the guarantee is universal: it holds for any grain-inferring operation set, over any engine. Correctness is established in three layers (grain, behavioral class, and domain) at design time, at zero cost, with no access to data: grain by a data-independent computation (CalcG), behavioral class by the type checker, and domain rules by a proof-carrying composition over operation contracts. A Pipeline Correctness theorem collapses the rest to a single input-boundary check: the only data-dependent residue is whether inputs meet the design's preconditions (data quality, not code correctness), which PDD emits as SQL/PySpark verification queries. Correctness by construction is a spectrum: the same design can be verified by runtime checks, the deployed type-level checker, or machine-checked proofs in Agda/Lean 4. This recasts the engineer's role: an agent instantiates a pre-verified pattern and ships a machine-checkable certificate; the human validates a compact specification and checks it. We realize the methodology in a production toolchain and set out an evaluation across pipeline patterns, behavioral classes, and data modelling paradigms. Because it rests on grain alone, the same design-time check extends to AI-generated queries over semantic layers and ontologies.
Problem
Data pipelines, increasingly generated by AI agents, suffer silent grain inconsistencies such as fan traps that inflate aggregates. Schema checks, type checks and sampled tests do not catch them. Verifying pipelines, rather than writing them, has become the bottleneck.
Approach
Pipeline Denotational Design specifies pipelines in a semantic domain using a typed Pipeline Design Algebra in which well-typed compositions are grain-correct by construction. Correctness is checked in three layers at design time: grain via a data-independent computation (CalcG), behavioral class via typing, and domain rules via proof-carrying operation contracts. Remaining data-dependent preconditions become generated SQL/PySpark queries at the input boundary. For full rigor, the algebra and its constraint logic are embedded in Agda/Lean 4 as PDL, so that type-checking a design yields a machine-checked proof.
Results
A Pipeline Correctness theorem reduces the runtime residue to a single input-boundary check. A production toolchain realizes the methodology, and a case-study pipeline is mechanized end to end in the dependently typed embedding. The quantitative evaluation is designed but not yet reported.
