Diagnostics and CLI

Reading diagnostics

On failure the CLI prints a spec-aware multi-line diagnostic per failing check. Diagnostics carry a category, a primary source span, related spans, an optional counterexample, and an opt-in suggestion.

Categories

Worked example: preservation violation

service BrokenUrlShortener {

  entity UrlMapping {
    click_count: Int
  }

  state {
    metadata: Int -> lone UrlMapping
    totalClicks: Int
  }

  operation Tamper {
    input: code: Int

    requires:
      code in metadata

    ensures:
      metadata'[code].click_count = pre(metadata)[code].click_count - 100
  }

  operation Drain {
    requires:
      true

    ensures:
      totalClicks' = -1
  }

  invariant clickCountNonNegative:
    all c in metadata | metadata[c].click_count >= 0

  invariant totalClicksNonNegative:
    totalClicks >= 0
}

✘ <spec>: 2 failure(s), 0 skipped in 9 consistency checks (<elapsed>)
✘ 
✘ <spec>:22:2: error: operation 'Drain' violates invariant 'totalClicksNonNegative'
  related: <spec>:33:2 (invariant 'totalClicksNonNegative' declared here)

  Counterexample:
  entities:
    UrlMapping#0 { click_count = 0 }
    UrlMapping#1 { click_count = 0 }
  pre-state:
    metadata = {}
    totalClicks = 0
  post-state:
    metadata' = {}
    totalClicks' = -1

  Why this violates the invariant:
    1. Invariant 'totalClicksNonNegative' requires:
         (totalClicks >= 0)
    2. Operation 'Drain' computes 'totalClicks' from:
         (- 1)
    3. The solver picked pre(totalClicks) = 0, producing post-state totalClicks' = -1.
    4. The post-state value violates the bound on 'totalClicks' from invariant 'totalClicksNonNegative'.

  hint: 'Drain' violates 'totalClicksNonNegative'. Tighten 'ensures' so the fields 'totalClicksNonNegative' constrains are pinned by '=' or a range predicate; see counterexample.
