Policy Verification (`autonomy policy verify`)¶

Offline, read-only pre-deployment verification of a policy bundle against a declared input model, using the same evaluation engine the runtime enforces with — so a verdict here is the verdict the edge would produce for the same input and bundle.

What a clean run means — and does not

A clean run means “no defect was found under this input model at this sample count and seed.” It is not a safety certification and not a proof of correctness. Randomized verification increases coverage within a declared input model; it does not prove the policy is safe, nor that the declared input model matches what your robots actually see. policy verify never prints PASS or SAFE — a finding-free run reports “no findings under this input model”.

Verification is entirely offline: inputs are a policy bundle (.tar.gz or dir), a scenario YAML, and optional invariants YAML. It never mutates the bundle, registry, keystore, or runtime state, and needs no simulator, ROS, or hardware.

Modes¶

Command	What it does
`run`	Seeded Monte Carlo over a scenario’s input model → decision distribution, invariant findings, rule coverage; optional boundary/perturbation passes.
`scenario`	Mine an empirical `scenario.yaml` from recorded scene-state telemetry (`--from-wal`) — grounds the input model in real field data, no simulator.
`replay`	Re-evaluate exported failure fixtures against a bundle, OR faithfully replay captured production decisions (`--from-wal`) and diff against the recorded outcome.
`compare`	Behavioural diff of two bundle revisions over one seeded stream → which verdicts changed.
`cases`	Run a curated suite of fixed `(scene → expected)` cases, OR replay recorded scenes (`--from-wal`) → outcome distribution + gate.

The one-line happy path:

autonomy policy verify run --bundle bundle.tar.gz --scenario scenario.yaml

Scenario YAML¶

A scenario declares the input model — the field domains the generator samples over — and the action under test.

name: cmd-vel-zone-speed
seed: 7
iterations: 10000
action:
  kind: tool.ros2.topic.publish   # the action the edge evaluates
  scene_source: sensors           # generated fields land at input.scene.sensors.fields.*
inputs:
  speed:                          # numeric range → uniform sampling
    min: 0.0
    max: 2.0
  mode:                           # categorical → uniform over the value set
    values: [nominal, degraded]
constants:
  zone: slow_zone                 # fixed on every case
invariants: invariants.yaml       # optional; path relative to this file

inputs — each field is either a numeric range (min/max → uniform) or a categorical set (values). Numeric values are emitted as json.Number so they match the runtime exactly. These populate input.scene.<scene_source>.fields.*.
constants — scene fields held fixed on every generated case.
seed makes a run reproducible: the same (bundle, scenario, seed) yields the same result. Override with --seed / --iterations.

Command params (`input.params.*`)¶

Scene fields aren’t the only policy input. Command-gated policies — ROS actuator governance on the decoded message (the native governed_ros2_bridge typed-decode path: input.params.topic, input.params.linear.x, …) — gate on the action’s params. Declare a params: channel so those cases are exercised (without it, a command-gated policy fail-closes every case to DENY — a run that looks clean but reached nothing):

action:
  kind: tool.ros2.topic.publish
  # scene_source is optional — omit it for a params-only scenario
params:
  constants:
    topic: /cmd_vel               # → input.params.topic
  inputs:
    linear.x:  {min: -0.6, max: 0.6}   # → input.params.linear.x  (dotted keys nest)
    angular.z: {min: -2.0, max: 2.0}   # → input.params.angular.z

Dot-separated keys expand into the nested object the evaluator reads (linear.x → input.params.linear.x), mirroring the bridge’s server-side KnownTypes decode.
params.inputs / params.constants mirror the top-level inputs / constants (same spec syntax), and compose with the scene channel for hybrid cmd+scene policies. --boundary sweeps params numerics too, so a speed-cap / reverse cliff on linear.x is found. Invariants can gate on params fields by their dotted name.
If a run comes back ~100% one verdict, run warns — that usually means the input model never reaches the policy’s gates (e.g. a missing params: block).

Invariants YAML¶

Invariants are declarative decision constraints — not an expression language. Each has a when: list of conditions (implicitly AND-ed) and an expected outcome and/or effect. When all when: conditions hold, the decision must be in the expected set, or it’s a violation.

invariants:
  - id: fast-in-slow-zone-must-deny
    severity: high                # low | medium | high (default medium)
    description: above 0.5 m/s in a slow zone must be denied
    when:
      - {field: speed, op: gt, value: 0.5}
      - {field: zone,  op: eq, value: slow_zone}
    expect_outcome_in: [deny]     # allow | deny | defer
    # expect_effect_in: [replace]     # optionally constrain the resolved effect
    # expect_verdict_in: [CONSTRAIN]  # graded verdict band — requires --deployment-manifest

