Parts of the theory underlying ProvSQL have been formally verified in Lean 4, providing a rigorous mathematical foundation for the provenance semiring framework on which ProvSQL is built. The development is sorry-free: lake build is its whole test suite, so every statement below is one the Lean kernel has checked.

Browse the Lean Documentation   Source

What Has Been Formalized

The formalization covers the core algebraic and database-theoretic foundations of provenance:

Semirings with monus (m-semirings). The central algebraic structure used by ProvSQL – commutative semirings extended with a monus operator for handling set difference – is formally defined (SemiringWithMonus) and its properties proved: monus is characterised by its Galois connection and is unique, and the natural preorder is shown not to be antisymmetric in general. Concrete instances are formalised for Boolean, counting (natural numbers), tropical (min-plus, over the naturals, integers, rationals or reals extended with ∞), Łukasiewicz, min-max, Viterbi, multivariate polynomial semirings (How[X]), the lineage-based semirings Which[X] and Why[X], Boolean-function semirings (Bool[X]), and intervals and interval unions over dense linear orders (used for temporal databases). One further instance, ChainFive, exists only as a counterexample: absorptive but without ⊗-over-⊖ distributivity, it pins down which hypotheses the HAVING results genuinely need.

Database foundations. Formal definitions of tuples, relations, and databases, together with the standard relational algebra operations (selection, projection, join, union, difference).

Annotated databases and query semantics. The lifted semantics of relational algebra over annotated databases – showing how each operator propagates provenance annotations through the m-semiring operations – is formally developed and proved correct. Two adequacy results relate it back to ordinary SQL semantics: forgetting the annotations turns annotated evaluation into plain evaluation of the query, exactly on the positive fragment and as a sub-multiset inclusion in general (Provenance.QueryAdequacy), and the support of a Boolean-annotated evaluation is the plain evaluation of the support of the database, difference and duplicate elimination included, transferring along any homomorphism into 𝔹 (Provenance.SupportAdequacy).

A kind-indexed query language. The library’s primary query syntax, AggQuery, is indexed by three column kinds – regular values, aggregate tokens, provenance values – mirroring the three data types through which ProvSQL enforces its own discipline (regular SQL values, agg_token, uuid). The scope restrictions on aggregate results – no deduplication, no difference, no re-grouping over them – are therefore static typing in the formalization, exactly as they are typing in the system, rather than side conditions on theorems. An aggregate result is a symbolic token (AggValue) carrying the annotated payload of its group, with world-faithful, per-world and deterministic readings, and the tie-break used to order that payload is proved semantically invisible (AggValue.predProv_congr).

Homomorphism commutation. Query evaluation commutes with m-semiring homomorphisms on the whole language, aggregation and HAVING included (AggQuery.evaluateAnnotated_hom), with no hypothesis beyond being an m-semiring; the restriction to the non-aggregating fragment is Query.evaluateAnnotated_hom. This generalises Green-Karvounarakis-Tannen Proposition 3.5 (lifted to m-semirings à la Geerts-Poggi) and extends it to aggregation. It is the formal backing for ProvSQL’s architecture: a single persistent provenance circuit is stored once, and each sr_* evaluator is the realisation of one m-semiring homomorphism out of it. The m-semiring class carries, for that purpose, a δ support operator (SemiringWithMonus.delta) with four axioms (delta_zero, delta_natCast_pos, delta_regrouping, delta_absorb), and every concrete semiring instance ships a concrete δ.

Query rewriting. A query rewriting evaluation strategy on annotated relations, implementing rules (R1)–(R5) of the ProvSQL ICDE 2026 paper. Correctness is fully formalised: on the classical relational-algebra syntax, (R1)–(R4) are proved by Query.rewriting_valid; the same rules stated natively on the kind-indexed syntax are AggQuery.rewriting_valid; and the aggregation rule (R5) – a GROUP BY whose aggregate columns flow onward as output values – is AggQuery.gammaRew_valid. The three base rewritings are then closed under composition (AggQuery.rewritesTo_valid): selection, projection, union, duplicate elimination and product all compose over token-bearing subqueries, so the SELECT … FROM (GROUP BY …) shape is covered, and the HAVING site is handled with its aggregates exposed, for an arbitrary predicate mixing aggregate and regular atoms (AggQuery.havingPredRew) – the shape ProvSQL actually emits. Only difference above a grouping is left out.

Provenance of HAVING. The possible-world semantics of a grouping followed by an aggregate comparison (Having.havingProv), the algebraic identities behind counting aggregates, the corresponding probability identities under contributor independence (MIN/MAX factorisation, Poisson-binomial recurrences for COUNT and SUM), a closed form for MIN, MAX and PICKFIRST computable by a single scan over the occurrences in an absorptive m-semiring (Having.minScan_correct), and the enumeration algorithms with their correctness proofs (CountEnum.countEnum_correct, SumDP.sumDP_correct). Machine-checked counterexamples show that absorptivity and ⊗-over-⊖ distributivity are both genuinely required where they are assumed.

Probability. Probabilistic query evaluation is anchored in the possible-worlds reading of Boolean-function annotations (randomWorld_evaluateAnnotated), and lifted to the full language: for arbitrary queries with aggregate comparisons anywhere, the probability that a random world has a non-empty answer, and the marginal probability of an answer tuple, are the probabilities of the corresponding provenance annotations (AggQuery.boolean_pqe, AggQuery.tuple_pqe). Block-independent databases are covered too: Provenance.CategoricalBlock re-proves weighted model counting over categorical block variables, backing ProvSQL’s repair_key / mulinput route and its deterministic-OR mark (CatAssignment.singleBlock_detOR_sound).

Provenance circuits. The circuit representation, its evaluation in any m-semiring, and the two bottom-up probability evaluators ProvSQL relies on – read-once with the inclusion-exclusion correction (Circuit.prob) and direct summation under decomposability and determinism (Circuit.probDD) – are proved correct against the sum-over-valuations semantics, and the Tseitin CNF transformation is proved equisatisfiable (Circuit.tseitin_equisat), which is the step taken just before a knowledge compiler is invoked.

Complexity. Deciding whether the HAVING SUM provenance of a group is non-zero is NP-complete, already in data complexity (havingSumNonzero_NP_complete), with hardness by a first-order reduction from Knapsack – hence stronger than a Karp reduction. The bridge to the semiring semantics is havingSumProv_ne_zero_iff. This part builds on a companion Lean library, descriptive-complexity.

Papers, Releases and Citing

A paper’s hyperlinks live in a PDF and cannot be fixed after publication, so each published paper gets a frozen module restating its claims and proving them by applying the declarations it cites: a generalisation of the library keeps compiling, while a weakening breaks the build, and the anchors themselves are checked separately against the deployed documentation. Provenance.Papers.Icde2026 is the frozen module for Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data, ICDE 2026.

The library carries its own version numbers, independent of the ProvSQL extension’s; a tag freezes a citable state of the code, and the lean-toolchain file at each tag is authoritative for the Mathlib version it was checked against. Releases are listed on GitHub and archived on Zenodo, where the concept DOI 10.5281/zenodo.21809151 resolves to the latest version and every release additionally has its own version DOI. Cite the version DOI of the tag you used, so that the citation names a specific state of the code, following the metadata in CITATION.cff. The repository is also archived in Software Heritage.