Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Building a Correct-by-Design Lakehouse. Data Contracts, Versioning, and Transactional Pipelines for Humans and Agents

Weiming Sheng, Jinlang Wang, Manuel Barros, Aldrin Montana, Jacopo Tagliabue, Luca Bigon

TL;DR

Bauplan addresses correctness in lakehouses faced with untrusted data actors by proposing a code-first design that fuses typed data contracts, Git-like data versioning, and transactional pipeline runs. It integrates static and runtime checks, point-in-time reproducibility, and atomic multi-table publication to prevent schema, collaboration, and correctness failures. A lightweight Alloy model grounds the correctness arguments and reveals counterexamples that guide API and protocol design. This approach offers a practical path toward correct-by-design lakehouses with improved verification, reproducibility, and safe collaboration for both humans and automated coding agents.

Abstract

Lakehouses are the default cloud platform for analytics and AI, but they become unsafe when untrusted actors concurrently operate on production data: upstream-downstream mismatches surface only at runtime, and multi-table pipelines can leak partial effects. Inspired by software engineering, we design Bauplan, a code-first lakehouse that aims to make (most) illegal states unrepresentable using familiar abstractions. Bauplan acts along three axes: typed table contracts to make pipeline boundaries checkable, Git-like data versioning for review and reproducibility, and transactional runs that guarantee pipeline-level atomicity. We report early results from a lightweight formal transaction model and discuss future work motivated by counterexamples.

Building a Correct-by-Design Lakehouse. Data Contracts, Versioning, and Transactional Pipelines for Humans and Agents

TL;DR

Bauplan addresses correctness in lakehouses faced with untrusted data actors by proposing a code-first design that fuses typed data contracts, Git-like data versioning, and transactional pipeline runs. It integrates static and runtime checks, point-in-time reproducibility, and atomic multi-table publication to prevent schema, collaboration, and correctness failures. A lightweight Alloy model grounds the correctness arguments and reveals counterexamples that guide API and protocol design. This approach offers a practical path toward correct-by-design lakehouses with improved verification, reproducibility, and safe collaboration for both humans and automated coding agents.

Abstract

Lakehouses are the default cloud platform for analytics and AI, but they become unsafe when untrusted actors concurrently operate on production data: upstream-downstream mismatches surface only at runtime, and multi-table pipelines can leak partial effects. Inspired by software engineering, we design Bauplan, a code-first lakehouse that aims to make (most) illegal states unrepresentable using familiar abstractions. Bauplan acts along three axes: typed table contracts to make pipeline boundaries checkable, Git-like data versioning for review and reproducibility, and transactional runs that guarantee pipeline-level atomicity. We report early results from a lightweight formal transaction model and discuss future work motivated by counterexamples.
Paper Structure (18 sections, 4 figures)

This paper contains 18 sections, 4 figures.

Table of Contents

  1. Introduction
  2. Lakehouse failure modes: an industry perspective
  3. Design principles
  4. Programming abstractions
  5. Collaboration workflows
  6. Transactional pipelines
  7. A lightweight formal model
  8. Commits and branches.
  9. The only state-changing write.
  10. Runs as step-by-step writes on a chosen branch.
  11. Minimal counterexamples.
  12. Related work
  13. DAG frameworks and abstractions.
  14. MVCC and Git modelling.
  15. Conclusion and future work
  16. ...and 3 more sections

Figures (4)

  • Figure 1: A run in Bauplan: 1) a user (humans and / or coding assistants) writes code locally, and triggers the run; 2) the control plane parses the code into a plan and sends it to a worker for execution; 3) the worker reads/writes data from/to S3 and 4) streams logs and results to the user.
  • Figure 2: Git-for-data and collaboration. Git-like abstractions -- such as commits, branches and merges -- enable PR-based reviews and reproducibility. As argued in Section \ref{['sec:trans']}, these concepts are however not sufficient for global correctness.
  • Figure 3: Transactional pipelines. Top: without coupling temporary branches with runs, run_2 leaves main with a new version of $Parent$ but an old version of $Child$ and $Grandchild$. Bottom: the run API guarantees atomic publication of all tables on success, and isolation in case of failure.
  • Figure 4: A counterexample. A user's run failed after the first commit, leaving an aborted branch open. An agent can do arbitrary work by branching off that commit: if a merge back to main happens from run_2, the system ends up in an inconsistent state with respect to run_1 semantics.