Corvid core semantics

July 15, 2026 · View on GitHub

Auto-generated from corvid_guarantees::GUARANTEE_REGISTRY. Do not hand-edit. Update by running cargo run -q -p corvid-cli -- contract regen-doc docs/reference/core-semantics.md and committing the result.

Every public Corvid promise about effects, approvals, grounding, budgets, confidence, replay, provenance, and the ABI surface is enumerated below. Each row carries:

a stable id referenced by diagnostics, tests, the bilateral verifier, and corvid claim --explain,
a kind (which moat dimension it belongs to),
a class — static (compiler refuses to produce a binary on violation), runtime_checked (runtime detects and surfaces), or out_of_scope (a documented promise that does NOT have a check today; reason recorded inline below),
the pipeline phase that owns the enforcement.

Per the no-shortcuts rule, every out_of_scope entry carries an explicit reason. Anything Corvid does not defend appears below in plain language; we do not rely on omission.

Summary

id	kind	class	phase
`approval.dangerous_call_requires_token`	approval	static	typecheck
`approval.trust_tier_requires_token`	approval	static	typecheck
`approval.token_lexical_only`	approval	static	typecheck
`approval.dangerous_marker_preserved`	approval	out_of_scope	typecheck
`approval.reachable_entrypoints_require_contract`	approval	static	typecheck
`effect_row.body_completeness`	effect_row	static	typecheck
`effect_row.caller_propagation`	effect_row	out_of_scope	typecheck
`effect_row.import_boundary`	effect_row	static	resolve
`secrets.trace_never_carries_value`	effect_row	runtime_checked	runtime
`io_source.fs_path_confinement`	effect_row	runtime_checked	runtime
`io_source.fs_write_quarantine_on_replay`	effect_row	runtime_checked	runtime
`io_source.fs_read_quarantine_on_replay`	effect_row	runtime_checked	runtime
`io_source.http_ssrf_structural_block`	effect_row	runtime_checked	runtime
`io_source.http_allowlist_enforcement`	effect_row	runtime_checked	runtime
`io_source.sqlite_parameter_binding_only`	effect_row	runtime_checked	runtime
`io_source.sqlite_write_quarantine_on_replay`	effect_row	runtime_checked	runtime
`io_source.sqlite_read_passthrough_on_replay`	effect_row	runtime_checked	runtime
`io_source.http_quarantine_on_replay`	effect_row	runtime_checked	runtime
`json.parse_safety_no_panic`	effect_row	runtime_checked	runtime
`json.field_type_safety_at_access_boundary`	effect_row	runtime_checked	runtime
`taint.untrusted_cannot_reach_dangerous`	effect_row	static	typecheck
`grounded.provenance_required`	grounded	static	typecheck
`grounded.propagation_across_calls`	grounded	out_of_scope	typecheck
`grounded.no_laundering`	grounded	static	typecheck
`budget.compile_time_ceiling`	budget	static	typecheck
`budget.runtime_termination`	budget	out_of_scope	runtime
`confidence.min_threshold`	confidence	static	typecheck
`trust.constraint_enforcement`	trust	static	typecheck
`replay.deterministic_pure_path`	replay	runtime_checked	runtime
`replay.trace_signature`	replay	runtime_checked	runtime
`provenance_trace.receipt_signature`	provenance_trace	runtime_checked	runtime
`abi_descriptor.cdylib_emission`	abi_descriptor	static	codegen
`abi_descriptor.byte_determinism`	abi_descriptor	static	codegen
`abi_descriptor.bilateral_source_match`	abi_descriptor	runtime_checked	abi_verify
`abi_attestation.envelope_signature`	abi_attestation	runtime_checked	abi_verify
`abi_attestation.descriptor_match`	abi_attestation	runtime_checked	abi_verify
`abi_attestation.absent_reports_unsigned`	abi_attestation	runtime_checked	abi_verify
`abi_attestation.sign_requires_claim_coverage`	abi_attestation	static	codegen
`jobs.cron_schedule_durable`	jobs	runtime_checked	runtime
`jobs.retry_budget_bound`	jobs	out_of_scope	runtime
`jobs.idempotency_key_uniqueness`	jobs	runtime_checked	runtime
`jobs.lease_exclusivity`	jobs	runtime_checked	runtime
`jobs.durable_resume`	jobs	runtime_checked	runtime
`jobs.cron_dst_correct`	jobs	runtime_checked	runtime
`jobs.approval_wait_resume`	jobs	out_of_scope	runtime
`jobs.loop_bounds_enforced`	jobs	runtime_checked	runtime
`jobs.explain_sources_grounded`	jobs	runtime_checked	runtime
`jobs.replayable_side_effects`	jobs	runtime_checked	runtime
`auth.session_rotation_on_privilege_change`	auth	runtime_checked	runtime
`auth.api_key_at_rest_hashed`	auth	runtime_checked	runtime
`auth.api_key_scope_subset_check`	auth	runtime_checked	runtime
`auth.jwt_kid_rotation`	auth	runtime_checked	runtime
`auth.oauth_pkce_required`	auth	runtime_checked	runtime
`auth.csrf_double_submit`	auth	runtime_checked	runtime
`tenant.cross_tenant_compile_error`	auth	out_of_scope	typecheck
`approval.policy_clause_static_check`	auth	out_of_scope	typecheck
`approval.batch_equivalence_typed`	auth	out_of_scope	typecheck
`approval.batch_refuses_cross_data_class_drift`	auth	runtime_checked	runtime
`approval.explain_sources_grounded`	auth	runtime_checked	runtime
`approval.confused_deputy_typecheck`	auth	out_of_scope	typecheck
`connector.scope_minimum_enforced`	connector	runtime_checked	runtime
`connector.write_requires_approval`	connector	out_of_scope	typecheck
`connector.rate_limit_respects_provider`	connector	runtime_checked	runtime
`connector.contract_drift_detected`	connector	runtime_checked	runtime
`connector.drift_narration_grounded`	connector	runtime_checked	runtime
`connector.webhook_signature_verified`	connector	runtime_checked	runtime
`connector.replay_quarantine`	connector	runtime_checked	runtime
`observability.otel_conformance`	observability	runtime_checked	runtime
`observability.lineage_completeness`	observability	runtime_checked	runtime
`observability.redaction_determinism`	observability	runtime_checked	runtime
`observability.contract_aware_grouping`	observability	runtime_checked	runtime
`eval.drift_attribution`	observability	runtime_checked	runtime
`eval.promotion_signed_lineage`	observability	runtime_checked	runtime
`review_queue.cost_of_being_wrong_ranking`	observability	runtime_checked	runtime
`deploy.reproducible_build`	deploy	runtime_checked	platform
`deploy.attestation_chain`	deploy	runtime_checked	platform
`deploy.sbom_completeness`	deploy	runtime_checked	platform
`release.signed_artifact`	release	runtime_checked	platform
`release.notes_grounded`	release	runtime_checked	platform
`upgrade.claim_regression_check`	upgrade	runtime_checked	platform
`ops.live_introspection_signed`	ops	runtime_checked	runtime
`claim.audit_runnable_artifacts`	claim	runtime_checked	platform
`claim.audit_explain_failures_grounded`	claim	runtime_checked	platform
`platform.host_kernel_compromise`	platform	out_of_scope	platform
`platform.signing_key_compromise`	platform	out_of_scope	platform
`platform.toolchain_compromise`	platform	out_of_scope	platform
`app.pr_describe_grounded`	app	runtime_checked	runtime
`app.adversarial_refresh_grounded`	app	runtime_checked	runtime
`app.boot_summary_grounded`	app	runtime_checked	runtime
`package.hosted_registry_available`	platform	out_of_scope	platform

Detail

Approval boundaries

`approval.dangerous_call_requires_token`

class: static
phase: typecheck

A call site invoking a @dangerous tool must have an approve token lexically in scope; otherwise the typechecker rejects the program.

Positive tests:

crates/corvid-types/src/tests.rs::dangerous_tool_with_matching_approve_is_ok

Adversarial tests:

crates/corvid-types/src/tests.rs::dangerous_tool_without_approve_is_compile_error
crates/corvid-types/src/tests.rs::tagged_unapproved_dangerous_call_carries_approval_guarantee_id

`approval.trust_tier_requires_token`

class: static
phase: typecheck

A call site invoking a tool whose composed effect row carries trust: supervisor_required or trust: human_required must have an approve token lexically in scope, exactly like a dangerous tool — the requirement is DERIVED from the trust tier so a declaration that forgets the dangerous marker still gets compile-time protection. The diagnostic names the deriving effect and tier. autonomous and the confidence-gated autonomous_if_confident(...) (which typechecks as autonomous and escalates at runtime) derive nothing.

Positive tests:

crates/corvid-types/src/tests.rs::high_trust_tool_with_matching_approve_is_ok

Adversarial tests:

crates/corvid-types/src/tests.rs::high_trust_tool_without_approve_is_compile_error
crates/corvid-types/src/tests.rs::high_trust_error_names_deriving_effect_and_tier

`approval.token_lexical_only`

class: static
phase: typecheck

Approval tokens are lexically scoped — they cannot be returned, stored in fields, or passed across opaque boundaries to unlock a call site outside the original approve block.

Positive tests:

crates/corvid-types/src/tests.rs::outer_approve_authorizes_inner_call

Adversarial tests:

crates/corvid-types/src/tests.rs::approve_does_not_leak_out_of_if_branch
crates/corvid-types/src/tests.rs::mutation_nested_inner_approve_does_not_authorize_outer_call

`approval.dangerous_marker_preserved`

class: out_of_scope
phase: typecheck

A @dangerous marker cannot be erased by re-exporting or aliasing the tool through another module — every public alias preserves the original danger annotation.

Why out of scope: Structural property of the language, not a separately-fired diagnostic. Corvid's source syntax has no import use form that can declare the alias's effect — aliases inherit their source's @dangerous marker by construction. The property is verified indirectly: when a dangerous imported tool is aliased and then called without approve, the parent diagnostic approval.dangerous_call_requires_token fires correctly, which is only possible because the marker was preserved through the alias. The cited test_refs assert that parent-diagnostic firing through the alias path. Phase 35V-T1-B (2026-05-08) downgraded this row from Static to OutOfScope because no separate diagnostic site exists to tag with this id; the property remains documentary, the enforcement remains structural via the parent diagnostic. A future syntax slice that introduces an explicit alias-effect-override surface would promote this row back to Static with a tagged diagnostic at the override-rejection site.

`approval.reachable_entrypoints_require_contract`

class: static
phase: typecheck

Externally reachable routes, schedules, and exported agents are walked through their reachable agent calls; any reachable @dangerous tool call must still have a matching lexical approval contract.

Positive tests:

crates/corvid-types/src/tests.rs::server_route_approve_authorizes_dangerous_tool

Adversarial tests:

crates/corvid-types/src/tests.rs::server_route_reachability_reports_helper_without_approval
crates/corvid-types/src/tests.rs::schedule_reachability_reports_job_without_approval

