CLI Reference

The spec-to-rest binary is built from modules/cli and runs locally via sbt "cli/run …" or as a GraalVM native image. Every subcommand exits with a numeric code; CI consumers should branch on these.

Subcommands

Global flags

These flags are accepted by every subcommand:

• --verbose / -v — show stage timings and per-check breakdowns on stderr.
• --quiet / -q — suppress everything except errors.
• --color / --no-color — force ANSI color on or off. Default is auto: color is enabled when stderr is a TTY and NO_COLOR is not set. CLICOLOR_FORCE=1 forces color even when piped.

compile flags

sbt "cli/run compile [flags] <spec-file>"

• --framework <id> / -f — framework (default fastapi). Known: fastapi, chi, express.
• --db <id> — database dialect (default postgres): postgres, sqlite, mysql. The accepted set depends on the chosen framework.
• --lang <id> — language (python, go, ts). Always accepted and validated against the framework's supported languages; only required when the framework supports more than one language (otherwise inferred). Passing a language the framework does not support (e.g. --lang go --framework fastapi) is a hard error, not a silent fallback.

Any unsupported (language, framework, database) combination is rejected with a typed error that lists what the chosen framework actually supports — the resolver never warns-and-falls-back to a default target.

• --out <dir> / -o — output directory (required).
• --dry-run — run the full pipeline (parse, verify, build, in-memory emit) but do not write anything. Prints a manifest of create / update / unchanged / preserve actions per file. Exits 0 even when the plan is empty.
• --ignore-verify — skip the verification gate. Emits unverified code with a warning. Use only for spec exploration.
• --with-tests — also emit the behavioral + stateful + structural test suite (tests/ directory) and the conformance runner. Supported for all nine targets (python-fastapi-*, ts-express-*, go-chi-* × postgres / sqlite / mysql); the suite is emitted in each target's native language (pytest + Hypothesis + Schemathesis / Vitest + fast-check / go test + rapid). See Test Generation.
• --strict-strategies — fail compile when --with-tests would emit incomplete property strategies. See Test Generation.
• --with-synthesis — splice verified Dafny bodies (translated to the target language) into the emitted project. Requires synth verify to have populated the cache. See LLM Integration.
• --allow-skeletons — fall back to unverified skeleton bodies (from synth verify --fallback) when the verified cache misses. Generated handlers halt at runtime with a Dafny HaltException when invoked.
• --synthesis-partial — use verified bodies where cached; for an LLM_SYNTHESIS op with no verified body, emit a fail-loud stub (skipped by testgen) instead of failing the build.
• --synthesis-model <name> — model to look up in the cache (default claude-sonnet-4-6).
• --synthesis-temperature <num> — temperature to look up in the cache (default 1.0).
• --synthesis-cache-dir <path> — override the cache root.
• --dafny-bin <path> — path to the Dafny binary (defaults to $DAFNY_BIN or PATH).
• --dafny-translate-timeout <sec> — wall-clock timeout for dafny translate (default 60s).

--dry-run example

$ sbt "cli/run compile --framework fastapi --db postgres --ignore-verify \
       --dry-run --out /tmp/svc fixtures/spec/url_shortener.spec"

  create    .gitignore
  create    Dockerfile
  create    Makefile
  create    alembic/env.py
  create    app/main.py
  create    app/routers/url_mappings.py
  ...
✔ dry-run: 26 files planned for /tmp/svc (create=26 update=0 unchanged=0 preserve=0)

diff flags

sbt "cli/run diff --framework <id> --db <id> --out <dir> <spec-file>"

• --framework/--db/--lang — same target axes as compile.
• --out <dir> / -o — directory to compare against (required).
• --ignore-verify — compare regardless of whether the spec verifies.
• --with-tests — include the test files in the comparison.

diff exits 0 when the directory is in sync with what compile would produce, 1 when there is drift. The output lists only files that would be created or updated; unchanged and user-preserved files are summarised at the bottom.

test flags

sbt "cli/run test --out <generated-dir> [--profile thorough] [--server-url ...]"

• --out <dir> / -o — directory containing the previously emitted project (required). Must contain tests/run_conformance.py (the Python runner; ts-express-* / go-chi-* suites are run natively — see below).
• --profile <name> — conformance profile: smoke (fast), thorough (default), exhaustive (multi-minute).
• --server-url <url> — base URL for the service under test (default http://localhost:8000). The service must be running with ENABLE_TEST_ADMIN=1 so the runner can hit /__test_admin__/reset between phases.
• --python-bin <path> — interpreter to use (default python3).

test is a thin wrapper around python tests/run_conformance.py <profile> — the runner itself is part of the generated test suite. It drives the Python runner only, so it applies to python-fastapi-* targets emitted with --with-tests. ts-express-* and go-chi-* now emit fully native conformance suites, but with native runners — run those directly:

• ts-express-*: node tests/run_conformance.mjs <profile> (or npm test), service booted with ENABLE_TEST_ADMIN=1.
• go-chi-*: bash tests/run_conformance.sh <profile> (or go test -tags conformance ./tests/...), against a server built with -tags conformance and ENABLE_TEST_ADMIN=1.

Invoking spec-to-rest test against a ts/go project exits 2 (no tests/run_conformance.py); a unified multi-runner wrapper is a tracked follow-up.

verify flags

See Verification Pipeline for the full reference. The most useful flags for CI:

• --timeout <ms> — per-check Z3/Alloy timeout (default 30000).
• --parallel <n> — number of concurrent checks (0 for serial; default is the host's available processors).
• --json / --json-out <path> — emit a machine-readable report to stdout or a file (suppresses text output). The --dump-* flags print the translation and exit before the solver runs.
• --explain — extract Z3 unsat cores and surface contributing spec spans on failures.
• --dump-smt / --dump-alloy — write the translated SMT-LIB or Alloy source and exit without running the solvers.

check flags

check is the cheapest stage: parse → IR → lint. It does not invoke Z3 or Alloy. Use it as a fast pre-commit gate.

sbt "cli/run check fixtures/spec/url_shortener.spec"

inspect flags

inspect dumps internal compiler state for debugging.

• --format <fmt> — summary (default), json (full IR + synthesis tally), ir (raw IR toString), dafny (Dafny module skeleton), dafny-prompt (LLM prompt material per LLM_SYNTHESIS operation).
• --operation <name> — filter dafny-prompt to a single operation.

Exit codes

CI consumers can treat 0 as pass, 1 as user error to surface verbatim, 2–3 as infrastructure problems requiring a retry or operator intervention, and 4 as a soft warning.

Environment variables