Step-by-Step: Modeling a Flash-Sale Checkout in Conseqa

This guide walks you through building a realistic flash-sale checkout model from scratch. You will create an order data model with a typed outbox, model a request-driven placement operation that charges payment asynchronously, add a downstream receipt consumer, and tie the pieces together with a runtime layer that proves both idempotency and ordering.

Declare schemas

The checkout pipeline uses request, event, and response schemas. completeness: complete tells the verifier these declarations describe the full logical shape.

schemas:
  schema.PlaceOrderRequest:
    kind: canonical
    completeness: complete
    fields:
      idempotency_key: string
      order_id: uuid
      tenant_id: uuid
      amount: decimal

  schema.OrderPlaced:
    kind: canonical
    completeness: complete
    fields:
      event_id: string
      order_id: uuid
      tenant_id: uuid
      amount: decimal

  schema.ChargeCardRequest:
    kind: canonical
    completeness: complete
    fields:
      charge_id: uuid
      amount: decimal

  schema.ChargeAccepted:
    kind: canonical
    completeness: complete
    fields:
      charge_id: uuid

  schema.ChargeDeclined:
    kind: canonical
    completeness: complete
    fields:
      reason: string

  schema.ReceiptSent:
    kind: canonical
    completeness: complete
    fields:
      receipt_id: uuid
      order_id: uuid

The event_id field on schema.OrderPlaced is what enables keyed message identity on the outbox. Without it the verifier cannot establish that duplicate deliveries carry the same logical message.

Declare the data model and outbox

Persistent state lives in a data model. The checkout flow has one data model with an object and a typed outbox.

data_models:
  data.orders:
    objects:
      object.order:
        schema: schema.OrderPlaced
        identity:
          - order_id
    outboxes:
      outbox.order_events:
        messages:
          - schema.OrderPlaced
        message_identity:
          kind: keyed
          mapping:
            schema.OrderPlaced:
              - event_id

The outbox is a typed logical message collection belonging to the same transactional state boundary as the data model’s objects. A transaction declaring this data model may atomically mutate objects and admit messages to the outbox in one commit.

An outbox is not a topic. The outbox belongs to a data model and is written transactionally. A topic is an L0 logical channel that is produced by effect execution outside any transaction. The two are intentionally separate semantic concepts.

Model op.place_order

The placement operation receives a request, inserts the order inside a deduplicated transaction, stages the outbox message atomically, launches an async payment charge, awaits the charge with join_all, then branches on the result.

operations:
  op.place_order:
    service: service.checkout
    inputs:
      input.place_order.request:
        kind: request
        schema: schema.PlaceOrderRequest
        identity:
          kind: keyed
          fields:
            - idempotency_key
        result:
          ok: schema.ChargeAccepted
          err:
            schema: schema.ChargeDeclined
            disposition: terminal
    program:
      steps:
        - kind: transaction
          id: tx.place_order
          data_model: data.orders
          isolation: read_committed
          idempotency:
            kind: deduplicated_by
            key:
              components:
                - source: input:input.place_order.request
                  path: idempotency_key
          steps:
            - kind: insert
              object: object.order
              values:
                kind: deterministic
                from:
                  - source: input:input.place_order.request
                    path: order_id
                  - source: input:input.place_order.request
                    path: tenant_id
                  - source: input:input.place_order.request
                    path: amount
            - kind: write_outbox
              effect_id: effect.place_order.outbox_placed
              effect:
                outbox: outbox.order_events
                schema: schema.OrderPlaced
                idempotency_key_propagation:
                  - source:
                      components:
                        - source: input:input.place_order.request
                          path: idempotency_key
                    target:
                      components:
                        - source: effect:effect.place_order.outbox_placed
                          path: event_id
              values:
                kind: deterministic
                from:
                  - source: input:input.place_order.request
                    path: idempotency_key
                  - source: input:input.place_order.request
                    path: order_id
                  - source: input:input.place_order.request
                    path: tenant_id
                  - source: input:input.place_order.request
                    path: amount
        - kind: execute_effect_async
          handle: async.charge
          effect_id: effect.place_order.charge
          effect:
            kind: external
            name: payment_provider.charge
            idempotency:
              kind: deduplicated_by
              key:
                components:
                  - source: input:input.place_order.request
                    path: idempotency_key
            result:
              ok: schema.ChargeAccepted
              err:
                schema: schema.ChargeDeclined
                disposition: terminal
          values:
            kind: deterministic
            from:
              - source: input:input.place_order.request
                path: order_id
              - source: input:input.place_order.request
                path: amount
        - kind: join_all
          handles:
            - handle: async.charge
              bind: result.charge
        - kind: match_result
          result: result.charge
          ok:
            steps:
              - kind: return
                request: input.place_order.request
                outcome:
                  kind: ok
                  values:
                    kind: deterministic
                    from:
                      - source: effect_result_ok:result.charge
                        path: charge_id
          err:
            steps:
              - kind: return
                request: input.place_order.request
                outcome:
                  kind: err
                  values:
                    kind: deterministic
                    from:
                      - source: effect_result_err:result.charge
                        path: reason
    requirements:
      idempotency:
        - key:
            components:
              - source: input:input.place_order.request
                path: idempotency_key
          result: replay_consistent
      recoverability:
        - key:
            components:
              - source: input:input.place_order.request
                path: idempotency_key
          completion: resumable

