Requirements are the correctness properties you want your architecture to satisfy. You declare them on operations under the requirements key. The verifier then attempts to prove each requirement from the facts declared elsewhere in the model — topic ordering, transaction isolation, delivery semantics, dispatch routing, and so on. Declaring a requirement says “this must hold.” It does not assert that it does hold. Only a proven verdict does that.
Declaring a requirement is not the same as proving it. Always check the verification output for the verdict (proven, unknown, or disproven) before relying on a correctness property in production.
The four requirement kinds
An operation’s requirements block contains four lists. Each list is empty ([]) by default, meaning no obligation is declared for that property.
Serialization
A serialization requirement declares that same-key invocations must not execute concurrently.
key is a single ValueRef — a source and a field path. The requirement constrains only invocations triggered by the input the key is sourced from. Invocations with different key values may run concurrently; invocations with the same key value must not overlap.
Serialization establishes mutual exclusion only. It does not establish which same-key invocation comes first. A non-FIFO lock or single-lane execution with any enqueue order may prove serialization without proving ordering.
Proven by: a mechanism that prevents overlap for equal key values — for example, by_topic_key dispatch with lane_concurrency: bounded(1), or an exclusive lock acquired before any conflicting work.
Ordering
An ordering requirement declares that same-key invocations must take effect in the semantic precedence order established by their source.
Ordering is strictly stronger than serialization. A proof must establish both where the relevant precedence comes from and that the execution mechanism preserves it. Arbitrarily serializing concurrent inputs satisfies serialization but cannot invent a required semantic precedence.
V1 recognizes one precedence source: the order declared on the key’s subscription topic — a keyed topic’s per-key order (when the ordering key carries the topic key for every admitted schema), or a global topic’s order for any key.
The standard execution mechanism:
Each declaration contributes a different fact; none substitutes for another.
Idempotency
An idempotency requirement identifies a logical invocation by a composite IdempotencyKey and declares that repeated attempts representing the same logical invocation must not cause externally distinguishable duplicate logical work beyond what the declared idempotency contract permits.
Idempotency key
key is an IdempotencyKey: an ordered tuple of ValueRef components. Two attempts share the same logical invocation identity when all components evaluate to equal values. The key is a composite — not a set of alternatives.
Every component must be sourced from a single input of the operation (the triggering input). A component sourced from mutable state or from an artifact the invocation itself produces cannot define a pre-execution equivalence class; such a key yields an unknown verdict.
result: replay_consistent
When result: replay_consistent is declared, the verifier additionally checks that repeated admitted attempts in the same idempotency class that return a request result return the same result variant and a replay-equivalent payload. Omit this or use result: unspecified when you need only side-effect safety, not a stable return value.
What the verifier checks
For each admitted path through the program, the verifier checks three legs:
- State leg. Every transaction on the path must be retry-safe: either naturally replayable or deduplicated by a stable key.
- Effect leg. Every effect-executing step must be duplicate-safe: a publication is safe when topic identity and all modeled consumers’ idempotency collapse duplicates; a request is safe when the target proves its own idempotency; an external effect is safe when
deduplicated_by with a stable key.
- Control leg. Every decision on the path must replay: a
branch condition is deterministic over replay-stable roots; a match_result matches a replay-stable result.
The verifier computes verdicts as a greatest fixpoint across mutual dependencies between operations (publications through topics, requests to other operations), so a cycle of requirements that each collapse the others’ duplicates can be proven.
Recoverability
A recoverability requirement declares that the logical invocation identified by its key must reach a valid terminal (return or complete) after any modeled interruption.
Recoverability is a progress obligation. Idempotency is a safety obligation. Neither implies the other.
- Idempotency without recoverability — repeated attempts are safe, but there is no obligation to re-drive the invocation to completion. An interrupted operation that is never retried violates nothing idempotency-wise.
- Recoverability without idempotency — the invocation must eventually reach a terminal, but repeating the work is assumed harmless. Use this when the operations are inherently safe to repeat.
completion: resumable
An interrupted attempt must be able to resume and drive the program to a terminal. The verifier checks that every already-committed transaction resolves on re-encounter (by natural replay or by deduplicated_by key), and that every artifact a later step consumes is replay-available.
resumable does not oblige the architecture to actually re-drive the invocation. Use it when the retry driver lies outside the model — typically a request input whose caller Conseqa does not model.
completion: guaranteed
In addition to resumability, the architecture must guarantee that the logical invocation is re-driven until the program reaches a terminal. This is a liveness obligation.
A guaranteed proof requires a modeled retry driver:
delivery: at_least_once on the triggering subscription, or- an inbound
RequestEffect whose retry is may_repeat
guaranteed recoverability proofs are conditional on the delivery abstraction genuinely redelivering until the invocation succeeds. at_least_once delivery does not encode retry timing, retry count, backoff, or a bounded eventual-delivery liveness guarantee. The proof rests on the modeled fact, subject to implementation conformance.
If you declare completion: guaranteed on an operation that has no idempotency requirement keyed from the triggering input, the verifier emits a warning. The retry driver makes retries expected, and nothing declares them safe.
Verdicts
After running conseqa model.yaml, every declared requirement receives one of three verdicts:
unknown is epistemic — it means the model does not provide enough facts to complete a proof. It does not mean the implementation is actually incorrect. Respond to unknown by adding the missing declarations (a keyed transaction deduplication, a declared message identity, a dispatch routing fact) rather than treating the requirement as satisfied.
disproven identifies a specific structural gap or contradiction. The obligation summary names the path and the obstacle.
A complete requirements example
The following is the full requirements block from operation.apply_payment in the flash checkout model. It declares serialization and ordering over order_id (so same-order payment applications are serialized and ordered), idempotency keyed by event_id (so duplicate deliveries of the same PaymentCaptured event are safe), and guaranteed recoverability (so the order is never left in paid state without the downstream effect having been attempted).
Requirements and the verification cascade
Idempotency verdicts are mutually dependent: a publication effect is safe only when every modeled consumer collapses duplicates, and a request effect is safe only when the target proves its own idempotency. The verifier computes all verdicts together as a greatest fixpoint. A cycle of requirements that each collapse the others’ duplicates is marked proven (coinductive) — the proof rests on the mutual assumption, which is sound by a minimal-counterexample argument.
The same fixpoint governs result: replay_consistent requirements through request chains. A proof of replay consistency in one operation may depend on replay consistency in the operation it calls, and vice versa. 
