ContractRefine — Pre-execution Contract Verification

ContractRefine is a semantic preflight layer above the AutonomyOps ADK runtime’s existing mechanical enforcement stack. Mechanical layers answer “is this call shape-valid, identity-valid, and allowed?”. ContractRefine answers a different question: “is the planned action internally consistent with the governance configuration the operator agreed to?”.

It returns one of three top-level outcomes on the PreflightDecision.outcome field:

Outcome	Meaning	Execution?
pass	No blocking contract failed.	May proceed to /v1/tool.
repair_required	A blocking contract failed AND a deterministic, bounded repair hint exists.	Caller may retry once with corrections; not allowed as-is.
deny	A blocking contract failed with no repair path.	Execution is blocked.

The outcome field is always one of those three values — it is the operator’s primary decision signal and the wire-format enum is closed. There is no fourth “advisory” outcome.

Where advisory signals live

A contract may fail at severity: advisory rather than severity: blocking. Advisory failures are recorded inside the response — PreflightDecision.contract_results[] carries one entry per evaluated contract, each with its own outcome (pass | fail | not_applicable) and severity (info | blocking | advisory). The top-level outcome aggregates only severity: blocking failures; advisory failures surface in contract_results and in the WAL but do not change the top-level verdict.

The canonical advisory case in Phase 1 is chain_unverifiable_offline (Contract Taxonomy), which records that the verifier could not prove decision-chain completeness because evaluating it would require substrate the edge node cannot reach offline. The operator chose disconnected operation and accepts the residual risk; the WAL preserves the signal for audit. The top-level outcome for this case is pass (no blocking contract failed), and /v1/tool proceeds normally.

Clients implementing automated retry-on-repair logic SHOULD switch on the top-level outcome only. Clients implementing audit dashboards or operator-explain UIs SHOULD additionally surface any contract_results entry whose severity is advisory so the operator sees what the verifier could not verify.

Every preflight emits an autonomy.preflight WAL event correlated to the eventual /v1/tool decision under a shared audit_id.

Where it sits in the stack

ContractRefine is additive. It does not bypass or replace any existing layer; it adds an earlier checkpoint that the operator can opt into.

[caller / agent / planner]
        │
        │   POST /v1/preflight {intent, plan, context}
        ▼
┌─────────────────────────────────────────────────────────────────┐
│  runtime/server.go : handlePreflight                            │
│                                                                 │
│   runtime/contract.Verifier                                     │
│     ├─ resolve actor / entitlement / attestation / policyctx    │
│     ├─ run contract checks  (deterministic)                     │
│     └─ produce PreflightDecision                                │
│                                                                 │
│   ── WAL emit(autonomy.preflight, attrs{audit_id,...})          │
└─────────────────────────────────────────────────────────────────┘
        │
        │   caller may then proceed with X-Autonomy-Preflight-Id header
        ▼
┌─────────────────────────────────────────────────────────────────┐
│  runtime/server.go : handleTool      (unchanged today)          │
│                                                                 │
│   ── pre-policy admission gates ──   (mavlink, ros 2 mediator)  │
│   ── policy.Evaluator.Eval ──        (Rego, data.autonomy.allow)│
│   ── attestation.Gate ──             (enrollment / rollout)     │
│   ── executeTool ──                  (allowlist / egress-DLP)   │
│                                                                 │
│   ── WAL emit(autonomy.decision, attrs{audit_id,...})           │
└─────────────────────────────────────────────────────────────────┘

The two WAL events join under a shared audit_id, producing a forward-traceable record: intent stated → preflight verdict → tool decision → tool outcome, all under one correlation key.

The same ServerOptions wiring pattern used today by the MAVLink supervisor (runtime/mavlink_gate.go) and the ROS 2 mediator (runtime/ros2/) is reused: a nil ContractVerifier ⇒ preflight is disabled, /v1/preflight returns 503, and /v1/tool keeps its current semantics verbatim. This is the backward-compatibility door (see INV-CR-1).

Why a new endpoint, not a wrapper around /v1/tool

/v1/tool is execution-bound, single-call, post-decision. A preflight evaluates a plan (one or more tool calls), and may legitimately return repair_required without firing any execution. Reusing /v1/tool would muddy its semantics. The existing runtime/server.go dual-emit pattern — policy frame + runtime-enforcement frame under one audit_id — already demonstrates the discipline ContractRefine extends forward in time, not backward.

