ProvSQL adds (m-)semiring provenance and uncertainty management to PostgreSQL, enabling computation of probabilities, Shapley values, and various semiring evaluations, as a PostgreSQL extension.
Website: https://provsql.org/ – Documentation: https://provsql.org/docs/
Prerequisites: PostgreSQL ≥ 11, a C++17 compiler, PostgreSQL development
headers, uuid-ossp, and the Boost libraries (libboost-dev,
libboost-serialization-dev).
make
make install # as a user with write access to the PostgreSQL directoriesAdd to postgresql.conf and restart PostgreSQL:
shared_preload_libraries = 'provsql'
Then in each database:
CREATE EXTENSION provsql CASCADE;See the full installation guide for prerequisites, optional dependencies, testing, and Docker instructions.
ProvSQL Studio is a separate Python package that adds a web UI on top of the extension: a Circuit mode that renders the provenance DAG behind any result UUID, with frontier expansion, an inspector, and on-the-fly semiring evaluation; and a Where mode that hover-highlights the source cells of each output value.
pip install provsql-studio
provsql-studio --dsn postgresql://localhost/mydbSee the Studio chapter of the documentation.
The theory ProvSQL implements – m-semirings and their δ operator, the
semantics of annotated databases, the query rewriting and its compositional
closure, HAVING provenance, provenance circuits and probabilistic
evaluation – has a machine-checked counterpart in the companion Lean 4
library provenance-lean,
a sorry-free development whose API documentation is browsable at
https://provsql.org/lean-docs/Provenance.html. See the
Lean formalization page for an overview of what
is proved.
ProvSQL was designed and is maintained by Pierre Senellart. Over the years it has received contributions from students and colleagues, listed on the contributors page of the repository.
Since 2026, a large part of the code, tests, and documentation has been written with the assistance of generative models from Anthropic (Claude); ProvSQL Studio and the website, both of that period, were written and designed that way. The design, the SQL interface and the semantics of what ProvSQL computes were decided and reviewed by the maintainer, who is responsible for the whole. The test suite run in continuous integration on Linux, macOS and WSL is used to verify the behavior of the library; part of this behavior, the query rewriting in particular, is also verified by the Lean formalization described above.
ProvSQL is provided as open-source software under the MIT License. See LICENSE.
https://github.com/PierreSenellart/provsql
Pierre Senellart pierre@senellart.com
Bug reports and feature requests are preferably sent through the Issues feature of GitHub.