{"id":"d45accc0-360f-4515-ab71-bcbb83867dfd","arxiv_id":"2608.00501","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"partial","parameter_count":0,"one_line_summary":"Crash recovery cannot decide re-delivery from the crashed side's durable state; only the sink's authoritative acceptance record, with proved fences, gives exactly-once guarantees.","lead":"Using machine-checked proofs in Isabelle/HOL, this paper analyzes crash recovery between a committed log and an external sink. It proves that recovery from local durable state alone can never be exactly-once, while reading the sink's acceptance record restores exactness under stated premises.","discovery_kind":"first_principles","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified","rationale":"The reader's weakest assumption — that the sink exposes an authoritative, complete, durable, per-operation accepted record — is real but is explicitly stated as the premise of the positive result rather than a hidden flaw. The paper's own Section 5 says a stale replica or paginated projection is a different observation, and Section 10 lists the model's deliberate absences, including atomicity of the fenced re-drive. I agree that this premise is the most important condition for applying Theorem 4, but because the paper is careful to make the theory conditional and to state the practical consequences when the premise fails, I do not treat it as a load-bearing objection to the paper's central claim. The negative bounds are constructions over explicit machines and policy classes, and the positive results are conditional theorems with their premises in print. The machine-checked artifact is the main evidence, and the inability to independently execute it here is a reproducibility concern rather than a discovered defect. The reader's verdict of ACCEPT therefore stands unchanged.","tokens_in":31146,"tokens_out":14187,"duration_ms":171468,"concrete_test":"Download the archived Isabelle/HOL development (Zenodo DOI 10.5281/zenodo.21734366) and rebuild from cold with stock Isabelle2025-2 using the provided index that maps every numbered theorem, lemma, and corollary to its mechanized counterpart. Confirm that all numbered statements through Theorem 12 build successfully and that no theorem depends on unlisted axioms or oracles. If any proof fails or relies on an undeclared assumption, the machine-checked support for the central claim is weakened.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I find no load-bearing defect in the central argument. The negative results are explicit information-theoretic constructions: Theorems 1 and 3 exhibit reachable post-crash states that agree on everything a local recovery policy can read and differ only in the world-side accepted record, so any batch chosen by such a policy either duplicates in one world or loses in the other. The checkpointed-machine version closes the natural objection to Theorem 1 by making the pair arise from one deterministic protocol with crash placement as the only nondeterminism. The positive escape (Theorem 4) is conditional on premises P1-P4, and the paper states plainly that a stale, partial, or non-durable sink record is a different observation outside the theorem. The fenced and claim-fenced extensions in Sections 6-7 are likewise scoped, including the explicitly disclosed absence of a crash inside the fenced re-drive atom. These are disclosed premises and model boundaries, not hidden assumptions. The one residual risk is that the Isabelle/HOL archive was not independently executed in this review, so confidence in the machine-checked claim rests on the author's reported build; that affects confidence but not the internal structure of the argument.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a machine-checked (Isabelle/HOL) theory of crash recovery across a dual-write boundary: a source commits facts to a durable log, a relay delivers effects to an independent sink, and the relay checkpoints its own progress. The central claim is an information bound (Theorems 1–3): two reachable post-crash states can agree on everything recovery can read from the crashed side—including a faithfully maintained checkpoint—while differing in what the sink accepted, so any recovery policy computed from that side either duplicates a delivery or leaves one owed. The paper then proves conditional positive results: reading the sink's durable accepted record and re-driving the delta (Theorem 4), an arrival fence for in-flight stragglers (Theorems 5–6), a claim fence for concurrent recoverers (Theorems 7–8), evidence-lifetime limits from bounded dedup memory and truncated history (Theorems 9–10), and an exact store-tier equivalence for CDC/outbox derivation (Theorem 11). All numbered theorems are claimed to be machine-checked, with an archived artifact.","tokens_in":31336,"tokens_out":25484,"duration_ms":279857,"significance":"If the machine-checked claims hold, this is a significant contribution: it gives precise, conditional boundary conditions for exactly-once recovery, separating the impossibility result from the achievable mechanisms, and it names the premises that each escape requires. The negative results are explicit constructions with reachable witnesses rather than sweeping impossibility statements; the positive results are scoped by displayed premises. The paper is unusually honest about model boundaries, including the single one-way pair shape, the atomic re-drive, the absence of a crash inside the fenced composite, the lack of an independent cold-read of the development, and the deliberate exclusion of dual-direction and chained configurations. The main residual risk is model fidelity—especially the assumption that the sink exposes an authoritative, complete, durable per-operation accepted record at the decision frontier—and the fact that I could not independently execute the Isabelle artifact. If the formal claims hold, the paper provides both a theoretical map and a practical review discipline for deployed delivery stages.","major_comments":[],"minor_comments":[{"comment":"Please specify explicitly whether the unfenced re-drive's batch is an ordinary publish (entering the wire W as well as the inner ledger) or is placed directly into the ledger. As written, the literal reading would violate the stated conservative bookkeeping invariant, and the proof sketch of Theorem 5 ('the straggler arrives ... and the record duplicates') depends on the re-driven batch eventually reaching the accepted record. A one-sentence clarification would remove the ambiguity.","section":"§6, 'The re-drive relation lifts unchanged'"},{"comment":"The phrase 'both genuinely emitting' is used in the theorem statements but not formally defined. Please replace it with a formal condition, e.g., E ≠ [], or state the intended frontier-relative completeness condition, so the reader can see exactly what is being claimed.","section":"§3–§4, Theorem 1 and Theorem 3"},{"comment":"The claim that 'the delta emits in committed source order—a proved fact' is given without a lemma or theorem number. Since ordering is not part of the hazard predicates and is stated as a separate property, it would help to attach a numbered statement or a reference to the mechanized lemma.","section":"§5, after Theorem 4"},{"comment":"The sentence 'A sink exposing its own durable, complete per-operation accepted record gives the escape results ahead their raw material' is grammatically and semantically hard to parse. Rephrase, e.g., 'gives the escape results their raw material' or 'provides the raw material for the escape results.'","section":"§2, paragraph on sink readability"},{"comment":"The notation P(u) = g⟨t, A(u), φ(u)⟩ uses angle brackets for a tuple but the same delimiter is used for state components elsewhere. A brief note defining the tuple notation here would prevent confusion with the channel state ⟨t, W, A, φ⟩.","section":"§6, Definition 6.1"}],"recommendation":"minor_revision","confidential_remarks":"I did not execute the Isabelle/HOL artifact, so the machine-checked claim rests on the author's report of a successful build; an independent artifact evaluation would materially increase confidence. The self-citation [2] is clearly disclosed as the substrate for the Section 10 worked instance and is not prior art for the recovery claims. The paper has no experimental evaluation; its value is conceptual and formal, which fits the journal's scope for a theory paper in cs.DB."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know: this is not another essay about exactly-once delivery. It is a machine-checked Isabelle/HOL theory of the recovery decision after a crash, and it proves an information bound: any policy computed from the crashed side's durable state alone must duplicate or lose, with the checkpoint cursor inside the indistinguishable state. The closest prior work is bounded model checking of outboxes; this is a higher-order claim over arbitrary policy functions, so it genuinely goes beyond enumeration.\n\nThe paper is unusually careful. Every theorem has explicit premises. The negative results are constructions—they exhibit reachable states and defeat a named policy class, not a blanket \"exactly-once is impossible.\" The positive results (sink-delta escape, arrival fence, claim fence) are conditional on stated premises, and the paper lists its deliberate absences in Section 10: crash inside the fenced re-drive, per-entry firing, truncation on the wire machine, and others. It also flags the weakest assumption directly: the sink's durable accepted record must be authoritative, complete, and current; a stale or partial record is a different observation. That is honest.\n\nI could not run the artifact, so the machine-checked claim rests on the author's report and the archive. That is the main confidence risk. The model is also deliberately small—single one-way pair, atomic recovery steps, no partial batches. The theorems are exact within that model, but moving to a deployed system requires additional arguments that the paper does not supply. The self-citation to the DBLog substrate is for a consumed bridge, not prior art for the recovery claims, so I don't see a citation problem.\n\nWho is this for? A systems person who wants a precise vocabulary for what a retry can and cannot know, and a formal methods person who wants a clean mechanized boundary result. It is worth a serious referee; the main review task is verifying the artifact and probing whether the model's idealizations hide the hazards the paper claims to exclude.","headline":"Machine-checked formalization of the dual-write recovery boundary—the real thing, with disclosed limits; deserves a serious referee.","tokens_in":31828,"tokens_out":1474,"would_cite":true,"duration_ms":18845,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"After a crash, a delivery process cannot tell from its own durable state whether the other side accepted the effect; this paper proves that bound, and the exact conditions under which reading the sink's accepted record escapes it.","keywords":["dual writes","exactly-once delivery","crash recovery","fencing","change data capture","outbox pattern","formal verification","machine-checked proof"],"falsifier":"Take the two-event history (insert k 7, update k 9), run the deterministic deliver-then-persist protocol, and crash after the second send but before the cursor persists. If any recovery policy that reads only the database, log, outbox, acknowledgements, generation, and cursor can re-send correctly in both branches—no duplicate in the branch where the sink already accepted and no omission in the branch where it did not—then the checkpoint dilemma is false. For the positive side, query a sink whose accepted record lags behind actual acceptance: the sink delta should fail exactly-once on that sta","tokens_in":31003,"feed_emoji":"📬","tokens_out":9048,"duration_ms":91656,"temperature":0.7,"pith_summary":"This paper is a machine-checked theory of the oldest corner of exactly-once delivery: after a crash, the process that sends effects to another authority cannot, from its own durable state, know whether the other side already accepted them. The central result is an information bound: two reachable post-crash states can be identical in everything recovery can read locally—commit log, outbox, acknowledgements, generation, even a faithfully maintained checkpoint cursor—and yet differ in what the sink accepted, forcing any local recovery policy to either duplicate a delivery or leave one owed. The escape is specific and conditional: read the sink's own durable, complete, per-operation accepted record and re-send exactly the committed obligations missing from it. The paper then proves what keeps that answer stable (fences against old in-flight sends and against concurrent recoverers) and what ends it (expiring deduplication memory, truncated source history). A sympathetic reader would care because every exactly-once claim in production is really an assertion about one of these objects, and the paper states which assertion is true, under which premises, and for how long.","feed_headline":"Crash recovery cannot be exactly-once from its own durable state alone","feed_subtitle":"The sink's accepted record is the only thing that can tell a duplicate from a lost delivery — and it has a shelf life.","key_machinery":"The load-bearing object is the sink's accepted record and the delta computed against it: Δ⟨f⟩(t) lists the scoped committed obligations at frontier f that are not yet present in the sink's record. The negative half of the paper is carried by constructed confusable pairs—two reachable states with equal durable-local views but different emission ledgers—whose existence is proved on the effect machine, on a checkpointed machine with a durable cursor, on a channel machine with a wire, and on a concurrency machine with competing recoverers. The positive half is carried by the sink delta under premises P1–P4, by the arrival fence (set the generation fence in the same atomic act as heal-and-redrive","core_discovery":"Two reachable post-crash states can agree on everything recovery reads locally—database, committed log, outbox, acknowledgements, generation, and a faithfully checkpointed cursor—while the sink's accepted record differs. Any policy computed from that local view issues the same batch in both, so it must duplicate a delivery in one world or leave one owed in the other; even a single deterministic deliver-then-persist protocol is defeated by crash timing alone. The escape is the sink delta: re-send exactly the committed obligations missing from the sink's durable accepted record. Under four stated premises (hazard-free record, crashed run, in-range frontier, strictly ascending source coordinate","pith_inferences":["The paper's three-question test—what did the sink accept, what can still change that answer, and how long will the evidence last—could be adopted directly as a review checklist for exactly-once claims; wider adoption in postmortems would shift blame from checkpoint bugs to missing acceptance evidence.","If the sink's accepted record is itself produced by another relay, the same dual-write shape repeats one level down; the paper names chains as out of scope, leaving a hop-by-hop composition theorem as a natural next step.","The proved trade in the fence corollary suggests a deployment can deliberately choose its recovery frontier by deciding which straggler rescues it is willing to forfeit; making that choice explicit is an engineering policy the paper leaves to the reader.","A testable extension: run the two-event crash schedule against a real outbox or CDC relay and verify that any local-only recovery duplicates or loses, confirming the bound in practice without relying on the formal proof alone."],"forward_implications":["A checkpoint-after-send protocol has a provable at-least-once window: a crash between a delivery and the checkpoint persist makes the next recovery re-send, no matter how carefully the cursor is maintained.","A recovery policy that reads an authoritative, complete, current sink accepted record and re-drives the delta is exactly-once at the chosen frontier, with per-instance counting when source coordinates ascend strictly.","An old in-flight send arriving after the read can duplicate an honest recovery; a generation fence set atomically with the re-drive rejects superseded incarnations, at the cost of converting possible straggler rescues into drops.","Concurrent recoverers defeat every fence-free one-shot policy; the surviving discipline is an atomic claim that fences to your generation, arms the batch read under it, and fires under the fence.","The exactly-once guarantee inherits the lifetime of its evidence: expiring deduplication memory re-admits honest duplicates, and a truncated source history leaves recovery choosing between fabricating work and abandoning it."],"supporting_citations":[{"why":"Supplies the dual-writes and log-based problem framing and the 'derive from the log' advice the paper formalizes.","marker":"[17]"},{"why":"Book form of the dual-writes and log-centric architecture advice; one of the texts whose recovery half this paper completes.","marker":"[19]"},{"why":"Log-centric architecture essay the paper names alongside [17,19] as the operational lineage it formalizes.","marker":"[20]"},{"why":"The essay asserting exactly-once delivery is impossible; supplies the folk claim the paper refines into conditional, premised guarantees.","marker":"[31]"},{"why":"Kafka's idempotent-producer epoch is used as the deployed cousin of the generation-and-fence mechanism at the acceptance boundary.","marker":"[4]"},{"why":"Kafka's producer-id expiration window is cited as a concrete finite deduplication horizon relevant to Section 8's windowed-control theorem.","marker":"[5]"},{"why":"Stripe's idempotency-key retention window is the deployed example of deduplication memory expiring.","marker":"[28]"},{"why":"The Isabelle/HOL proof assistant is the system in which every numbered theorem and construction is machine-checked.","marker":"[23]"}],"fun_headline_variants":["Exactly-once recovery is impossible from local state alone","The sink's accepted record tells you if you already delivered","Recovery can't be exactly-once without the sink's acceptance-that evidence expires","Sink acceptance is the only recovery truth, and it has a shelf life"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The sink keeps an authoritative, complete, durable, per-operation record of what it accepted, and recovery can read that record at the moment it decides what to re-send; if that record is stale, partial, or not yet durable, the paper's exactly-once escapes do not apply.","fun_headline_variants_meta":{"raw":{"variants":["Exactly-once recovery is impossible from local state alone","The sink's accepted record tells you if you already delivered","Recovery can't be exactly-once without the sink's acceptance-that evidence expires","Sink acceptance is the only recovery truth, and it has a shelf life"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001337,"raw_usage":{"total_tokens":5332,"prompt_tokens":863,"completion_tokens":4469,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":607,"completion_tokens_details":{"reasoning_tokens":4392}},"tokens_in":607,"tokens_out":4469,"duration_ms":29504,"temperature":1.0,"reasoning_tokens":4392,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T00:49:27.558196+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the two-event history (insert k 7, update k 9), run the deterministic deliver-then-persist protocol, and crash after the second send but before the cursor persists. If any recovery policy that reads only the database, log, outbox, acknowledgements, generation, and cursor can re-send correctly in both branches—no duplicate in the branch where the sink already accepted and no omission in the branch where it did not—then the checkpoint dilemma is false. For the positive side, query a sink whose accepted record lags behind actual acceptance: the sink delta should fail exactly-once on that sta","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the dual-writes and log-based problem framing and the 'derive from the log' advice the paper formalizes."},{"cited_title":"2017.Designing Data-Intensive Applications: The Big Ideas Behind Reliable, Scalable, and Maintainable Systems","cited_arxiv_id":null,"evidence_quote":"Book form of the dual-writes and log-centric architecture advice; one of the texts whose recovery half this paper completes."},{"cited_title":"Beresford, and Boerge Svingen","cited_arxiv_id":null,"evidence_quote":"Log-centric architecture essay the paper names alongside [17,19] as the operational lineage it formalizes."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The essay asserting exactly-once delivery is impossible; supplies the folk claim the paper refines into conditional, premised guarantees."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Kafka's idempotent-producer epoch is used as the deployed cousin of the generation-and-fence mechanism at the acceptance boundary."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Kafka's producer-id expiration window is cited as a concrete finite deduplication horizon relevant to Section 8's windowed-control theorem."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Stripe's idempotency-key retention window is the deployed example of deduplication memory expiring."},{"cited_title":"Paulson, and Markus Wenzel","cited_arxiv_id":null,"evidence_quote":"The Isabelle/HOL proof assistant is the system in which every numbered theorem and construction is machine-checked."}],"review_version":2}