Core architectural commitments

1. Verifier is interface-driven. contract.Verifier is a Go interface in runtime/contract/types.go; the default implementation is the exported contract.DefaultVerifier in runtime/contract/verifier.go. Wired into runtime.ServerOptions.ContractVerifier the same way MavlinkSupervisor and ROS2Mediator are wired today.

2. No global state. The verifier resolves its inputs from the request body plus injected resolvers (entitlement, attestation snapshot, policy context). No singletons; no module-level mutable state.

3. Deterministic. Same PreflightRequest bytes + same resolvers + same policy bundle ⇒ same PreflightDecision bytes (modulo the freshly generated preflight_id and audit_id). See INV-CR-5.

4. Same fail-closed discipline as /v1/tool. Verifier unavailable, resolver error, unknown contract kind ⇒ deny. Never pass on error. See INV-CR-2.

5. Reason-shape contract reused. A new layer prefix contract: matches the existing regex enforced by runtime/reasons_shape_test.go. See INV-CR-4.

6. Same WAL discipline. A new EventKind is added to telemetry/emitter.go (the file that defines the EventKind type and its constants; telemetry/events.go holds the per-kind builder helpers). Same Entry envelope, same fsync + safe_seq durability, same audit_id correlation. See INV-CR-8.

Backward compatibility

ContractRefine is gated by a single config knob, runtime.contract_refine.mode, with three positions that mirror the existing attestation.mode ladder:

Mode	/v1/preflight	/v1/tool binding-mismatch behavior	requires_preflight: true bundle gate	Default
disabled	503 — verifier wired but disabled	Header ignored; no binding check runs	Field is parsed but never enforced — bundle behaves identically to one without the field	Explicit opt-out only
advisory	Returns a decision	Binding check runs; any failure emits an autonomy.decision WAL frame with outcome=deny and reason=contract: preflight_* under the same audit_id the /v1/tool request will use, but the request CONTINUES to the policy layer with Action.Preflight=nil. Operator opts in to observe the deny signal in production traffic without enforcing it.	Missing header emits an autonomy.decision deny frame with reason=contract: preflight_required and then the request continues — same WAL signal as a real deny, no wire-level 403	Default (post-C12)
enforce	Returns a decision	Binding check runs; mismatch ⇒ deny with contract: preflight_binding_mismatch. This is the GA posture.	Bundle’s requires_preflight: true capabilities deny /v1/tool calls without a matching X-Autonomy-Preflight-Id header	GA after future soak

INV-CR-3 (Invariants) is authoritative on the binding-check ladder; the table above is the operator-facing summary. The two MUST agree — if a future change updates one, the other follows.

Existing deployments are unaffected:

• Old clients that never send X-Autonomy-Preflight-Id continue to work because the header is optional. In the post-C12 default (advisory), a missing header on a requires_preflight: true bundle emits a deny decision frame to the WAL but the request still reaches the policy layer — no wire-level 403, no behavioral change relative to a pre-#1020 deployment serving the same client.

• Policy bundles without requires_preflight are loaded unchanged and behave exactly as they did pre-#1020. The absent field is treated as false; the bundle loader MUST NOT reject for the field’s absence under any mode (see INV-CR-1 enforcement).

• WAL consumers ignore unknown event kinds; the autonomy.preflight addition is non-breaking.