Operators: eq, ne, gt, ge, lt, le, in. A condition compares a field to a literal value or another field via value_from. Numeric comparisons are exact (large integers/timestamps don’t collapse through float64).

At least one of expect_outcome_in, expect_effect_in, or expect_verdict_in is required. expect_verdict_in asserts the graded verdict band and only resolves with a deployment manifest — see Graded verification.

Every policy that gates on typed fields should also ship the fail-closed decode rule so a malformed payload denies rather than slips through — see ROS 2 Scene State + Typed Field Policy Authoring.

`run` — what it reports¶

Decision distribution — ALLOW / DEFER / DENY counts, plus a rule-effect breakdown.
Findings — distinct kinds (invariant_violation, invariant_path_missing, eval_error, and the opt-in cliff / oscillation), grouped by severity with a replayable witness (seed + iteration + input).
Rule coverage — which declared rules the sample exercised. Available for IR-authored bundles (yaml-dsl / json-rules / graph, which embed rules_meta); hand-authored Rego honestly reports coverage as unavailable rather than a fabricated number. “Uncovered” means not exercised by this sample, not “unreachable”.
Input coverage — cross-checks the scenario’s declared inputs against the input.* paths the compiled policy actually reads (works for hand-authored Rego too), catching a scenario disconnected from the policy:
- undeclared reads (⚠ the dangerous case): an input the policy reads that the scenario never sets — the gated rule can never fire, so an all-one-verdict run is false-clean (e.g. the policy reads input.scene.probe.fields.d but the scenario declares only bogus_field).
- dead inputs: a scenario field the policy never references (typo / stale).
Single-verdict warning — a run where every case shares one verdict is flagged as a likely “the input model never reached the policy’s gates” smell.
Rego coverage (opt-in, --rego-coverage) — expression/line coverage of the policy Rego, measured by tracing the sampled evaluations through OPA’s cover instrumentation. This is the hand-authored-Rego complement to rule coverage above (which needs the IR compiler’s rules_meta): it reports which policy lines the sample exercised and, more usefully, the line ranges it never reached — a rule the input model never triggers, or dead code. “Not covered” means not exercised by this sample, not “unreachable”. Opt-in because it re-runs the sample with tracing attached:
```
autonomy policy verify run --bundle b.tar.gz --scenario s.yaml --rego-coverage
```

Boundary + perturbation (opt-in)¶

Off by default. --boundary sweeps each numeric input across its range on a fixed grid and reports decision cliffs (sharp thresholds); --perturb reports oscillation (a decision that flips back and forth ≥N times across the sweep — a hysteresis/instability smell). Both are deterministic (no RNG). These findings are LOW severity by default so they don’t drown real findings — unless they occur on a field a declared invariant governs, in which case they inherit that invariant’s severity.

autonomy policy verify run --bundle b.tar.gz --scenario s.yaml --boundary --perturb

Regression & change-control loops¶

Freeze a failure, prove the fix (`--export-failures` → `replay`)¶

# Export every finding as a self-contained, replayable fixture.
autonomy policy verify run --bundle v1.tar.gz --scenario s.yaml --export-failures ./failures

# After a fix: do the frozen failures still reproduce against the new bundle?
autonomy policy verify replay --bundle v2.tar.gz ./failures --fail-on-reproduced

A fixture carries the exact action + frozen verdict + bundle digest, so it replays forever without the original scenario. Replaying against the same bundle must reproduce every verdict — a divergence there signals nondeterminism or a tampered fixture (a hard failure). --export-failures owns its directory (it reconciles stale fixtures on rerun), so a clean rerun never leaves ghosts.

Diff two revisions (`compare`)¶

autonomy policy verify compare --scenario s.yaml v1.tar.gz v2.tar.gz --fail-on-changed

Reports both distributions, the count of changed verdicts, and per-transition counts (e.g. ALLOW -> DENY). --fail-on-changed asserts a revision is behaviour-preserving.

