Skip to main content
Conseqa treats idempotency as a transitive, coinductive property over the entire causal effect graph of an operation. The verifier does not settle for declaring a key or checking a unique index. It traces every effect an operation causes, including cascades into downstream operations through topics, requests, and outbox writes, and establishes that none of them perform externally distinguishable duplicate work.

​
The three-leg proof

For each declared idempotency requirement, the verifier analyzes every admitted path through the program and checks three independent legs. All three must hold on every admitted path. State leg. Every transaction on the path must be retry-safe. A transaction is retry-safe in one of two ways:
  1. Keyed commit deduplication — the transaction declares deduplicated_by with a stable key. On re-encounter, the prior commit resolves and its artifacts are restored without re-executing the body.
  2. Natural replayability — the verifier can establish from the transaction’s declared isolation, mutation semantics, and deterministic provenance that a second execution produces the same logical outcome.
Effect leg. Every effect-executing step must be duplicate-safe. Publications, requests, external effects, and outbox writes each have their own discharge conditions. Critically, the check is transitive: a publication is only safe if every modeled consumer collapses duplicate deliveries, which means that consumer’s idempotency must also be proven. An outbox boundary does not terminate the causal graph: the cascade continues through every outbox input admitting the written schema. Control leg. Every decision on the path must replay. A match_result replays if the matched result is replay-stable across attempts. A branch replays if its condition is deterministic over stable roots. An unstable decision means a retry may take a different arm and do different work.

​
Declaring an idempotency requirement

Add idempotency to the operation’s requirements block:
The key identifies the logical invocation class. All key components must come from a single input of the operation: the triggering input. The verifier uses this key to determine which two attempts it reasons about as “the same logical invocation.” result: replay_consistent adds a further obligation: not only must repeated attempts avoid duplicate work, they must return the same result variant and a replay-equivalent payload. Omit it if you only care about effect safety and not result stability.

​
Greatest-fixpoint coinductive reasoning

Request and consumer discharge make idempotency verdicts mutually dependent, and cycles are legal models. V1 computes each family’s verdicts as a greatest fixpoint: every requirement with an admissible governing key is assumed, and whatever fails under that assumption is dropped until nothing more fails. The iteration is monotone, and a cycle whose members each pass their local checks under the mutual assumption is proven and marked coinductive. The soundness argument is by minimal counterexample. Suppose some member of a self-consistent set were violated: some execution in which duplicate attempts at one of its logical invocations cause distinguishable duplicate work. Among all such violations across the set, take one whose duplicate work lies at the shortest causal distance from the duplicated attempts. That work is not on the invocation’s own path, because the state leg, the external leg, and the publication leg are discharged by local facts that assume nothing about the set. So it lies downstream of a request, publication, or outbox write, and the local check establishes that the duplicates reached the target or consumer as payload-equal inputs, falling into one class of that downstream requirement. The duplicate work is then caused by duplicate attempts of that downstream invocation, at a strictly shorter causal distance, contradicting the choice of violation.

​
Producer-suppressed vs consumer-collapsed outbox discharge

An outbox write introduces two distinct discharge routes. Producer-suppressed. The containing transaction’s keyed commit deduplication, over a key stable for the governing attempt class, admits at most one logical commit per class. Hence at most one committed occurrence of the write exists. No class-fixity of the message instance is needed: the single commit admits whatever it admitted, once. This route reuses the existing transaction idempotency rules and is independent of what consumers do. Consumer-collapsed. Where repeated executions may commit repeated writes, the publication pattern applies: the destination outbox declares a keyed message identity covering the written schema, the instance is class-fixed (repeated writes denote the same logical message), and every modeled consumer of that message collapses duplicate deliveries through an idempotency requirement keyed from its outbox input that is itself proven, or through at_most_once outbox delivery. The two routes remain distinct in the proof and carry different evidence. A model may discharge one route, both, or neither.

​
What acknowledge_on_success does not do

