Extending DBLog-Based Incremental Snapshots to Handle Orphan Rows in CDC Pipelines
Andreas Andreakis
cs.DB
Nov 7, 2026 · v1
cs.DC cs.LO
TL;DR
Safety and convergence of the DBLog orphan-row deletion extensions are mechanically verified in Lean 4 alongside Isabelle/HOL, with published sources.
Abstract
Applications use heterogeneous datastores where a source feeds sinks such as search indexes or data warehouses via change data capture (CDC). As transaction logs have limited retention, CDC alone cannot bootstrap sinks, and traditional approaches either stall source writes or hold back log events. DBLog-based incremental snapshots, adopted by Debezium and Flink CDC, read tables in chunks interleaved with the log without blocking writes or long log stalls and resume where they stopped. After the initial bootstrap, a sink can drift when losing change events or receiving unintended writes. Even a repeated bootstrap can leave orphan rows that exist in the sink and not at the source. A common remedy is to populate a new empty sink, but repairing an existing sink avoids parallel pipelines, a switch and serving traffic from a drifted sink until the new sink is ready. In DBLog's original design, each chunk only emits the latest state of the rows the table still contains, so it does not handle orphan rows. We extend DBLog to delete them using what a chunk read already knows, namely the keys that the range select did not return, emitting a new kind of event that sinks apply as deletes. We also add a repair request that an external process calls with orphan candidates, which the connector checks with its own read, emitting these events for keys confirmed absent. This enables three modes. In the fully integrated mode, every chunk pass removes the orphans it finds during full or periodic repairs. In the second mode, an external drift process hands suspected orphans to the connector. The third mode combines both and is what we recommend. Together, they turn DBLog into a complete data synchronization engine whether a sink catches up on live changes or missing rows, holds wrong column values, or contains orphan rows. Their safety and convergence are formally verified in Isabelle/HOL and Lean 4.
Problem
DBLog-based incremental snapshots, as used in Debezium and Flink CDC, bootstrap and repair CDC sinks. Each chunk emits only the rows the source table still contains, so orphan rows that exist in the sink but not at the source are never removed. Repairing an existing drifted sink avoids the cost of building and switching to a new sink.
Approach
DBLog is extended so that each chunk read emits a new delete-type event for keys absent from the range select. A repair request lets an external drift-detection process submit orphan candidates, which the connector confirms with its own read before deleting. This yields three modes: integrated, external, and combined. The extensions are modeled on the Generalized DBLog formal model. Safety and convergence are proved over all event histories and initial sink states in Isabelle/HOL, with the main results proved again in Lean 4.
Results
The extended protocol handles missing rows, wrong column values and orphan rows, so DBLog can serve as a complete data synchronization engine. All proofs are complete without custom axioms. Every theory except the Flink CDC range merge is proved in both Isabelle/HOL and Lean 4.