Quickstart: Verify Your First Conseqa Model in Minutes

This guide walks you through installing Conseqa from source, writing a minimal model, running your first verification, and exploring the result in the interactive visualizer. The model starts with the application itself and then adds a small amount of runtime topology so serialization can be proved. By the end you will have a working model on disk and know how to extend it.

Install Conseqa

Conseqa builds from source with the standard Rust toolchain. You need a recent stable Rust release; no other runtime dependencies are required.Clone the repository and build both binaries in release mode:

git clone https://github.com/umran/conseqa
cd conseqa
cargo build --release

This produces two binaries:

target/release/conseqa — the validator and verifier
target/release/conseqa-viz — the visualization tool

Optionally add them to your PATH:

export PATH="$PWD/target/release:$PATH"

Confirm both tools are reachable:

conseqa --help
conseqa-viz --help

The conseqa-viz front end is a pre-built React bundle embedded in the binary at compile time. You do not need Node.js to run it — only to rebuild the front end itself after modifying viz/.

Write a minimal model

Create a file called model.yaml. The model below declares a single backend service, a canonical schema for a completed upload, a data model with an outbox for typed messages, a keyed topic, and a complete operation. A short runtime block at the end pins request routing and pool concurrency so the operation’s serialization requirement can be discharged.

revision: 1

services:
  service.ingest:
    kind: backend

schemas:
  schema.UploadCompleteRequest:
    kind: canonical
    description: A client reports that an upload to the object store has finished.
    completeness: complete
    fields:
      upload_id: string
      video_id: uuid
      owner_id: uuid
      source_uri: string

  schema.VideoUploaded:
    kind: canonical
    description: A new source video is available for transcoding.
    completeness: complete
    fields:
      event_id: string
      video_id: uuid
      owner_id: uuid
      source_uri: string

data_models:
  data.videos:
    objects: {}
    outboxes:
      outbox.video_events:
        messages:
          - schema.VideoUploaded
        message_identity:
          kind: keyed
          mapping:
            schema.VideoUploaded:
              - event_id

topics:
  topic.video_events:
    messages:
      - schema.VideoUploaded
    message_identity:
      kind: keyed
      mapping:
        schema.VideoUploaded:
          - event_id

state_machines: {}

operations:
  operation.complete_upload:
    service: service.ingest
    inputs:
      input.complete_upload.request:
        kind: request
        schema: schema.UploadCompleteRequest
        identity:
          kind: keyed
          fields:
            - upload_id
        result:
          ok: schema.VideoUploaded
          err:
            schema: schema.RequestRejected
            disposition: terminal
    program:
      steps:
        - kind: transaction
          id: tx.complete_upload
          data_model: data.videos
          isolation: read_committed
          idempotency:
            kind: deduplicated_by
            key:
              components:
                - source: input:input.complete_upload.request
                  path: upload_id
          steps:
            - kind: write_outbox
              effect_id: effect.complete_upload.outbox
              effect:
                outbox: outbox.video_events
                schema: schema.VideoUploaded
                idempotency_key_propagation:
                  - source:
                      components:
                        - source: input:input.complete_upload.request
                          path: upload_id
                    target:
                      components:
                        - source: effect:effect.complete_upload.outbox
                          path: event_id
              values:
                kind: deterministic
                from:
                  - source: input:input.complete_upload.request
                    path: upload_id
                  - source: input:input.complete_upload.request
                    path: video_id
                  - source: input:input.complete_upload.request
                    path: owner_id
                  - source: input:input.complete_upload.request
                    path: source_uri
            - kind: establish_transaction_output
              bind: output.complete_upload
              schema: schema.VideoUploaded
              values:
                kind: deterministic
                from:
                  - source: input:input.complete_upload.request
                    path: video_id
                  - source: input:input.complete_upload.request
                    path: owner_id
                  - source: input:input.complete_upload.request
                    path: source_uri
        - kind: return
          request: input.complete_upload.request
          outcome:
            kind: ok
            values:
              kind: deterministic
              from:
                - source: transaction_output:output.complete_upload
                  path: video_id
                - source: transaction_output:output.complete_upload
                  path: owner_id
                - source: transaction_output:output.complete_upload
                  path: source_uri
    requirements:
      idempotency:
        - key:
            components:
              - source: input:input.complete_upload.request
                path: upload_id
          result: replay_consistent
      recoverability:
        - key:
            components:
              - source: input:input.complete_upload.request
                path: upload_id
          completion: resumable

runtime:
  execution_pools:
    pool.web:
      member_concurrency:
        kind: bounded
        value: 1
  routers:
    router.complete_upload:
      boundary:
        operation: operation.complete_upload
        input: input.complete_upload.request
      pool: pool.web
      routing:
        key:
          - upload_id
        member_assignment:
          kind: consistent_hash

