conseqa-viz turns a Conseqa YAML model into a single self-contained HTML file you can open in any browser, attach to a pull request, or share with your team. The output makes no network requests and works fully offline. When you add a prover report — either by pointing to an existing one or by running the model checker inline — the visualization colors every operation, topic, and state machine by its worst obligation status.
Arguments and Options
string
required
Path to the YAML model file to visualize. Validation runs before rendering;
diagnostics go to stderr and rendering proceeds regardless. Use
--no-validate
to suppress the validation pass.string
Output path for the generated HTML file. Defaults to
<MODEL>.html — the
same base name as the input, with the extension replaced. For --example-report
with no --out, output goes to stdout.string
Load a prover report JSON file and overlay its obligation verdicts on the
visualization. Mutually exclusive with
--verify. Use this when you have a
report produced by a previous conseqa --report run. If the report’s
model_revision does not match the current model, a warning is printed to
stderr and rendering continues.flag
Run the model checker in-process and overlay the resulting obligation report
on the visualization. Mutually exclusive with
--report. This is the
equivalent of running conseqa --report and conseqa-viz --report in one
step.flag
Emit the page data — title, model, derived graph, and report — as JSON
instead of rendering HTML. Intended for the front-end development server and
custom tooling. The output is the same data the HTML bundle would receive as
window.CONSEQA.string
Page title shown in the browser tab and the visualization’s top bar. Defaults
to the model file’s stem (the filename without path or extension).
flag
Instead of rendering, emit a scaffold prover report that enumerates every
obligation implied by the model’s declared requirements, with every status set
to
unknown. Useful for understanding the report format, annotating
obligations manually, or bootstrapping a custom report. Output goes to stdout
unless --out is given.flag
Skip the validation pass. Diagnostics from the analyzer are suppressed. The
model is rendered regardless of structural errors, which is useful for
inspecting a work-in-progress model.
flag
Print usage information and exit.
The HTML Output
The generated file is fully self-contained: every script and stylesheet is inlined, no fonts or assets are fetched at runtime, and the file opens directly from disk without a local server. Graph layouts are rendered as SVG in the browser. The visualization supports dark and light mode, toggled from the top bar.Three Views
The visualization presents your architecture across three navigable views.System View
The top-level architecture graph. Services appear as boundary boxes containing
their operations; topics, external systems, and a synthetic “clients” vertex
sit around them. Edges show publications (operation → topic), subscriptions
(topic → operation), request effects (operation → operation), and external
effects. Dashed edges are declared-but-unexecuted capabilities.
Operation View
A full drill-down into one operation: requirements table with verdict chips
when a report is loaded, inputs table with delivery and dispatch semantics,
and the operation’s program rendered as a step-by-step flow diagram.
Transaction steps expand in place to show reads, writes, inserts, transitions,
and artifact establishments.
State Machine View
The state graph for one state machine: legal states, the initial state,
transitions with side-effect counts, and a transitions table listing
from/to sets, side effects, and the operations that execute each transition.
Selecting a transition updates the URL so you can share deep links.
disproven > unknown > proven). Requirement rows in the operation view are colored by their obligation status, and the top bar’s Obligations button opens a filterable panel of all obligations grouped by subject.
Example Invocations
Mutual Exclusion: --verify and --report
--verify and --report are mutually exclusive. Both produce an obligation overlay; they differ only in where the report comes from. Use --verify when you want a single command that checks and visualizes in one step. Use --report when you have a report from CI, a prior conseqa run, or another tool, and want to visualize it separately.
Passing both flags at once is an error:
conseqa-viz will exit with
--verify and --report are mutually exclusive.