Why Recovery Paths Need Separate Verification

The correctness of a recovery procedure depends on what it reads as evidence of success and on the order in which it runs. Code that passes normal-path tests can leave both conditions unchecked.

Recovery code in a distributed system runs when the system is already degraded. For example, nodes are overloaded, the network is partitioned, or a write between two stores stopped halfway. Normal-path tests run code under conditions where each step's result is directly visible and actions do not overlap.

Two things decide whether a recovery procedure is correct. The first is what the procedure uses as evidence of success. Some signals look like evidence: a record that a command was sent, a sender-side checkpoint, or a failed health check. These signals may not record the result of the action being judged.

The second is execution order. When several recovery actions overlap, the difference in the time each action takes effect changes the result. Research and operational reports on cluster membership, outbox relays, and consistency checkers point to the same conclusion from different layers. This post collects that evidence into a checklist for recovery procedures.

Order of Overlapping Recovery Actions

Characterizing Metastable Faults and Failures (arXiv:2606.00942, 2026-05) analyzes an incident on a commercial gaming platform. This platform has hundreds of millions of users, and its cluster manager keeps at least W_min active workers. It sends sleep to a worker that misses heartbeats and wakeup to an idle worker.

After some workers crashed, the number of active workers did not return to W_min. It oscillated instead. The oscillation continued after the crashed workers recovered, and the paper states that packet loss and queueing delay were not causes. Nothing in the worker or cluster manager implementations suggested the root cause.

The cause is a combination of two implicit properties. Overloaded workers miss heartbeats, and wakeup takes effect later than sleep. The paper gives an example: wakeup includes provisioning a virtual machine, while sleep is a single state change.

flowchart TD
  A["Some workers crash"] --> B["Remaining workers overloaded"]
  B --> C["Heartbeats missed"]
  C --> D["sleep and wakeup issued together"]
  D --> E["sleep takes effect first"]
  E --> F["Active workers decrease"]
  F --> B
  D --> G["wakeup completes late"]
  G --> H["New workers also overloaded"]
  H --> C

Workers try to handle load, and the cluster manager tries to restore the active worker count. Each component, seen alone, acts in a stabilizing direction. The failure comes from the time gap between sleep and wakeup. If the remaining workers are not overloaded, missed heartbeats do not continue, and this cycle does not start.

Rules That Keep Removal Tentative

The paper classifies sleep as a destabilizing action and wakeup as a stabilizing action. It sets two principles: destabilizing actions must be tentative (R1), and stabilizing actions must take precedence (R2). The proposed cluster manager does not change functionality. It controls only the timing of actions.

This cluster manager puts a timed-out worker in the snoozing state and delays sleep by an artificial delay d'_sleep. The replacement worker enters waking-up and becomes active only after confirmation. Without confirmation, it returns to idle. If no idle worker exists, the cluster manager records the old worker as pending-timeout. It retries until a heartbeat arrives or it finds an idle worker.

These states also address the evidence problem. A record that wakeup was sent is not evidence of startup, and only a confirmed startup counts as an active worker. The paper explains that with only idle and active states, overlapping actions can send wakeup to an overloaded worker.

The delay value is also set for overlapping actions. If the design keeps only d_wakeup < d'_sleep, it guarantees order only for the sleep and wakeup pair from the same timeout. A sleep can still take effect before a wakeup from a different timeout, so the paper requires the condition below.

d_wakeup + T < d'_sleep
 
d_wakeup : time until wakeup takes effect
T        : heartbeat check period, also the pending-timeout retry period
d'_sleep : artificial delay added to sleep

The paper implemented this case in Nyx, a domain-specific language (DSL), to study its dynamics. It generated a vector field for a 40-worker cluster with fixed timeouts from 1,000 runs, each simulating 100 seconds. Generation took about three minutes. This result shows the tendency to oscillate. It is not a measurement of recovery time in a production environment.

Where Recovery Reads Evidence of Success

In outbox and change data capture (CDC) relay recovery, where the procedure reads its evidence decides correctness. From 2PC to the Commit Log covers the information bound of sender-only recovery. It also covers how a sink acceptance record lets recovery compute the missing operations. This section covers only which records count as evidence.

