Model checking exposed failures in cloud recovery

A worker creates a disk for a Virtual Machine, then crashes before recording that the operation finished. On restart, the work looks incomplete.

Recovery can create the disk again, stop with an error or look for the result of the first attempt. The right choice depends on what the system can still establish after the crash.

These are the gaps we use model checking to explore. Our June 2026 review led to 14 correctness findings. Thirteen fixes are in the main codebase, and the fourteenth is written and awaiting merge. The findings came from modeling the implementation’s workflows and checking those models against the rules each workflow must follow.

We use TLA+, a language for describing how a system can change from one state to another. The model leaves out most implementation detail so we can concentrate on the decisions that affect correctness.

For a create operation, the important distinction is between doing the work and durably recording its result. We allow a crash between those steps and examine what recovery can observe.

The checker explores the states reachable under the model’s assumptions and bounds. If a rule fails, it produces a sequence of steps that leads to the failure. That sequence is often easier to discuss than a broad claim that retries are safe.

Before writing a model, we need a precise statement of what correct behavior means. A retry should not create an extra resource. A resource should not be reported ready before the required work is complete.

Progress matters too. A design can avoid duplicate work by refusing to proceed, yet leave an administrator with a job that never finishes. We examine both unsafe outcomes and the conditions needed to make progress.

We also keep deliberately broken versions of models. Removing a safeguard should produce a failing sequence that explains why the safeguard matters. This checks that our models can detect the mistakes they were written to prevent.

With safe replay disabled, the checker found a duplicate-disk failure in five states: creation starts, the clone completes, the worker crashes, recovery resumes, and the clone runs again. A single request can leave two disks. Restoring the safeguard prevents that sequence in the model.

A retried operation must account for work already done. The failing trace identifies the crash boundary where that requirement breaks.

Engineers can use that sequence when reviewing the recovery code and its tests.

The findings were practical. We changed recovery that could repeat destructive provisioning work, replay behavior that mishandled an already-attached volume, and completion checks that could overstate a snapshot’s consistency.

The review also exposed a deletion path that could lose its record before cleanup finished. Retaining that record gives a failed teardown something to resume from. Across these cases, the model forced us to say what evidence actually establishes completion.

One hibernation model needed correction too. A process disappearing did not prove that its memory image had been saved. We strengthened the completion rule and kept a deliberately failing model of the old assumption. The models are part of the engineering work, so they need review as well.

A model checker examines the model we give it, so each model has to be tied back to the running software.

We link modeled requirements to named implementation tests and check those links automatically. That makes missing evidence visible when the software changes. The report marks each property as implemented or still in design.

Our models abstract the storage, networking and compute systems around a workflow and bound the failures, so the checker explores a finite problem. Implementation tests and failure experiments cover the real systems.

The model suite and its implementation checks run in under a minute on a workstation, which makes frequent checking practical. Most of the effort goes into writing accurate models and linking them to code. Next, selected models will generate implementation tests directly.

Published work from AWS, MongoDB and Datadog helped shape this approach. Their accounts show how formal models can sit alongside testing in everyday engineering work.

For us, a useful starting point is a small workflow with a clear crash boundary. It gives the team a tractable question before attempting to model more of the system.