conseqa-viz. It renders your entire architecture as a directed SVG graph, giving you an at-a-glance picture of what services exist, how operations communicate, and where the model’s proof obligations land.
Layout and nodes
The graph places services as boundary boxes with their operations inside. Topics, external systems, and a synthetic Client node sit around them:- Service boxes — each service is drawn as a named boundary box containing its operations as labeled nodes inside it.
- Topic nodes (pill-shaped) — one node per declared topic.
- External system nodes — one node per external effect target.
- A synthetic Client node — represents callers that invoke request inputs no modeled operation invokes.
Edge types
Every edge in the graph corresponds to a declared information route. The style tells you what kind of route it is:
Dashed edges indicate a declared but unexecuted capability: the effect exists on the operation but no step in its program ever executes it. A solid edge names the program step locations (for example,
2 or 3.ok.1) that execute it in its detail panel. Effects owned by state-machine transitions are attributed to the operations that execute them through intents and marked “via transition.”
Requirement badges
Each operation node carries badges for the requirement kinds declared on it:- S — Serialization
- O — Ordering
- I — Idempotency
- R — Recoverability
Proof overlays
When you load a report (via--verify or --report), the graph gains status indicators:
- Status rings appear around operation and topic nodes, colored by the worst obligation status across that node’s requirements: green for proven, amber for unknown, red for disproven.
- Rollup chips display a count of obligations at each status level.
- Requirement badges on operation nodes are colored individually to reflect their obligation’s verdict.