Export the Stave Intermediate Representation (SIR) for the configured
controls and observations as a deterministic document.
The SIR is the vendor-neutral fact set the Z3 solver consumes for compound
risk reasoning. It carries every control fact, asset, identity (with
transitive role chains), effective-permission edge, and exposure window
that the engine's evaluation pipeline produces — but stripped of
infrastructure noise (file paths, git metadata, tool versions).
Scope: the SIR is a curated projection, not a complete dump of every
property a control reads. The export currently covers 13 top-level
configuration domains (IAM, Cognito, S3 storage policies, Bedrock AI
agents, delegation, credential lifecycle, trail logging, network, and
a subset of compute / k8s). Properties in uncovered domains (Azure,
GCP, M365, databases, messaging, secrets, monitoring, and 80+ others)
are evaluated by CEL controls inside 'stave apply' but are NOT in the
export. A solver UNSAT verdict is valid for chains the SIR can express;
it is silent about chains whose members live in uncovered domains. See
the Fact Export reference in stave-guide for the full domain table.
Three output formats are supported:
json — full nested SIR document (default).
jsonl — one (subject, predicate, object) triple per line. Lossy
projection optimised for Datalog/Soufflé and ASP/Clingo
consumers that prefer flat predicate(s, o) facts.
smt2 — SMT-LIB v2 declarations + assertions. The output contains
facts only — no (check-sat), no queries — so any SMT solver
(Z3, cvc5, Yices) reads the same file. Reasoning programs
append their own query to the file before invoking the
solver.
Inputs:
--controls, -i Control definitions directory (default: controls)
--observations, -o Observation snapshots directory (default: observations)
--format, -f Output format: json | jsonl | smt2 (default: json)
--now RFC3339 timestamp for deterministic output
Outputs:
stdout: SIR document in the requested format.
stderr: errors and progress (when stderr is a TTY).
Exit codes:
0 success
2 input error (bad flag, malformed --now)
4 internal error (load failure, builder error)
130 SIGINT
Usage:
stave export-sir [flags]
Examples:
# Export SIR for the project's default controls + observations
stave export-sir > sir.json
# Pin --now for byte-identical reproduction
stave export-sir --now 2026-05-01T12:00:00Z > sir.json
# Pretty-print for inspection
stave export-sir | jq .
# Triple form for Datalog / ASP consumers
stave export-sir --format jsonl > facts.jsonl
# SMT-LIB v2 facts; append a query before piping into z3 / cvc5
stave export-sir --format smt2 > facts.smt2
cat facts.smt2 query.smt2 | z3 -in
# Strip catalog metadata for leaner solver input (observation facts only)
stave export-sir --format smt2 --strip-catalog > facts-lean.smt2
# Closed-world axioms for negative proofs (use with small fact sets)
stave export-sir --format smt2 --closed-world > facts-closed.smt2
Flags:
--allowlist-mode string scalar projector mode: curated (default — 59 hand-authored entries) | full (experimental — emit one auto_prop_<path> triple per control-read property path the predicate index advertises; measures coverage gain, no downstream solver consumes the auto_prop_* names yet) (default "curated")
--closed-world emit closed-world forall axioms in SMT2 output (restricts each predicate to its asserted tuples only; needed for negative proofs but causes solver timeout on large fact sets)
-i, --controls string control definitions directory (default "controls")
-f, --format string output format: json | jsonl | smt2 (default "json")
-h, --help help for export-sir
--now string override current time (RFC3339) for deterministic output
-o, --observations string observation snapshots directory (default "observations")
--strip-catalog omit control catalog metadata (has_severity, has_type, has_domain) from the fact stream; reduces SMT2/JSONL output to observation-derived facts only
--validate check SIR coverage against CEL controls and warn on stderr about projection gaps (controls that fire in CEL but evaluate properties not projected as SIR facts)
Global Flags:
--allow-symlink-output Allow writing output through symlinks (default: refuse)
--force Allow overwriting existing output files
--log-file string Write logs to file (default: stderr)
--log-format string Log format: text|json (default "text")
--log-level string Log level: debug|info|warn|error (overrides -v)
--log-timestamps Include timestamps in logs (breaks determinism)
--log-timings Include timing information (breaks determinism)
--no-color Disable ANSI colors in output
--path-mode string Path rendering in errors/logs: base (basename only) or full (absolute paths) Resolved default may come from STAVE_* env vars, stave.yaml, user config, or built-in.
--quiet Suppress output (exit code only) Resolved default may come from STAVE_* env vars, stave.yaml, user config, or built-in.
--require-offline Assert offline operation: fail if proxy env vars (HTTP_PROXY, HTTPS_PROXY, ALL_PROXY) are set
--sanitize Sanitize infrastructure identifiers (bucket names, ARNs, policies) from output Resolved default may come from STAVE_* env vars, stave.yaml, user config, or built-in.
--strict Enable strict integrity checks for embedded registries and references
-v, --verbose count Increase verbosity (-v=INFO, -vv=DEBUG)
-y, --yes Auto-confirm all interactive prompts (distinct from --force which controls file overwriting)