§02b Jupiter — Certification & Attestation — The conformance certificate
Mars® Spec › §02b Jupiter — Certification & Attestation › The conformance certificate
← What this layer covers · Section index · The specification registry →
2. The conformance certificate
The terminal artifact of governed conformance verification. For each verified target, the system emits a typed, cryptographically-signed integrity certificate.
The inventive matter is the set of structural invariants, not a field count. A conformance certificate under this architecture is defined by the co-presence of nine structural invariants — each independently required, none waivable. The canonical realization carries exactly these nine invariants as nine declared fields. A certificate that carries all nine invariants is conforming regardless of how many additional fields it contains, how those fields are named, or how they are serialized. A certificate that omits any one invariant is structurally deficient regardless of field count. Adding a tenth field does not avoid this architecture. Dropping the recomputation witness invariant does not produce a different architecture — it produces a non-conforming certificate.
Provenance bundle co-presence (anti-substitution invariant). The nine structural invariants are not independently satisfiable from separate origins. They must be co-present as a bundle: all nine invariants must have been produced by, and remain traceable to, the same governed analysis event over the same target under the same governing specification. A certificate that satisfies each of the nine invariants by sourcing them from different analysis events, different targets, or different governing specifications — even if each individual invariant is internally valid — is structurally non-conforming. The bundle co-presence requirement is the mechanism by which the nine invariants function as a unit rather than as a checklist. Specifically:
- Field 4 (grounded verdict) and Field 7 (recomputation witness) must be co-derived from the same analysis battery record; a certificate where the verdict was derived from one battery run and the witness was attached from a different battery run does not satisfy co-presence.
- Field 2 (governing-specification identity) must be the same specification identity referenced by Field 7’s witness; a witness re-derived under a different governing specification than the one named in Field 2 does not satisfy co-presence.
- Field 9 (tamper-evident cryptographic binding) must be computed over Fields 1–8 as they exist in this certificate instance; a binding computed over a different set of field values — even if re-using field values from another valid certificate — does not satisfy co-presence.
Emission gate. A certificate is not emitted until all nine structural invariants are present and their co-presence is verified. No partial certificate is registered. No invariant may be deferred for later attachment after registration. A registered certificate that was found to have been assembled from invariants of distinct origins is immediately revoked with a cascade record; it does not retain any validity during the investigation period.
The nine structural invariants and their canonical field assignments:
| Invariant | Canonical field | What it requires |
|---|---|---|
| Target identity | Field 1 | A record sufficient to unambiguously identify what was certified, including target class and provenance |
| Governing-specification identity with bootstrap provenance | Field 2 | The registered specification version plus the custody chain linking it to its source authority |
| Certification-path record | Field 3 | Declaration of the method(s) by which the verdict was derived, each with a matching evidence reference |
| Grounded verdict | Field 4 | A verdict derived from and traceable to the analysis battery — not asserted |
| Declared scope | Field 5 | The scope under which the verdict holds, drawn from the governing specification’s scope conditions |
| Falsifier record | Field 6 | Structured enumeration of conditions under which the certificate is invalidated |
| Order-typed recomputation witness | Field 7 | A record from which an independent inspector re-derives the verdict without deployment access |
| Temporal validity window | Field 8 | Issuance timestamp, expiration timestamp, and re-attestation cadence |
| Tamper-evident cryptographic binding | Field 9 | A binding computed over all other invariants rendering the certificate tamper-evident and the verdict attributable |
2.1 Target classes
The certification mechanism applies to three target classes. The distinction between Class B and Class C is structurally significant and must be enforced at issuance.
Class A — Non-linguistic analysis program. A computational artifact that operates on non-linguistic data under an analysis specification. Four forms:
- Synthesized — produced by a synthesis procedure under a synthesis-target specification; synthesis-correctness proof available
- Native — a pre-existing program; source code and/or model weights amenable to empirical characterization or test
- Interaction-mediated — a third-party service operated behind an interaction protocol; internal implementation unavailable
- Pipeline-composed — a directed graph of agents or computation stages whose composed output — not any individual stage’s output — is the certified artifact; the pipeline itself is the target of analysis. No single agent’s output certificate substitutes for a pipeline-level certificate.
Non-linguistic data includes physical-domain signals (sensor, radar, acoustic, biometric, telemetry, transaction), digital-artifact signals (configuration files, logs, scan results, application state, structured records), mathematical and symbolic artifacts, UI-state artifacts, and program artifacts analyzed as data. The mechanism is modality-agnostic.
Class B — Generated interpretation. A typed linguistic predicate or other typed/structured interpretive artifact produced by lifting a non-linguistic engineering result through an interpretation-generation specification governing the result-domain-to-predicate-vocabulary mapping, scope conditions, loss-of-information records, and citation linkage. The generated interpretation is the artifact under analysis; the conformance question is whether the artifact is the sound image of the result under that mapping.
A Class B certificate requires a non-linguistic provenance chain record in Field 1: the identity of the non-linguistic engineering result from which the interpretation was lifted, a reference to its certification or analysis record, and the lift-path identity (interpretation-generation specification identifier plus mapping-execution record). A certificate that traces only to a linguistic analysis of the interpretation — without anchoring to the non-linguistic engineering result — is not a valid Class B certificate. It is a Class C certificate of the interpretation and must be issued as such.
Class C — Linguistic artifact of arbitrary provenance under a registered language specification. A linguistic artifact verified against a registered language specification, irrespective of producer and origin. The producer may be the present system, another system, or a human. This is a language-to-language conformance that does not contain or require the non-linguistic bridge of Classes A and B.
Target-of-analysis symmetry (S10 — load-bearing behavioral invariant). The interpretation-producing mapping that generates a Class B artifact is itself a program — a Class A artifact in its own right. The generated interpretation is its analyzed emitted artifact. This symmetry is not taxonomic labeling: it means the same certification triad, the same recomputation witness structure, and the same structurally-defined invariant set (§02b §2) apply to the interpretation-producing mapping as to any other Class A program, and the certificate for the generated interpretation as a Class B artifact is structurally grounded in the certificate for that mapping. An inspector verifying a Class B certificate must be able to confirm: (i) the interpretation-producing mapping is covered by a valid Class A certificate; (ii) the generated interpretation’s Field 1 non-linguistic provenance chain references that Class A certificate; and (iii) the recomputation witness in Field 7 re-derives the interpretation verdict from the lift under that mapping’s governing specification. A Class B certificate that cannot be so grounded does not satisfy the symmetry invariant and is non-conforming.
Classes A and B are symmetric: both involve the non-linguistic-to-linguistic boundary. The same certification triad, the same certificate invariant structure, and the same recomputation witness apply to all three classes.
Interaction-protocol substitution. Where the target is an interaction-mediated analysis program whose internal implementation is unavailable, the verified target is the interaction protocol. The certification path is interaction-protocol conformance testing against an interaction-protocol specification, recorded as an interaction-protocol-conformance record containing: interaction-protocol-specification identifier; identity of the interacted-with program (name, version, provenance); the conformance record produced by exercising a declared test-vector set.
2.2 Field 1 — Target identity
Contents vary by target class:
| Class | Required contents |
|---|---|
| Class A — synthesized | Synthesis-target-specification identifier; synthesis-procedure identifier; produced program’s content hash; synthesis-correctness-proof reference (where available); form classification = synthesized |
| Class A — native | Source-code hash; model-weight hash; verification-artifact reference; test-suite identifier; or statistical-certification-report reference; form classification = native |
| Class A — interaction-mediated | Interaction-protocol-specification identifier; identity of the interacted-with program (name, version, provenance); interaction-protocol-conformance record; form classification = interaction-mediated |
| Class A — pipeline-composed | Pipeline-topology content hash; declared graph of stages (stage identity, version, governing-specification binding per stage); composition rule governing stage-output aggregation; form classification = pipeline-composed. Field 7 carries a pipeline witness chain: each stage contributes a witness link at the stage level, chaining through the aggregation step to the composed-output verdict. Certifying the composed output without this topology record and stage-level witness chain is not a valid pipeline-composed certificate. |
| Class B | Interpretation content hash; interpretation-generation identity (specification identity, version, mapping-execution record); non-linguistic provenance chain record |
| Class C | Linguistic-artifact content hash; producer identity (one of: the verification system / another system / a machine producing an interpretation / a human); reference to the registered language specification |
2.3 Field 2 — Governing-specification identity with bootstrap provenance
The registered specification identity and version, together with bootstrap provenance. Bootstrap provenance has three components:
- Source-authority hash — content hash of the natural-language source authority from which the specification was derived
- Attestation statistic — declared inter-rater agreement statistic identity and computed value (satisfying the five agreement-statistic properties of §01 §8), computed over the per-predicate rating-unit population against the declared threshold; the statistic identity and the threshold are each named, versioned, registered parameters held in the specification registry alongside the governing specification record; Field 2 must carry both the statistic identity, the computed value, the threshold value, and their registry identities
- Scope-certificate hash — content hash of the scope-of-applicability certificate of the specification
These three components together verify the custody chain from natural-language source to formal specification. Self-referential scope-certificate hashes are not valid.
Reverse-composition case. Where the governing specification is reverse-composed (§02a §6), Field 2 carries: a composition-origin digest (covering the set of artifacts from which the specification was derived) in place of the source-authority hash; the composition method and the phase (i) composition-process witness in place of the attestation statistic; and a composition-provenance flag in place of the scope-certificate hash.
Bootstrap provenance verification failure. Where bootstrap provenance cannot be independently confirmed — because one or more of its three components is absent, does not match the declared values, or references an unresolvable source — the following consequence applies:
| Component | Failure consequence |
|---|---|
| Source-authority hash absent or unresolvable | Certificate is conditionally-conforming at best; falsifier annotation (Field 6, condition (e) with bootstrap-provenance-gap subtype) required; declared scope must include the gap as a scope condition |
| Attestation statistic absent, below threshold, or not reproducible | Same consequence as source-authority hash failure |
| Scope-certificate hash absent, self-referential, or fails hash verification | Same consequence |
| Multiple components fail | Certificate is non-conforming; may not be issued until gap is resolved or specification is declared reverse-composed |
Where a bootstrap-provenance gap is declared permanent, the governing specification transitions to reverse-composed status: Field 2 is rewritten to carry the composition-origin digest, composition method, and composition-process witness. The gap is then a declared structural condition, not an unresolved failure.
2.4 Field 3 — Certification-path record
Path identifier drawn from the typed enumeration: {classical-formal-verification, empirical-characterization, test-or-oracle-backed-validation}. Each path identifier is paired with a matching evidence reference:
| Path | Evidence reference |
|---|---|
| Classical formal verification | Proof-artifact reference |
| Empirical characterization | Empirical-characterization-report reference with declared metrics |
| Test or oracle-backed validation | Test-suite identifier with last-pass-execution record and declared re-attestation cadence |
Interaction-protocol conformance as sub-case. For interaction-mediated targets, interaction-protocol conformance is the sub-case of test-or-oracle-backed validation in which the test oracle is the interaction-protocol specification and the test vectors are the declared interaction trace. The evidence reference is an interaction-protocol-conformance record containing: interaction-protocol-specification identifier; identity of the interacted-with program (name, version, provenance); conformance record from exercising the declared test-vector set. Field 3 carries test-or-oracle-backed-validation as the path identifier; the interaction-protocol-conformance sub-type is declared in the evidence reference, not as a distinct path identifier.
Where two or more paths are used jointly, the record enumerates each constituent path and its matching evidence reference.
Battery-record binding. Each path identifier in Field 3 must correspond to at least one method entry in the analysis battery record, and each matching evidence reference must be the content-addressed identity of a specific battery-method output artifact recorded in that battery record. A Field 3 certification-path record whose evidence references cannot be resolved to entries in the analysis battery record does not satisfy the grounded-verdict invariant (Field 4).
2.5 Field 4 — Grounded verdict
A grounded typed value drawn from the canonical enumeration: {conforming, non-conforming, conditionally-conforming}. The enumeration is stable and not extended by appending qualifiers to verdict names — variations in the nature or number of conditions are carried in the conditions record, not encoded into the verdict value itself. Where the verdict is conditionally-conforming, a conditions record is co-required: a non-empty structured record enumerating the conditions under which conformance holds, each condition specifying the aspect or clause to which it applies, the nature of the condition, and the action required to clear it.
Field 4 must be a grounded verdict — derived from and traceable to the analysis battery record. An asserted verdict without traceable grounding does not satisfy this field.
2.6 Field 5 — Declared scope
Field 5 is an order-typed scope expression — the bounded region of the governing artifact space within which the verdict holds. It is not a free-text annotation. It is a computable, registered artifact in a declared expression language whose containment relation is mechanically evaluable. Gate check #5 (§3) — refusing when an operation’s typed scope exits the certificate’s declared scope — is a solver call against the lowered form of this expression, not a human judgment.
5.1 Scope expression forms
A scope expression is one of six typed forms, or a composed intersection of any combination of them:
| Form | What it bounds | Source |
|---|---|---|
| Aspect-set scope | An explicit set of (order × perspective × variant) tuples from the domain model’s metric space (§01 §3.1, §01 §5); the verdict holds only for artifacts located at or within these aspect positions |
Domain model |
| Predicate-set scope | An explicit subset of predicate identities from the compiled formal specification bundle (§01 §7 Component A); the verdict holds only under the declared predicate subset | Formal specification |
| Guard-condition scope | A logical guard predicate over the subject or input space — expressed in the same decidable fragment as the compiled formal specification — that must be satisfied for the verdict to apply; may reference domain model vocabulary, formal specification terms, or both | Domain model and/or formal specification |
| Temporal scope | A declared version window and/or time interval; the verdict holds only under the governing artifact versions and within the time range declared here; the version identifiers are content-addressed registry references | Governing artifact registry |
| Cross-domain interface scope | The scope-of-applicability certificate of a registered cross-domain typed interface (§02c §3); the verdict holds only within the input range that interface certifies | Cross-domain typed interface registry |
| Composed scope | The conjunction (intersection) of any combination of the above forms; the effective scope is the intersection of all constituent scopes; no constituent scope may be widened by composition | All of the above |
The form used must be declared. A scope expression that does not declare its form is structurally deficient and refused at registration.
5.2 Required lowering to the decidable fragment
Every scope expression, regardless of form, must be lowered to a formula in the decidable logical fragment declared in the governing specification’s bootstrap record (§2.3; the same fragment used for compiled predicates — QF_UFLIA or declared equivalent). Lowering is required, not optional. A scope expression that resists lowering to the declared fragment is not a valid scope expression; the operator must reformulate it until it is lowerable.
The lowered formula is the canonical scope formula. It is the form over which gate check #5 evaluates containment. The containment check is: does the lowered formula of the operation’s typed scope logically entail the lowered formula of the certificate’s declared scope? This is a decision-procedure call, not a string match and not a human judgment. A deployment that evaluates containment by any means other than the declared decision procedure applied to the canonical scope formula is non-conforming.
The canonical scope formula is carried as a required field of the scope expression record alongside the structured form declaration. Both are required: the structured form declaration (which human-readable form was used) and the canonical scope formula (the lowered, solver-evaluable form). A scope expression record missing either is structurally deficient.
5.3 Per-governing-specification binding and multi-spec map
A scope expression is bound to a specific registered governing specification version. Where a single governing specification is active, Field 5 is a single scope expression record carrying the governing specification version identity alongside the expression.
Where the governing collection (§01 §12.1) declares two or more active governing specifications, Field 5 is a scope expression map: an ordered set of (governing-specification-version-identity → scope expression record) pairs, one per active specification. The effective scope of the certificate is the intersection of all constituent scope expressions across all active specifications. No constituent scope may be widened by the intersection.
The scope expression map is not optional when multiple governing specifications are active. A certificate issued under a multi-spec governing collection that carries only a single scope expression — not a map — is structurally deficient: it asserts scope under fewer than the full active governing collection and may over-attest.
5.4 Scope derivation as a governed act
A scope expression may be statically declared — asserted by the analysis authority at issuance time — or derived by governed traversal of the governing artifact space. Derivation is the stronger form: the scope expression is computed from the governing artifacts rather than asserted, making it grounded in the same sense as the verdict.
Governed scope derivation traverses any combination of: the active domain model(s), the compiled formal specification bundle(s), the active knowledge base(s), the active data source(s), and prior attestations, certificates, and recomputation witnesses registered in the specification registry. The traversal is governed by the same traversal machinery as analysis (§02a §4b): it is initiated from declared inputs, parameterized, recomputable, and order-typed.
Where derivation is used, the scope derivation act produces a scope derivation witness — a record sufficient for an independent inspector to re-derive the scope expression from the governing artifact space without deployment access. The scope derivation witness is a required link in the multi-stage witness chain (§02a §5a.2), positioned between the traversal witness links and the analysis act links:
[pre-invocation signal links] → [IR stage links] → [traversal witness links] → [scope derivation witness link] → [analysis act links] → [verdict link]The scope derivation witness carries as minimum required fields:
| Field | Content |
|---|---|
| Governing artifacts traversed | Identities and versions of every domain model, formal specification, knowledge base, data source, and prior registered artifact (attestation, certificate, witness) consulted during derivation |
| Scope conditions contributed | Per traversed artifact: the scope condition(s) it contributed to the derived expression, keyed to the artifact identity and the aspect or predicate from which the condition was drawn |
| Composition record | How the contributed conditions were combined into the final scope expression — specifically the intersection operations applied across constituent conditions and, where a multi-spec map was produced, which conditions map to which governing specification version |
| Conflict record | Any governing-conflict conditions detected during derivation (§5.5 below), the gap identities opened, and the resolution procedure declared for each |
| Canonical scope formula derivation | The lowering procedure applied to produce the canonical scope formula from the structured form, with sufficient record for an inspector to re-apply the lowering and reproduce the formula |
| Witness content hash | Tamper-evident binding over all fields of this witness link |
A scope expression that was derived but whose scope derivation witness is absent from the multi-stage witness chain is treated as statically declared — the derivation provenance is lost, and the stronger grounding claim is not available to downstream consumers.
Static declaration. Where a scope expression is statically declared, no scope derivation witness link is produced. The certificate carries a scope_derivation_class field with value static; derived scope expressions carry derived. A downstream consumer can determine from this field whether the scope was asserted or grounded.
5.5 Pre-flight governing-conflict detection and REFER discipline
Before a CERTIFY verdict is emitted, a pre-flight scope consistency check runs against the full active governing collection. The check evaluates whether the proposed scope expression map is conflict-free: no two constituent scope expressions — one per active governing specification — assert incompatible conditions over the same domain aspect under the same order and perspective.
A conflict is detected when two constituent scope expressions, lowered to their canonical scope formulae and evaluated jointly by the declared decision procedure, are jointly unsatisfiable over the same aspect region. This is the same condition as the governing-conflict gap (§01 §12.4, §02a §7), triggered here at scope evaluation time rather than at traversal time.
On conflict detection, the certificate is held as REFER — specifically reason = "scope_governing_conflict_pending" with the divergence_id of the opened governing-conflict gap record carried in the reason record. No CERTIFY is emitted while the gap is in Open or In-resolution state. The conflict is not resolved by the scope expression language; it is routed to the conflict resolution procedure declared in the governing collection (§01 §12.1). That procedure may be automated, manual, or hybrid — the scope expression language does not constrain it. The certificate may be re-evaluated for CERTIFY only after the gap reaches Resolved state and the resolution outcome has been applied (§02a §3a.3 AR-gate.6 outcome taxonomy applies: ratify_amend, admit_after_review, refuse_with_justification, or escalate).
Cached containment checks. A containment check result (the gate check #5 decision-procedure output for a given (operation-scope, certificate-scope) pair) may be cached. A cached result is valid only while: (i) the certificate’s canonical scope formula has not changed (no delta-attestation on the scope expression record or on any governing artifact version it references); and (ii) the operation’s typed scope has not changed. A delta-attestation event on any governing artifact referenced in the scope expression invalidates all cached containment checks for certificates whose scope expression map references that artifact version — the same cascade mechanism as governing specification amendment (§5 delta-attestation lifecycle, cascade obligations).
5.6 Scope expression as a registered artifact
A scope expression record is a registered artifact in the specification registry. It carries: a content-addressed identity; the governing specification version identity it is bound to; the structured form declaration; the canonical scope formula; the scope_derivation_class (static or derived); and, where derived, a reference to its scope derivation witness. It is subject to the delta-attestation lifecycle (§5): amendment to a scope expression record — whether by changing the structured form, updating the canonical scope formula, or rebinding to a new governing specification version — is a delta-attestation event. The delta-classification is determined by the standard classification function (§5.2) applied to the structural difference between the prior and amended scope expression records. A scope-breaking scope expression amendment immediately invalidates all certificates whose Field 5 references the prior scope expression identity.
2.7 Field 6 — Falsifier annotations
Structured annotations of conditions under which the certificate verdict is falsified. Each annotation is a typed record containing:
- condition-type — drawn from a registered taxonomy
- condition-predicate — an order-typed expression
- detection-method — identifies how the condition would be detected in the artifact under certification
- effective-date — the date from which the condition is in effect
The behavioral taxonomy of falsifier conditions, designated (a)–(k), is:
| Label | Condition |
|---|---|
| (a) | Re-training of the target detected by change in the model-weight hash |
| (b) | Source-code amendment detected by change in the source-code hash |
| (c) | Synthesis-correctness-proof invalidation |
| (d) | Interaction-protocol-specification amendment, interacted-with-program version change, or withdrawal of an interaction-protocol-conformance record |
| (e) | Governing-specification amendment processed through a delta-attestation lifecycle where the delta-classification is scope-restricting or scope-breaking |
| (f) | Test-suite-execution failure on the declared re-attestation cadence |
| (g) | Scope-condition exceedance |
| (h) | Empirical-evidence amendment without re-attestation |
| (i) | (Class B only) Interpretation-generation-mapping amendment, withdrawal of joint-authority attestation on the interpretation-generation specification, or invalidation of an intermediate verification step in the interpretation lift |
| (j) | Re-verification traversal (§02a §4b) surfaces a higher-order-analysis gap at an aspect cited by the issued certificate’s declared scope — the relationship between known values of known rules in the governed domain is unresolved at higher-order level |
| (k) | Re-verification traversal (§02a §4b) surfaces a cross-artifact-consistency gap — two or more governing artifacts registered in the specification registry assert inconsistent values at the same domain aspect referenced by the certificate’s declared scope |
Conditions (j) and (k) are traversal-surfaced falsifier conditions: they fire when a governed traversal act during re-verification produces a traversal witness (§02a §4b.4) recording a gap locus of type higher-order-analysis or cross-artifact-consistency at a domain aspect within the certificate’s declared scope. The firing condition is the registration of such a traversal witness, not merely the traversal act itself. The cascade sequence upon firing is identical to that of conditions (a)–(i).
Field 6 carries whichever conditions from this taxonomy are applicable to the issued certificate. Governing-specification conflicts arising from the override layer are also recorded here.
Cascade upon firing. When any falsifier annotation in Field 6 fires, the cascade sequence executes immediately: (i) the audit trail is queried for all downstream operations that admitted artifacts referencing this certificate within the declared retention window; (ii) for each affected operation, a typed cascade record is emitted naming the operation identity, the revoked certificate identity, the cascade timestamp, and the cascade outcome; (iii) downstream consumers that admitted those operations receive notification. This cascade is not optional and may not be deferred by deployment configuration. A falsifier annotation that fires without cascade record emission is a registry conformance failure.
2.8 Field 7 — Order-typed recomputation witness
Field 7 must be an order-typed recomputation witness — a record from which an independent inspector re-derives the verdict and lifted forms from the source under the governing specification. It is not a log, an audit trail, or a pointer to an audit trail. The recomputation witness causally binds the verdict to the cited evidence under the named governing specification — not merely associative co-presence of evidence and verdict. An inspector who holds only Field 7 and the named governing specification must be able to independently re-derive the same verdict; a witness that requires access to internal deployment state, runtime context, or undeclared external resources to reproduce the verdict does not satisfy this invariant.
Order-governed retention content. The recomputation witness is retained under order-governed discipline: what is retained, at what granularity, and under which order-index is governed by the order-decomposition, not by a uniform retention policy. Specifically: a REFUSE verdict retains its falsifier — the affirmative typed evidence of the prohibited act — as a required component of the witness; a REFER verdict retains its coaching record — the typed record of the quality basis of the referral; and where the input carries segment provenance (user-authored, retrieved, or tool-returned), the witness retains provenance per segment as an order-indexed component. A witness that omits the falsifier for a REFUSE verdict, the coaching record for a REFER verdict, or per-segment provenance where provenance was declared is structurally incomplete at Field 7 regardless of whether the verdict itself is correctly recorded. A hash-chained or Merkle tamper-evident log is not a recomputation witness: tamper-evidence detects mutation of a retained record but cannot detect an originally-unsound decision — one that was never altered but was never validly derived from the governing specification. Re-derivation from a recomputation witness detects both mutation and original unsoundness; this is a stronger property than tamper-evidence alone, and the two are not equivalent and not interchangeable as Field 7 content.
Traversal witness retention. Where the certified analysis involved governed traversal (§02a §4b), Field 7 must retain the traversal witness link(s) as required components of the multi-stage witness chain (§02a §5a.2). The full retained chain is: [pre-invocation signal link(s)] → [raw input link] → [IR stage links] → [traversal witness link(s)] → [analysis act links] → [verdict link]. A Field 7 witness that carries analysis-act links and the verdict link but omits traversal witness links — where the underlying analysis used governed traversal — is structurally incomplete. The traversal witness minimum fields are declared in §02a §4b.4; all required fields must be present and re-derivable. An independent inspector re-derives the verdict by traversing this chain from the pre-invocation signal through the traversal positions reached, through the analysis acts, to the verdict; a chain with traversal witness links missing cannot be fully re-derived and does not satisfy Field 7.
Input binding and canonicalizer identity. The recomputation witness binds the verdict to the cited evidence; it additionally carries a content commitment to the public input — the artifact as presented, before canonicalization — and identifies the canonicalization or lift procedure applied to the input by name, version, and content hash, the canonicalizer being part of the trusted base. Where the canonicalization or lift is deterministic, re-derivation includes re-performing it on the public input and comparing the result to the witness’s lifted form, so that a witness that is internally sound but belongs to a different input fails verification. Substitution detection is a strictly stronger property than re-derivation alone: re-derivation detects mutation and original unsoundness; input binding additionally detects a sound witness re-attached to a different input.
Spec-version binding and drift re-binding. The recomputation witness is stamped with the governing-specification version under which the verdict was rendered. This version stamp enables drift re-binding: re-deriving, under a current specification version, whether a previously-rendered verdict retained under an earlier version still holds. A witness without a spec-version stamp does not support drift re-binding and is not a fully conforming Field 7 witness. Drift re-binding is the mechanism by which the delta-attestation lifecycle (§5) propagates through retained witnesses: a scope-restricting or scope-breaking amendment to the governing specification may change the verdict for inputs evaluated under the prior version; the spec-version stamp in Field 7 is what makes that change detectable without re-running the original analysis.
Path-specific forms:
| Certification path | Witness form |
|---|---|
| Classical formal verification | Proof-checker invocation record — re-run the proof checker on the proof-artifact reference against the governing specification; produces the same verdict |
| Empirical characterization | Empirical-replay record — re-compute declared metrics from the empirical-characterization report against the governing specification’s declared scope; same metrics within the declared tolerance ε_inv |
| Test or oracle-backed validation | Test-replay record — re-execute the test suite against the target at the last-pass-execution timestamp; same pass/fail outcome |
| Interaction-protocol | Interaction-protocol-replay record — see below |
Interaction-protocol-replay record. Contains: (i) the protocol specification as of the analysis instant (content-addressed); (ii) the complete interaction trace including all observable external-state transitions; (iii) the analysis method applied to the protocol and trace; (iv) the derivation of the verdict from (i)–(iii). Replay proceeds against the recorded trace, not against a live interaction; non-deterministic external state is encapsulated in the trace. An interaction-protocol-replay record that omits the external-state trace does not satisfy the witness requirement.
2.9 Field 8 — Temporal validity window
Declared issuance timestamp, expiration timestamp, and required re-attestation cadence.
2.10 Field 9 — Tamper-evident cryptographic binding
Computed over all invariant fields of the certificate — at minimum over the canonical Fields 1–8 and over any additional fields present in a conforming extension. Renders the certificate tamper-evident and the verdict attributable. A binding computed only over a subset of the invariant fields does not satisfy this invariant.
Admitted embodiments (non-limiting): digital signature under an EUF-CMA-secure scheme (Ed25519, Ed448, ECDSA/P-256, RSA-PSS, ML-DSA/Dilithium, SLH-DSA/SPHINCS+, FN-DSA/FALCON); keyed MAC (HMAC-SHA256/512/SHA3-256); Merkle inclusion proof in an append-only transparency log; hash-chain or content-addressed commitment; hardware-attestation quote (TPM, Intel SGX/TDX, AMD SEV-SNP, ARM CCA); zero-knowledge proof of the field conditions. The binding means is not the inventive matter.
← What this layer covers · Section index · The specification registry →