```{admonition} A clean --fail-on-changed can be vacuously true :class: warning

--fail-on-changed only proves “the revisions agree on the cases this scenario sampled” — not that they agree everywhere. If the scenario’s input model never reaches the region where the two bundles diverge (e.g. it samples speed ∈ [0, 0.5] but the change only affects speed ∈ [0.8, 1.0)), the gate passes while the behavioural change ships unseen. So compare runs the same guards as run:

Input coverage over the union of the inputs either bundle reads — an input a revision reads that the scenario never sets is flagged (⚠ dangerous): the diff can’t observe a rule that never fires.
Zero-change warning — when no verdict changed, the report says so explicitly, since that is exactly the shape a false-clean gate takes. (Comparing a bundle to itself legitimately yields zero — the warning asks you to confirm the input model actually covers where you expect the revisions to differ.)

### Curate a suite (`cases`)

```bash
autonomy policy verify cases --bundle bundle.tar.gz ./regression-suite

Each case’s expected.decision is the desired verdict — the answer the bundle should produce — so any mismatch fails the suite (nonzero exit) and gates CI directly. It must be a valid verdict (ALLOW, DEFER, or DENY, case-insensitive); a typo like DENIED fails loudly at load rather than masquerading as a verdict mismatch. The same validation applies to replay fixtures.

Polarity: don’t drop raw exported failures into a suite

Cases share the self-contained fixture format, but expected means the opposite thing than in replay. An exported failure (--export-failures) froze the observed verdict — which for a violation is the wrong answer. Using it as a case unchanged makes the suite pass while the bug persists (and fail once you fix it). To turn a failing input into a permanent guard, reuse its action but set expected to the intended verdict. For “did my fix eliminate the failure?”, use replay --fail-on-reproduced — that’s the failure-regression loop. cases warns when a case still carries an origin.finding_kind (a sign it came straight from --export-failures).

WAL-backed verification (real field data)¶

The scenario run above verifies the domain you declared. Two workflows ground verification in what the fleet actually observed — realistic inputs without a simulator — by reading the runtime’s telemetry WAL. All of them reuse the SAME evaluation engine as the edge, and normalize numeric fields to json.Number so a re-evaluation matches the exact runtime input shape.

Mine a scenario from recorded scenes (`scenario --from-wal`)¶

Aggregate the observed values in autonomy.scene_state frames (per source) into a runnable scenario.yaml: each numeric field becomes a uniform [min,max] over its observed range, each categorical field a values set.

autonomy policy verify scenario --from-wal ./wal --action-kind tool.ros2.topic.publish \
  --source nvblox -o scenario.yaml

Caveat: scene-state frames are a separate channel, not tied to a specific tool decision, so you supply --action-kind; params-driven inputs (topic/payload) aren’t in the scene channel and aren’t mined.

Replay recorded scenes (`cases --from-wal`)¶

“How would this bundle decide on the scenes we actually saw?” — re-evaluate every recorded scene and report the outcome distribution. Recorded scenes carry no expected answer, so this is a distribution + gate, not an assertion:

# Fail CI if the new bundle would DENY any scene the fleet actually observed.
autonomy policy verify cases --bundle v2.tar.gz --from-wal ./wal \
  --action-kind tool.ros2.topic.publish --fail-on-outcome DENY

--invariants additionally checks each observed decision.

Faithful production-decision replay (`replay --from-wal`)¶

The highest-fidelity signal: re-run every decision the fleet actually made against a new bundle and show what changed. This requires the runtime to have captured the evaluated actions.

Capture (opt-in, on the runtime): it logs request payloads, so it is off by default and sampleable + redactable.

# --capture-action-input : emit an autonomy.action_input frame per decision
# --capture-sample-n 10  : capture 1 in 10 (bounds the hot-path cost)
# --capture-params-allow : keep only these params verbatim; redact the rest
autonomy runtime start --policy ./bundle \
  --capture-action-input \
  --capture-sample-n 10 \
  --capture-params-allow topic

Replay + diff:

# Fail CI if any captured production decision changes under the new bundle.
autonomy policy verify replay --bundle v2.tar.gz --from-wal ./wal --fail-on-changed

The report gives unchanged / changed counts and a per-transition breakdown (ALLOW->DENY, …). Caveats, honest by construction:

A capture whose params were redacted is partial and is skipped (never diffed as if faithful).
The replayed outcome is the policy decision. For a graded / replace deployment the recorded wire outcome reflects runtime shaping (a replace verdict denies the original on the wire) that a policy re-evaluation does not reproduce, so a diff there is expected — not a regression.

Graded verification (execution-decision model)¶

A graded policy (the execution-decision model) keeps allow := true and returns a top-level verdict — ALLOW / CONSTRAIN / AVOID / HOLD — that the deployment manifest maps to an effect (pass_through / replace / reject). Offline, without that manifest, all four bands are allow=true and collapse into one indistinguishable ALLOW, and no effect is resolved. Pass the same signed manifest the runtime loads so verify applies the model exactly as the edge does:

