← All papers
First page of Generalized DBLog: A Verified Contract for Interleaving Copied Rows with a Change Log

Generalized DBLog: A Verified Contract for Interleaving Copied Rows with a Change Log

Andreas Andreakis

cs.DB Sep 8, 2026 · v4 cs.DC cs.LO
An independent Lean 4 formalization, using only the core library, re-proves the contract core, cut theorem, three corollaries and window-invariance lemmas; it ships in the paper's artifact.
Change-data capture (CDC) feeds downstream systems like caches, search indexes, and data warehouses from a database's log of committed row changes. When bootstrapping, adding a table, or repairing downstream data, a pipeline must also copy existing rows. Merging this copy with the active log introduces the copy-to-log handoff problem. Changes must not fall through a gap, and older copied state must not overwrite a newer logged update or resurrect a deleted row. DBLog, developed at Netflix, addressed this problem by reading tables in chunks and interleaving those reads with the live log. Watermarks identify the changes that overlap each read, and the log wins when a copied row is stale. Debezium and Flink CDC have since adapted this design. Earlier work proved that applying the original algorithm's copied rows and logged changes in their emitted order reconstructs the source's rows, including the effect of every logged insert, update, and delete processed. Generalized DBLog asks when the same result holds for variants of that design. We state the conditions the source and capture implementation must satisfy. Once copying and reconciliation are complete, we prove that the result holds across all selected tables and key ranges even when their rows were read at different times. A single database snapshot is not required for the copy. Further logged changes advance the reconstructed state one event at a time. We establish these guarantees for classic watermarking, Debezium's signal-table and read-only modes, Flink CDC's parallel chunks, reads and dumps tied to exact log positions, and engine-consistent backups whose log position lies within known bounds. The complete theory is machine-checked in Isabelle/HOL, its core independently verified in Lean 4, and the protocols are also examined by bounded model checking in TLA+.

Change-data-capture pipelines must merge a copy of existing rows with a live change log. The merge must not lose updates or let stale copied rows overwrite newer logged changes or resurrect deleted rows. DBLog's watermark-based approach has been adapted by Debezium and Flink CDC, but it was unclear when such variants remain correct.

The paper defines a source-side contract over keyed stores, commit-ordered logs and capture plans. A capture plan partitions the scope into units, each with a log bracket and read results, and a canonical log-wins merge rule defines the output. A cut theorem, built on a window-invariance lemma, shows the canonical replay equals the source state at the frontier. Further results prove merge-discipline equivalences and instantiate the contract for five production protocol shapes. The full theory is mechanized in Isabelle/HOL, its core is re-proved in Lean 4, and the protocols are model-checked in TLA+.

Conforming plans reconstruct the source's row state at the observation frontier across all tables and key ranges, without needing a single database snapshot, and later log events advance the state one event at a time. Guarantees are established for classic watermarking, Debezium's signal-table and read-only modes, Flink CDC parallel chunks, exact-position reads and dumps, and bounded-position backups.