• Operators who want the pre-C12 silent posture set runtime.contract_refine.mode: disabled explicitly; the zero-value default is no longer disabled (C12 #1032).

What this is NOT

ContractRefine is deliberately narrow. Operators reading the architecture sometimes ask whether the layer also does the following — it does not:

• Not an LLM rubric. No model-in-the-loop scoring, no “LLM judge”. Contracts are deterministic predicates over a typed input. See INV-CR-7.

• Not an unbounded refinement loop. At most one repair attempt per preflight session by default; configurable up to a small constant. Beyond that, deny. See INV-CR-6.

• Not a planner. ContractRefine does not generate plans; it accepts them.

• Not a replacement for policy. Rego policy still runs at /v1/tool. ContractRefine produces an additional signal that policy can read; it does not bypass policy. See INV-CR-9.

• Not Isaac-aware, not ROSOrin-aware. No domain-specific contract kinds, no NVIDIA APIs, no robot-specific assumptions. Isaac (#849) and ROSOrin (#793) consume ContractRefine; they do not extend it.

Integration surface

The contract Isaac (#849) and ROSOrin (#793) consume. This section is the single source of truth for what downstream consumers code against — endpoints, headers, contract names, eligibility shape, and the reason-stacking rule. Anything not listed here is internal to the verifier and may change without notice.

Endpoints

Method	Path	Purpose	Lands in PR
POST	/v1/preflight	Submit a PreflightRequest; receive a PreflightDecision. Supports ?dry_run=true (no WAL write; empty preflight_id + audit_id).	C05 (#1025), C09 (#1029) dry-run
GET	/v1/preflight/{preflight_id}	Retrieve a stored decision from the WAL.	C05 (#1025)
POST	/v1/tool	Execute an action. Reads X-Autonomy-Preflight-Id and gates on the binding ladder (see INV-CR-3).	C08 (#1028)
GET	/v1/audit/{audit_id}	Returns the chronological INV-CR-8 join of every autonomy.preflight + autonomy.decision frame sharing the audit_id.	C08 (#1028)

Mode (runtime.contract_refine.mode) gates the endpoints: disabled ⇒ /v1/preflight returns 503 and the /v1/tool binding check is bypassed; advisory and enforce differ only on whether a binding-check failure denies vs records. See the Backward compatibility table for the full matrix.

Header

X-Autonomy-Preflight-Id: <preflight_id>

Consumers set this header on /v1/tool to bind an action to a previously-issued preflight decision. The runtime resolves the id against the WAL, verifies the binding (kind in BoundToolKinds, ExpiresAt in the future, not previously consumed), and either attaches the resolved PreflightDecision to runtime.Action.Preflight (for Rego rules) or denies with one of the four binding reason codes (see below).

The dry-run path returns preflight_id = "" and audit_id = "" so a dry-run decision is unambiguously non-bindable (the empty string is rejected at header-validation time before any cache lookup).

Contract catalog

The Phase 1 catalog is enumerated on the Contract Taxonomy page and is the source of truth for what the verifier evaluates. The seven contracts:

plan_shape · argument_provenance · capability_in_zone · rollback_contract · expected_evidence · attestation_freshness · decision_chain_complete

Consumer epics MUST NOT depend on a contract that isn’t in this list. Domain-specific contracts (MAVLink obligations, mission-gate semantics, restricted-zone primitives) layer ON TOP of the neutral catalog in their own epics — they do not extend the catalog itself. See What the catalog is NOT on the taxonomy page.

ExecutionEligibility shape

A passing PreflightDecision carries an ExecutionEligibility block that names what /v1/tool will accept under the returned preflight_id. The wire shape (runtime/contract/types.go):

{
  "allowed":           true,
  "required_rollback": "rb.cancel.mission",
  "bound_tool_kinds":  ["tool.echo", "tool.shell"],
  "expires_at":        "2026-06-15T12:05:00Z"
}

Field semantics: allowed is false on deny / repair_required; required_rollback is optional (only when the request named one); bound_tool_kinds is optional and load-bearing for the /v1/tool binding check; expires_at is the verifier’s now + BindingWindow, RFC3339 UTC.

bound_tool_kinds is the load-bearing field for the binding check: the /v1/tool call’s kind MUST be in this list. expires_at bounds the binding lifetime (INV-CR-3); the verifier’s DefaultBindingWindow constant (defined in runtime/contract/verifier.go) is 5 minutes, configurable per-deployment via the verifier’s BindingWindow field.

The runtime separately enforces an in-memory binding-cache TTL ceiling of 60 seconds (runtime.PreflightBindingCacheCeiling). When the cache entry evicts, a subsequent /v1/tool call rehydrates from the WAL and (if a matching autonomy.preflight_consumed marker exists) resolves to contract: preflight_replay. The 60-second ceiling bounds runtime memory regardless of how long an operator’s BindingWindow is set to; it does NOT shorten the binding’s operator-visible lifetime, only the hot-lookup window.

Reason codes

Two layers of reason codes consumer epics MUST handle, both in the canonical <layer>: <subreason> shape that runtime/reasons_shape_test.go pins. Source of truth: runtime/contract/reasons.go.

Verifier-emitted (returned in PreflightDecision.Reason):

Code	When
contract: passed	Every blocking contract passed.
contract: repair_required	At least one blocking contract failed but EVERY blocking failure produced ≥1 bounded hint.
contract: repair_exhausted	The session’s bounded-repair budget (INV-CR-6) was already consumed.
contract: session_metadata_missing	A SessionStore is wired but the caller omitted actor.session_id / intent.plan_hash.
contract: <per-contract subreason>	One of the seven Phase 1 contracts failed — e.g. plan_shape_invalid, rollback_contract_not_ready. Full list on the taxonomy page.
contract: verifier_unavailable · contract: resolver_error · contract: introspector_error	Fail-closed paths owned by INV-CR-2.

Binding-layer (emitted at /v1/tool under the same audit_id):

Code	When
contract: preflight_required	Header absent when the bundle declares requires_preflight: true, OR header points at an id not in the WAL.
contract: preflight_binding_mismatch	Header resolves but the action’s kind is not in bound_tool_kinds.
contract: preflight_expired	ExpiresAt has passed (or the in-memory cache TTL elapsed and the runtime cannot reconstruct the binding).
contract: preflight_replay	The id was already consumed — INV-CR-3 single-purpose binding. Durable via the autonomy.preflight_consumed WAL marker; survives cache eviction and process restart.

Reason-stacking rule

When multiple verifier failures could fire on one preflight, the rule is most-specific-blocking-failure first, advisory failures stacked under it. The verifier composes a single top-level Outcome + Reason by walking ContractResults in deterministic catalog order:

1. If any blocking failure exists AND every blocking failure contributed ≥1 bounded hint → top-level is repair_required with Reason = contract: repair_required.

2. Otherwise if any blocking failure exists → top-level is deny with Reason = the first blocking failure's per-contract reason.

3. Otherwise → top-level is pass with Reason = contract: passed.

Advisory failures (severity advisory) stay in ContractResults under their own per-contract row but do NOT influence the top-level Outcome. The Where advisory signals live section above is the operator-facing summary of this rule; the implementation lives in runtime/contract/verifier.go composeOutcome.

Consumer epics that need a finer-grained view than the top-level Outcome walk ContractResults themselves. The catalog order (taxonomy page) is the deterministic iteration order; tests pin it.

What consumers MAY rely on across PRs

A small surface that ContractRefine treats as a frozen API once published — any future change goes through a deprecation cycle, not a silent break:

• Endpoint paths (/v1/preflight, /v1/preflight/{id}, /v1/tool, /v1/audit/{id}).

• The X-Autonomy-Preflight-Id header name.

• The seven Phase 1 contract names.

• The reason codes enumerated above and on the taxonomy page.

• PreflightDecision, PreflightRequest, ExecutionEligibility, Result JSON tags.

• The chronological INV-CR-8 join shape on /v1/audit — Frames[].kind ∈ {"autonomy.preflight", "autonomy.decision"}, sorted by timestamp ascending.

What consumers MAY NOT rely on: verifier internals (resolver construction, attempt counter shape, repair_hints content beyond the {field, suggestion, bounded} tuple, evidence-map keys outside the catalog).

Reference demo

The walk-through that exercises the full integration surface end-to- end (POST /v1/preflight → POST /v1/tool with header → GET /v1/audit chronological join) is the ContractRefine Demo Runbook. Headline command: autonomy demo contract-refine. Isaac and ROSOrin extend the same shape — see the Cross-epic section of the runbook.

Related substrate

Existing layer	Pattern reused by ContractRefine
runtime/server.go — ServerOptions injection	ContractVerifier field; nil ⇒ disabled
runtime/mavlink_gate.go — pre-policy admission	Verifier runs above policy, fail-closed shape
runtime/attestation/ — mode ladder (off/advisory/enforce)	contract_refine.mode mirrors the ladder verbatim
runtime/reasons_shape_test.go — reason regex	New contract: layer extends the allow-list
telemetry/emitter.go — open-ended EventKind enum (with telemetry/events.go builder helpers)	New autonomy.preflight kind, same envelope

For the catalog of contracts evaluated at preflight, see Contract Taxonomy.

For the formal safety + security invariants the layer must uphold, see INV-CR-1 .. INV-CR-9 in Invariants.

For the runnable end-to-end walkthrough Isaac and ROSOrin extend, see the Integration surface § Reference demo section above and the linked ContractRefine Demo Runbook.