Copying live data without losing the plot
- What it is
- The paper states conditions for copying database rows while live changes continue, without losing, reviving, or overwriting newer data.
- Who did it
- Andreas Andreakis
- What it could mean
- Imagine moving a database while everyone keeps editing it. This work could help engineers prevent old data overwriting new data—or deleted records coming back from the dead.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Generalized DBLog: A Verified Contract for Interleaving Database Rows with a Change Log ↗See the proposed checks
In an isolated environment, reproduce the stated artifact build/check routes; then map one DBLog watermark and stale-copy rule to its exact source/target state model and test that the formal endpoint covers all claimed protocol variants.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The paper states conditions under which a chunked database copy can be interleaved with an active change log without gaps, stale copied state overwriting newer logged updates, or deletion resurrection; it covers multiple DBLog/Debezium/Flink/back-up variants. This is a directly inspectable new proof-method result for committed-state handoff and reconciliation.
- Why this could matter
- Copying live data without losing the plot A database copy can collide with updates still arriving from the live system. This paper claims conditions that prevent missed changes, stale overwrites, and deleted rows returning during that handoff across several change-data-capture designs.
- If it holds up
- It would provide a verified foundation for reasoning about copy-to-log handoffs, including watermarking and related capture designs.
- If it does not
- One or more stated conditions or protocol variants may be incomplete, narrowing where the claimed reconstruction guarantee applies.
- Impact horizon
- Enabling · Databases · Distributed systems · Formal verification
- Version
- submitted 2026-09-08 02:44:49 UTC
- Why we tracked it
- a fresh formal-methods paper with a concrete commitment/reconciliation theorem, stated Isabelle/HOL, Lean 4, and TLA+ evidence routes, and source-linked artifacts; not independently replayed.
- Highest-risk dependency
- The paper’s state/reconciliation assumptions may not match a real provider’s authority, idempotency, ordering or unknown-outcome semantics. A formal database theorem cannot itself attest to an external reservation or commitment side effect.
- Available artifacts
- arXiv links a Zenodo formal-verification release; the abstract claims the complete theory is machine-checked in Isabelle/HOL, its core independently verified in Lean 4, and protocols bounded-model-checked in TLA+. No artifact was downloaded, executed, or replayed.
- Current boundary
- Intake record only; examination not started.