autonomy policy verify run --bundle graded.tar.gz --scenario scenario.yaml \
  --deployment-manifest deployment.json --invariants invariants.yaml

With --deployment-manifest, the verifier validates each returned verdict against the manifest’s declared vocabulary, computes the effect, and fail-closes an invalid (undeclared) verdict to DENY — matching the runtime, which drops the verdict entirely. It then surfaces:

run — a verdict summary breaking the permit band out by name (ALLOW / CONSTRAIN / AVOID / HOLD) alongside the decision distribution and effect summary, plus an invalid_verdict finding for any rejected verdict.
cases — a fixture can assert expected.verdict (e.g. CONSTRAIN), so a regression that swaps one band for another fails even though the coarse ALLOW/DEFER/DENY decision is unchanged:
```
# a graded case
expected: {decision: ALLOW, verdict: CONSTRAIN}
```
invariants — expect_verdict_in / expect_effect_in are checked against the resolved verdict/effect. Both run and cases --from-wal accept --deployment-manifest; recorded-scene replay then reports a verdict breakdown too.

Guard-rails so a graded assertion never silently passes:

expect_verdict_in without --deployment-manifest errors — the verdict is always empty and could never match.
An expect_verdict_in name outside the manifest’s declared vocabulary (a typo like CONSTRAIByN) errors at load rather than reporting every case as a violation.
A cases fixture asserting expected.verdict without a manifest errors likewise.

# graded verdicts on the scenes the fleet actually observed
autonomy policy verify cases --bundle graded.tar.gz --from-wal ./wal \
  --action-kind tool.ros2.topic.publish \
  --deployment-manifest deployment.json --invariants invariants.yaml

CI exit codes¶

Gate	Flag	Nonzero exit
`run` findings at/above a severity	`--fail-on low\|medium\|high`	a finding met the gate
`replay` frozen failures still reproduce	`--fail-on-reproduced`	any reproduced (or a same-digest divergence, always)
`replay --from-wal` production decisions changed	`--fail-on-changed`	any captured decision changed under the new bundle
`compare` verdicts changed	`--fail-on-changed`	any verdict changed
`cases` suite	(always)	any case failed
`cases --from-wal` observed scenes	`--fail-on-outcome DENY[,DEFER]`	any observed scene decides that way

Exit 5 (ExitVerifyFindings) is the verification-found-something code; 0 is a clean gate. All reports are also available as canonical JSON (--format json) for machine consumption.

Worked example — range-aware calibration¶

A calibration-uncertainty scenario sweeps a camera↔LiDAR yaw error against range, speed, and calibration confidence, and asserts that when the projected lateral error exceeds the association margin the action must not proceed:

# scenario.yaml
name: calib-uncertainty
seed: 1
iterations: 20000
action: {kind: tool.ros2.topic.publish, scene_source: perception}
inputs:
  yaw_error_deg:        {min: 0.0, max: 3.0}
  range_m:              {min: 1.0, max: 30.0}
  speed_mps:            {min: 0.0, max: 2.5}
  calibration_conf:     {min: 0.0, max: 1.0}
invariants: invariants.yaml

# invariants.yaml
invariants:
  - id: projected-error-exceeds-margin-must-hold
    severity: high
    when:
      - {field: yaw_error_deg,   op: gt, value: 1.5}
      - {field: range_m,         op: gt, value: 10.0}
    expect_outcome_in: [deny, defer]

Run it, gate CI on high findings, and — when you tighten the policy from a fixed threshold to a range-aware envelope — compare the two bundles to see exactly which cases the new envelope changes.

Scope & limits¶

Input-model fidelity is on the author for a hand-declared scenario — if the declared domain doesn’t match reality, a clean run verifies an unrealistic domain. Ground the input model in real field data instead with WAL-backed verification — scenario/cases --from-wal (#1312) and faithful production replay via replay --from-wal (#1313).
Single-decision, stateless. It samples independent decisions; it does not model temporal sequences or closed-loop behaviour.
Out of scope for this milestone: simulator sources, extra distributions (normal / grid / loguniform), HTML/JUnit/SARIF reporters, signed reports, and unreachable-rule detection — each a separate follow-up.

Policy Verification (autonomy policy verify)¶

Modes¶

Scenario YAML¶

Command params (input.params.*)¶

Invariants YAML¶

run — what it reports¶