Machine-Checked Dual-Write Recovery from a Committed Log

Abstract

Applications often need to make related facts durable in two independent systems without a transaction spanning both. If a process crashes after the second system accepts an operation but before a source-side checkpoint is written, recovery cannot tell from source state alone whether to retry. Transactional outboxes and change data capture move this dual write out of an application process, but relay delivery and checkpointing remain separate durable operations. The engineering problem is familiar, and systems address it with retries, checkpoints, idempotency keys, and fencing. Formal verification has covered transaction isolation, crash safety within one store, and protocols with a shared commit. The closest formal studies model-check particular outbox designs. What is missing is a deductive account of this recovery boundary over arbitrary policies that can read the source side but not the sink's acceptance record. We give this account in Isabelle/HOL. The main result is an information bound. We construct two reachable post-crash states with the same durable source-side state and different sink acceptance records. Any recovery policy based only on the source side must duplicate an effect in one state or leave it undelivered in the other. The same holds for a deterministic deliver-then-checkpoint protocol whose only nondeterminism is crash timing. An authoritative, complete, and current sink acceptance record lets recovery compute the missing operations when source coordinates distinguish them. We also prove arrival and claim fences for in-flight requests and concurrent recoverers. Finally, we show how bounded deduplication state and truncated source history limit the lifetime of the guarantee.