Skip to main content
conseqa-viz turns any Conseqa model into a single interactive HTML file you can open directly from disk, attach to a pull request, or share as a design artifact. The output makes no network requests, has no external dependencies, and works fully offline.

Generating a visualization

Pass your model file as the only required argument. By default the tool writes an HTML file alongside the model:
To choose the output path or add a page title, use --out and --title:

Overlaying proof results

The HTML viewer becomes most useful when it shows the checker’s verdicts alongside your architecture. You have two options:
--verify runs the full model checker in-process before rendering. --report loads a JSON report you produced earlier with conseqa model.yaml --report proof.json. The two flags are mutually exclusive.
Use --report in CI so the visualization step never needs to re-run verification. Produce the report once with conseqa, archive it as an artifact, then render the HTML separately with conseqa-viz --report.

Validation during rendering

conseqa-viz runs analyzer validation before rendering and prints any diagnostics to stderr. Rendering proceeds even on a model with validation warnings — imperfect models can still be inspected. To suppress the validation pass entirely, pass --no-validate.

Scaffolding a report

If you want to understand the report format or fill in verdicts manually, generate a scaffold with every obligation set to unknown:
The output goes to stdout unless you supply --out.

The three views

The HTML contains three interconnected views. Navigate between them using the breadcrumbs in the top bar or by clicking entities in the current view.

System View

The full architecture as an SVG graph — services, topics, external systems, and the edges that connect them.

Operation View

Program flow, requirements, and inputs for any individual operation. Double-click an operation node to drill in.

State Machine View

Lifecycle diagrams for every declared state machine, with transitions, side effects, and proof overlays.

Modeling a Checkout Flow

A step-by-step walkthrough of the flash-sale checkout example, from YAML to visualization.