Machine-Checked Dual-Write Recovery from a Commit Log (arXiv:2608.00501, 2026-08) defines evidence narrowly. Reading a source outbox or a relay cursor does not turn that record into the sink's acceptance record. An outbox table can act as the acceptance record only if it holds sink-owned acceptance state that is updated atomically with acceptance.

The acceptance record must be authoritative, complete, and current at the time of the decision. The paper classifies a stale replica, a paginated status endpoint, and a lagging projection of sink state as different observations. The theorems do not apply to them without a separate argument.

The paper explains that more careful checkpoint management or a different checkpoint encoding does not close this gap. The gap is the interval between two durable writes, not the way the cursor records progress.

An operational case can be read the same way. Toss Payments does not fail a whole payment when an Outbox write fails. It gives priority to payment availability, and some external payment provider integrations do not support rollback. Its 2025-12 post states that it identified transactions missing from the Outbox through Elasticsearch (ES) logs and a fallback log on the server's local disk.

Toss Payments republished events for all transactions in the outage window. As a result, the service that loads events showed duplicate approvals and cancellations. Toss Payments then added an idempotency key to the event header so that consumers can identify the same transaction. The public text reads as if recovery did not use the consumer's existing records to set the republish scope. This is an estimate based on the public text.

The public text does not describe the deduplication store, the retention period, or the atomicity implementation. Idempotency and Transaction Integrity in Payment Systems covers how to store an idempotency key and change state atomically.

Evidence That Fits the Action

The same signal can be evidence for one action and not for another. A 2023-04 AWS post divides Elastic Load Balancing (ELB) health checks into two types. Shallow checks look only at local state, and deep checks also test external dependencies. It then compares the results of connecting each check to replacement decisions in an Auto Scaling group (ASG).

In the third setup, the load balancer fails open and sends traffic to all targets. The ASG marks all instances unhealthy and starts to replace them. Service returns only after the new instances bootstrap and pass health checks. The post explains that this can take significantly longer than waiting for the transient problem to end.

Under the AWS recommendation, a failed deep check is evidence for routing decisions and not for instance replacement. Gray Failure Detection in Adaptive Routing covers how to detect gray failures that pass health checks.

The AWS post gives a heartbeat table pattern to replace instances with local failures while deep checks stay in use. Each instance writes its local status and a timestamp to a DynamoDB table. A watcher runs every minute and finds entries that are unhealthy or not updated for a set time, such as five minutes. It marks those instances unhealthy.

The watcher also has a velocity control. The post gives an example: replace only one instance per minute, and alert a human if the watcher tries to replace more. One minute, five minutes, and one instance per minute are examples for explanation, not values set by experiment.

Signals that observe recovery state need the same distinction. A 2024-01 Woowa Brothers post explains that a Resilience4j fallback runs whenever the protected method fails, independent of the circuit breaker state. Fallback execution therefore does not show the current circuit breaker state, so the post records state transition events separately with onStateTransition.

Criteria Used by Consistency Checkers

In fault injection testing, the checker's criterion acts as the evidence of success. Jepsen injects server failures, packet delays, network partitions, and clock skew, and passes the operation history observed by clients to a consistency checker. A history that the checker passes is correct only under that criterion.

A 2026-08 paper (arXiv:2608.17388) generalizes consistency checking for non-transactional distributed storage. It gives three reasons why formally verified systems still violate their guarantees. One reason is that the verification process did not consider certain types of faults.

The paper also identifies a limit of checker criteria. The existing non-transactional checkers, Porcupine and Knossos, check only linearizability. ZooKeeper does not provide linearizability, so a Jepsen analysis that checked ZooKeeper histories with Knossos was not considered meaningful.

The Wing-Gong linearizability checking algorithm checks three properties: SingleOrder, RVal, and RealTime. The paper's tool, Pine, keeps SingleOrder and generalizes RVal to Validity and RealTime to Ordering.

Pine also adds ordering information that systems return in responses, such as revision numbers, zxid values, and instance numbers, as constraints between pairs of operations. With this change, the guarantee that a system actually promises becomes the checking criterion.

