---
title: "Failure transparency proof"
description: "Dex has a computer-checked proof that failures add only one thing you can"
canonical_url: "https://docs.superdurable.io/correctness-and-expressiveness/failure-transparency-proof/"
source: "docs/content/correctness-and-expressiveness/failure-transparency-proof.mdx"
locale: "en"
---

# Failure transparency proof

Dex has a computer-checked proof that failures add only one thing you can
observe: repeated external effects. The proof holds under the conditions in
[What the proof assumes](https://docs.superdurable.io/correctness-and-expressiveness/failure-transparency-proof.md#what-the-proof-assumes).

- [Download the paper (PDF)](https://docs.superdurable.io/papers/dex-expressiveness.pdf)
- [Formal sources on GitHub](https://github.com/superdurable/dex/tree/main/formal)

<a id="the-claim"></a>

## The claim

The proof covers these failures:

- the server crashes and restarts from its durable log;
- a standby server takes over;
- a Step method attempt fails, for example on a Worker error, a timeout, or a
  Worker disconnect, and Dex retries it;
- a Worker keeps running an attempt after Dex gave up on it;
- a Worker result arrives twice, or arrives after its attempt was replaced;
- a client sends the same **StartFlow** request again.

It compares runs with these failures to runs of the same Flow without them,
in three parts.

- **Remove the repeats, and a sequence without failures remains.** Remove
  every repeated external effect from the events of a run with failures so
  far. The rest is a sequence that the Flow can produce without failures, for
  the same requests minus the **StartFlow** retries.
- **Every sequence without failures stays possible.** A run in which no
  failure happens produces it.
- **Fair runs end the same way.** Take the whole event sequence of a fair run
  with failures, and remove the repeats. The result is the whole event
  sequence of a fair run without failures. Both runs complete, both get
  stuck, or both keep running. The reverse direction is proved for requests
  without **StartFlow** retries. A retry advances the server's clock, so it
  can change which timer is due first.

Each repeated effect is an exact copy of an earlier effect of the same Step
method.

Combined with the
[Expressiveness proof](https://docs.superdurable.io/correctness-and-expressiveness/expressiveness-proof.md),
this covers every well-formed program of its small concurrent language. On
Dex, such a program produces the events of a run without failures, except
that external effects can repeat. For these programs, each extra effect
equals an earlier effect in value.

<a id="why-repeats-stay-simple"></a>

## Why repeats stay simple

A Step method can run in several attempts. Every attempt reads the same
snapshot: Dex takes it at the first attempt, and every retry reuses it.

The proof assumes that a Step method's effects depend only on what Dex passes
it, and not on which attempt is running. Then every attempt computes the same
external effects, in the same order.

An attempt makes its effects one after another, so each effect first appears
in list order. The first copy can come from any attempt, including an old one
that Dex gave up on. Every later copy is a repeat. No attempt adds a new
effect or changes the order of the first copies.

<a id="what-it-means-for-you"></a>

## What this means for your code

Make each external call safe to repeat and safe to arrive late. A retry can
run a Step method's external calls again. An older attempt can make a call
late, after a newer attempt made the same call. The proof does not prevent
these repeats.

A common way to do this is an idempotency key that the external system
deduplicates on.
Build it from the Flow run, the Step execution, the method, and the effect.
The [Step guarantees](https://docs.superdurable.io/concepts/step.md#guarantees) say more about keys.

When a client retries a request:

- **StartFlow**: reuse the request ID of the first start, set the option that
  returns the existing run on both the first start and the retry, and keep the
  default ID reuse policy. The proof then covers the retry if the server's log
  orders it before Dex purges the closed run. Reaching the server first is not
  enough. See [Start options](https://docs.superdurable.io/concepts/flow.md#start-options).
- **PublishToChannel**: a request sent again after a lost response is a second
  request, and it can publish the message twice. Publishing once through RPC
  request IDs is planned in
  [issue 1519](https://github.com/superdurable/dex/issues/1519).
- **StopFlow**: a retry without a run ID can stop a newer run of the same Flow
  ID. Passing a run ID is planned in
  [issue 1520](https://github.com/superdurable/dex/issues/1520).

<a id="what-the-proof-assumes"></a>

## What the proof assumes

The proof holds under these conditions:

- **The scope of the expressiveness proof.** One Flow is started once and
  receives Channel messages. Under failures, RPCs, SubFlows, **StopFlow**, and
  Attribute locks are outside the proof.
- **SYNC methods only.** An **ASYNC** method can lose its start in a server
  crash. It then runs again on a new snapshot, so its effects can differ.
- **Retries never run out, and every error is retryable.** Running out of
  retries, or a non-retryable error, fails the Flow. Without failures, a Flow
  fails only when its own code fails it. A long server outage can use up the
  retry time.
- **No failure policy.** A policy that proceeds after a failure changes what
  runs next.
- **Code ignores its attempt.** Effects and results do not depend on the
  attempt number, the first attempt time, the last error, or the last
  heartbeat value. Code that resumes from a heartbeat checkpoint is outside the
  proof.
- **No hard-delete Attributes.** Dex reads them again on every attempt.
- **Every attempt command names its task.** The server tags each command of a
  started attempt, such as its result, a heartbeat, or its failure, with the
  task that ran it. Every logged command of this kind carries the tag.
- **The clock does not step back.** On one server, the clock does not step
  back between checking that a timer is due and stamping the command that
  fires it.
- **Timers fire in order.** Each firing takes the earliest due timers first,
  ordered by fire time, and timers due at the same time in a fixed order. The
  real server has a short window in which it can fire a timer while an
  earlier-due timer still waits. Both proofs leave that window out.
- **One server at a time.** A standby takeover is covered. Several servers
  that own the same Flows at once are not.

The ending part of the claim holds for fair runs. A run is fair when:

- Every request of the outcome word gets its final outcome, in order. The
  outcome word lists the client requests in the order of their final
  outcomes. A request lost before any outcome is not in it.
- The server's clock grows without bound.
- Failures happen only finitely often, and the server comes back after each
  crash.
- A timer that stays armed and due eventually fires.
- A Step method that stays ready to start while the server is up eventually
  starts.
- Every Worker task, including an abandoned one, eventually finishes or is
  dropped.
- Every finished result eventually commits or is ignored.
- Every attempt that a crash interrupted is eventually handled, or cleared by
  a later crash.

<a id="what-it-does-not-say"></a>

## Server time and real time

The proof measures time in the server's stamps. By those stamps, a timer never
fires before its time. A server clock that runs ahead can still fire it early
in real time.

<a id="how-it-was-checked"></a>

## How it was checked

- **A written failure model.** Every failure rule is written down with the
  server code that implements it. Reviewers checked each rule against that
  code.
- **A computer-checked proof.** The proof is written in the Lean proof
  assistant, which checks every step.
- **Tests before the proof.** A fuzzer walked random runs with crashes,
  retries, and late attempts, and checked the argument at every step.
- **Examples and counterexamples.** The proof assistant checks example runs
  with a crash, retries, and a late repeated effect, and applies the proof to
  them. It also checks runs that break an assumption, such as code that reads
  its attempt number, and shows that the claim then fails.

<a id="related-pages"></a>

## Related pages

- [Correctness and expressiveness](https://docs.superdurable.io/correctness-and-expressiveness.md)
- [Expressiveness proof](https://docs.superdurable.io/correctness-and-expressiveness/expressiveness-proof.md)
- [Step guarantees](https://docs.superdurable.io/concepts/step.md#guarantees)