Product documentation
Proof Artifacts
Proof is maintained as a claim registry linked to source references and artifact records.
Claim Registry
Claims are versioned records with required mechanism, source reference, and artifact linkage.
claim/policy-outside-runtime
The control plane attempts to enforce policy before tool execution in verified code paths.
Runtime output is treated as untrusted proposal input; capability checks and policy evaluation gate side effects before tool execution.
- Status:
- partial
- Evidence strength:
- moderate
- Last verified:
- 2026-03-19
- Product version:
- 0.5.0
- Source reference:
- product-repo:internal/policy/evaluator.go
- Artifact references:
- approval-binding-evidence
Assumptions
- Tool execution requests pass through control-plane authorization in the traced execution path.
- Only locally embedded topology (v1) has been verified.
Invalid when
- Execution path bypasses policy evaluation before side effects.
- Offline or degraded mode disables the control plane gate.
- Code paths outside the traced verification scope are not enforced.
- Subprocess spawns outside the tool boundary enforcement.
Breakage signals
- Tool invocation executes despite deny policy decision.
- Side effect occurs without prior policy evaluation.
- Policy evaluation disabled in offline mode.
Challenge questions
- If runtime output requests write access outside allowed scope, does control-plane policy deny execution before sandbox invocation?
claim/event-attribution-replayability
Execution events attempt to record actor, approval id, policy decision metadata, and run identifiers for incident analysis.
Event envelopes attempt to record actor, approval id, policy decision metadata, and run identifiers for deterministic reconstruction.
- Status:
- planned
- Evidence strength:
- illustrative
- Last verified:
- 2026-03-19
- Product version:
- 0.5.0
- Source reference:
- product-repo:internal/db/store.go
- Artifact references:
- event-replay-lineage
Assumptions
- Event pipeline writes immutable sequence metadata when operational.
- All significant state transitions produce corresponding event envelopes.
- Event types cover all significant transitions.
Invalid when
- Required attribution fields are omitted from event envelopes.
- Event recorded after state change rather than at transition point.
- Hash chain gaps prevent reconstruction.
- Event emission fails silently in degraded mode.
Breakage signals
- Replay chain cannot resolve actor for an executed action event.
- Event envelope missing required attribution fields.
- Gap detected in hash chain sequence.
Challenge questions
- When an event arrives without approval_id under replay conditions, does the event model mark lineage as incomplete instead of asserting full attribution?
- Are all significant state transitions covered by defined event types?
claim/approval-argument-binding
The control plane attempts to bind approvals to exact normalized action arguments in verified execution paths.
Control plane computes a digest of normalized action payload and rejects execution when digest, scope, or expiry does not match approval state.
- Status:
- partial
- Evidence strength:
- moderate
- Last verified:
- 2026-03-19
- Product version:
- 0.5.0
- Source reference:
- product-repo:internal/canonicalization/fingerprint.go
- Artifact references:
- approval-binding-evidence
Assumptions
- Action normalization is deterministic for equivalent payloads.
- Approval checks execute before side effects in the traced execution path.
- Only locally embedded topology (v1) has been verified.
Invalid when
- Normalized argument digest differs from stored approval digest.
- Approval is expired, revoked, or scope-mismatched.
- Execution path bypasses approval check.
- Normalization differs between proposal and execution time.
Breakage signals
- Approval accepted when normalized_args_hash differs from approval_args_hash.
- Execution event missing approval_id for approved action.
- Tool executes despite digest mismatch.
Challenge questions
- If approval scope is narrowed after request creation, does the control plane reject execution under the new scope condition?
- When normalized arguments change after approval issuance, does the approval validator deny execution before tool invocation?
Artifact Index
event-log
Approval hash binding
Approval records include normalized action hash and are checked at execution time.
- Claim supported:
- Approvals bind to exact normalized actions rather than broad prompts.
- Status:
- partial
- Last verified:
- 2026-03-19
- Provenance:
- synthetic
- Traceability:
- partial
- Artifact origin:
- constructed
- Product version:
- 0.1.0
- Source of truth:
- product-repo:internal/controlplane/approvals/*
- Source system:
- control-plane
- Source path:
- internal/controlplane/approvals
- Source commit:
- redacted
- Capture hash:
- sha256:example-approval-binding-record
This artifact is synthetic and should be read as illustrative, not as direct production output.
Source references
- product-repo:internal/controlplane/handler_approvals.go
- product-repo:internal/controlplane/server.go
policy-doc
Replayable event lineage
Event envelopes include run identifiers, actor, approval id, and policy decision metadata.
- Claim supported:
- Execution events are attributable and replayable for incident review.
- Status:
- pending
- Last verified:
- 2026-03-19
- Provenance:
- conceptual
- Traceability:
- partial
- Artifact origin:
- constructed
- Product version:
- 0.1.0
- Source of truth:
- product-repo:internal/audit/*
- Source system:
- control-plane
- Source path:
- internal/audit
- Source commit:
- redacted
- Capture hash:
- sha256:example-replay-lineage-record
This artifact is conceptual and should be read as illustrative, not as direct production output.
Source references
- product-repo:internal/audit/event_store.go
- product-repo:migrations/*audit*
Verification Records
Records capture concrete examples of system behavior with claim and source linkage.
policy-doc
Replay lineage envelope
- Claim ref:
- event-attribution-replayability
- Status:
- planned
- Verification:
- manual
- Verification confidence:
- low
- Reproducible:
- no
- Verified at:
- 2026-03-19
- Product version:
- 0.5.0
- Verified by:
- platform-engineering
- Replay fidelity:
- approximate
- Source ref:
- product-repo:internal/db/store.go@9af059973ade9b4f45046747bb268690b82fbeb5
- Freshness:
- unknown
Proof boundaries
Proves: Event envelope schema includes minimum required fields for replay, Field structure supports attribution workflow
Does not prove: All state transitions produce event envelopes, Event emission is complete for all significant transitions, Hash chain integrity can be verified, Production event samples match schema
Assumptions: Event types defined in event_types.go cover all significant transitions, Envelope schema is stable
Failure modes: Transition occurs without corresponding event type, Event recorded after state change rather than at transition point, Hash chain gaps prevent reconstruction
Break this claim
Conditions: State transition occurs without recorded event, Event recorded with incorrect actor attribution, Hash chain contains gaps or inconsistencies
Required evidence: Production trace showing gap in event sequence, Demonstration of state without corresponding event
Artifact refs: event-replay-lineage
View recordpolicy-doc
Policy gate before side effects
- Claim ref:
- policy-outside-runtime
- Status:
- partial
- Verification:
- manual
- Verification confidence:
- medium
- Reproducible:
- yes
- Verified at:
- 2026-03-19
- Product version:
- 0.5.0
- Verified by:
- controlplane
- Replay fidelity:
- approximate
- Source ref:
- product-repo:internal/policy/evaluator.go@663e9e35b615e163cd5ef478cd0470be495b8ba2
- Freshness:
- unknown
Proof boundaries
Proves: Policy evaluation occurs before tool execution in the traced code path, Deny decisions prevent tool execution completion
Does not prove: All code paths enforce policy before execution (only the traced path verified), Offline or degraded mode behavior, Subprocess spawn outside tool boundary enforcement
Assumptions: Trace represents typical production execution flow, No bypass paths exist in untraced code
Failure modes: Bypass path discovered in untraced code, Policy evaluation disabled in offline mode
Break this claim
Conditions: Tool executes after policy evaluation returns denied, Side effect occurs without prior policy evaluation, Offline mode disables policy gate
Required evidence: Policy trace showing denied action executing, Event log showing execution without prior policy decision
Artifact refs: approval-binding-evidence
View recordevent-log
Approval argument match event
- Claim ref:
- approval-argument-binding
- Status:
- partial
- Verification:
- manual
- Verification confidence:
- medium
- Reproducible:
- yes
- Verified at:
- 2026-03-19
- Product version:
- 0.5.0
- Verified by:
- security-engineering
- Replay fidelity:
- approximate
- Source ref:
- product-repo:internal/canonicalization/fingerprint.go@b0c9dc604a6fed33ac7403ac9d0939a8df68b6e9
- Freshness:
- unknown
Verification command: node scripts/verify-proof.mjs approval-argument-match-event
Output validation: contains (lenient) | hash-match=true
Normalize: trim
Verification artifact: approval-binding-evidence
Verification artifact hash: sha256:example-approval-binding-record
Command type: deterministic
Determinism assumptions: Verification command reads static redacted fixture and does not call external services.
Proof boundaries
Proves: Approval record contains normalized_args_hash field, Hash matching logic exists in approval validation, Event envelope structure includes approval_id and decision
Does not prove: This proof does not establish that every approval request is hash-bound (structural evidence only), This proof does not establish that execution_context captures all environment state, This proof does not establish deterministic digest computation across every serialization path, Production traffic confirms hash matching behavior
Assumptions: Redacted fixture represents actual production structure, Hash computation is deterministic for included fields
Failure modes: Digest computation misses relevant execution state, Normalization differs between proposal and execution time, Tool behavior differs despite identical normalized arguments
Break this claim
Conditions: Approved action executes with different effect than approved, Arguments normalized differently at proposal vs execution, Execution context differs despite hash match
Required evidence: Production trace showing hash match but unexpected execution, Demonstration of normalization inconsistency
Artifact refs: approval-binding-evidence
View recordVerification Contract
- No fact claim is published without at least one artifact reference.
- Artifact records must include source-of-truth pointer and verification status.
- Planned and partial claims remain visibly labeled.