Integrating Conseqa Verification into Your CI Pipeline

Running Conseqa in CI gives your team a formal check on every change that touches the architecture model. A regression that would introduce a disproven obligation or break a previously proven one is caught before it merges, and the obligation report and visualization HTML become searchable artifacts attached to every build.

Build step

Conseqa ships as a Rust crate. Build the release binaries once per pipeline environment or Docker layer:

cargo build --release
# binaries at target/release/conseqa and target/release/conseqa-viz

If you maintain pre-built binaries or a container image, place them on PATH and use conseqa and conseqa-viz directly in subsequent steps.

Run the verifier

Verify your model and write the obligation report to a file:

conseqa model.yaml --report report.json

The tool prints an obligation summary to stdout and exits with a non-zero code only when the model fails to parse or fails validation (malformed YAML, invalid references). A model that validates and verifies, regardless of how many obligations are proven, unknown, or disproven, exits zero. Use the report JSON to inspect verdicts and enforce your own pass/fail policy.

unknown obligations are epistemic: the checker could not establish the property from the declared facts. They are never evidence of a violation. disproven obligations mean the checker found a counterexample: inspect these with conseqa-viz --report report.json to understand the evidence.

Generate the visualization artifact

After the report is written, generate the HTML visualization:

conseqa-viz model.yaml --report report.json --out architecture.html

This step uses the already-computed report rather than re-running verification, so it adds minimal time to the pipeline. The output is a single self-contained HTML file with the full interactive proof overlay.

GitHub Actions example

Add a job to your workflow that runs on any push touching the model file:

name: Architecture verification

on:
  push:
    paths:
      - "model.yaml"
      - "Cargo.toml"
      - "Cargo.lock"
  pull_request:
    paths:
      - "model.yaml"

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install Rust toolchain
        uses: dtolnay/rust-toolchain@stable

      - name: Cache Cargo registry
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
            target
          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock')}}

      - name: Build Conseqa
        run: cargo build --release

      - name: Verify architecture model
        run: ./target/release/conseqa model.yaml --report report.json

      - name: Generate visualization
        if: always()
        run: >
          ./target/release/conseqa-viz model.yaml
          --report report.json
          --out architecture.html
          --title "${{ github.repository }} architecture"

      - name: Upload proof report
        if: always()
        uses: actions/upload-artifact@v4
        with:
          name: proof-report
          path: report.json

      - name: Upload visualization
        if: always()
        uses: actions/upload-artifact@v4
        with:
          name: architecture-visualization
          path: architecture.html

The if: always() guards on the visualization and upload steps ensure that artifacts are produced even when the verify step fails, so you can inspect the proof state on a failing build.

Keeping the model with your service code

Store model.yaml in the same repository as your service code, not in a separate architecture repository. This keeps the model in sync with the implementation it describes and makes diff review natural:

my-service/
  src/
  model.yaml        ← lives here
  report.json       ← committed baseline (see tip below)
  Cargo.toml

When a code change requires a model update, the model diff and the implementation diff land in the same pull request. Reviewers can see both together, and CI verifies the updated model against the updated code in the same build.

Failing on disproven obligations

conseqa exits zero after verification regardless of verdict counts: the exit code only signals whether the model is structurally valid. To fail the build on unwanted obligation statuses, add an explicit check using the report JSON:

# Fail if any obligation is disproven
jq -e '[.obligations[] | select(.status == "disproven")] | length == 0' report.json

To require that every obligation is proven, rejecting both unknown and disproven:

# Fail if any obligation is not 'proven'
jq -e '[.obligations[] | select(.status != "proven")] | length == 0' report.json

Adjust the filter to match your team’s policy. A newly added requirement starts as unknown; you can choose to treat that as a warning or a hard block depending on your workflow.

Tracking obligation status over time

Commit report.json to your repository as a baseline. When the verifier’s output changes (a previously unknown obligation becomes proven, or a new requirement is added), the diff in report.json makes the change visible in code review. Reviewers can confirm that new obligations are intentional and that any regression from proven to unknown is understood.

A committed report also means the visualization step in CI never needs to re-run verification: it loads the committed report directly, which keeps the viz step fast regardless of model complexity.

Obligation scope in the report

Each obligation in the report now carries a scope field:

l0_only: the proof required no runtime facts.
runtime_dependent: the proof consumed at least one L1 fact (delivery semantics, routing, pool concurrency, outbox runtime, and so on).

This is useful for CI matrices that verify both a minimal L0-only model and a full model with runtime topology. Removing the runtime block from a valid model leaves it valid: runtime-dependent proofs simply become unproven, never structural errors. A CI job that strips the runtime block and re-runs the verifier can confirm that the L0 layer stands on its own, while the full-runtime variant checks the complete architecture.

jobs:
  verify-l0:
    steps:
      - uses: actions/checkout@v4
      - run: yq 'del(.runtime)' model.yaml > model.l0.yaml
      - run: conseqa model.l0.yaml --report report.l0.json
      - run: jq -e '[.obligations[] | select(.scope == "l0_only" and .status != "proven")] | length == 0' report.l0.json

  verify-full:
    steps:
      - uses: actions/checkout@v4
      - run: conseqa model.yaml --report report.full.json
      - run: jq -e '[.obligations[] | select(.status != "proven")] | length == 0' report.full.json

Get Started

Core Concepts

Runtime Topology

DSL Reference

Verification

Visualization

Guides

Integrating Conseqa Verification into Your CI Pipeline

Build step

Run the verifier

Generate the visualization artifact

GitHub Actions example

Keeping the model with your service code

Failing on disproven obligations

Tracking obligation status over time

Obligation scope in the report

​Build step

​Run the verifier

​Generate the visualization artifact

​GitHub Actions example

​Keeping the model with your service code

​Failing on disproven obligations

​Tracking obligation status over time

​Obligation scope in the report

Build step

Run the verifier

Generate the visualization artifact

GitHub Actions example

Keeping the model with your service code

Failing on disproven obligations

Tracking obligation status over time

Obligation scope in the report