conseqa is the primary CLI tool. Give it a YAML model file and it parses the model, validates its structural coherence, runs the verification engine over every declared requirement, and prints a one-line obligation summary. Pass --report to write the full structured findings as JSON.
Arguments and Options
string
required
Path to the YAML model file. Parsed, then validated, then verified in that
order. Validation errors are printed and verification is skipped.
string
Write the full obligation report as a JSON file to
PATH. The report contains
every obligation with its status, assumptions, evidence, and any model-wide
notes. Consumable by conseqa-viz --report and any tooling that reads the
format. See Obligations Report for the schema.flag
Print usage information and exit.
What It Prints
After a successful run,conseqa prints a single summary line to stdout:
error, warning, or note), an optional subject ID in brackets, and a message. Evidence items are indented beneath their parent diagnostic.
If --report is given and the file is written successfully, conseqa prints the output path to stderr:
Exit Codes
conseqa exits with code 0 on a successful run (including runs that produce unknown obligations) and code 1 on any error — a parse failure, a validation error, or an I/O error writing the report.
unknown obligations do not cause a non-zero exit. An unknown verdict means
the verifier could not establish the property from declared facts; it is not
evidence of a violation and does not indicate a broken model. See
Verdicts for the precise meaning.Example Invocations
Validation vs. Verification
Validation is a prerequisite for verification. The two phases check different things:
A model can be structurally valid and still have
unknown obligations. That is the normal working state for a model under development.
Passing Reports to conseqa-viz
Once you have a report, pass it toconseqa-viz to see the obligation findings overlaid on an interactive architecture visualization:
conseqa-viz --verify: