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. It renders both layers of the model: L0, the abstract application machine, is always drawn; L1, the optional runtime realization under Model.runtime, can be toggled from the top bar.

​
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, all rendered as SVG in the browser. 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, operations, topics, outboxes, external systems, and every information route between them. L1 runtime vertices (routers, subscription dispatches, execution pools) appear as intermediate nodes on their corresponding edges when L1 is enabled.

Operation View

Program flow, requirements, and inputs for any individual operation, including write_outbox steps, async launches (execute_effect_async, execute_effect_intent_async), and synchronization barriers (join_all, race). Proof scope badges indicate whether an obligation is l0_only or runtime_dependent.

State Machine View

Lifecycle diagrams for every declared state machine, with transitions, side-effect badges, and proof overlays. Transition side effects appear as implicit effect-intent artifacts.

Modeling a Checkout Flow

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