Each block serves a specific purpose:

Data model with an outbox (data_models.data.videos.outboxes.outbox.video_events): A typed logical message collection that lives in the same transactional boundary as the data model’s objects. The transaction can atomically write objects and admit messages to this outbox in one commit.
Topic (topics.topic.video_events): A logical channel that carries schema.VideoUploaded with keyed message identity on event_id.
Operation (operations.operation.complete_upload): A request-driven operation with a transaction containing deduplicated_by on the request’s upload_id, a write_outbox step staging VideoUploaded atomically, and an establish_transaction_output step exporting values for the return.
Runtime (runtime.execution_pools and runtime.routers): Realization facts. A serial execution pool plus a router that assigns request invocations onto that pool by consistent hash of upload_id. Adding these lets the verifier discharge the operation’s serialization requirement.

The completeness: complete declaration tells the verifier this schema describes the full logical shape. Fields absent from a complete schema are treated as nonexistent. Use partial when the real schema may contain undeclared fields.

Run the verifier

Pass your model to conseqa:

conseqa model.yaml

With the model above, the verifier checks idempotency and recoverability obligations and reports their verdicts:

obligations: 2 proven, 0 unknown, 0 disproven (2 total)

Now try the fuller example from the repository’s test fixtures, which models a transactional outbox with a relay and downstream consumer:

conseqa tests/fixtures/transactional_outbox.yaml

obligations: 6 proven, 0 unknown, 0 disproven (6 total)

For a model with deliberate gaps, run the flash checkout fixture. The checker reports each gap honestly:

conseqa tests/fixtures/flash_checkout.yaml

obligations: 10 proven, 4 unknown, 0 disproven (14 total)

unknown is epistemic: the verifier could not establish the property from the declared facts. It is not evidence of a violation. The flash checkout model deliberately leaves gaps in recoverability and idempotency for illustration.

To save the full obligation report as JSON for later use or visualization:

conseqa tests/fixtures/video_streaming.yaml --report video_streaming.report.json

obligations: 8 proven, 0 unknown, 0 disproven (8 total)
wrote video_streaming.report.json

The JSON report follows the ProverReport format (format: 2). Each obligation object carries an id, property, subject, status, summary, assumptions, evidence, and scope (l0_only or runtime_dependent).

Generate a visualization

Run conseqa-viz with --verify to produce and overlay the obligation report in one step:

conseqa-viz tests/fixtures/video_streaming.yaml --verify --out video_streaming.html

wrote video_streaming.html

You can also overlay a report you produced earlier:

conseqa-viz tests/fixtures/video_streaming.yaml \
  --report video_streaming.report.json \
  --out video_streaming.html

Other useful options:

# Set a custom page title
conseqa-viz model.yaml --verify --title "Upload pipeline" --out upload.html

# Generate a scaffold report with every obligation status unknown
# (useful for understanding the report format)
conseqa-viz model.yaml --example-report

# Skip validation warnings during rendering
conseqa-viz model.yaml --verify --no-validate --out model.html

Open the HTML output

Open the generated file in any browser. The visualization makes no external network requests and works directly from disk:

open video_streaming.html         # macOS
xdg-open video_streaming.html     # Linux
start video_streaming.html        # Windows

The visualization has three main views:

System view (#/system)

Services are drawn as boundary boxes with their operations inside. Topics, external systems, and a synthetic “clients” vertex sit around them. Edges are the model’s information routes: publications, subscriptions, request effects, and external effects. Solid edges carry program step details; dashed edges are declared but unexecuted capabilities. Click any vertex or edge for a structured detail panel.

Operation view (#/op/<id>)

Shows a page header with the operation’s facts, then its declared requirements (with obligation status when a report is loaded), its inputs, and a full program diagram — every step in order, transactions expanded in place, match/branch arms side by side, and step locations labeled as the checker names them (3, 3.ok.1).

State machine view (#/machine/<id>)

Displays the state graph with legal states, the initial state, and transitions annotated with side effects. A transitions table shows from/to sets and the operations that execute each transition through an intent.

When a report is loaded, every vertex gains a status ring and a rollup chip (worst status wins: disproven > unknown > proven). The obligations panel groups obligations by the operation they anchor to, with a status filter and expandable evidence cards.

Next steps

Core Concepts

Learn how operations, requirements, and the proof mechanics fit together.

CLI Reference

Full reference for every flag on conseqa and conseqa-viz.

Get Started

Core Concepts

Runtime Topology

DSL Reference

Verification

Visualization

Guides

Quickstart: Verify Your First Conseqa Model in Minutes

Next steps

Core Concepts

CLI Reference

​Next steps

Core Concepts

CLI Reference

Next steps