A subscription or outbox input may declare acknowledge_on_success: true. This states that when an invocation reaches successful logical completion, the triggering source item is acknowledged for this consumer. It does not close an idempotency proof, and it does not prove duplicate collapse. Under at_least_once delivery, failure or uncertainty before acknowledgement may admit another attempt, so the consumer’s own idempotency requirement is what the discharge cites. Acknowledgement defines the consumption-completion boundary, not a duplicate-delivery guarantee.

​
Concrete example: publish plus downstream consumer

Consider a minimal pipeline with a producer operation and a consumer operation connected by a topic. Producer (op.publish_event):
  • Request input with keyed identity on request_id.
  • Transaction deduplicated_by on request_id.
  • write_outbox staging Event with idempotency_key_propagation from request_id to event_id.
  • Idempotency requirement keyed on request_id.
Consumer (op.handle_event):
  • OutboxInput consuming the outbox, keyed message identity on event_id.
  • Transaction deduplicated_by on event_id.
  • Idempotency requirement keyed on event_id.
The verifier proceeds as follows:
  1. Assume op.publish_event idempotency holds. On the producer’s path, the transaction suppresses duplicate commits via deduplicated_by. The outbox write is therefore producer-suppressed. No duplicate logical work is possible at the source. The cascade continues through the outbox because an outbox boundary does not terminate the graph.
  2. The outbox declares keyed message identity on event_id, and the producer’s propagation maps request_id to event_id, so payload-equal producer duplicates yield payload-equal outbox messages. Those fall into one class of the consumer’s event_id key.
  3. Assume op.handle_event idempotency holds. Its transaction suppresses duplicate commits by event_id, so duplicates at the consumer collapse. The consumer therefore performs no distinguishable duplicate work for payload-equal inputs.
  4. Both assumptions hold together under the greatest-fixpoint iteration. The proof is marked coinductive because the producer and consumer each close the other: the producer’s suppressed commit means no new work reaches the consumer, and the consumer’s collapsed duplicates mean any work that does reach it is idempotent.
If you remove deduplicated_by from the consumer’s transaction, the fixpoint drops it: the consumer cannot collapse duplicates, so the producer’s cascade is no longer closed, and both obligations become unknown.

​
Proof scope: l0_only vs runtime_dependent

Every proof records the semantic layers its argument consumed:
  • l0_only — no explicit L1 fact was required. Proofs resting on transaction structure, keyed commits, deterministic provenance, and declared identities stay in this scope.
  • runtime_dependent — at least one L1 fact was necessary. Proofs that consume delivery semantics (at_least_once), routing, member_concurrency, or outbox runtime facts fall here.
For example, a proof that a transaction’s deduplicated_by suppresses an outbox duplicate is l0_only: it uses only the transaction declaration and the request identity, both L0 facts. A proof that at_least_once outbox delivery guarantees recoverability is runtime_dependent: it consumes an L1 delivery fact.

​
Going from unknown to proven

When an obligation is unknown, the checker’s evidence tells you exactly what is missing. Common patterns and their fixes:
The transaction is not deduplicated_by a stable key and cannot be proven naturally replayable. Add deduplicated_by with a key whose components all derive from the triggering input, using only key components or identity-pinned fields as roots.
The external effect is not_deduplicated or has unspecified idempotency. If the external boundary supports deduplication, declare deduplicated_by with a stable key. If it genuinely does not, the obligation cannot be proven without redesigning the integration.
A match_result branches on an unstable result. For an external effect, ensure the boundary declares deduplicated_by and the error disposition is terminal. For a request effect, ensure the target operation proves result: replay_consistent for the targeted input. A result bound by race is conservatively treated as unstable by V1.
A publication or outbox write’s safety is conditional on every modeled consumer collapsing duplicates. If a consumer’s idempotency is unknown, the upstream obligation inherits the gap. Fix the consumer’s obstacles first; the upstream proof follows automatically through the verifier’s greatest-fixpoint computation.
Without a keyed message_identity on the topic or outbox, two messages with equal identity fields are not declared to be the same logical message. Declare message_identity with a mapping for each admitted schema. Without it, duplicate deliveries may have different payloads from the verifier’s perspective and cannot be proven safe.

Checkout Flow Guide

Build a full flash-sale checkout with outbox and async payment.

CI Integration

Automate verification in your CI pipeline.