✘ 
✘ <spec>:12:2: error: operation 'Tamper' violates invariant 'clickCountNonNegative'
  related: <spec>:30:2 (invariant 'clickCountNonNegative' declared here)

  Counterexample:
  inputs:
    code = 1
  entities:
    UrlMapping#0 { click_count = -1 }
    UrlMapping#1 { click_count = 99 }
    UrlMapping#2 { click_count = -1 }
  pre-state:
    metadata = { 1 → UrlMapping#1 }
    totalClicks = 0
  post-state:
    metadata' = { 1 → UrlMapping#0 }
    totalClicks' = 0

  Why this violates the invariant:
    1. Invariant 'clickCountNonNegative' requires:
         (all c in metadata | (metadata[c].click_count >= 0))
    2. Operation 'Tamper' computes 'click_count' from:
         (pre(metadata)[code].click_count - 100)
    3. The solver picked code = 1, pre(metadata)[1].click_count = 99, producing post-state metadata'[1].click_count = -1.
    4. The post-state value violates the bound on 'click_count' from invariant 'clickCountNonNegative'.

  hint: 'Tamper' violates 'clickCountNonNegative' on field(s) 'click_count' — see counterexample. Tighten 'ensures' with a range predicate or a constructor that initialises click_count correctly.
✘ <spec>: exit 1 (violations): a check was violated, or a verification, synthesis, or test step failed (for example a parse or build error, an unsatisfiable invariant, an exhausted synthesis budget, or a conformance failure)
exit codes: 0 ok | 1 violations | 2 translator-limit | 3 backend-error | 4 trust-limit

The hint names the violating operation, the violated invariant, and the field(s) the invariant constrains, extracted from the IR rather than re-rendered. Suggestions are capped at 200 chars and can be turned off entirely with --no-suggestions (the suggestion field then comes back as null in JSON output as well). The phrasing is intentionally non-stable text intended for humans; downstream tooling should switch on the category enum, not on the suggestion string.

The numbered "Why this violates" block is the narration layer added in #89: a deterministic structural walk over the violated invariant's IR, the relevant ensures clause, and the decoded counterexample. Steps 1 and 2 pretty-print IR (fully parenthesized, readability cost is small, ambiguity cost is none); step 3 reads input/pre/post values directly off the model (no interpreter, no arithmetic re-evaluation); step 4 is a fixed phrasing keyed to the invariant name. Narration is populated for invariant_violation_by_operation, contradictory_invariants, and unreachable_operation. Other categories surface narrative: null in JSON. Suppress with --no-narration (mirrors --no-suggestions).

The decoder enumerates the model's entity universe, evaluates field functions, and shows pre-/post-state relations side by side. Uninterpreted sort values like UrlMapping!val!0 are rewritten to the readable UrlMapping#N labels.

Worked example: contradictory invariants

service Contradiction {
  invariant: 1 >= 10
  invariant: 1 <= 5
  invariant: 1 >= 10 and 1 <= 5
}

✘ <spec>: 1 failure(s), 0 skipped in 1 consistency checks (<elapsed>)
✘ 
✘ <spec>:2:2: error: invariants are jointly unsatisfiable — no valid state exists
  related: <spec>:3:2 (invariant 'inv_1')
  related: <spec>:4:2 (invariant 'inv_2')

  Why these invariants conflict:
    1. The verifier could not satisfy all invariants jointly.
    2. Invariants involved: inv_0, inv_1, inv_2.
       (Run with --explain to see the contributing pair.)

  hint: The invariant set is jointly unsatisfiable; for example, review 'inv_0', 'inv_1', 'inv_2' for a pair whose range constraints cannot overlap (e.g., 'x >= 10' alongside 'x <= 5'); narrow or drop one.
✘ <spec>: exit 1 (violations): a check was violated, or a verification, synthesis, or test step failed (for example a parse or build error, an unsatisfiable invariant, an exhausted synthesis budget, or a conformance failure)
exit codes: 0 ok | 1 violations | 2 translator-limit | 3 backend-error | 4 trust-limit

No counterexample is emitted here: the engine concluded unsat on the invariant conjunction alone, so there's no model to decode. Pass --explain to extract the unsat core and sharpen the related: list to the minimal contradictory subset; with --explain off, the related spans cover the full invariant set.

Using the CLI

service UrlShortener {

  // --- Type Definitions ---

  type ShortCode = String where len(value) >= 6
                              and value matches /^[a-zA-Z0-9]+$/

  type LongURL = String where len(value) > 0 and isValidURI(value)

  type BaseURL = String where isValidURI(value)

  // --- Entities ---

  entity UrlMapping {
    code: ShortCode
    url: LongURL
    created_at: DateTime
    click_count: Int where value >= 0

    invariant: isValidURI(url)
  }

  // --- State ---

  state {
    store: ShortCode -> lone LongURL
    metadata: ShortCode -> lone UrlMapping
    base_url: BaseURL
  }

  // --- Operations ---

  operation Shorten {
    input:  url: LongURL
    output: code: ShortCode, short_url: String

    requires:
      isValidURI(url)

    ensures:
      code not in pre(store)
      store' = pre(store) + {code -> url}
      short_url = base_url + "/" + code
      #store' = #pre(store) + 1
      metadata'[code].url = url
      metadata'[code].click_count = 0
  }

  operation Resolve {
    input:  code: ShortCode
    output: url: LongURL

    requires:
      code in store

    ensures:
      url = store[code]
      store' = store
      metadata'[code].click_count = pre(metadata)[code].click_count + 1
  }

  operation Delete {
    input: code: ShortCode

    requires:
      code in store

    ensures:
      code not in store'
      code not in metadata'
      #store' = #pre(store) - 1
  }

  operation ListAll {
    output: entries: Set[UrlMapping]

    requires:
      true

    ensures:
      entries = { m in metadata | true }
      store' = store
  }

  // --- Global Invariants ---

  invariant allURLsValid:
    all c in store | isValidURI(store[c])

  invariant metadataConsistent:
    dom(store) = dom(metadata)

  invariant clickCountNonNegative:
    all c in metadata | metadata[c].click_count >= 0

  // --- Convention Overrides ---

  conventions {
    Shorten.http_method = "POST"
    Shorten.http_path = "/shorten"
    Shorten.http_status_success = 201

    Resolve.http_method = "GET"
    Resolve.http_path = "/{code}"
    Resolve.http_status_success = 302
    Resolve.http_header "Location" = output.url

    Delete.http_method = "DELETE"
    Delete.http_path = "/{code}"
    Delete.http_status_success = 204

    ListAll.http_method = "GET"
    ListAll.http_path = "/urls"
    ListAll.http_status_success = 200
  }
}

✔ <spec>: 21/21 consistency checks passed (<elapsed>)

Add -v for stage timing, per-check timing, and the full check table. Each per-check line carries its routed backend tag ([z3] or [alloy]):

service SafeCounter {
  state {
    count: Int
  }

  operation Increment {
    requires:
      true

    ensures:
      count' = count + 1
  }

  operation Decrement {
    requires:
      count > 0

    ensures:
      count' = count - 1
  }

  invariant countNonNegative:
    count >= 0
}

  Parsed in <elapsed>ms
  Built IR in <elapsed>ms
  Timeout: <elapsed>ms
  Alloy scope: 5
  Max parallel: <cores>
✔ <spec>: 7/7 consistency checks passed (<elapsed>)
    ✔ [z3]    [sound]       global                       sat <elapsed>ms
    ✔ [z3]    [sound]       Decrement.requires           sat <elapsed>ms
    ✔ [z3]    [sound]       Decrement.enabled            sat <elapsed>ms
    ✔ [z3]    [sound]       Decrement.preserves.countNonNegative sat <elapsed>ms
    ✔ [z3]    [sound]       Increment.requires           sat <elapsed>ms
    ✔ [z3]    [sound]       Increment.enabled            sat <elapsed>ms
    ✔ [z3]    [sound]       Increment.preserves.countNonNegative sat <elapsed>ms

Skipped checks (translator coverage gap) print as a separate WARN translator limitation on check '<id>': <reason> warning block before the surviving entries in the per-check table; they don't appear inline as a skipped row.

Options

Exit codes

Precedence (highest to lowest): Backend (3), Violation (1), Translator (2), Trust (4), Ok (0). A backend crash always wins over a translator gap; a violation always wins over a soundness gap.

Exit 2 is a partial-success signal: the spec may still be correct, but the verifier could not fully discharge every check. Skipped checks print as warnings with a translator_limitation diagnostic so CI / editors can surface the coverage gap alongside successes. Exit 4 is the same shape but driven by the verified subset: the skipped checks carry a soundness_limitation diagnostic, which signals that the spec uses constructs the formal soundness theorem does not yet cover (rather than constructs the translator does not handle). Verify routes every check that does run through the extracted (Isabelle-verified) translator; checks that would route through the hand-written translator at the check-body level always skip instead.

Inspecting the SMT-LIB

--dump-smt emits a standalone .smt2 file you can hand to any SMT solver, useful for cross-solver sanity checks, bug reports, or pasting into the Z3 web playground.

$ spec-to-rest verify --dump-smt-out /tmp/out.smt2 fixtures/spec/url_shortener.spec
Wrote SMT-LIB to /tmp/out.smt2

$ z3 /tmp/out.smt2
sat

CI runs exactly this cross-check against the checked-in fixtures/golden/smt/url_shortener.smt2 snapshot using apt-get install -y z3, if the emitter ever produces invalid SMT-LIB or loses satisfiability, CI fails loudly.

Machine-readable output (--json / --json-out)

spec-to-rest verify --json <spec> runs the full engine and emits a structured JSON report to stdout instead of the human-readable text. --json-out <file> writes the same JSON to a file and keeps stdout clean. Either flag can compose with --explain (core spans land in the JSON) and --dump-vc <dir> (VC artifacts go to the dir, JSON to stdout/file).

Exit codes (text and JSON modes alike): 0 pass, 1 violation, 2 translator gap, 3 backend error, 4 soundness gap (at least one check was skipped because its source exprs fall outside the verified subset). Backend errors take precedence over violations and over soundness gaps; the JSON complements the exit signal rather than replacing it.

Combining --json / --json-out with --dump-smt / --dump-alloy is rejected with a clear error: the dump flags short-circuit before any checks run, so there is no report to serialize.

Top-level schema

{
  "schemaVersion": 2,
  "specFile": "fixtures/spec/url_shortener.spec",
  "ok": false,
  "totalMs": 842.0,
  "checks": [ /* ... */ ]
}

Each entry in checks mirrors the internal CheckResult 1:1:

{
  "id": "Tamper.preserves.clickCountNonNegative",
  "kind": "preservation",
  "tool": "z3",
  "trust": "best-effort",
  "operationName": "Tamper",
  "invariantName": "clickCountNonNegative",
  "status": "unsat",
  "durationMs": 142.0,
  "detail": "operation 'Tamper' does not preserve invariant '...', counterexample found",
  "sourceSpans": [{ "startLine": 11, "startCol": 2, "endLine": 19, "endCol": 3 }],
  "diagnostic": {
    "level": "error",
    "category": "invariant_violation_by_operation",
    "message": "operation 'Tamper' violates invariant 'clickCountNonNegative'",
    "primarySpan": { "startLine": 11, "startCol": 2, "endLine": 19, "endCol": 3 },
    "relatedSpans": [{ "span": {...}, "note": "invariant '...' declared here" }],
    "counterexample": {
      "entities": [{ "sortName": "UrlMapping", "label": "UrlMapping#0",
                     "rawElement": "UrlMapping!val!0",
                     "fields": [{ "name": "click_count",
                                  "value": { "display": "-1", "entityLabel": null } }] }],
      "stateRelations": [{ "stateName": "metadata", "side": "pre",
                           "entries": [{ "key": {...}, "value": {...} }] }],
      "stateConstants": [],
      "inputs": [{ "name": "code", "value": { "display": "2", "entityLabel": null } }]
    },
    "suggestion": "Tighten the 'ensures' clause so...",
    "narrative": "Why this violates the invariant:\n  1. Invariant 'clickCountNonNegative' requires:\n       (all c in metadata | (metadata[c].click_count >= 0))\n  ...",
    "coreSpans": []
  }
}

Passing checks have diagnostic: null. Checks without a counterexample (e.g. global unsat) have counterexample: null. coreSpans is an empty array when --explain is off or the backend can't provide a core. narrative is null outside the three categories that support narration (see Reading diagnostics) or when --no-narration is set.

Stable enum tokens

These snake_case strings are the contract consumers depend on. Breaking changes bump schemaVersion.

Example consumer queries

# Did verification pass?
spec-to-rest verify --json spec.spec | jq .ok

# List every failing check ID.
spec-to-rest verify --json spec.spec | jq '.checks[] | select(.status != "sat" and .status != "skipped") | .id'

# Extract the first preservation counterexample's inputs.
spec-to-rest verify --json spec.spec \
  | jq '.checks[] | select(.diagnostic.category == "invariant_violation_by_operation") | .diagnostic.counterexample.inputs'

The JSON is complementary to --dump-vc: --dump-vc emits the raw solver inputs for replay; --json emits the decoded diagnostic data for consumption by editors, CI bots, and aggregators.

Timeout, cancellation, and parallel dispatch

--timeout maps to a solver-native deadline (Z3's timeout parameter, Alloy's Future.get(timeout, MILLISECONDS)); there is no outer IO.timeoutTo wrapper. The solver_timeout diagnostic above is the only verifier-specific surface; the inner deadline expiry produces a CheckOutcome.Unknown carrying that category. 0 disables the solver-native deadline; the 30 s default is conservative headroom for heavier preservation checks on large specs.

--parallel n (or 0 for serial) and the cancel-on-Ctrl+C / SIGINT path live entirely in the effect layer: per-check fibers via parTraverseN, Resource[IO, WasmBackend] / Resource[IO, AlloyBackend] for backend lifecycle, Context.interrupt() wired into onCancel, and a CommandIOApp shutdown hook for signal handling. The full mechanics (JMH numbers, native-memory caveats, the cancellation contract, and the Context.interrupt() mid-call abort details) are documented in Concurrency & Cancellation.