The HoliPaxos result shows the difference. Tests with network partitions produced histories that passed the linearizability check but violated the HoliPaxos criterion, which adds instance-number order. The replication log showed that one operation was committed three times, at instances 451, 456, and 461. Only the last result went back to the client.

The ballot number in responses changed from 258 to 770, which indicates a leader re-election after the partition. The cause was non-idempotent handling of retried operations after a new leader was elected. Raft Leader Leases and Linearizable Reads covers how the interval right after a leader change affects read guarantees.

The authors changed put operations to increment operations and confirmed that the linearizability check then also failed. They fixed the bug with the RIFL approach, which gives each operation a unique ID and stores its result.

A put that writes the same value gives the same read value however many times it is applied. Thus a criterion that checks only values can miss duplicate application. Whether a recovery-path bug becomes visible depends on fault injection, and also on the checking criterion and the shape of the workload.

The authors tested 8 distributed storage systems and report 6 new consistency violation bugs in 4 of them. Existing checkers could not find 5 of these bugs. Checking system-specific criteria was up to 370 times faster than checking the basic consistency criteria. The paper does not state which system produced this value. The two results come from different conditions, as shown below.

Conditions Under Which the Claim Does Not Hold

Not all bugs come from the recovery path. The three bugs that Pine found in EPaxos-revisited appeared even without fault injection. Separate verification of the recovery path does not replace checking the normal path with strong criteria.

The convergence proof in the membership paper rests on narrow assumptions. It assumes that overload is an instantaneous function of the active worker count, that W_noOverload = W_min, and that the shock is temporary. The reliability of the control message path is an assumption that the authors inferred from the incident. An environment where the control path is also overloaded is outside the scope of this proof.

The dual-write paper proves its theorems in an Isabelle/HOL model under conditions P1-P4. Its verdicts apply to the state after recovery finishes, and it makes no liveness claim that delivery eventually completes. Each system must check separately whether its real sink acceptance record is authoritative, complete, and current.

None of the three papers measures how much separate verification of the recovery path reduces failures. The evidence consists of cases where implementation review or a weak checking criterion did not reveal the cause. Extending these cases into a general principle is a judgment. For some systems, the cost of building a fault injection environment and system-specific criteria can be larger than the benefit.

Checklist for Verifying Recovery Procedures

Answer the questions below for each recovery action. The first four questions are about evidence, the next three about order, and the last four about verification methods.

Normal-path tests cannot answer most of these questions. To answer them, create failure states and record the evidence that recovery actions read and the order in which they ran. If failure detection time, command issue time, and effect confirmation time are recorded separately, order problems can be reconstructed later. This is a judgment drawn from the cases above.

Incident Response and Management covers Game Day procedures that run fault injection as an operational exercise.

References

• Characterizing Metastable Faults and Failures, arXiv:2606.00942 (2026-05, based on v2 from 2026-06)
• Machine-Checked Dual-Write Recovery from a Commit Log, arXiv:2608.00501 (2026-08, based on v5 from 2026-09)
• Generalizing and accelerating consistency checking for non-transactional distributed storage systems, arXiv:2608.17388 (2026-08)
• Choosing the right health check with Elastic Load Balancing and EC2 Auto Scaling (AWS, 2023-04)
• 레거시 결제 원장을 확장 가능한 시스템으로 (Scaling a Legacy Payment Ledger) (Toss Payments, 2025-12, in Korean)
• 개발자 의식의 흐름대로 적용해보는 서킷브레이커 (Applying a Circuit Breaker Step by Step) (Woowa Brothers, 2024-01, in Korean)

Every figure was checked against each original source as of 2026-10.

Summary

The correctness of a recovery procedure depends on what it reads as evidence of success and on the order in which it runs. In the membership case, sleep took effect before wakeup and the active worker count oscillated. The dual-write paper does not accept a relay cursor or a lagging projection as evidence of acceptance. In the HoliPaxos case found by Pine, a history with duplicate commits after a leader re-election passed the linearizability check.

Problems with both conditions often stay hidden on the normal path, where actions do not overlap and results are directly visible. The recovery path therefore needs separate verification under injected failures, with the checking criterion that the system actually promises. The evidence consists of cases and conditional proofs, and no source measures how much separate verification reduces failures.