Several things work together here:

tx.place_order is deduplicated_by the request’s idempotency_key. A second attempt under the same key resolves the prior commit instead of inserting a duplicate order and staging a second outbox message.
The write_outbox step stages OrderPlaced into the outbox atomically with the insert. Both commit together or abort together.
execute_effect_async launches the payment charge without blocking. The join_all step establishes complete(charge) < continuation so the program waits for the charge before returning.
The external payment effect declares deduplicated_by on the same idempotency_key, so duplicate executions collapse. Both ok and err dispositions are terminal, so the result is replay-stable.

Model op.dispatch_receipt

The downstream operation consumes the outbox and sends a receipt. It uses an OutboxInput, which is the honest way to consume a data model outbox: each committed message becomes one logical invocation.

  op.dispatch_receipt:
    service: service.receipts
    inputs:
      input.dispatch_receipt.orders:
        kind: outbox
        outbox: outbox.order_events
        messages:
          kind: only
          schemas:
            - schema.OrderPlaced
        acknowledge_on_success: true
    program:
      steps:
        - kind: execute_effect
          effect_id: effect.dispatch_receipt.email
          effect:
            kind: external
            name: email_provider.send
            idempotency:
              kind: deduplicated_by
              key:
                components:
                  - source: input:input.dispatch_receipt.orders
                    path: event_id
            result: null
          values:
            kind: deterministic
            from:
              - source: input:input.dispatch_receipt.orders
                path: event_id
              - source: input:input.dispatch_receipt.orders
                path: order_id
        - kind: complete
    requirements:
      idempotency:
        - key:
            components:
              - source: input:input.dispatch_receipt.orders
                path: event_id
          result: unspecified
      recoverability:
        - key:
            components:
              - source: input:input.dispatch_receipt.orders
                path: event_id
          completion: guaranteed

The acknowledge_on_success: true declaration says that when an invocation reaches successful completion, the triggering outbox message is acknowledged for this consumer. This does not close an idempotency proof and does not prove duplicate collapse: under at_least_once delivery, failure or uncertainty before acknowledgement may still admit another attempt, so the consumer’s own idempotency requirement is still needed.

Add the runtime layer

The optional runtime block declares how the L0 machine is realized. Here it declares execution pools, a router for the request, and an OutboxRuntime for the downstream consumer.

runtime:
  execution_pools:
    pool.checkout:
      member_concurrency:
        kind: bounded
        value: 1
    pool.receipt_workers:
      member_concurrency:
        kind: bounded
        value: 1
  routers:
    router.place_order:
      boundary:
        operation: op.place_order
        input: input.place_order.request
      pool: pool.checkout
      routing:
        key:
          - idempotency_key
        member_assignment:
          kind: consistent_hash
  outboxes:
    op.dispatch_receipt:
      input.dispatch_receipt.orders:
        delivery: at_least_once
        partitioning:
          kind: keyed
          mapping:
            schema.OrderPlaced:
              - tenant_id
        ordering: partition
        dispatch:
          pool: pool.receipt_workers
          member_assignment:
            kind: consistent_hash
          batching:
            ordering: preserved

Each runtime declaration serves a specific purpose:

execution_pools: member_concurrency: bounded(1) declares that each pool member executes at most one invocation at a time. This is the key fact that serialization and ordering proofs build on.
routers: The router keys request invocations by idempotency_key and assigns them to one member of pool.checkout via consistent hash. Equal keys map to the same routing domain, and bounded(1) concurrency means same-key invocations cannot overlap.
outboxes: The outbox runtime declares keyed partitioning on tenant_id, partition-level ordering, and dispatch onto a serial pool with order-preserving batching. This is the precedence source and execution topology that the ordering proof consumes.

A declared batching stage stops the serialization route because batch-internal overlap is intentionally unmodeled. For ordering, batching.ordering: preserved lets the established precedence pass through.

Run the verifier

With your model file complete, run:

conseqa checkout.yaml

You will see a summary of obligations and verdicts. With the declarations above, the obligations should prove as follows:

op.place_order idempotency: proven — the transaction’s deduplicated_by suppresses duplicate commits, the outbox write shares that commit, and the external charge deduplicates by the same key.
op.place_order recoverability: proven — resumable by same-path continuation.
op.dispatch_receipt idempotency: proven — the external email boundary deduplicates by event_id, which is the outbox message identity field.
op.dispatch_receipt ordering: proven — the outbox runtime declares keyed partitioning on tenant_id, partition ordering, consistent-hash assignment to a serial pool, and order-preserving batching. This is an outbox-routed discharge.
op.dispatch_receipt recoverability: proven — guaranteed because the outbox runtime declares at_least_once delivery.

If you want to see a deliberately unproven obligation, remove the disposition: terminal from the external payment effect’s err variant and rerun. The verifier will report op.place_order idempotency as unknown because the match_result on the charge result is no longer established to replay: a retry might observe a different result variant.

# With terminal disposition removed
obligations: 4 proven, 1 unknown, 0 disproven (5 total)

Generate the visualization

Produce the proof overlay in one command:

conseqa-viz checkout.yaml --verify --out checkout.html

Open checkout.html in a browser. The system view shows services, topics, and external systems with obligation status rings. Double-click op.place_order to see its program diagram: transaction steps expanded in place, the async launch, join_all, and the match_result arms. Click op.dispatch_receipt to inspect the outbox input and runtime topology that the ordering proof consumed.

Understanding the proof structure

Idempotency via producer-suppressed outbox discharge

The op.place_order idempotency proof is discharged through the producer-suppressed route: the transaction declares deduplicated_by on idempotency_key, which is replay-stable because the request input declares a keyed identity on that field. At most one logical commit per class is admitted, so at most one order insert and one outbox write occur. The outbox boundary does not terminate the causal graph: the verifier continues through outbox.order_events to op.dispatch_receipt and checks that the consumer also collapses duplicates, which it does because the email boundary deduplicates by event_id.

Ordering via outbox-routed discharge

The op.dispatch_receipt ordering proof is discharged through the outbox-routed route: the outbox runtime declares keyed partitioning, which establishes that same-tenant_id messages share a partition. The ordering: partition declaration supplies the precedence source. Dispatch with member_assignment: consistent_hash gives each partition one active owning member, and member_concurrency: bounded(1) on the target pool means later invocations cannot overtake earlier ones. The batching.ordering: preserved declaration lets the precedence pass through the batching stage.

Closing the unknown verdict

The deliberate gap mentioned above (removing disposition: terminal) produces an unknown verdict because the control decision no longer replays. To close it, restore the terminal disposition on both variants of the external effect’s result contract. This makes the match_result replay-stable: every attempt observes the same variant and proceeds down the same arm.

Proving Idempotency

Deep dive into the three-leg proof and greatest-fixpoint reasoning.

CI Integration

Automate verification in your CI pipeline and track obligations over time.

Get Started

Core Concepts

Runtime Topology

DSL Reference

Verification

Visualization

Guides

Step-by-Step: Modeling a Flash-Sale Checkout in Conseqa

Understanding the proof structure

Idempotency via producer-suppressed outbox discharge

Ordering via outbox-routed discharge

Closing the unknown verdict

Proving Idempotency

CI Integration

​Understanding the proof structure

​Idempotency via producer-suppressed outbox discharge

​Ordering via outbox-routed discharge

​Closing the unknown verdict

Proving Idempotency

CI Integration

Understanding the proof structure

Idempotency via producer-suppressed outbox discharge

Ordering via outbox-routed discharge

Closing the unknown verdict