DBLog is a change-data-capture (CDC) mechanism for copying a whole table or selected keys from a live source database while continuing to stream new changes. It reads the table in primary-key ordered chunks and brackets each chunk with watermarks in the source log. Rows returned by a chunk become refresh events. CDC events that are newer than a refresh prevent stale chunk values from becoming the final replay result. This approach allows backfills that can run at any time, and not only initially, while source writes and live change capture continue. Because chunks are read at different source-log positions, their rows do not form one physical snapshot. The 2020 paper described the mechanism operationally but left the state reconstructed by its replay implicit. We now formalize that state as a virtual cut: replaying a finite prefix produces the same per-key state as the source at a chosen frontier on a chosen scope. A certified virtual cut packages this equality in a certificate and evidence bundle carrying the source observations needed to check it. This achieves a snapshot-equivalent replay without taking a single physical snapshot. The equivalence is in the replay outcome at the chosen frontier and scope, not in a source timestamp shared by all chunk rows. We prove that every wellformed DBLog run produces a virtual cut and that, under faithful source observation and the stated checker assumptions, an accepted certificate witnesses one. A whole-table result follows under additional coverage conditions. We also prove that a cut advances to later frontiers by appending the source CDC events for keys in scope committed in between, and that it can be restricted to smaller scopes. The results do not establish exactly-once delivery, destination-state convergence, or correctness of any named deployment. All proofs are machine-checked in Isabelle/HOL.

翻译：暂无翻译