Effect rows

`effect_row.body_completeness`

class: static
phase: typecheck

A function's declared effect row must cover every effect actually produced by its body (including effects of called functions); under-reporting is a compile error.

Positive tests:

crates/corvid-types/src/tests.rs::mutation_tool_uses_declared_effect_is_ok

Adversarial tests:

crates/corvid-types/src/tests.rs::mutation_baseline_trust_violation_exists
crates/corvid-types/src/tests.rs::mutation_multiple_effects_on_one_tool_compose_cost_and_trust

`effect_row.caller_propagation`

class: out_of_scope
phase: typecheck

Callers inherit the union of their callees' effects unless they declare a wider row; callers cannot silently shrink the effect surface.

Why out of scope: Subsumed by effect_row.body_completeness at the diagnostic level. The shipped analyze_effects analysis composes effects across calls (collect_body_effects walks the body and unions every called tool/prompt/agent's effect row into the composed profile) and fires a single EffectConstraintViolation per dimension when the declared row doesn't cover the composed result. The violation message says "dimension X: constraint requires Y, but composed value is Z" without distinguishing whether the offending contribution came from a direct body call or from a transitive callee — the unified analysis treats them identically. The user's mitigation is the same in both cases: widen the declared effect row to cover the composed value. Phase 35V-T1-B (2026-05-08) downgraded this row from Static to OutOfScope because the analyzer's ConstraintViolation struct does not carry a body-vs-callee source field, so there is no discriminable diagnostic site to tag with this id; the property is documentary, the enforcement is via the parent's unified diagnostic. A future slice that extends ConstraintViolation with a source field plus per-violation discrimination at the firing site would promote this row back to Static.

`effect_row.import_boundary`

class: static
phase: resolve

Cross-module imports preserve effect annotations exactly; an importer cannot use a re-exported function with a stripped or weakened effect row.

Positive tests:

crates/corvid-types/src/tests.rs::python_import_with_unsafe_effect_warns

Adversarial tests:

crates/corvid-types/src/tests.rs::python_import_without_effects_is_rejected

`secrets.trace_never_carries_value`

class: runtime_checked
phase: runtime

The executing secret_read tool returns the real secret value to the program, but the recorded ToolResult trace event carries a redacted copy (<redacted:XY> marker, value_redacted: true) — traces never persist secret values. Substitute-mode replay RE-READS the live environment instead of substituting (there is nothing usable to substitute), so a changed environment diverges honestly. Residual channel stated as explicit non-scope: a secret the program forwards into another tool's arguments is recorded by that tool's own events; the structural taint fix (an opaque SecretHandle value) is the tracked post-v1.0 deepening.

Positive tests:

crates/corvid-driver/tests/executing_secrets_cache_through_driver.rs::secret_read_returns_real_value_to_the_program
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_rereads_secret_from_live_environment

Adversarial tests:

crates/corvid-driver/tests/executing_secrets_cache_through_driver.rs::secret_value_never_lands_in_the_trace

`io_source.fs_path_confinement`

class: runtime_checked
phase: runtime

Every call to an executing file-I/O tool (io.read_text / io.write_text / io.list_dir, from std/io.cor) resolves the caller's path through the project's configured [io] root before reaching the filesystem. Paths that traverse out of the root (via .. segments or absolute-prefix escapes) are refused with a structured diagnostic naming the offending path AND the configured root. When no [io] root is configured, every call fails closed — the executing file-I/O surface refuses to operate without an explicit security boundary declared in corvid.toml. At the language surface the refusal is an honest Err value (the io/db tools return Result), so programs observe the diagnostic without the boundary weakening.

Positive tests:

crates/corvid-runtime/src/io.rs::io_tool_policy_relative_root_resolves_against_corvid_toml_dir
crates/corvid-runtime/tests/executing_io_tools.rs::executing_io_tools_resolve_both_absolute_and_relative_roots

Adversarial tests:

crates/corvid-runtime/src/io.rs::io_tool_policy_rejects_parent_traversal_escape
crates/corvid-runtime/src/io.rs::io_tool_policy_strips_leading_separator_to_confine_absolute_inputs
crates/corvid-runtime/src/io.rs::io_tool_policy_unconfigured_fails_closed_on_resolve
crates/corvid-runtime/tests/executing_io_tools.rs::executing_io_tools_reject_path_traversal_with_clear_diagnostic
crates/corvid-runtime/tests/executing_io_tools.rs::executing_io_tools_fail_closed_without_io_root_configured

`io_source.fs_write_quarantine_on_replay`

class: runtime_checked
phase: runtime

A Substitute-mode replay runtime refuses every executing file-write call. Both the low-level IoRuntime::write_text path AND the Runtime::call_tool("io.write_text", ...) dispatch path are covered: the low-level path returns QuarantineViolation directly; the dispatch path goes through the replay-substitution path first (so writes either substitute from the recorded trace OR diverge — they never reach the live filesystem). The filesystem is provably untouched in both cases.

Positive tests:

crates/corvid-runtime/tests/executing_io_tools.rs::executing_io_tools_round_trip_through_runtime_dispatch

Adversarial tests:

crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_quarantines_io_writes
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_blocks_executing_io_write_tool_dispatch_from_escaping_to_filesystem

`io_source.fs_read_quarantine_on_replay`

class: runtime_checked
phase: runtime

A Substitute-mode replay runtime gates every executing file-read call (read_text / list_dir). The low-level IoRuntime::read_text path passes through transparently during replay (reads don't escape the process and the quarantine flag is write-only). The Runtime::call_tool dispatch path goes through replay-substitution first, so dispatch-path reads either substitute from the recorded trace OR diverge when no recorded event matches — they never reach the live filesystem unless the trace prescribed it.

Positive tests:

crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_passes_through_io_reads

Adversarial tests:

crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_blocks_executing_io_read_tool_dispatch_without_recorded_event

`io_source.http_ssrf_structural_block`

class: runtime_checked
phase: runtime

Every call to an executing HTTP tool (http_get / http_post_json, from std/http.cor) parses the request URL and refuses any host that lexically resolves to a private RFC1918 range (10.0.0.0/8, 172.16.0.0/12, 192.168.0.0/16), loopback (127.0.0.0/8 + ::1), link-local (169.254.0.0/16 + fe80::/10), unspecified (0.0.0.0/8 + ::), ULA (fc00::/7), or the localhost DNS alias. The block is a STRUCTURAL property of the language: it runs regardless of [http] allow contents — even a fully-misconfigured allowlist containing 127.0.0.1 cannot bypass it. This is the security floor underneath the configurable allowlist. At the language surface the refusal is an honest Err value (the http tools return Result), so programs observe the diagnostic without the floor weakening.

Positive tests:

crates/corvid-runtime/src/http.rs::http_egress_policy_allowlist_permits_matching_host

Adversarial tests:

crates/corvid-runtime/src/http.rs::http_egress_policy_ssrf_block_refuses_all_private_loopback_ipv4_ranges
crates/corvid-runtime/src/http.rs::http_egress_policy_ssrf_block_refuses_ipv6_loopback_and_link_local
crates/corvid-runtime/src/http.rs::http_egress_policy_ssrf_block_refuses_localhost_dns_alias
crates/corvid-driver/tests/executing_http_through_driver.rs::ssrf_block_rejects_loopback_url_even_when_allowlist_contains_it

`io_source.http_allowlist_enforcement`

class: runtime_checked
phase: runtime

Every call to an executing HTTP tool checks the request URL's host against the project's configured [http] allow = [...] list (or the CORVID_HTTP_ALLOW env override). Case-insensitive exact-host comparison. When no allowlist is configured (missing [http] section, empty allow, or unset env), every call fails closed with a structured diagnostic naming the requested URL, the missing config, and the env-override pathway. This is the configurable layer on top of the always-on SSRF block. At the language surface the refusal is an honest Err value (the http tools return Result), so programs observe the diagnostic without the gate weakening.

Positive tests:

crates/corvid-runtime/src/http.rs::http_egress_policy_allowlist_permits_matching_host
crates/corvid-driver/src/run.rs::corvid_toml_with_http_allow_produces_configured_policy
crates/corvid-driver/src/run.rs::env_var_overrides_corvid_toml_http_allow
crates/corvid-driver/tests/executing_http_through_driver.rs::real_corvid_program_performs_get_through_executing_http_dispatch

Adversarial tests:

crates/corvid-runtime/src/http.rs::http_egress_policy_unconfigured_fails_closed_on_check
crates/corvid-runtime/src/http.rs::http_egress_policy_empty_allow_list_is_unconfigured
crates/corvid-runtime/src/http.rs::http_egress_policy_allowlist_refuses_unlisted_host_with_clear_diagnostic
crates/corvid-driver/src/run.rs::corvid_toml_with_empty_http_allow_produces_unconfigured_policy
crates/corvid-driver/src/run.rs::corvid_toml_without_http_section_produces_unconfigured_policy
crates/corvid-driver/tests/executing_http_through_driver.rs::missing_http_allowlist_fails_closed_with_actionable_diagnostic

`io_source.sqlite_parameter_binding_only`

class: runtime_checked
phase: runtime

Every parameter passed to db_query / db_execute (executing SQLite tools from std/db.cor) flows through rusqlite::params_from_iter over the typed DbValue enum — there is no string-interpolation path on the dispatch. The typechecker's List<DbParam> signature forces every value through the typed constructors (db_param_int, db_param_text, db_param_float, db_param_bool, db_param_null); a literal "'; DROP TABLE users; --" placed in a db_param_text value survives as TEXT data and never reaches SQLite's parser. This is the load-bearing structural property: SQL injection is prevented by the language's type system + the runtime's binding path, not by escaping or sanitisation.

Positive tests:

crates/corvid-runtime/src/db.rs::db_handle_registry_round_trip_against_memory_database
crates/corvid-driver/tests/executing_sqlite_through_driver.rs::real_corvid_program_round_trips_data_through_executing_sqlite_dispatch

Adversarial tests:

crates/corvid-runtime/src/db.rs::db_param_text_with_sql_metacharacters_is_bound_as_data
crates/corvid-driver/tests/executing_sqlite_through_driver.rs::db_param_text_with_sql_metacharacters_survives_round_trip_through_real_corvid_program

`io_source.sqlite_write_quarantine_on_replay`

class: runtime_checked
phase: runtime

A Substitute-mode replay runtime refuses every executing db_execute call. The dispatch path goes through Runtime::db_execute_tool which delegates to DbHandleRegistry::execute; the registry's write-quarantine flag (flipped by RuntimeBuilder::build during replay) short-circuits with QuarantineViolation { surface: "db", .. } regardless of SQL contents — INSERTs, UPDATEs, DELETEs, and DDL all blocked. The database is provably untouched during replay.

Positive tests:

crates/corvid-runtime/src/db.rs::db_handle_registry_round_trip_against_memory_database

Adversarial tests:

crates/corvid-runtime/src/db.rs::db_handle_registry_quarantine_blocks_execute_with_db_surface_violation
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_blocks_executing_db_execute_dispatch_from_escaping_to_database

`io_source.sqlite_read_passthrough_on_replay`

class: runtime_checked
phase: runtime

A Substitute-mode replay runtime passes db_query calls through to the live DbHandleRegistry — SQLite reads don't escape the process so the write-quarantine flag is the floor for mutations only. A follow-up slice will add the trace-substitution upper gate (replay db_query against a recorded row event yields the recorded rows; a missing event diverges); 33S3d pins the dispatch-side read-passthrough property so a future refactor can't silently flip the policy and start blocking reads during replay.

Positive tests:

crates/corvid-runtime/src/db.rs::db_handle_registry_quarantine_does_not_block_query
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_does_not_block_executing_db_query_dispatch_during_write_quarantine

Adversarial tests:

crates/corvid-runtime/src/db.rs::db_handle_registry_quarantine_does_not_block_query

`io_source.http_quarantine_on_replay`

class: runtime_checked
phase: runtime

A Substitute-mode replay runtime refuses every executing HTTP call. POST calls through the Runtime::call_tool("http_post_json", ...) dispatch path go through the replay-substitution path first (so they substitute from the recorded trace OR diverge — they never reach the live network); the HttpClient::quarantine flag is the floor underneath that returns QuarantineViolation from any direct HttpClient::send call. GET calls through dispatch are also gated by the substitution path (read-quarantine equivalent — they substitute OR diverge, never reaching the live network).

Positive tests:

crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_quarantines_http_client_send

Adversarial tests:

crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_blocks_executing_http_post_tool_dispatch_from_escaping_to_network
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_blocks_executing_http_get_tool_dispatch_without_recorded_event

`json.parse_safety_no_panic`

class: runtime_checked
phase: runtime

Calling json_parse(text) against arbitrary bytes returns Result::Err(message) rather than panicking. The runtime's crate::json::parse routes through serde_json::from_str whose parse failure surfaces as a structured error description; the Result wraps the error in the standard Err(String) envelope so user code can pattern-match via ? propagation and route the diagnostic up to its caller. A Corvid program calling json_parse on malformed text cannot crash the runtime regardless of what bytes are in the input. The typed-decoder convention (decode_<X>_from_json) inherits this property — malformed input through the decoder dispatch path also returns Result::Err.

Positive tests:

crates/corvid-runtime/src/json.rs::parse_round_trips_a_typical_object
crates/corvid-driver/tests/executing_json_through_driver.rs::real_corvid_program_round_trips_data_through_opaque_json_dispatch

Adversarial tests:

crates/corvid-runtime/src/json.rs::malformed_json_returns_recoverable_error_never_panics
crates/corvid-driver/tests/executing_json_through_driver.rs::malformed_json_returns_result_err_through_real_corvid_program

`json.field_type_safety_at_access_boundary`

class: runtime_checked
phase: runtime

Each typed accessor on the executing JSON surface (json_get_int / json_get_float / json_get_string / json_get_bool / json_get_object / json_get_array) returns Result<T, String> where the Err branch fires on missing fields AND on type mismatches. json_get_int(value, field) against a string-valued field returns Err("field 'x' is not an Int") rather than coercing or panicking. The typed-decoder convention inherits the same property — shape mismatches (a JSON String where the user declared an Int) flow through json_to_value against the target struct and surface as Result::Err with a structured diagnostic.

Positive tests:

crates/corvid-runtime/src/json.rs::get_object_returns_subtree_for_further_typed_access
crates/corvid-driver/tests/executing_json_through_driver.rs::real_corvid_program_decodes_typed_struct_via_decode_x_from_json_convention

Adversarial tests:

crates/corvid-runtime/src/json.rs::typed_accessor_mismatch_returns_recoverable_error
crates/corvid-runtime/src/json.rs::missing_field_returns_recoverable_error_naming_the_field
crates/corvid-driver/tests/executing_json_through_driver.rs::typed_decoder_shape_mismatch_returns_result_err_through_real_corvid_program

`taint.untrusted_cannot_reach_dangerous`

class: static
phase: typecheck

Untrusted content — a value from a data: untrusted effect source (retrieved documents, user messages, untrusted MCP output) or the output of a prompt that consumed one — is typed Tainted<T> and cannot parameterize an approval-requiring call (a dangerous tool, or one whose trust tier is supervisor_required/human_required). Taint is never assignable to T and is unwrapped only by the explicit, greppable trusted(expr) boundary. This makes prompt injection (OWASP LLM #1) a compile error: attacker-influenced data cannot reach a consequential action without a human-reviewed sanitization point.

Positive tests:

crates/corvid-types/src/tests.rs::trusted_boundary_unwraps_taint_to_reach_dangerous

Adversarial tests:

crates/corvid-types/src/tests.rs::tainted_prompt_output_cannot_reach_dangerous_tool

Grounded provenance

`grounded.provenance_required`

class: static
phase: typecheck

Constructing a Grounded<T> value requires citing a source; unsourced Grounded construction is a compile error.

Positive tests:

crates/corvid-types/src/tests.rs::mutation_direct_grounded_return_with_retrieval_chain_is_ok
crates/corvid-types/src/tests.rs::grounded_connector_tool_return_is_wrapped_and_flows

Adversarial tests:

crates/corvid-types/src/tests.rs::mutation_grounded_return_without_retrieval_errors
crates/corvid-types/src/tests.rs::grounded_connector_return_strip_is_the_tracked_legacy_coercion

`grounded.propagation_across_calls`

class: out_of_scope
phase: typecheck

Provenance is preserved across function boundaries — a Grounded<T> returned from a callee retains its citation chain into the caller without separate annotation.

Why out of scope: Subsumed by grounded.provenance_required at the diagnostic level. The shipped grounded-return analysis fires a single UngroundedReturn diagnostic when a function declares a Grounded<T> return type but the returned expression's provenance chain is empty. The check is unified: it does not distinguish whether the missing provenance came from a directly-constructed value (parent's framing: provenance must be cited at construction) or from a value flowed across a callee boundary (this row's framing: provenance must be preserved across calls). The user's mitigation is the same in both cases: ensure the returned value carries a non-empty provenance chain. Phase 35V-T1-B (2026-05-08) downgraded this row from Static to OutOfScope because the analyzer fires one diagnostic for both perspectives; there is no discriminable site to tag separately. The property is documentary; the enforcement is via the parent's unified diagnostic. A future slice that splits the analyzer to distinguish construction-site failures from call-boundary propagation failures would promote this row back to Static.

`grounded.no_laundering`

class: static
phase: typecheck

An agent annotated @grounded_pure fails compile if its body launders a Grounded<T> value into a non-grounded slot — either via the silent legacy coercion at a slot-check site (return / parameter / field), an explicit .unwrap_discarding_sources() call, or a transitive call into another agent not itself marked @grounded_pure. The moat composes through the call graph the same way @deterministic does.

Positive tests:

crates/corvid-types/src/tests.rs::grounded_pure_passes_when_body_preserves_grounded
crates/corvid-types/src/tests.rs::grounded_pure_passes_when_calling_another_grounded_pure_agent

Adversarial tests:

crates/corvid-types/src/tests.rs::grounded_pure_rejects_implicit_coercion
crates/corvid-types/src/tests.rs::grounded_pure_rejects_explicit_unwrap
crates/corvid-types/src/tests.rs::grounded_pure_rejects_call_to_non_grounded_pure_agent

Budgets

`budget.compile_time_ceiling`

class: static
phase: typecheck

An agent annotated @budget($X) fails compile if the sum of statically known per-call costs along any reachable path exceeds $X.

Positive tests:

crates/corvid-types/src/tests.rs::multi_dimensional_budget_within_bound_is_clean
crates/corvid-types/src/tests.rs::mutation_budget_within_limit_is_ok

Adversarial tests:

crates/corvid-types/src/tests.rs::multi_dimensional_budget_violation_reports_path
crates/corvid-types/src/tests.rs::mutation_budget_exceeded_is_effect_violation

`budget.runtime_termination`

class: out_of_scope
phase: runtime

Live runtime termination of an agent when actual runtime cost crosses the @budget($X) threshold mid-execution.

Why out of scope: Today Corvid enforces budgets at compile time via budget.compile_time_ceiling, and the runtime observes per-call cost in trace events; live mid-execution termination on threshold crossing is not yet implemented. A future slice can promote this entry back to RuntimeChecked once the enforcement ships. The compile-time ceiling is the load-bearing guarantee for v1.0.

Confidence thresholds

`confidence.min_threshold`

class: static
phase: typecheck

An agent annotated @min_confidence(X) requires every input carrying a confidence tag to meet X; lower-confidence inputs are rejected at the call site.

Positive tests:

crates/corvid-types/src/tests.rs::min_confidence_passes_when_composed_confidence_meets_floor
crates/corvid-types/src/tests.rs::tagged_invalid_confidence_carries_confidence_guarantee_id

Adversarial tests:

crates/corvid-types/src/tests.rs::min_confidence_fires_when_composed_confidence_below_floor
crates/corvid-types/src/tests.rs::effect_confidence_out_of_range_is_rejected

Trust constraints

`trust.constraint_enforcement`

class: static
phase: typecheck

An agent annotated @trust(<level>) (or @trust(autonomous_if_confident(threshold))) fails compile when the agent's body composes a trust dimension stricter than the declared ceiling — e.g. an @trust(autonomous) agent that reaches a trust: human_required tool without an approve boundary is rejected. The lattice is autonomous < supervisor_required < human_required; the confidence-gated variant treats autonomous_if_confident(t) as autonomous at typecheck and routes to human_required at runtime when composed confidence < t. Added 2026-06-05 under slice 33Q3 so @trust annotations participate in corvid build --sign's claim coverage and surface in claim --explain output.

Positive tests:

crates/corvid-types/src/tests.rs::mutation_budget_within_limit_is_ok
crates/corvid-driver/src/build/tests.rs::signed_claim_coverage_accepts_trust_constrained_agent

Adversarial tests:

crates/corvid-types/src/tests.rs::mutation_baseline_trust_violation_exists
crates/corvid-driver/src/build/tests.rs::signed_claim_coverage_rejects_trust_when_id_missing_from_descriptor

Replay determinism

`replay.deterministic_pure_path`

class: runtime_checked
phase: runtime

A trace recorded from a @replayable agent reproduces deterministically across corvid replay invocations on the same compiled binary; non-deterministic divergence raises the documented replay-divergence error.

Positive tests:

crates/corvid-types/src/tests.rs::replayable_agent_with_pure_body_compiles_clean
crates/corvid-types/src/tests.rs::deterministic_agent_with_pure_body_compiles_clean

Adversarial tests:

crates/corvid-types/src/tests.rs::deterministic_agent_calling_tool_is_rejected
crates/corvid-types/src/tests.rs::deterministic_agent_calling_prompt_is_rejected

`replay.trace_signature`

class: runtime_checked
phase: runtime

Trace receipts produced with --sign carry a DSSE envelope whose signature corvid receipt verify checks against the supplied verifying key.

Positive tests:

crates/corvid-cli/tests/receipt_signing.rs::sign_then_verify_roundtrips_end_to_end

Adversarial tests:

crates/corvid-cli/tests/receipt_signing.rs::verify_rejects_envelope_signed_with_different_key
crates/corvid-cli/tests/receipt_signing.rs::verify_rejects_tampered_payload

Provenance traces

`provenance_trace.receipt_signature`

class: runtime_checked
phase: runtime

corvid receipt verify rejects any DSSE-wrapped receipt whose signature does not validate against the supplied verifying key, with a non-zero exit and the documented verification failed message.

Positive tests:

crates/corvid-cli/tests/receipt_signing.rs::sign_then_verify_roundtrips_end_to_end

Adversarial tests:

crates/corvid-cli/tests/receipt_signing.rs::verify_rejects_envelope_signed_with_different_key
crates/corvid-cli/tests/receipt_signing.rs::verify_rejects_tampered_payload

ABI descriptor

`abi_descriptor.cdylib_emission`

class: static
phase: codegen

Every corvid build --target=cdylib output exports a CORVID_ABI_DESCRIPTOR symbol whose payload is the canonical effect/approval/provenance surface for the compiled program.

Positive tests:

crates/corvid-codegen-cl/tests/cdylib_emission.rs::cdylib_target_produces_shared_library_file
crates/corvid-codegen-cl/tests/cdylib_emission.rs::cdylib_symbol_is_resolvable_via_dlopen

Adversarial tests:

crates/corvid-cli/tests/build_cdylib.rs::cli_build_cdylib_fails_cleanly_on_non_scalar_signature

`abi_descriptor.byte_determinism`

class: static
phase: codegen

Two byte-identical Corvid sources compiled with the same toolchain version produce byte-identical descriptor JSON; the descriptor is canonical, not pretty-printed.

Positive tests:

crates/corvid-abi/tests/determinism.rs::identical_source_produces_byte_identical_descriptor_modulo_generated_at
crates/corvid-abi/tests/byte_fuzz_corpus.rs::descriptor_bytes_are_byte_identical_across_two_emissions_of_same_source

Adversarial tests:

crates/corvid-abi/tests/byte_fuzz_corpus.rs::descriptor_section_rejects_random_byte_flips

`abi_descriptor.bilateral_source_match`

class: runtime_checked
phase: abi_verify

corvid-abi-verify --source <file> <cdylib> independently rebuilds the ABI descriptor from source and byte-compares it against the embedded CORVID_ABI_DESCRIPTOR symbol; mismatch is rejected before host acceptance.

Positive tests:

crates/corvid-abi-verify/src/lib.rs::verifier_accepts_matching_cdylib_descriptor
crates/corvid-abi-verify/src/lib.rs::verifier_accepts_matching_cdylib_with_imported_agent

Adversarial tests:

crates/corvid-abi-verify/src/lib.rs::verifier_rejects_source_descriptor_mismatch

ABI attestation

`abi_attestation.envelope_signature`

class: runtime_checked
phase: abi_verify

corvid receipt verify-abi rejects a signed cdylib whose attestation envelope does not validate against the supplied verifying key, exiting 1 with attestation verification failed.

Positive tests:

crates/corvid-cli/tests/abi_attestation.rs::signed_cdylib_verifies_against_matching_key
crates/corvid-abi/tests/byte_fuzz_corpus.rs::signing_key_round_trip_baseline

Adversarial tests:

crates/corvid-cli/tests/abi_attestation.rs::signed_cdylib_rejects_wrong_key
crates/corvid-abi/tests/byte_fuzz_corpus.rs::dsse_envelope_signature_tampering_is_rejected
crates/corvid-abi/tests/byte_fuzz_corpus.rs::dsse_envelope_payload_tampering_is_rejected
crates/corvid-abi/tests/byte_fuzz_corpus.rs::dsse_envelope_payload_type_swap_is_rejected
crates/corvid-abi/tests/byte_fuzz_corpus.rs::attestation_section_rejects_every_magic_or_version_byte_flip
crates/corvid-abi/tests/byte_fuzz_corpus.rs::attestation_section_body_mutations_break_signature_verification

`abi_attestation.descriptor_match`

class: runtime_checked
phase: abi_verify

After signature validation, the recovered attestation payload must bit-match the embedded CORVID_ABI_DESCRIPTOR; mismatch is rejected even when the signature is valid.

Positive tests:

crates/corvid-cli/tests/abi_attestation.rs::signed_cdylib_verifies_against_matching_key

Adversarial tests:

crates/corvid-cli/tests/abi_attestation.rs::signed_cdylib_rejects_wrong_key

`abi_attestation.absent_reports_unsigned`

class: runtime_checked
phase: abi_verify

corvid receipt verify-abi on a cdylib lacking the CORVID_ABI_ATTESTATION symbol exits 2 with the documented unsigned message, leaving the host policy to decide whether to accept it.

Positive tests:

crates/corvid-cli/tests/abi_attestation.rs::signed_cdylib_verifies_against_matching_key

Adversarial tests:

crates/corvid-cli/tests/abi_attestation.rs::unsigned_cdylib_reports_absent_attestation

`abi_attestation.sign_requires_claim_coverage`

class: static
phase: codegen

corvid build --target=cdylib --sign refuses to sign when any contract declared by the source lacks a non-out-of-scope guarantee id in the descriptor's signed claim set.

Positive tests:

crates/corvid-driver/src/build/tests.rs::signed_claim_coverage_accepts_registered_contracts

Adversarial tests:

crates/corvid-driver/src/build/tests.rs::signed_claim_coverage_rejects_missing_declared_contract_id
crates/corvid-driver/src/build/tests.rs::signed_claim_coverage_rejects_out_of_scope_contract_id

Durable jobs

`jobs.cron_schedule_durable`

class: runtime_checked
phase: runtime

A schedule "cron" zone "…" -> job(args) declaration persists to the durable queue store and survives process restart. Slice 35-N walks Decl::Schedule so a signed cdylib that declares a cron schedule cannot ship without this guarantee in its descriptor.

Positive tests:

crates/corvid-driver/src/build/tests.rs::signed_claim_coverage_walks_schedule_decl

Adversarial tests:

crates/corvid-driver/src/build/tests.rs::signed_claim_coverage_rejects_schedule_without_jobs_coverage

`jobs.retry_budget_bound`

class: out_of_scope
phase: runtime

@retry(max_attempts: N, backoff: ...) bounds the runtime retry envelope of a job so a transient failure cannot escalate into unbounded re-spend.

Why out of scope: The runtime queue and lease envelopes are shipped and the retry policy is configurable at enqueue time via the host API + corvid jobs limit. @retry as a Corvid source-level attribute is filed as a post-v1.0 ergonomic improvement (35V2-P38-H), not a launch-blocker — the runtime behaviour the attribute would surface is already shipped. Slice 38K promoted the runtime; the syntactic promotion of this row tracks with the post-v1.0 syntax slice.

`jobs.idempotency_key_uniqueness`

class: runtime_checked
phase: runtime

Across N concurrent workers, exactly one durable queue row exists for a given non-null idempotency key. Enforced by a partial UNIQUE INDEX on queue_jobs(idempotency_key) WHERE idempotency_key IS NOT NULL in the SQLite schema, plus the existing enqueue_typed_idempotent collision-fallback path that returns the surviving row when the insert hits the UNIQUE constraint.

Positive tests:

crates/corvid-runtime/src/queue/tests/durable_basics.rs::durable_queue_idempotency_key_collapses_duplicate_jobs

Adversarial tests:

crates/corvid-runtime/tests/durability_corpus.rs::t38l_d1_four_workers_collapse_to_one_row

`jobs.lease_exclusivity`

class: runtime_checked
phase: runtime

A job lease prevents two workers from running the same job concurrently. Slice 38K's WorkerPool over DurableQueueRuntime runs N tokio tasks each contesting lease_next_at; the SQLite UPDATE that flips pending → leased is atomic, so exactly one worker wins each contention round. Lease expiry plus a fresh worker re-leasing is shipped (slice 38L's D3 test); heartbeat extension for long-running steps remains a follow-up.

Positive tests:

crates/corvid-runtime/src/worker_pool.rs::t38k_pool_runs_each_job_exactly_once

Adversarial tests:

crates/corvid-runtime/src/worker_pool.rs::t38k_two_workers_cannot_both_lease_same_job
crates/corvid-runtime/src/worker_pool.rs::t38k_pool_drains_gracefully_without_claiming_new_work

`jobs.durable_resume`

class: runtime_checked
phase: runtime

A worker that drops uncleanly mid-step (the SIGKILL surrogate the queue runtime is responsible for) leaves behind durable checkpoint rows; a fresh worker that opens the same SQLite file after the lease TTL elapses can re-lease the job and resume from those checkpoints. SQLite WAL fsync makes this property structural. The count-bounded no double LLM call extension joins the Phase 21 Replay corpus when step-skip semantics land at the VM layer.

Positive tests:

crates/corvid-runtime/src/queue/tests/checkpoints.rs::durable_queue_records_ordered_agent_checkpoints

Adversarial tests:

crates/corvid-runtime/tests/durability_corpus.rs::t38l_d3_checkpoints_survive_unclean_shutdown

`jobs.cron_dst_correct`

class: runtime_checked
phase: runtime

Cron schedules expressed in America/New_York (and other DST-observing timezones) produce monotonic UTC fire times across the spring-forward and fall-back transitions, with no duplicates and no fire at the non-existent local instant. chrono-tz is wired into the queue runtime; the cron-crate's Schedule::after iterator is timezone-aware.

Positive tests:

crates/corvid-runtime/tests/durability_corpus.rs::t38l_d2_dst_spring_forward_is_deterministic

Adversarial tests:

crates/corvid-runtime/tests/durability_corpus.rs::t38l_d2_dst_fall_back_is_monotonic

`jobs.approval_wait_resume`

class: out_of_scope
phase: runtime

An approval boundary inside a job pauses the run until an approval token arrives, expires, or is denied; the resume path writes the audit transition.

Why out of scope: Runtime approval-wait state ships and is reachable via corvid jobs wait-approval + corvid jobs approval approve/deny (the shipped surface). await_approval as a Corvid source-level keyword is filed as a post-v1.0 ergonomic improvement (35V2-P38-H), not a launch-blocker — the runtime behaviour already ships, the syntax just surfaces it more compactly.

`jobs.loop_bounds_enforced`

class: runtime_checked
phase: runtime

Agent loops driven by jobs honor max-steps, max-wall-time, max-spend, and max-tool-calls; exceeding any bound moves the job to loop_budget_exceeded and writes a loop_bound_exceeded audit event listing the violated bounds. Post-termination record_loop_usage calls are refused so a stale worker cannot silently keep charging spend / steps against a terminal job.

Positive tests:

crates/corvid-runtime/src/queue/tests/loops.rs::durable_queue_enforces_loop_budget_limits_with_audit

Adversarial tests:

crates/corvid-runtime/src/queue/tests/loops.rs::durable_queue_refuses_loop_usage_after_budget_exceeded_termination

`jobs.explain_sources_grounded`

class: runtime_checked
phase: runtime

corvid jobs explain <job_id> renders a typed operational summary whose sources array names every audit-event id the explanation consulted — the Grounded shape at the JSON layer. Every transition surfaced in the explanation has a back-reference in sources, so an operator can audit-trail every claim back to a queue row. A missing job id is refused with an explicit diagnostic rather than served as an empty report.

Positive tests:

crates/corvid-cli/src/jobs_explain_cmd.rs::jobs_explain_denied_approval_carries_grounded_sources

Adversarial tests:

crates/corvid-cli/src/jobs_explain_cmd.rs::jobs_explain_unknown_job_refuses

`jobs.replayable_side_effects`

class: runtime_checked
phase: runtime

A job marked @replayable records a per-job JSONL trace (slice C-2) at <trace_dir>/<job_id>.jsonl, and a later corvid jobs replay --source <path>.cor --job <job_id> (slice C-3) drives the same agent body against a runtime in RuntimeMode::Replay(source) with every side-effect surface quarantined — LLM adapters wrap into QuarantinedLlmAdapter (slice C-4); HTTP / store writes / file writes refuse with typed QuarantineViolation (slice C-5). The recorded substitution path consumes recorded LlmCall / LlmResult events for matched dispatch; any call that bypasses substitution and reaches the manager layer fails closed. The durable queue uses raw rusqlite and trace emission uses JsonlTraceWriter, so neither routes through the quarantined manager types.

Positive tests:

crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_passes_through_store_reads
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_passes_through_io_reads
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::live_mode_does_not_quarantine_any_surface
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::differential_replay_does_not_quarantine_llm_registry

Adversarial tests:

crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_quarantines_llm_registry_direct_calls
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_quarantines_http_client_send
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_quarantines_store_writes
crates/corvid-runtime/tests/replay_quarantine_corpus.rs::replay_quarantines_io_writes

Auth and approvals

`auth.session_rotation_on_privilege_change`

class: runtime_checked
phase: runtime

A session id rotates on a named privilege-change event (role upgrade, password change, MFA enrolment, admin elevation) so a stolen pre-escalation cookie cannot exercise the post-escalation privilege. The rotation is recorded in the auth-audit trail with the typed PrivilegeChangeReason as evidence; the pre-elevation cookie is rejected from that point on. Catches the session-fixation adversarial-corpus threat.

Positive tests:

crates/corvid-runtime/src/auth/sessions.rs::session_rotation_on_privilege_change_rejects_pre_elevation_session_fixation_attempt

Adversarial tests:

crates/corvid-runtime/src/auth/sessions.rs::session_rotation_on_privilege_change_refuses_empty_trace_id

`auth.api_key_at_rest_hashed`

class: runtime_checked
phase: runtime

API keys are stored only as Argon2id hashes; the plaintext leaves Corvid memory exactly once at issuance and is never logged. Verified by the existing hash_api_key_secret/verify_api_key_secret path in corvid-runtime/src/auth.rs.

Positive tests:

crates/corvid-runtime/src/auth/api_keys.rs::api_key_runtime_resolves_service_actor_with_argon2_hash_and_redacted_audit

Adversarial tests:

crates/corvid-runtime/src/auth/api_keys.rs::api_key_runtime_rejects_wrong_tenant_revoked_expired_and_user_actors

`auth.api_key_scope_subset_check`

class: runtime_checked
phase: runtime

An API key's granted scope is a structured set of <resource>.<action> permissions, not an opaque hash. enforce_scope_grant(granted, required) refuses the call when the required set is not a subset of the granted set, and the typed error names every missing permission so the audit trail records exactly which scope was attempted. Catches the scope-escalation adversarial-corpus threat: a key issued with {orders.read} cannot satisfy a required {refunds.write} action. Canonical fingerprint over the sorted set is stable across permission-insertion order so the value can be persisted alongside ApiKeyRecord::scope_fingerprint without re-computing the source set. Wiring the enforcement into every route is downstream work; this row commits the typed model + the predicate.

Positive tests:

crates/corvid-runtime/src/auth/scope.rs::scope_with_subset_satisfies_required_grant

Adversarial tests:

crates/corvid-runtime/src/auth/scope.rs::scope_escalation_attempt_refused_with_specific_missing_permission
crates/corvid-runtime/src/auth/scope.rs::scope_escalation_lists_every_missing_permission_not_just_the_first
crates/corvid-runtime/src/auth/scope.rs::empty_granted_scope_refuses_any_non_empty_required

`auth.jwt_kid_rotation`

class: runtime_checked
phase: runtime

JWT verification fetches the JWKS, picks the key by kid, verifies the signature with jsonwebtoken, and rejects tokens whose kid is missing from the current JWKS, whose alg does not match the contract, whose signature fails to verify, whose exp/iss/aud do not align with the contract, or whose required subject/tenant claim is missing. Out-of-scope at Phase 39 base; promoted to RuntimeChecked by slice 39K when corvid-runtime/src/jwt_verify/ shipped.

Positive tests:

crates/corvid-runtime/src/jwt_verify/verifier.rs::parse_alg_accepts_supported_and_refuses_others
crates/corvid-runtime/src/jwt_verify/verifier.rs::decoding_key_for_rsa_jwk_constructs
crates/corvid-runtime/src/jwt_verify/mod.rs::error_slugs_are_stable_for_audit_log

Adversarial tests:

crates/corvid-runtime/src/jwt_verify/verifier.rs::kid_downgrade_returns_kid_not_found
crates/corvid-runtime/src/jwt_verify/verifier.rs::header_alg_must_match_contract_alg
crates/corvid-runtime/src/jwt_verify/verifier.rs::alg_none_in_header_is_refused
crates/corvid-runtime/src/jwt_verify/verifier.rs::malformed_token_is_refused_before_fetch
crates/corvid-runtime/src/jwt_verify/verifier.rs::jwks_fetch_failure_is_surfaced
crates/corvid-runtime/src/jwt_verify/verifier.rs::decoding_key_for_rejects_rsa_without_n
crates/corvid-runtime/src/jwt_verify/verifier.rs::decoding_key_for_rejects_unknown_kty

`auth.oauth_pkce_required`

class: runtime_checked
phase: runtime

OAuth callback state requires PKCE for public clients; the state record carries the code-verifier hash and is single-use, tenant-scoped, and expiry-bound.

Positive tests:

crates/corvid-runtime/src/auth/oauth.rs::oauth_callback_state_is_hashed_single_use_and_restart_safe

Adversarial tests:

crates/corvid-runtime/src/auth/oauth.rs::oauth_callback_rejects_expired_and_cross_tenant_state

`auth.csrf_double_submit`

class: runtime_checked
phase: runtime

CSRF protection on cookie-bearing state-changing requests (POST / PUT / PATCH / DELETE) uses a double-submit token of shape <binding>.<hex_hmac> where hex_hmac is HMAC-SHA256(server_secret, "corvid-csrf-v1:" || binding). The verifier enforces three independent checks: header and cookie both present, equal under constant-time comparison (the double-submit invariant — a cross-site request cannot read the cookie), and the HMAC component verifies against the server secret (so a forged token without the secret is rejected). Safe methods (GET / HEAD / OPTIONS) skip the check; unknown methods fail closed. An empty server secret also fails closed on state-changing requests. The rendered axum server wires the verifier into its middleware when CORVID_CSRF_SECRET is set; the canonical implementation lives in corvid-runtime::auth::csrf with 8 exhaustive unit tests, and the rendered-server end-to-end test asserts the wire behaviour matches.

Positive tests:

crates/corvid-runtime/src/auth/csrf.rs::mint_and_verify_round_trip_on_each_state_changing_method
crates/corvid-cli/tests/build_server.rs::rendered_server_csrf_middleware_refuses_state_change_without_double_submit_token

Adversarial tests:

crates/corvid-runtime/src/auth/csrf.rs::csrf_bypass_attempt_without_header_refused_on_put_patch_delete
crates/corvid-runtime/src/auth/csrf.rs::csrf_token_forged_without_server_secret_refused_on_hmac
crates/corvid-runtime/src/auth/csrf.rs::csrf_header_and_cookie_must_match_constant_time
crates/corvid-runtime/src/auth/csrf.rs::csrf_empty_server_secret_fails_closed_on_state_changing_methods

`tenant.cross_tenant_compile_error`

class: out_of_scope
phase: typecheck

A function whose actor came from tenant A may not pass a record owned by tenant B to a tool that writes back into A — the typechecker rejects the cross-tenant reference.

Why out of scope: Tenant tagging exists in runtime envelopes + the CLI (corvid approvals honours tenant scoping; the approval_bypass_rejects_tenant_crossing_actor test pins the runtime half). The parser-level tenant Org { ... } block + the typechecker reachability that would refuse a cross-tenant value at compile time does not exist yet. Filed as post-v1.0 35V2-P39-I-post-v1.0-auth-syntax-sugar — the runtime behaviour ships today, the syntactic promotion of this row tracks with the post-v1.0 parser surface slice.

`approval.policy_clause_static_check`

class: out_of_scope
phase: typecheck

An approval Name: block's policy { ... } clause type-checks at compile time so a malformed predicate (wrong field name, wrong type, undeclared role) cannot ship.

Why out of scope: Approval store + queue API ship and are reachable via corvid approvals queue/inspect/approve/deny. The approval Name: parser-level block is post-v1.0 ergonomic surface — filed as 35V2-P39-I-post-v1.0-auth-syntax-sugar. The runtime behaviour (typed approval contracts with required fields validated at issue time) ships today via the host API; the source-level policy { ... } clause is the sugar.

`approval.batch_equivalence_typed`

class: out_of_scope
phase: typecheck

An approval ... batch_with: same_tool, same_data_class, same_role clause groups equivalent approvals so a reviewer can approve one record and have N equivalent-by-typed-shape records auto-resolve.

Why out of scope: The runtime half of the batch-equivalence guarantee ships today as approval.batch_refuses_cross_data_class_drift (RuntimeChecked): corvid approvals batch refuses to span >1 data class unless --require-data-class pins the batch. The typecheck-time batch_with: same_tool, same_data_class, same_role source-level clause is post-v1.0 ergonomic surface — filed as 35V2-P39-I-post-v1.0-auth-syntax-sugar. The runtime check prevents the threat today; the source-level sugar lets contracts declare the batch shape directly.

`approval.batch_refuses_cross_data_class_drift`

class: runtime_checked
phase: runtime

corvid approvals batch refuses outright when the supplied ids span >1 data_class unless the operator pins the batch with --require-data-class <CLASS>. Catches the batch-approval-drift-across-data-classes threat where financial and pii records would otherwise resolve in the same invocation under a single reviewer's role check.

Positive tests:

crates/corvid-cli/src/approvals_cmd/interaction.rs::approvals_batch_require_data_class_pins_to_one_class

Adversarial tests:

crates/corvid-cli/src/approvals_cmd/interaction.rs::approvals_batch_refuses_cross_data_class_drift_without_pin

`approval.explain_sources_grounded`

class: runtime_checked
phase: runtime

corvid approvals explain <id> renders a typed reviewer summary whose sources array names every audit-event id the explanation consulted — the Grounded shape at the JSON layer. Every transition surfaced in the explanation has a back-reference in sources, so a reviewer can audit-trail every claim back to a queue row. Cross-tenant requests are refused with an explicit diagnostic rather than silently leaking state.

Positive tests:

crates/corvid-cli/src/approvals_cmd/explain.rs::approvals_explain_pending_carries_grounded_sources

Adversarial tests:

crates/corvid-cli/src/approvals_cmd/explain.rs::approvals_explain_cross_tenant_refused

`approval.confused_deputy_typecheck`

class: out_of_scope
phase: typecheck

A reachable path from any route or job to a @dangerous tool must have an approve token whose required_role covers every reachable caller — otherwise typecheck rejects.

Why out of scope: Lexical-scope approve-presence check ships (approval.dangerous_call_requires_token + approval.token_lexical_only). The role-coverage extension needs a typechecker pass that walks the call graph from every route / job entry point AND a source-level role-declaration syntax for the pass to reason over. Recon under slice 35V2-P39-J-LR-role-coverage-reachability found the role syntax does not exist in the AST today (AgentAttribute variants today are Replayable, Deterministic, Wrapping, GroundedPure — no @requires(role) or @approval(role) variant). The required source-level surface is filed at post-v1.0 35V2-P39-I-post-v1.0-auth-syntax-sugar (the auth / tenant / role / permission / approval Name: / @requires / @approval keyword set). The role-coverage typechecker pass therefore moves to post-v1.0 too, blocked on the same syntax dependency. The runtime half of the confused-deputy threat — approve-presence check + role-fingerprint match at request time — already ships (test: approval_bypass_rejects_confused_deputy_self_approval in crates/corvid-runtime/src/approval_queue.rs).

Connectors

`connector.scope_minimum_enforced`

class: runtime_checked
phase: runtime

A connector cannot use a scope its manifest does not declare and an actor cannot use a scope its auth state does not authorise. The runtime fires ConnectorAuthError::MissingScope (or UnknownScope) before any HTTP layer touches the network, so a leaked low-scope token cannot escalate to a higher-scope operation by guessing the scope id.

Positive tests:

crates/corvid-connector-runtime/src/runtime.rs::mock_mode_checks_auth_rate_limit_and_emits_trace

Adversarial tests:

crates/corvid-connector-runtime/tests/threat_corpus.rs::t1_github_rejects_unauthorised_scope
crates/corvid-connector-runtime/tests/threat_corpus.rs::t1_gmail_rejects_unauthorised_scope
crates/corvid-connector-runtime/tests/threat_corpus.rs::t1_slack_rejects_unauthorised_scope

`connector.write_requires_approval`

class: out_of_scope
phase: typecheck

A connector method whose effect set names a write (gmail.send, slack.post, github.create_issue) reaches typecheck only when its caller has a matching approve boundary in lexical scope.

Why out of scope: Manifest declares write effects (*.write, send_*) in shipped_manifests and the runtime refuses unsafe effects via ConnectorRuntimeError::ReplayWriteQuarantined when not authorized. The source-level connector ... uses dangerous declaration that would let typecheck refuse a call without a lexical-scope approve does not exist yet — connectors are configured by Rust data, not Corvid source. Filed as post-v1.0 35V2-P41-I-post-v1.0-connector-syntax-sugar — the runtime behaviour (manifest enforcement at write time) ships today; the typecheck-time form is the syntax sugar that promotes this row to Static.

`connector.rate_limit_respects_provider`

class: runtime_checked
phase: runtime

A connector honors the provider's rate-limit advice (Retry-After, 429, 5xx). The shared ReqwestRealClient parses RFC 7231 Retry-After integer-seconds into milliseconds via parse_retry_after_header and surfaces it as ConnectorRuntimeError::RateLimited { retry_after_ms }, which the runtime forwards verbatim to the caller instead of retrying behind their back.

Positive tests:

crates/corvid-connector-runtime/src/real_client.rs::parse_retry_after_seconds_form

Adversarial tests:

crates/corvid-connector-runtime/src/real_client.rs::parse_retry_after_returns_none_for_malformed
crates/corvid-connector-runtime/src/runtime.rs::real_mode_propagates_rate_limited_from_bound_client
crates/corvid-connector-runtime/tests/threat_corpus.rs::t5_rate_limited_propagates_retry_after_ms

`connector.contract_drift_detected`

class: runtime_checked
phase: runtime

corvid connectors check --baseline <file> --observed <file> runs a schema-agnostic structural drift detector over two JSON payloads and exits non-zero when any field is added, removed, or type-changed between the baseline and the observed response. The detector reports each drift site as a sorted JSON path so the output is deterministic and diff-friendly in CI. The canonical detector ships in corvid_connector_runtime::contract_drift (9 unit tests, schema-agnostic so adopting it does not require a manifest schema change). The CLI wires it via the file-input flow — capture the provider response separately in CI and pipe it through the command. The live-HTTP fetch path that would compute observed from a real provider call stays operational scope at 35V2-P41-E-LR-live-provider-ci-matrix (provider credentials live in CI secrets, not local config).

Positive tests:

crates/corvid-connector-runtime/src/contract_drift.rs::identical_shapes_produce_empty_drift_report
crates/corvid-cli/src/connectors_cmd/check.rs::contract_drift_identical_files_report_no_drift

Adversarial tests:

crates/corvid-connector-runtime/src/contract_drift.rs::provider_removed_field_appears_in_removed_paths_central_threat
crates/corvid-connector-runtime/src/contract_drift.rs::provider_type_change_appears_in_type_changed_paths
crates/corvid-cli/src/connectors_cmd/check.rs::contract_drift_removed_field_surfaces_with_non_empty_report
crates/corvid-cli/src/connectors_cmd/check.rs::contract_drift_malformed_baseline_file_surfaces_typed_error

`connector.drift_narration_grounded`

class: runtime_checked
phase: runtime

corvid connectors check --baseline <file> --observed <file> --narrate pairs every site in the structural drift report with a typed DriftNarration carrying a one-line consequence (e.g. "connector code that consumed this field is now broken at deserialization"), a typed severity (breaking for removed/type-changed sites, compatible for added sites), and a Grounded sources array that back-references the detector bucket + path the narration summarised. The order is breaking-first so an operator triaging CI output reads the most consequential items first. Deterministic + LLM-free; the slice's "RAG-grounded" framing refers to the evidence-citation property, not to a live LLM round-trip. The first sub-slice of 35V2-P41-H-LR-connectors-ai-helpers to ship; mock-fixture-gen (generative) and fail-sim (adversarial) need LLM work and remain filed under the umbrella.

Positive tests:

crates/corvid-connector-runtime/src/contract_drift.rs::every_drift_narration_carries_grounded_sources
crates/corvid-cli/src/connectors_cmd/check.rs::contract_drift_narration_flow_pairs_every_site_with_grounded_sources

Adversarial tests:

crates/corvid-connector-runtime/src/contract_drift.rs::drift_narration_classifies_breaking_versus_compatible
crates/corvid-connector-runtime/src/contract_drift.rs::removed_field_narration_names_deserialization_consequence
crates/corvid-connector-runtime/src/contract_drift.rs::drift_narration_orders_breaking_before_compatible

`connector.webhook_signature_verified`

class: runtime_checked
phase: runtime

Inbound webhook payloads from Slack, GitHub, and Linear are HMAC-SHA256 verified against the manifest's shared secret before any handler runs. Per-provider schemes are honored: GitHub uses X-Hub-Signature-256: sha256=<hex>, Slack uses v0:<ts>:<body> with a 5-minute replay window, and Linear uses a bare hex digest. Comparison is constant-time; a malformed header, mismatched digest, or stale Slack timestamp returns a categorical WebhookVerificationOutcome that the dispatcher must reject before any side effect.

Positive tests:

crates/corvid-connector-runtime/src/webhook_verify.rs::github_verifies_correct_signature
crates/corvid-connector-runtime/src/webhook_verify.rs::slack_verifies_correct_signature_inside_window
crates/corvid-connector-runtime/src/webhook_verify.rs::linear_verifies_correct_signature

Adversarial tests:

crates/corvid-connector-runtime/tests/threat_corpus.rs::t7_github_webhook_forgery_rejected
crates/corvid-connector-runtime/tests/threat_corpus.rs::t7_slack_webhook_replay_outside_window_rejected
crates/corvid-connector-runtime/tests/threat_corpus.rs::t7_linear_webhook_wrong_secret_rejected

`connector.replay_quarantine`

class: runtime_checked
phase: runtime

A connector running in replay mode must not perform provider writes. The runtime returns ConnectorRuntimeError::ReplayWriteQuarantined for any scope whose effects include a *.write or send_* effect when the active mode is Replay, regardless of whether a real client is bound. Read-shaped operations still complete from the recorded cassette so deterministic replay continues to work.

Positive tests:

crates/corvid-connector-runtime/src/test_kit.rs::fixture_runs_mock_and_replay_read_paths

Adversarial tests:

crates/corvid-connector-runtime/src/runtime.rs::replay_mode_quarantines_writes
crates/corvid-connector-runtime/src/test_kit.rs::fixture_proves_replay_write_quarantine
crates/corvid-connector-runtime/src/calendar.rs::calendar_replay_quarantines_writes
crates/corvid-connector-runtime/src/slack.rs::slack_replay_quarantines_writes

Observability and evals

`observability.otel_conformance`

class: runtime_checked
phase: runtime

Lineage events flow through the standard opentelemetry + opentelemetry-otlp SDK and emit OTLP/HTTP spans whose attributes carry corvid.guarantee_id, corvid.cost_usd, corvid.approval_id, corvid.replay_key. The attribute set is constructed by corvid_runtime::otel_sdk_export::corvid_span_attributes and the live wire path is exercised by the docker-compose Jaeger harness in docs/operations/observability-conformance.md.

Positive tests:

crates/corvid-runtime/src/otel_sdk_export.rs::span_attributes_include_corvid_named_keys
crates/corvid-runtime/src/otel_sdk_export.rs::span_name_uses_corvid_prefix_with_kind
crates/corvid-runtime/src/otel_sdk_export.rs::span_kind_maps_lineage_to_otel

Adversarial tests:

crates/corvid-runtime/src/otel_sdk_export.rs::span_attributes_omit_missing_optional_keys
crates/corvid-runtime/src/otel_sdk_export.rs::sdk_exporter_reaches_in_process_otlp_receiver

`observability.lineage_completeness`

class: runtime_checked
phase: runtime

Every lineage event carries a (trace_id, span_id) pair plus parent linkage when a parent exists, so a SQL JOIN against the local trace store reconstructs the route → job → agent → prompt → tool → approval → DB tree. Validated on every event via corvid_runtime::lineage::validate_lineage.

Positive tests:

crates/corvid-runtime/src/lineage.rs::lineage_ids_are_stable_and_parented_across_backend_kinds

Adversarial tests:

crates/corvid-runtime/src/lineage.rs::lineage_validation_fails_closed_for_missing_parent_or_duplicate_root

`observability.redaction_determinism`

class: runtime_checked
phase: runtime

Redacting the same lineage event twice with the same LineageRedactionPolicy yields byte-identical output; trace topology (trace_id, span_id, parent linkage) is preserved across redaction so observe / eval / OTel keep correlating after sensitive values are removed.

Positive tests:

crates/corvid-runtime/src/lineage_redact.rs::redaction_preserves_topology_and_redacts_identifiers_deterministically

Adversarial tests:

crates/corvid-runtime/src/lineage_redact.rs::redaction_removes_obvious_secrets_from_serialized_lineage

`observability.contract_aware_grouping`

class: runtime_checked
phase: runtime

corvid observe show groups incidents by guarantee_id, effect, budget, provenance, and approval rule rather than by service.name — so an analyst's first pivot lands on the contract that broke. Implemented by lineage_incidents::group_lineage_incidents.

Positive tests:

crates/corvid-runtime/src/lineage_incidents.rs::incidents_group_by_guarantee_effect_budget_provenance_and_approval

Adversarial tests:

crates/corvid-runtime/src/lineage_incidents.rs::non_incident_ok_events_are_not_grouped

`eval.drift_attribution`

class: runtime_checked
phase: runtime

corvid eval-drift --explain decomposes the drift between two trace runs into the four named dimensions (model_id, prompt_hash, retrieval_index_hash, input_fingerprint) plus a residual percentage for unattributable changes. The output's sources array carries the trace_id + span_id of every event the analysis consulted.

Positive tests:

crates/corvid-cli/src/observe_helpers_cmd/eval_drift.rs::drift_explain_attributes_model_swap

Adversarial tests:

crates/corvid-cli/src/observe_helpers_cmd/eval_drift.rs::drift_explain_surfaces_residual_when_status_flips_alone

`eval.promotion_signed_lineage`

class: runtime_checked
phase: runtime

corvid eval-from-feedback synthesises a typed eval fixture from a 'wrong answer' feedback record, redacting the matching lineage trace via the production redaction policy before writing the fixture. The fixture's sources field lists every redacted event so downstream consumers can reconstruct evidence without seeing raw identifiers.

Positive tests:

crates/corvid-cli/src/observe_helpers_cmd/eval_from_feedback.rs::eval_generate_from_feedback_writes_redacted_fixture

Adversarial tests:

crates/corvid-cli/src/observe_helpers_cmd/eval_from_feedback.rs::eval_generate_from_feedback_missing_trace_id_refused

`review_queue.cost_of_being_wrong_ranking`

class: runtime_checked
phase: runtime

corvid review-queue list --rank=cost-of-being-wrong surfaces low-confidence + high-risk outputs ranked by the cost_of_being_wrong policy.

Positive tests:

crates/corvid-cli/src/review_queue_cmd.rs::rank_cost_of_being_wrong_sorts_highest_first

Adversarial tests:

crates/corvid-cli/src/review_queue_cmd.rs::rank_unknown_policy_refused

Deploy packaging

`deploy.reproducible_build`

class: runtime_checked
phase: platform

Building the same corvid deploy package input twice on the same host with two different CARGO_TARGET_DIR values produces bit-identical signed artifacts (binary + SBOM + DSSE attestation envelope). A second build that differs is a build-environment leak — embedded timestamps, hostnames, paths baked at compile time — and the verification CI rejects it. The original determinism gap that kept this row OutOfScope until 2026-05-30 was a cargo:rustc-env=CORVID_STATICLIB_DIR=<absolute target dir> emission from crates/corvid-codegen-cl/build.rs that link.rs and cdylib.rs read through env!(), baking the host's target-build-1 / target-build-2 path into the corvid binary's read-only data section. Closed by routing the staticlib lookup through crate::staticlib_discovery::discover_staticlib at runtime (current_exe()-relative resolution with an explicit CORVID_STATICLIB_DIR override env var); the build script no longer emits any host-dependent strings. The production-grade oracle remains .github/workflows/reproducible-build.yml running on every push to main; structural test refs below lock the regression in place locally.

Positive tests:

crates/corvid-codegen-cl/tests/reproducibility.rs::build_script_emits_no_corvid_staticlib_dir_env_var
crates/corvid-codegen-cl/tests/reproducibility.rs::link_and_cdylib_do_not_read_corvid_staticlib_dir_via_env_macro
crates/corvid-codegen-cl/tests/reproducibility.rs::staticlib_discovery_module_is_wired_into_consumers

Adversarial tests:

crates/corvid-codegen-cl/tests/reproducibility.rs::reproducible_build_workflow_file_exists_and_diffs_two_target_dirs
crates/corvid-codegen-cl/src/staticlib_discovery.rs::override_env_var_pointing_at_missing_file_falls_through
crates/corvid-codegen-cl/src/staticlib_discovery.rs::resolution_strategy_descriptions_are_stable

`deploy.attestation_chain`

class: runtime_checked
phase: platform

corvid deploy package --cdylib <path> binds the deploy attestation to the SHA-256 of the cdylib's bytes; the cdylib itself carries its corvid claim --explain embedded attestation, so the chain claim --explain → cdylib bytes → deploy attestation cannot drift without changing one of the digests. The attestation payload carries chain_status: "complete" + cdylib_sha256: <hex> when --cdylib is provided; chain_status: "incomplete" + cdylib_sha256: null when omitted so downstream verification can refuse an unchained deploy.

Positive tests:

crates/corvid-cli/src/deploy_cmd.rs::deploy_attestation_binds_to_cdylib_digest_when_provided

Adversarial tests:

crates/corvid-cli/src/deploy_cmd.rs::deploy_attestation_marks_chain_incomplete_without_cdylib

`deploy.sbom_completeness`

class: runtime_checked
phase: platform

corvid deploy package emits an SPDX 2.3 JSON SBOM (sbom.spdx.json) naming the app's Corvid source (by SHA-256) and the Corvid runtime the image links against, with the relationship between them declared. A future slice expands this to enumerate every transitively-linked Rust dependency via cargo metadata — the full-dep-enumeration completeness check tracks separately at the dep-enumeration registry row that lands when 43V wires cargo metadata into the SBOM.

Positive tests:

crates/corvid-cli/src/deploy_cmd.rs::deploy_sbom_is_structurally_valid_spdx_2_3
crates/corvid-cli/src/deploy_cmd.rs::deploy_sbom_names_app_source_and_corvid_runtime

Adversarial tests:

crates/corvid-cli/src/deploy_cmd.rs::deploy_sbom_names_app_source_and_corvid_runtime

Release channels

`release.signed_artifact`

class: runtime_checked
phase: platform

Every artifact emitted by corvid release nightly/beta/stable is signed with the release key + paired with a SHA256SUMS.txt whose contents the user can verify with sha256sum -c. The signed manifest is a DSSE envelope over the release contents, with payload type application/vnd.corvid.release.manifest.v1+json. The channel + version pair must satisfy the channel's naming convention (-nightly. / -beta. / plain MAJOR.MINOR.PATCH) — a stable-shaped version cannot be published to the nightly channel and vice versa.

Positive tests:

crates/corvid-cli/src/release_cmd.rs::release_validate_version_accepts_each_channel_shape
crates/corvid-cli/src/release_cmd.rs::sign_release_manifest_emits_v1_payload_type

Adversarial tests:

crates/corvid-cli/src/release_cmd.rs::release_validate_version_refuses_channel_version_mismatch

`release.notes_grounded`

class: runtime_checked
phase: platform

corvid release notes <from> <to> walks git log <from>..<to> over the current repository, categorises each non-merge commit by conventional-commit prefix (feat / fix / perf / refactor / docs / test / chore / build / ci / style), and emits markdown grouped by category. Every rendered line ends with the short SHA so every claim in the notes back-references commit history — the Grounded property at the release-notes layer. Empty ranges produce a typed "No changes between X and Y" stub rather than a partially-rendered section header with no entries. The slice's "RAG-grounded" framing in the 43T umbrella refers to this commit-history citation property, not to a live LLM round-trip: the renderer is deterministic, the generative half of the audit's helper set stays filed under 35V2-P43-T-LR-phase-43-ai-helpers for the other four sub-helpers that need LLM prompt-grounding.

Positive tests:

crates/corvid-cli/src/release_cmd.rs::release_notes_categorise_commits_routes_each_prefix
crates/corvid-cli/src/release_cmd.rs::release_notes_markdown_renders_sections_with_grounded_shas

Adversarial tests:

crates/corvid-cli/src/release_cmd.rs::release_notes_unrecognised_prefix_falls_through_to_other
crates/corvid-cli/src/release_cmd.rs::release_notes_empty_range_renders_no_changes_stub
crates/corvid-cli/src/release_cmd.rs::release_notes_ref_validation_refuses_empty_or_flag_shapes
crates/corvid-cli/src/release_cmd.rs::release_notes_parse_git_log_output_drops_malformed_lines

Upgrade compatibility

`upgrade.claim_regression_check`

class: runtime_checked
phase: platform

corvid upgrade check --claims-current <path> --claims-target <path> compares two claim manifests and refuses (exit 1) if the upgrade target removes any registered guarantee id OR downgrades any class (Static → RuntimeChecked / OutOfScope, RuntimeChecked → OutOfScope). Upgrades (OutOfScope → RuntimeChecked, etc.) are NOT regressions. The two manifests are JSON arrays of {id, class} rows the operator produces via corvid claim --explain --json <cdylib> against the current and target binaries. The --json mode of claim --explain itself lands as a sibling launch- readiness slice — the comparison + rejection is what this row promises.

Positive tests:

crates/corvid-cli/src/upgrade_cmd.rs::claim_regression_check_passes_when_manifests_match

Adversarial tests:

crates/corvid-cli/src/upgrade_cmd.rs::claim_regression_check_flags_removed_guarantee
crates/corvid-cli/src/upgrade_cmd.rs::claim_regression_check_flags_class_downgrades_only
crates/corvid-cli/src/upgrade_cmd.rs::upgrade_check_refuses_unpaired_claim_manifest_flag

Live ops introspection

`ops.live_introspection_signed`

class: runtime_checked
phase: runtime

The Phase 36-generated axum server exposes a /__ops endpoint returning a signed DSSE envelope over a typed OpsShowSnapshot (build_id, started_unix_ms, generated_unix_ms, request_count, claim_manifest_ids). The envelope is signed with the ed25519 key supplied via CORVID_OPS_SIGNING_KEY — empty/unset key returns 503 (fail-closed; an unsigned snapshot is what a MITM would produce). The corvid ops show --envelope-file <path> --pubkey <path> CLI verifies the envelope against an operator-supplied public key: a signature mismatch (wrong key, MITM), payload tampering, or wrong payload-type (corvid.ops.show.v1 is pinned so a signature valid over an ABI attestation cannot be replayed against the ops surface) all fail closed with typed errors. The canonical implementation lives in corvid_runtime::ops_show with 5 unit tests; the rendered server inlines the producer side (matching DSSE PAE byte-for-byte) and the CLI reads + verifies via the runtime helper.

Positive tests:

crates/corvid-runtime/src/ops_show.rs::ops_snapshot_round_trips_through_sign_then_verify
crates/corvid-cli/src/ops_cmd.rs::ops_show_verifies_envelope_signed_with_matching_key
crates/corvid-cli/tests/build_server.rs::rendered_server_ops_show_signs_snapshot_and_cli_verifies_it

Adversarial tests:

crates/corvid-runtime/src/ops_show.rs::ops_snapshot_signed_with_wrong_key_fails_verification
crates/corvid-runtime/src/ops_show.rs::ops_snapshot_tampered_payload_fails_verification
crates/corvid-runtime/src/ops_show.rs::ops_snapshot_refuses_envelope_with_wrong_payload_type
crates/corvid-cli/src/ops_cmd.rs::ops_show_refuses_envelope_signed_with_wrong_key
crates/corvid-cli/src/ops_cmd.rs::ops_show_refuses_malformed_envelope_file

Claim audit

`claim.audit_runnable_artifacts`

class: runtime_checked
phase: platform

Every claim listed in docs/meta/launch-claim-audit.md points at either a runnable command (backticked code), a linked artifact ([link]-style markdown), or an explicit blocked / non-scope status. corvid claim audit exits 0 only when every claim has evidence; aspirational wording flagged at audit time fails the check unless the row carries an explicit blocked/non-scope status.

Positive tests:

crates/corvid-cli/src/claim_cmd.rs::audit_passes_when_every_claim_resolves

Adversarial tests:

crates/corvid-cli/src/claim_cmd.rs::audit_fails_when_a_claim_lacks_evidence

`claim.audit_explain_failures_grounded`

class: runtime_checked
phase: platform

corvid claim audit --explain-failures pairs every finding with a typed ClaimFindingKind (missing_evidence or aspirational_wording) + a suggested_fix string that back-references the inventory line (Grounded shape: every remediation cites the row it addresses). Without the flag, the kind + suggested_fix fields are absent from the JSON so the pre-existing {line, claim, reason} shape stays backward-compatible for CI scripts that read the legacy output. The narration layer never synthesises explanations for rows that aren't flagged. Same deterministic-narrator pattern as corvid connectors check --narrate and corvid release notes; the audit's "adversarial — narrates each failed claim with the specific evidence path + suggested fix" framing in the 43T umbrella refers to this typed-remediation property, not to a live LLM round-trip.

Positive tests:

crates/corvid-cli/src/claim_cmd.rs::explain_failures_classifies_missing_evidence_with_line_grounded_fix
crates/corvid-cli/src/claim_cmd.rs::explain_failures_classifies_aspirational_wording_with_typed_remediation

Adversarial tests:

crates/corvid-cli/src/claim_cmd.rs::explain_failures_off_preserves_legacy_finding_shape
crates/corvid-cli/src/claim_cmd.rs::explain_failures_on_clean_inventory_yields_zero_findings

Per-app helpers

`app.pr_describe_grounded`

class: runtime_checked
phase: runtime

corvid app pr-describe --base <base.cor> --head <head.cor> lowers both sources to ABI descriptors in-process and renders a typed PrDescription summarising what the change set means for the app's claim surface. Emits typed sections (Breaking, Additive, Informational) over agents, tools, approval gates, types, stores, claim guarantees, and ABI / compiler versions. Every bullet carries a non-empty sources array back-referencing the descriptor field that diverged. Sections are sorted by severity (Breaking → Additive → Informational) then alphabetically by heading so the reviewer reads the most consequential changes first. The walker catches the subtle cases the helper exists to surface: removed agents/tools/approvals are flagged Breaking; pub extern "c" revoked or approval-tier weakened (operator → autonomous, human_required → anything else) is Breaking; field count drops on a same-name type is Breaking. Replay-stable: two invocations on the same (base, head) pair produce byte-identical output. Deterministic + LLM-free; the helper's "generative" framing describes its purpose (generating PR-description text) not an LLM round-trip. The third sub-slice of 35V2-P42-H-LR-per-app-ai-helpers to ship; the umbrella closes with it.

Positive tests:

crates/corvid-abi/src/pr_describe.rs::pr_describe_emits_bullets_grounded_to_descriptor_fields
crates/corvid-cli/src/app_cmd.rs::pr_describe_renders_added_agent_in_additive_section_with_grounded_sources

Adversarial tests:

crates/corvid-abi/src/pr_describe.rs::no_change_case_produces_typed_grounded_description
crates/corvid-abi/src/pr_describe.rs::breaking_section_precedes_additive_in_rendered_output
crates/corvid-abi/src/pr_describe.rs::approval_tier_weakening_is_flagged_breaking
crates/corvid-abi/src/pr_describe.rs::render_pr_description_is_byte_identical_across_two_invocations
crates/corvid-cli/src/app_cmd.rs::pr_describe_with_unparseable_base_returns_typed_error_not_panic

`app.adversarial_refresh_grounded`

class: runtime_checked
phase: runtime

corvid app adversarial-refresh <source.cor> walks every surface element in the app's ABI descriptor and emits one typed AdversarialSuggestion per (surface_element, threat_category) pair. Threat categories include CrossTenant, MissingBudget, ApprovalBypass, UnauthorisedCaller, ReplayWithoutToken, WriteWithoutApproval, RoleBypass, ExpiredApprovalReuse, DataClassDrift, and MalformedPayload. Per-surface coverage: every approval site gets cross-tenant + role-bypass + expired-approval-reuse suggestions, plus data-class-drift when dangerous_targets is non-empty; every dangerous: true tool gets cross-tenant + approval-bypass + missing-budget; every pub extern "c" agent gets malformed-payload + unauthorised-caller, plus replay-without-token when @replayable; every writeable store gets cross-tenant-write + write-without-approval. Each suggestion carries a non-empty sources array back-referencing the descriptor field it was derived from. Suggestions are sorted deterministically (kind → name → threat) so two runs on the same descriptor produce byte-identical reports. Deterministic + LLM-free; the helper's purpose is to make every surface element's adversarial coverage requirements visible so no surface ships without its named adversarial counterpart. The second sub-slice of 35V2-P42-H-LR-per-app-ai-helpers to ship.

Positive tests:

crates/corvid-abi/src/adversarial_refresh.rs::every_suggestion_carries_non_empty_sources
crates/corvid-cli/src/app_cmd.rs::adversarial_refresh_for_extern_agent_renders_grounded_suggestions

Adversarial tests:

crates/corvid-abi/src/adversarial_refresh.rs::empty_surface_descriptor_produces_empty_report_not_sourceless
crates/corvid-abi/src/adversarial_refresh.rs::render_adversarial_refresh_is_byte_identical_across_two_invocations
crates/corvid-abi/src/adversarial_refresh.rs::non_dangerous_tools_get_no_suggestions
crates/corvid-abi/src/adversarial_refresh.rs::read_only_stores_get_no_write_suggestions
crates/corvid-abi/src/adversarial_refresh.rs::replayable_agents_get_replay_without_token_suggestion_non_replayable_do_not
crates/corvid-cli/src/app_cmd.rs::adversarial_refresh_for_unparseable_source_returns_typed_error_not_panic

`app.boot_summary_grounded`

class: runtime_checked
phase: runtime

corvid app boot-summary <source.cor> lowers the supplied Corvid source through the standard frontend pipeline, builds the ABI descriptor in-process, and renders a typed BootSummary (surface counts, flagship pub extern "c" entrypoints, approval gates, enforced guarantees, dangerous-surface counts, stores-writeable flag, descriptor sha256). Every derived field is paired with a BootSource entry naming the descriptor field that supplied the value, mirroring the Grounded sources posture that connector.drift_narration_grounded uses for the drift narrator. Replay-stable: two invocations on the same source produce byte-identical output. The first sub-slice of 35V2-P42-H-LR-per-app-ai-helpers to ship; adversarial-refresh and pr-describe remain filed under the umbrella as the next slices.

Positive tests:

crates/corvid-abi/src/boot_summary.rs::boot_summary_grounds_every_derived_field_to_a_descriptor_source
crates/corvid-cli/src/app_cmd.rs::boot_summary_for_minimal_app_renders_grounded_block

Adversarial tests:

crates/corvid-abi/src/boot_summary.rs::boot_summary_empty_surface_descriptor_returns_grounded_summary_not_sourceless
crates/corvid-abi/src/boot_summary.rs::render_boot_summary_is_byte_identical_across_two_invocations
crates/corvid-cli/src/app_cmd.rs::boot_summary_for_unparseable_source_returns_typed_error_not_panic

Platform — explicit non-defenses

`platform.host_kernel_compromise`

class: out_of_scope
phase: platform

Defending against a compromised host kernel or privileged-process tampering with the running Corvid binary's memory.

Why out of scope: Outside Corvid's trust boundary — a kernel that can rewrite user-space memory can defeat any user-space invariant. The security model assumes a non-malicious kernel; otherwise the host is responsible.

`platform.signing_key_compromise`

class: out_of_scope
phase: platform

Defending against compromise of the ed25519 signing key used to attest a cdylib or sign a receipt.

Why out of scope: Key management is a host responsibility. Corvid signs and verifies; rotating, revoking, and protecting keys is outside the language's scope and explicitly delegated to the host's key-management practice.

`platform.toolchain_compromise`

class: out_of_scope
phase: platform

Defending against a compromised Rust toolchain, Cranelift release, or system linker producing a Corvid binary that does not match its source.

Why out of scope: Reproducible builds across heterogeneous toolchains are a post-v1.0 hardening goal. Today Corvid trusts the rustc and Cranelift releases the user installs; the bilateral verifier (Slice 35-H) is the closest approximation of toolchain-independence available pre-v1.0.

`package.hosted_registry_available`

class: out_of_scope
phase: platform

A Corvid-operated public package registry service that serves the published index format and source artifacts.

Why out of scope: No hosted Corvid package registry service runs yet; The CLI ships the published index format + signed-publish tooling (corvid package publish, verify-registry, verify-lock) and --url-base accepts file:// and any http endpoint a user runs themselves. A hosted public registry is post-v1.0 work; see docs/internals/package-manager-scope.md for the full boundary.

Updating this document

This file is generated. To change a description, add a new guarantee, or move an entry between static / runtime_checked / out_of_scope, edit crates/corvid-guarantees/src/lib.rs and run:

cargo run -q -p corvid-cli -- contract regen-doc docs/reference/core-semantics.md

Then commit the regenerated file together with the registry change. CI fails if the committed text drifts from the registry — there is no quiet way to evolve the spec away from the implementation.