# The GAD Formal Specification ## Governed Execution as Decidable Predicates over a Finite Witness **Version 1.3 · Atlas North Institute · July 2026** **Companion to the GAD Manifesto and Glossary. Tool-agnostic. Sections 1 through 11, Section 12A, Section 14, and Section 15 are normative; Section 12B is non-normative. MUST, MUST NOT, and MAY are used in their standards sense. This version incorporates four rounds of external formal review. This document is a Trial 0-ratified implementation specification: Trial 0's record-level results are ratified and recorded in docs/trial-0/. Independent formal and cryptographic review remains pending (Phase 5), and Section 1's results are labeled Propositions and Claims, not Theorems, until it completes. Record-level Trial 0 results do not establish general implementation conformance or GAD-4 defensibility: BUNDLE conformance is demonstrated per-record, permanently, while CONSTRUCTOR conformance and OPERATIONAL conformance require their own inspection and audit under Section 11's three levels, and no passing record confers either on the tooling that produced it. Revisions arrive by succession, only from concrete implementation findings, tracked in the companion specification register. On publication this document is hash-chained and anchored per its own Section 9, and versioned in the open thereafter.** --- ## 0 · Purpose and the core reduction Governed AI Development's prose documents define a doctrine and a method. This specification extracts the algorithms underneath them, so that the status of AI-executed work stops being a judgment and becomes a computation. The core reduction, stated once and load-bearing everywhere: > **Governed execution is a decidable predicate over a finite, integrity-linked witness. Where externally committed, the committed prefix is independently tamper-evident. Contract satisfaction is a separate predicate over the same witness.** Four statuses, in ascending strength: A run produces a core bundle B_core; the evidence envelope E packages it with anchors and later attestations (both defined in Section 2). The statuses are computed over the precise objects: - **VALID_RECORD(B_core):** the core bundle is a structurally sound governed record. - **OUTCOME(B_core) ∈ {COMPLETED, SUPERSEDED, HALTED, INCOMPLETE, INVALID}:** how the run ended. - **CONTRACT_SATISFIED(B_core):** VALID_RECORD(B_core) ∧ OUTCOME(B_core) = COMPLETED, every active obligation verified, and approved where gated. - **DEFENSIBLE(E, Q, Π):** VALID_RECORD(B_core) ∧ the anchors required by policy Π verify over E ∧ a valid independent-evaluation attestation Q exists whose evaluator is independent of the operator under Π. Whether an independent party has checked is a fact about the world, carried by a signed artifact, not a property a bundle can confer on itself. The separation preserves the doctrine's central idea: **a halt can be the system working.** Validity is about the record; satisfaction is about the work; defensibility is about who has checked, under what policy. --- ## 1 · The algorithms, stated whole Given in full before any explanation, first as pseudocode and then as mathematics. Sections 2 through 11 define the terms and defend the design; nothing in them adds a step that is not below. ### Algorithm 1 · CONSTRUCT (the run loop; run by a conforming implementation) ``` CONSTRUCT(intent): P ← author(intent) # human judgment; see Section 10 assert acyclic(P.D); assert wellformed(P) append(freeze, {hash: h(P), plan: canon(P)}) optionally COMMIT(h(P)) # external pre-dispatch anchor; see Section 9 RUN_LOOP: loop: # the run loop is LABELED: RUN_LOOP is the # target every succession exit names if ∀n ∈ active(P): st(n) = APPROVED where risk(n) = gated, st(n) = VERIFIED where risk(n) = normal: append(plan_completed); break if READY(P, W) = ∅ and no pending human resolution: if succession is authorized: SUCCEED(P); break RUN_LOOP # the succession exit is LABELED control flow: break RUN_LOOP leaves # the run loop as a whole, never an inner loop a reader could scope # to; P is terminal as SUPERSEDED, and control lands in the SEALING # section below, which ALWAYS runs as P's record lifecycle, which # outlives the run's terminal (Section 3): checkpointing and export # are never skipped by a succession exit else: append(plan_halted, {unresolved: obligations(P, W)}); break # THE SESSION. The supervised object is THE SESSION, never a single node: # a session is commissioned over a node set, runs, exits, and is closed. # The node remains the unit of obligation, and no node of the session is # verified until the session closes. N_s ← choose_session_scope(READY(P, W)) # the node SET this session covers base ← ENGINE.workspace_baseline() # engine-taken, before spawn session ← {session_id: fresh_session_id(), nodes: N_s, input: ⊕_{m ∈ N_s} (desc(m) ⊕ prior_failure(m)), workspace_baseline_digest: h(base)} # the SESSION OBJECT is constructed explicitly, BEFORE dispatch: it is # the object the dispatch commissions, SUPERVISE_EXECUTOR supervises, # and the executor_exit and execution_result attach to append(dispatch, {session_id: session.session_id, nodes: session.nodes, executor_identity: (model, version, provider), instruction_digest, instruction_ref, workspace_baseline_digest: session.workspace_baseline_digest, input: session.input}) # PER-SESSION (RUL-8, resting REG-19): the dispatch COMMISSIONS a session # over the node set N_s, and names NO single node. One executor session # works many nodes, so naming one node would attribute the whole session's # work to it. Per-node attribution is DERIVED instead; see "Derived # attribution" below. |N_s| = 1 is the one-session-per-node POLICY TIER, # which a trust policy MAY require where the stakes demand engine-observed # per-node deltas; it is a policy tier, not the base requirement. # DISPATCH RESETS: the transition table resets a node's completed attempt # at every dispatch naming it (the completedAttempt reset rule), which is # why the candidates' verdicts are recorded BETWEEN sessions, below. r ← SUPERVISE_EXECUTOR(session, timeout, process_tree_policy, cancellation_policy) # SUPERVISE_EXECUTOR takes THE SESSION, never a single node. The executor # may never return; the supervisor always does: it enforces the budget, # detects process or session loss, terminates descendants per policy, and # yields the SESSION's exit status (full semantics: transition table, REG-1) append(executor_exit, {session_id, # REQUIRED (RUL-12) node: (the single member of N_s if |N_s| = 1, else null), # NULLABLE status ∈ {completed, crashed, timed_out, killed, malformed}, exit_code, available_output_ref, available_output_digest}) # the exit attaches to THE SESSION. session_id is REQUIRED: it is the key # by which an exit pairs with its dispatch, and the only thing the engine # observes at the exit moment. # completed NECESSARILY implies exit_code = 0: an exit whose status reads # completed while its exit code is nonzero is malformed, never completed, # so a status test against completed is total over exit codes (I5). # node is NULLABLE and engine-observed: non-null exactly when the session # covered one node (the POLICY TIER), null when it covered many. Null is # STATED ABSENCE per I5 (RUL-12, mirroring RUL-10 as amended), never a # second key at a different strength. # One session dies once, so a required scalar node here would imply one # exit per covered node and demand a name no honest writer can supply, # forcing exactly the synthesis RUL-8 forbids. # Per-node consequences of a multi-node exit, including which node routes # to FAILED, are DERIVED through the single mechanism below, classed # proxy, never a second mechanism. QUIESCE(session) # stop or isolate the executor process # tree, apply the filesystem settling policy, record the quiescence # outcome; the profile defines what "execution ended" means (REG-2); # surfaces are computed only after quiescence, or they can change # after capture delta ← ENGINE.compute_delta(base, current_workspace) touched ← ENGINE.compute_touched_surface(base, current_workspace, session_monitor) # the session delta and touched surface are captured at SESSION CLOSE, # after quiescence; they are session-level observations of session work append(execution_result, {session_id, # REQUIRED (RUL-10 as amended) node: (the single member of N_s if |N_s| = 1, else null), # NULLABLE delta_ref, delta_digest: h(delta), touched_surface: touched, output_status ∈ {captured, partial, not_recorded}}) # engine-captured; mandatory; exists even when the executor never returned; # dispatch + executor_exit + execution_result = the GAD-1 minimum record # the result attaches to THE SESSION. session_id is REQUIRED: it is the # key by which a result attaches to its dispatch. Its absence is what # broke that join once RUL-8 made the node non-singular for a dispatch # (REG-24). # node is NULLABLE and engine-observed: non-null exactly when the session # covered one node, null when it covered many. Null is STATED ABSENCE per I5, # never a second key at a different strength. # delta and touched_surface are SESSION-LEVEL: they are what the engine # actually observed. Per-node attribution is DERIVED; see below. if r.status = completed and r.claims present: for (m, text) ∈ r.claims: append(claim, {node: m, text}) # optional testimony # THE SESSION IS CLOSED. Everything below runs BETWEEN SESSIONS, in # nobody's session: verification is post-quiescence, over the captured # surface, never a live judgment inside an open session. if r.status ≠ completed: # abnormal exit, including every nonzero # exit code: completed NECESSARILY implies # exit_code = 0, so this condition is total # a FAILED SESSION routes EVERY in-flight node of that session to # retry/trip and NO node of that session to verification: its surface # was captured, its work is not credited for m ∈ inflight(N_s, W): # every node of the session the chain # shows unresolved at session close st(m) ← FAILED enter retry, trip, halt, or succession logic per the breaker rules continue loop C_s ← ENGINE.derive_verification_candidates(N_s, execution_result, bound_output_artifacts(execution_result)) # the VERIFICATION CANDIDATES are DERIVED BY THE ENGINE, AFTER the # session closes, from the closed session's integrity-bound evidence: # the node set N_s, the session's execution_result, and the executor # output artifacts that execution_result binds by digest. Normative # requirements (the Derived candidacy section below): every candidate # MUST belong to N_s; the derivation input MUST be integrity-bound by # the execution_result; attribution is classed proxy when the session # covered multiple nodes; ABSENCE of sufficient bound evidence means a # node is not a candidate (fail closed); the derivation procedure is # CONSTRUCTOR-PUBLISHED: Profile One defines the minimum requirements # for derivation, and each constructor MUST publish and hash-identify # its concrete derivation procedure, which is assessed under # CONSTRUCTOR conformance (the Derived candidacy section below). # Candidacy is a derivation over captured evidence, never a live # judgment inside a session, and it mints no witness entry type. U_s ← N_s ∖ C_s # the EXCLUDED nodes: commissioned by this # session and derived into no candidacy for m ∈ U_s: st(m) ← FAILED, reason: insufficient_bound_evidence enter retry, trip, halt, or succession logic per the existing transition table (governed failure resolution) # the fail-closed promise is PERFORMED by this branch, never only # narrated beside the algorithm: a commissioned node that lacks # sufficient bound evidence after a completed session receives no # verification credit and enters governed failure resolution for m ∈ C_s: # the candidates' verdicts are recorded BETWEEN sessions, strictly after # the session's execution_result and BEFORE any dispatch that names m # again: dispatch resets the completed attempt (the completedAttempt # reset rule), so a verdict recorded inside any later session would # follow a fresh dispatch of its node and be illegal touched_m ← DERIVE_ATTRIBUTION(touched, delta, m) # per-node attribution of the session surface is DERIVED at proxy # against each candidate node's fence, never observed (see "Derived # attribution" below); where |N_s| = 1 the session surface IS the # node's surface and no derivation is needed if touched_m ⊄ m.fence: # engine-captured surface; attribution # derived at proxy, never executor-reported append(flag, {node: m, paths: touched_m ∖ m.fence}) choose action: removal: remove stray work; append(remediation, {node: m, action: removal}) v_s ← ENGINE.scope_recheck(m) append(scope_closed, SIGN_engine({node: m, verdict: v_s})); require v_s = pass succession: SUCCEED(P); break RUN_LOOP # a contract change is not a scope closure; # the predecessor never verifies out-of-fence # work against its old fence. The exit is # LABELED control flow: break RUN_LOOP # leaves the run loop as a whole, never the # inner candidate loop, and control lands in # the SEALING section below, which ALWAYS # runs as P's record lifecycle: checkpointing # and export are never skipped by a # succession exit for t in m.T: v ← ENGINE.evaluate(t) # engine-side; executor has no write path here if v = unavailable: v ← fail # totalization: unknown is fail append(verdict, SIGN_engine({node: m, test: t, capture ∈ {attested_capture, engine_capture}, observation_layers ⊆ {authenticated_engine_observation, independently_replayable}, signal_kind ∈ {direct_observable, worker_authored_proxy}, test_spec_digest, # binds to the frozen contract signal_artifact_digest, # binds to the artifact actually executed subject_digest, env_digest, result: v, output_digests})) if ∀t ∈ m.T: result(t) = pass ∧ eff(v_t) ≥ m.c_min: # eff per eq. 3 if m.risk = gated: append(gate_request, {node: m, findings: engine_refs(m)}) a ← HUMAN() # registered principal; evidentiary basis: # engine findings; executor claims MAY appear # as labeled context append(a.decision = proceed ? approval : refusal, SIGN_who(a)) if a.decision = refuse: st(m) ← REFUSED resolve only by succession, plan_halted, or revised_approval_request after a recorded change; no silent re-entry continue to the next candidate st(m) ← APPROVED else: st(m) ← VERIFIED else: if retries(m) < m.B: append(retry, {node: m, input: failure_output(m)}) # diagnosis, not reroll else: append(trip, {node: m, history: failures(m)}) resolve only by succession or plan_halted # At any point during RUNNING, the side operation SNAPSHOT_SEAL() MAY emit an # immutable snapshot artifact S_k, the sealed prefix of W through checkpoint k, # exported with no terminal plan entry while the run itself continues in # RUNNING; OUTCOME over S_k is INCOMPLETE (Model A, Section 3) SEALING: # the record lifecycle is LABELED and ALWAYS # runs: every exit from RUN_LOOP, including # break RUN_LOOP at a succession exit, lands # here; the run outcome is terminal, and the # record lifecycle continues append(checkpoint, SIGN_engine({range: [a, k-1], digest_over_range})) # a checkpoint at seq k signs [a, k-1], never itself; ranges contiguous and # non-overlapping (or per a declared overlap policy); checkpoints MAY also be # appended periodically during the run under the same rule require every engine-issued, non-individually-signed entry is covered by exactly the checkpoint scheme the bundle declares; final checkpoint after the terminal plan entry; record state ← SEALED EXPORT(): assemble B_core = (P_frozen, W, artifacts, M_core) from immutable sources run VALID_RECORD(B_core) locally if assembly defect (manifest, canonicalization, omitted member): rebuild the candidate from the immutable sources # packaging is repairable if witness or conformance defect (missing event, invalid transition, missing approval, absent probe, open flag, anything backfilled): never repair the historical witness; emit with a nonconformance_notice, or begin a governed successor or remediation run # history is not repairable root_core ← H(dom ‖ canon(M_core)) optionally ANCHOR(root_core) # anchors sign what already exists emit evidence envelope E = (B_core, anchors, attestations, M_envelope) SUCCEED(P): P2 ← AUTHOR_SUCCESSOR(P, unresolved_obligations(P, W)) assert wellformed(P2); freeze P2 (its own witness, its own hash) s ← SIGN_authority({predecessor: h(P), successor: h(P2), reason, named_authority, obligation_map: carried | removed | changed, changed_class_floors, changed_fences, changed_tests}) append(plan_superseded, s) # predecessor terminates as SUPERSEDED ``` **The session-scoped loop is demonstrated, not aspirational (REG-58).** Trial 0's run 20 record (docs/trial-0/) and the supervisor's between-sessions verifier are the demonstrating implementations of this loop: that record carries every verdict strictly between its node's execution_result and the node's next dispatch, and the referee's evaluation computes zero verdict-preconditions errors over it (REG-54). The between-sessions verifier runs before commissioning any session, and once more at completion for a final stranded node, which is exactly where this algorithm places verification: between sessions, after a session closes, in nobody's session. **Derived attribution (RUL-8; RUL-10 as amended).** A session covers a set of nodes, and the engine observes the session: the dispatch it recorded before spawn, the exits, the quiescence, and one session-level delta and touched surface. The node remains the unit of obligation, but per-node attribution WITHIN a session is not observed, it is DERIVED, and this is the single place the specification derives it. It is computed from the closed session's integrity-bound evidence, joined with executor-authored commit boundaries; the engine-log events recording claiming, submission for verification, and verification passes, each timestamped inside the session's window, MAY be consumed by the derivation as inputs, and they are exactly that, engine-log events consumed by the derivation, never formal witness entry types the evaluator sees or requires. It is classed **proxy** and MUST NOT be upgraded, because the engine did not observe those boundaries; the executor authored them, and structure is not history. Where |N_s| = 1 no derivation is needed, because the session's delta IS the node's delta and execution_result names the node directly. **Derived candidacy (REG-61).** The verification candidate set C_s is DERIVED by the engine, never declared by the executor and never defined by an entry type the formal system does not carry. Its inputs are the closed session's integrity-bound evidence: the commissioned node set N_s, the session's execution_result, and the executor output artifacts that execution_result binds by digest. Five requirements are normative. Every candidate MUST belong to N_s. The derivation input MUST be integrity-bound by the execution_result: evidence the result does not bind is not input. Attribution of the evidence to a node is classed proxy when the session covered multiple nodes, through the derived-attribution mechanism above. ABSENCE of sufficient bound evidence means the node is not a candidate: candidacy fails closed (I5), and Algorithm 1's U_s branch PERFORMS that promise rather than narrating it: a commissioned node that lacks sufficient bound evidence after a completed session receives no verification credit and enters governed failure resolution, routed with reason insufficient_bound_evidence to retry, trip, halt, or succession per the existing transition table, never to verification. The derivation procedure is CONSTRUCTOR-PUBLISHED: Profile One defines the minimum requirements for derivation (an execution-result-bound artifact identifying the node and binding its claimed completion boundary, the subject artifacts, and the relevant portion of the session delta), and each constructor MUST publish and hash-identify its concrete derivation procedure, which is assessed under CONSTRUCTOR conformance, per this document's own rule that structure is not history. No new mandatory witness entry type is minted by this derivation, so no sealed record is retroactively orphaned: the engine-log events named in the preceding paragraph MAY inform the derivation, and no condition R1 through R9 requires them, because they are never record types the evaluator sees. Engine-log events MAY be consumed by candidacy derivation only where they are included in, or cryptographically bound by, the session's execution_result or its listed output artifacts. **Synthesized per-node dispatch records are FORBIDDEN.** The supervisor MUST NOT emit a dispatch for a boundary it did not observe. A dispatch is an engine-observed record of a real moment before a real spawn; emitting one per node for a session that covered many manufactures evidence, and a record that says the engine watched something it did not watch is worse than a record that admits it watched a session. Where per-node engine-observed deltas are required, the answer is the one-session-per-node POLICY TIER, which a trust policy MAY demand, and not a synthesized record. The specification does not dictate deployment topology; it states what each topology may honestly claim. **Reading a pre-v0.7 dispatch (REG-29, blessed by succession 2).** An evaluator MAY read a scalar dispatch node in a pre-v0.7 record as the one-member set containing it; this is a spelling of a legal set, never a synthesized boundary. Reading node n as the set containing n invents no boundary the engine did not observe, which is exactly what separates it from the synthesis the preceding paragraph forbids. The blessing is a READ rule for records written before the per-session shape existed, and it authorizes no writer to emit the scalar spelling. **completedAttempt** reads execution_result.node directly when it is non-null, and derives per node through this section when it is null, at proxy. The GAD-1 invariant is unchanged by either succession: dispatch, executor_exit, and execution_result remain the mandatory minimum record, all three engine-captured, and all three exist even when the executor never returns. **The triplet's philosophy is now uniform: dispatch names the commissioned set; exit and result each name the session plus a node only when singularity was observed.** Succession 1 left executor_exit's scalar node standing, because it carried session_id too and its join therefore never depended on node being singular; REG-28 recorded what that survival hid, a semantic fiction in which one exiting process implies one exit per covered node. RUL-12 rests it by mirroring RUL-10 rather than by inventing a second mechanism, and executor_exit now derives its per-node consequences through this section exactly as execution_result does. ### Algorithm 2 · EVALUATE (the computations; runnable by anyone, on any machine) ``` EVALUATE(E = (B_core, anchors, attestations, M_envelope), Π) → (valid, outcome, satisfied) and attestation Q: # Fails closed: any exception, missing field, or unparseable content # in a check makes that check false; VALID_RECORD requires all of R1..R9. VALID_RECORD: # over B_core # R1 · Integrity, issuers, coverage, sealing require M_core lists every member of B_core except itself; every hash matches; root_core = H(dom ‖ canon(M_core)) require M_envelope lists root_core, the anchor artifacts, prior evaluation attestations, and envelope metadata, and excludes itself; root_envelope = H(dom ‖ canon(M_envelope)); each envelope names its predecessor's root_envelope, if any h_prev ← g for e = (body, h) in W in order: require body.seq = prev.seq + 1 # contiguous; story gaps are not sequence gaps require h = H(dom ‖ h_prev ‖ canon(body)); h_prev ← h require issuer(body.τ) per the issuer table (Section 2) require checkpoint ranges contiguous, non-overlapping (or per declared policy), each signing only [a, k-1]; every engine-issued, non-individually-signed entry covered; a final checkpoint follows the terminal plan entry (SEALED), or, for a snapshot, coverage extends through the chain head with no terminal entry (SNAPSHOT_SEAL) # R2 · Recorded precedence (sequence-primary) require unique freeze f; f.payload.hash = h(P_frozen); idx(f) < idx(first dispatch) check wall-clock consistency under the declared clock policy (reference, not order) # R3 · Trace conformance require W ∈ L(C), including: every dispatch followed by executor_exit and an engine-captured execution_result (the GAD-1 minimum), claim optional; executor failure statuses route to FAILED and governed resolution; SEALING follows terminal, or the record is a sealed snapshot # R4 · Verification validity (effective class per eq. 3) for v in verdict entries: require SIG_verify(engine_key, v); require v.result ∈ {pass, fail} require v.capture, v.observation_layers, v.signal_kind declared require v carries test_spec_digest, signal_artifact_digest, subject_digest, env_digest, output digests eff(v) ← min(observation_assurance(v), signal_strength(v)) for n with terminal in {VERIFIED, APPROVED}: require ∀t ∈ T_n: result(v_t) = pass ∧ eff(v_t) ≥ c_min(n) # R5 · Probe binding (feeds signal_strength; binds the executed artifact) worker_authored_proxy reaches proxy strength only with probe q: idx(q) < idx(v) ∧ q.signal_artifact_digest = v.signal_artifact_digest ∧ q.env_digest = v.env_digest ∧ q.result = demonstrated_fail ∧ q.restoration = verified # R6 · Scope closure (engine-observed surface only) require flag.paths derives mechanically from the touched_surface of its referenced engine-authenticated execution_result, and flags close only by removal-remediation plus engine-signed scope_closed pass; succession terminates the plan and never closes a flag in place require no node with an open flag reaches VERIFIED or APPROVED # R7 · Gate completeness for n gated with terminal APPROVED: require gate_request(n) < approval(n) < first consequence entry of n require approval.who ∈ AuthorizedPrincipals(P_frozen) ∧ SIG_verify(cred(who), approval) ∧ approval.findings_ref ⊆ engine entries require refusals, where present, resolve per the REFUSED rule # R8 · Bounded persistence for n: require count(retry(n)) ≤ n.B; trips resolve only by succession or halt # R9 · Typed claims, strength derived from evidence of any kind for c in claims(B_core): require c = (predicate_id, subject_ref, evidence_refs, class, noncoverage, issuer) require every evidence_ref resolves within E to registry-acceptable evidence about the relevant subject, plan, and node support_class(c) ← min over evidence_refs of evidence_strength(e, c.predicate_id, registry) # for verdicts, evidence_strength = eff(v); for approvals, anchors, # successions, checkpoints, scope closures, the registry defines # applicable strength and required provenance require c.class ⊑ support_class(c) ∧ allowed(c.predicate_id, c.class) ∧ c.noncoverage ≠ ⊥ require issuer = machine ⇒ predicate_id ∉ JudgmentPredicates valid ← all R1..R9 OUTCOME: if not valid: outcome ← INVALID else match terminal plan entry: plan_completed → require (recomputed from W) ∀n ∈ active(P): gated ⇒ APPROVED, normal ⇒ VERIFIED; outcome ← COMPLETED plan_superseded → require the mandatory delta; outcome ← SUPERSEDED plan_halted → outcome ← HALTED none → outcome ← INCOMPLETE # reachable: a sealed snapshot has # full chain and checkpoint coverage through its head and # no terminal entry; absent snapshot-seal coverage, R1 # already failed and the outcome is INVALID satisfied ← valid ∧ outcome = COMPLETED q_body ← {root_core, predicate_results: (valid, outcome, satisfied), spec_version, evaluator_identity, evaluator_credential, evaluator_implementation: (name, version, source_or_binary_hash), canonicalization_version, predicate_registry_version, policy: (id, hash), replay_layers_exercised, conformance_suite_version, evaluation_time} Q ← {body: q_body, signature: SIGN_evaluator_key(canon(q_body))} # the signature is never a member of the body it covers DEFENSIBLE(E, Q, Π) ≜ valid ∧ RequiredAnchorsVerify(E, Π) ∧ AttestationValid(root_core, Q) ∧ IndependentUnder(Q.evaluator, operator(B_core), Π) ``` ### The same algorithms, as mathematics **Notation.** The core bundle B_core = (P, W, artifacts, M_core); the evidence envelope E = (B_core, anchors, attestations, M_envelope). W = (e_0, …, e_m), e_i = (body_i, h_i), body_i = (seq_i, t_i, τ_i, p_i): contiguous sequence, wall-clock reference time, type, payload. Classes attested ⊏ proxy ⊏ engine_observed (the prose corpus says server-verified; the property is epistemic, not topological). term_W by replay; L(C) the trace language; Π a trust policy; Q an evaluation attestation; op(B_core) the canonical operator record. **The chain, non-circularly.** > h_0 = H(dom ‖ g ‖ canon(body_0)), h_i = H(dom ‖ h_{i−1} ‖ canon(body_i)), seq_i = seq_{i−1} + 1. (1) Public mode is (1); keyed mode (HMAC_k) is operator-internal only and MUST NOT carry public integrity claims. The core manifest lists every B_core member except itself; root_core = H(dom ‖ canon(M_core)). Anchors sign root_core or declared chain heads, objects that existed before the anchor was issued; they live in the envelope, outside what they sign, which is what dissolves the recursion. **The totalization.** For eval over {pass, fail, ⊥}: > v*(t) ≜ fail if eval(t) = ⊥, else eval(t). (2) **Effective class: two independent axes, layered assurance.** > observation_assurance(v) ≜ attested if capture = attested_capture; > engine_observed if capture = engine_capture and at least one declared layer holds: > authenticated_engine_observation under the disclosed key-custody model, or > independently_replayable with replay succeeding, where Π's replay policy requires > or samples it; the evaluator performs every policy-required replay or fails closed, > so results are deterministic relative to (E, Π, evaluator version). > Layers are a set, not an exclusive mode; both MAY hold, and Q records which were exercised. > > signal_strength(v) ≜ engine_observed if direct_observable; proxy if worker_authored_proxy > with an R5-matching probe on signal_artifact_digest; attested otherwise. > > eff(v) ≜ min(observation_assurance(v), signal_strength(v)). (3) How a result was captured and what kind of signal was evaluated are different questions; the minimum refuses to let strength on one axis launder weakness on the other. **The computations.** > VALID_RECORD(B_core) ≡ ⋀_{i=1}^{9} R_i, each false on any evaluation failure. (4) > > OUTCOME by replay; COMPLETED ⇒ (∀n ∈ active(P)) [gated ⇒ APPROVED] ∧ [normal ⇒ VERIFIED]. (5) > > CONTRACT_SATISFIED ≜ VALID_RECORD ∧ OUTCOME = COMPLETED. (6) > > RequiredAnchorsVerify(E, Π) ≜ anchors ⊇ those Π requires ∧ each verifies over root_core or a declared head; vacuous only if Π requires none; GAD-4 floor: a post-run root anchor, plus a pre-dispatch commitment wherever bounded precedence is claimed. (7) > > DEFENSIBLE(E, Q, Π) ≜ VALID_RECORD ∧ RequiredAnchorsVerify(E, Π) ∧ AttestationValid(root_core, Q) ∧ IndependentUnder(Q.evaluator, op(B_core), Π). (8) > > support_class(c) ≜ min over c.evidence_refs of evidence_strength(e, c.predicate_id, registry), with evidence_strength(v) = eff(v) for verdicts and registry-defined strengths for approvals, anchors, successions, checkpoints, and scope closures; c.class ⊑ support_class(c). (9) **The constructor as a labeled transition system.** C = (Σ, σ_0, R, ε), rules including executor-outcome branching (executor_exit, execution_result), the terminal rules, SUCCEED, the scope branch, the refusal exits, and the post-terminal record lifecycle FROZEN → RUNNING → {COMPLETED, HALTED, SUPERSEDED} → SEALING → SEALED; each rule emits exactly one entry: > σ →_ρ σ′ only if G_ρ(σ), and W′ = W · ε(ρ, σ). (10) **Proposition 1 (Validated export).** If EXPORT emits a core bundle as valid, then VALID_RECORD(B_core) = 1. Definitional, from the fail-closed export rule. **Claim 2 (Constructor preservation).** Assuming conforming implementations of the delegated profile operations, every permitted transition of CONSTRUCT preserves the conditions required for successful validated export; a run terminating through an explicit terminal transition admits a validated export, and plan_completed termination yields CONTRACT_SATISFIED = 1. The nontrivial inductive statement, awaiting independent review; Proposition 1 alone is not soundness of construction. **Claim 3 (Anchored-prefix immutability).** Under collision resistance of H and unforgeability of the timestamp authority's signatures, no p.p.t. adversary can replace an anchored prefix with a different prefix verifying against the same anchor, except with negligible probability. **Proposition 4 (Trace-language membership).** VALID_RECORD = 1 implies W ∈ L(C). **Boundary, stated as prominently as the claims.** Membership is not history. An operator holding the signing keys can fabricate an internally consistent witness, chain it, and anchor it; the evaluator will find it valid-in-language and existent-by-time, and cannot, from structure alone, find it historically caused. An unanchored public chain is integrity-linked, not independently tamper-evident. Narrowing layers, each with its own trust assumptions: signed entries and checkpoints under protected keys; pre-dispatch commitments; externally witnessed checkpoints or a transparency log; assessor inspection of the constructor's write path; runtime or hardware attestation. A conforming envelope MUST declare its layers. The stranger verifies the record without trusting the operator's account of it; the stranger cannot verify history without trusting, or checking, at least one component that touched it. **Complexity, qualified.** Structural evaluation of R1 through R9 and OUTCOME runs in O(|W| + |P|) under indexed lookup and fixed-cost cryptographic-verification assumptions. Policy resolution, certificate-path validation, transparency checks, and replay execution are additional and bounded by their declared scopes. --- ## 2 · Objects **Plan.** P = (N, D, meta) with the authority registry AuthorizedPrincipals(P). Canonical serialization; hash h(P). FROZEN plans change only by SUCCEED. **Node.** n = (desc, fence, T, c_min, risk, B): allowlist fence; decidable done-tests; class floor; risk; retry bound. **Executor exit.** Engine-issued per session: {session_id, node, status ∈ {completed, crashed, timed_out, killed, malformed}, exit_code, available_output_ref, available_output_digest}, with session_id REQUIRED as the pairing key and node NULLABLE per RUL-12: non-null exactly when the session covered one node, null when it covered many, the null a stated absence per I5. Per-node consequences of a multi-node exit are derived, classed proxy, through the derived-attribution section of Algorithm 1. status = completed NECESSARILY implies exit_code = 0: an exit reporting completed with a nonzero exit code is malformed, never completed, which makes a status test against completed total over exit codes (I5). An executor that never returns still yields this entry: absence is evidence, not a missing transition. **Execution result.** Engine-captured, mandatory per dispatch: {session_id, node, delta_ref, delta_digest, touched_surface, output_status ∈ {captured, partial, not_recorded}}, with session_id REQUIRED as the pairing key and node NULLABLE per RUL-10 as amended: non-null exactly when the session covered one node, null when it covered many, the null a stated absence per I5. Delta and touched surface are session-level, computed by the engine from the workspace baseline and session monitor, never taken from executor output; per-node attribution of a multi-node result is derived, classed proxy, through the derived-attribution section of Algorithm 1. Dispatch, executor_exit, and execution_result together are the GAD-1 minimum record; claim is optional testimony. **Verdict.** Engine-signed: {node, test_id, capture ∈ {attested_capture, engine_capture}, observation_layers ⊆ {authenticated_engine_observation, independently_replayable}, signal_kind ∈ {direct_observable, worker_authored_proxy}, test_spec_digest, signal_artifact_digest, subject_artifact_digest, environment_digest, result ∈ {pass, fail}, exit_code, stdout_digest, stderr_digest, engine_identity, engine_signature}. test_spec_digest binds the verdict to the frozen contract; signal_artifact_digest binds it to the artifact actually executed, which for worker-authored suites can change while the plan's command stays constant, and that is exactly why the probe binds to it. Effective class is computed per equation (3), never declared. **Probe.** Engine-signed: {signal_artifact_digest, environment_digest, induced_defect, demonstrated_result = fail, restoration = verified, t}. **Claim (typed, evidence-derived).** {predicate_id, subject_ref, evidence_refs, evidence_class, noncoverage, issuer_type}. The predicate registry defines, per predicate: permitted issuer types, minimum class, required evidence shape, required noncoverage fields, and the evidence_strength rules for non-verdict evidence. Declared class never exceeds support_class (equation 9). JudgmentPredicates are never machine-issuable. Lexical scanning of rendered prose is non-normative lint. **Gate records, succession record, checkpoint.** As in v0.4, with SUCCEED the only emitter of successions, and checkpoints at seq k signing [a, k-1], never themselves, contiguous and non-overlapping or per a declared overlap policy, individually engine-signed, with a final checkpoint required after the terminal plan entry. **Operator record (canonical).** op(B_core) = {legal_or_organizational_identity, operator_credential, implementation_identity, organizational_unit, engagement_or_lane_id}. A required B_core member; IndependentUnder evaluates named parties against Π, never an undefined function over bytes. **Signed objects, globally.** Throughout this specification, SIGN_x(obj) denotes the pair {body: obj, signature: sig_x(canon(obj))}: the signature covers the canonical body and is never a member of it. The construction applies uniformly to verdicts, probes, scope closures, checkpoints, approvals, refusals, successions, nonconformance notices, and attestations, and the schemas encode it as such. **Evaluation attestation.** Q = {body: q_body, signature} per Algorithm 2, the body carrying root_core, the predicate results, and the full evaluator description (implementation hash, canonicalization and registry versions, policy hash, replay layers exercised), so two attestations are comparable as evaluations, not just verdicts. Q lives in the envelope, never in the core it evaluates. **Core bundle and evidence envelope.** B_core = (P_frozen, W, artifacts, M_core), root_core = H(dom ‖ canon(M_core)). E = (B_core, anchors over root_core or declared heads, attestations, M_envelope). The anchor signs what existed before it was issued. M_envelope lists root_core, the anchors, prior attestations, and envelope metadata, excludes itself, and yields root_envelope = H(dom ‖ canon(M_envelope)). Envelopes are versioned snapshots naming their predecessors: E_0 packages the core and its anchors; an evaluation of E_k yields Q_{k+1}; E_{k+1} = E_k + Q_{k+1}, because an envelope existing before an evaluation cannot already contain that evaluation's attestation. **Issuer table (normative).** Engine-signed individually: verdict, scope_closed, probe, checkpoint, nonconformance_notice. Principal-signed: approval, refusal. Authority-signed: plan_superseded (via SUCCEED; the successor's freeze lives in the successor's own witness, engine-issued there). Engine-issued, checkpoint-covered (or individually signed, per the bundle's declared scheme): freeze, dispatch, executor_exit, execution_result, claim (executor-attributed in content, engine-captured as a record), flag, remediation, retry, trip, gate_request, revised_approval_request, plan_completed, plan_halted, and sealing events where represented. **Trust policy.** Π declares: required anchors (equation 7), clock policy, IndependentUnder, accepted credential authorities, accepted provenance layers, accepted evaluator implementations, and a replay policy ∈ {none, required_for(test classes), required_for(all replayable completion evidence), sampled(declared rule)}. The evaluator performs every policy-required replay or fails closed, which makes evaluation results deterministic relative to (E, Π, evaluator version) rather than evaluator-dependent. Published, identified, hashed; a defensibility claim without a named Π is unscoped and therefore meaningless. Write-time rules (I3) apply throughout: entries at their moment, first capture wins, absence recorded as absence, additive schema, no backfill path. --- ## 3 · State machines **Plan and record lifecycle.** DRAFT → FROZEN → RUNNING → {COMPLETED, SUPERSEDED, HALTED} → SEALING → SEALED. SNAPSHOT_SEAL is a side operation, not a state: RUNNING, via SNAPSHOT_SEAL, returns to RUNNING, emitting an immutable snapshot artifact S_k, the sealed prefix of W through checkpoint k, with no terminal plan entry, while the live run continues undisturbed. Terminals are run outcomes, reached only by their explicit entries and recomputed at evaluation time; SEALING and SEALED describe the record lifecycle, in which checkpoints, nonconformance notices, and export occur after the operational terminal without contradiction; snapshots are artifacts of the lifecycle, never states of the run. A sealed snapshot evaluates as VALID_RECORD with OUTCOME = INCOMPLETE, which makes interrupted and long-running executions first-class records for recovery and incident analysis, and even defensible ones, since DEFENSIBLE never required completion. **Node states.** PENDING → READY → DISPATCHED → (executor_exit) → {CLAIMED, FAILED} → VERIFYING → {VERIFIED, FAILED}, with: executor statuses other than completed routing to FAILED and the breaker rules; gated nodes passing VERIFYING → AWAITING_APPROVAL → {APPROVED, REFUSED}, the good gated terminal being APPROVED; FAILED → DISPATCHED at most B_n times, diagnosis-shaped; then TRIPPED, exiting only via succession or plan halt; flags closing only through removal plus engine-signed recheck, succession terminating the plan instead; REFUSED exiting only via succession, plan halt, or revised_approval_request. **The witness invariant.** Every transition appends exactly one entry at its moment. --- ## 4 · Succession Only by SUCCEED, and the honest claim: **quiet erosion is unrepresentable.** Weakening remains possible, only through an explicit, attributed, signed record preserving the predecessor and stating every delta. A succession terminates its predecessor; it never legitimates out-of-fence work or closes obligations in place. Ritualized succession is a pattern assessors read for. --- ## 5 · The constructor, explained Algorithm 1's v0.5 refinements exist because review found the loop assuming what the methodology's own founding record disproved: that executors return. The executor-outcome branch makes death, timeout, kill, and malformed output first-class: executor_exit records what happened, execution_result records what the engine observed regardless, and the GAD-1 minimum survives an executor that vanishes, because absence is evidence, not a missing transition. The touched surface and delta are engine-computed from the baseline and the session monitor, never read from executor output, because the party being fenced does not get to report its own position relative to the fence. The checkpoint rule is exact (sign [a, k-1], never yourself; cover everything unsigned; final checkpoint after terminal), and the SEALING phase lets the record's lifecycle outlive the run's terminal without the transition language contradicting itself. Export's repair boundary stands: packaging is rebuildable from immutable sources; history is not repairable, only disclosed or remediated by a new governed run. Three properties remain normative: the executor has neither a write path to verdicts nor any signing key; the contract the loop reads is the frozen one, addressed by hash; every branch appends. **Verification is a read (REG-37).** VERIFYING under a public key is a READ of public material and does not cross a signing boundary; signing boundaries govern what keys SIGN. --- ## 6 · The computations, explained **R1** binds bytes to sequence, entries to issuers, and unsigned engine entries to checkpoint coverage, through sealing. **R2** is sequence-primary; wall clocks are reference under the declared clock policy. Recorded precedence is order inside the record; bounded precedence needs a pre-dispatch commitment. **R3** is membership, not history, and now requires the executor-outcome structure: every dispatch has its exit and its engine-captured result, claim optional, failures routed to governed resolution. **R4 and R5** implement equation (3): capture type, observation layers as a set (both may hold; Q records which were exercised), signal kind, and the minimum governing. The probe binds to signal_artifact_digest, the artifact actually executed, because a worker-authored suite can change while the plan's command string does not. **R6** is bundle-checkable exactly this far: flag paths must derive mechanically from the touched surface in their referenced engine-authenticated execution_result, closure requires the observed recheck, and successions terminate rather than close. That the engine genuinely computed that surface from the baseline, rather than fabricating it, is constructor conformance, per this document's own rule that structure is not history. **R7** is decidable exactly as far as bytes allow; the registry's correspondence to reality is an assessment question. **R8:** bounded, diagnosis-shaped, governed exits. **R9** generalizes strength beyond verdicts: evidence_strength(e, predicate, registry) covers approvals, anchors, successions, checkpoints, and scope closures, with eff(v) as its verdict case, so a claim's declared class never exceeds what its actual evidence, of whatever kind, supports. **OUTCOME** enforces the gated distinction per (5); **CONTRACT_SATISFIED** composes; **DEFENSIBLE** is issued over the envelope, with the operator a canonical named record and the attestation describing the evaluator itself. --- ## 7 · The six invariants - **I1 · Contract precedence.** T from P by hash; R2 by sequence; pre-dispatch commitments where bounded precedence is claimed. (R1, R2, Section 9.) - **I2 · Producer never grades.** No write path, no keys, engine-computed surfaces and deltas, and effective class computed on axes the producer cannot collapse. (R4, R5, R6, equation 3.) - **I3 · Witness at the moment.** Contiguous sequence, non-circular chain, issuer and checkpoint coverage, sealed lifecycle, anchors binding anchored prefixes (Claim 3), absence as a value, and the executor-outcome rule making even a vanished worker leave evidence. Structure is not history, stated beside the claims. (R1, R3, anchor rules.) - **I4 · Named human at consequence.** Registered principals, credential signatures, ordering, gated completion meaning APPROVED enforced in OUTCOME. (R7, equation 5.) - **I5 · Unknown is fail.** Totalization (2); allowlist fences over engine-observed surfaces; breakers; executor failure as first-class FAILED; the evaluator's exception semantics; fail-closed export with its repair boundary. (R4, R6, R8, both algorithms.) - **I6 · Claims carry boundaries.** Evidence-derived typed claims over all evidence kinds, mandatory noncoverage, machine judgments unrepresentable. (R9, equation 9.) --- ## 8 · The ladder, restated formally - **GAD-1 · Recorded:** the minimum record (dispatch, executor_exit, execution_result) exists for every executor invocation, engine-captured at the moment, and Algorithm 1 emits it by construction, including when the executor never returns. - **GAD-2 · Verified:** engine-side evaluation with two-axis effective classes and bound probes holds over the lanes claimed, **and every completion-crediting done-test requires effective class of at least proxy. Attested evidence MAY be retained as context and MUST NOT independently satisfy a completion obligation.** Without this floor the ladder would permit verified-by-attestation, which contradicts the discipline's central principle; c_min = attested remains legal for nodes whose obligations are explicitly testimony-recording, and such nodes do not count as completion-crediting. - **GAD-3 · Governed:** VALID_RECORD holds, R1 through R9, with GAD-2's evidentiary floor carried cumulatively. - **GAD-4 · Defensible:** DEFENSIBLE(E, Q, Π) under a published policy whose floor requires a post-run root anchor, plus a pre-dispatch commitment wherever the organization claims against outside challenge that its contracts predate its work; serialization-deterministic export; Q from an evaluator independent of the operator under Π. Level four is a property a bundle has demonstrated, and Q is the receipt. **Relation to the prose ladder.** The prose corpus is the practice register; this specification is the formal floor; where they differ, this document governs formal conformance claims, and the corpus carries a reconciliation note pointing here. Cumulative floors; an organization's level is the minimum over lanes it must stand behind. --- ## 9 · Time, anchoring, and export **Anchors** are RFC 3161 tokens or transparency-log inclusions over root_core or declared chain heads, held in the evidence envelope as immutable sidecars: the anchor signs what existed before it, and the envelope construction makes self-coverage unrepresentable. An anchor proves existence no later than its token time; it does not validate internal timestamps. **Anchor policy.** Per Π and equation (7); vacuous satisfaction impossible against a policy that requires anchors. GAD-4 floor: post-run root anchor always; pre-dispatch commitment where bounded precedence is claimed. **Pre-dispatch commitment.** Externally commit h(P) before first dispatch where bounded precedence is claimed; otherwise precedence claims are recorded precedence and MUST be labeled as such. **Export determinism.** Serialization determinism over the same immutable snapshot, schema, and anchor set; later anchors attach to a newly declared envelope snapshot. EXPORT validates before emitting, fails closed, and honors the repair boundary. **Key material, defined (REG-38).** A value IS key material iff it parses as a private key (PEM or DER PKCS#8) or derives a public key the tree trusts (including HMAC-derivation checks against held secrets). Pattern-matching on length or encoding is NOT a conforming check, because a secret scalar has no detectable shape (every 32-byte string is a valid Ed25519 seed); a conforming check asks what a value DERIVES, never what it looks like. Key-hygiene checks, including any check that key material never entered a repository, a state file, or an export, are judged against this definition. --- ## 10 · What this specification does not do **CONTRACT_SATISFIED is relative to P.** Adequacy of P is human judgment under the published assessment protocol. **Structure is not history.** Integrity, conformance, ordering, and bounded time; never that events physically occurred. Provenance is a declared, layered property; an unanchored chain is integrity-linked, not independently tamper-evident. **Gates prove authorization, not competence.** Registry membership and a credential signature, in order, over engine findings; a hollow gate produces a valid record of hollowness. **Truth and quality are out of scope.** No computation proves software good, secure, or fit for purpose, and by R9 no conforming system can express such a machine claim, because no evidence could support it. **Assumptions, enumerated.** Collision resistance of H; unforgeability and custody of engine, principal, evaluator, and timestamp-authority keys; append-only custody between anchors; capture completeness at the tooling boundary, including the session monitor's coverage of the touched surface; correctness of the stranger's evaluator and replay implementations; accuracy of the independence policy's organizational registry. --- ## 11 · Conformance, in three levels, and conformance trials **Bundle conformance:** a specific envelope passes EVALUATE. **Constructor conformance:** write-isolation, key separation, at-the-moment capture with no backfill path, engine-computed surfaces and deltas, the executor-outcome branch, the checkpoint and sealing rules, the export repair boundary; established by inspection under the published protocol. **Operational conformance:** key custody, access control, retention, clock policy, anchor cadence, capture coverage; established by operational audit under Π. Full implementation conformance requires all three. **Conformance trials.** Designed scenarios, real execution, adversarial intent. **Trial 0: the reference implementation audited against this specification, gap register published either way.** Then per condition family: tamper-and-manifest including issuer and checkpoint coverage (R1); precedence with and without pre-dispatch commitment (R2); executor-failure capture, the founding-record scenario replayed under the formal rules (R3); totalization (R4); two-axis class and probe binding, including the replayed-proxy laundering attempt and the mutated-suite attempt equation (3) and signal_artifact_digest exist to stop (R4, R5); scope closure including the succession branch and an executor-misreported surface (R6); approval authority (R7); breaker (R8); typed claims with unsupported-class attempts across evidence kinds (R9); and the stranger-verification trial, an independent party running EVALUATE cold and emitting a real Q. If a modified witness ever fools the evaluator, the finding publishes with the failing bytes; the measure's integrity outranks its stability. **The probe-fired standard (REG-39).** A planted-defect probe counts as FIRED only if it really spawned, exited NONZERO, and produced OUTPUT; conforming tooling judges probes by all three. A spawn failure also exits nonzero, and an exit code alone cannot distinguish a probe that proved its check can fail from a probe that never found its runner; the output is what separates them. --- ## 12A · Profile One: Governed AI Development (normative) Unit of work: a node of development work. Fence vocabulary: filesystem and repository paths. Done-test observables: command exit codes, HTTP observations, filesystem and database assertions, page-level checks, with capture type, observation layers, and replay support declared per observable. Consequence criteria: production-touching, data-destroying, or otherwise irreversible changes. Profile obligations owed at implementation: complete touched-surface detection (baseline workspace state, tracked and untracked files, symlinks, writes outside the repository, concurrent modification, declared handling of network side effects), workspace baseline and delta digest procedures, session-monitor coverage, the quiescence condition defining "execution ended" (process-tree stop or isolation, filesystem settling policy, recorded quiescence outcome), and the observation procedure for each declared done-test type. **Candidacy derivation minimums (REG-64, Option B).** Profile One defines the minimum requirements for verification-candidate derivation, never the concrete procedure: an execution-result-bound artifact identifying the node and binding its claimed completion boundary, the subject artifacts, and the relevant portion of the session delta. Each constructor MUST publish and hash-identify its concrete derivation procedure, and the published procedure is assessed under CONSTRUCTOR conformance. Meeting the minimums does not by itself confer candidacy: absence of sufficient bound evidence still fails closed, per Algorithm 1's U_s branch. **Key lifecycle (REG-14).** AuthorizedPrincipals(P) binds each principal's public material into the frozen plan, each key carrying a stable key_id, an algorithm, and a custody_statement. A key_id supersedes a prior one only through a SIGNED LIFECYCLE ENTRY naming both ids and the effective boundary. REVOCATION IS FORWARD-LOOKING: a revoked principal's past signatures remain valid for the records they signed; revocation withdraws authority from signatures not yet made, never validity from records already signed. Rotation and revocation events are recorded as signed lifecycle entries in the succession record stream. Until an implementation of these entries lands, a compromised key is handled by succession (a new frozen plan with a new registry); that is the interim rule already in force, stated here rather than improvised at the incident. Implementation of rotation and revocation remains post-v1.0 work; this paragraph fixes the design that implementation must conform to. **On the reference implementation, stated per this document's own rules:** GAD is the only profile with a reference implementation and published operational witnesses. Trial 0 established record-level bundle conformance for one specifically identified record under named artifacts (docs/trial-0/: the conformance matrix, the operator-signed ratification manifest, and the RFC 3161 anchor). It did not establish constructor-wide conformance, operational conformance, or general implementation conformance: BUNDLE conformance is demonstrated per-record, permanently; CONSTRUCTOR and OPERATIONAL conformance require their own inspection and audit under Section 11's three levels, and no passing record confers either on the tooling that produced it. Grandfathering the tooling into conformance would be exactly the counterfeit this specification defines. ## 12B · Candidate profiles (non-normative) Browser and computer-use agents, financial back-office work with its maker-checker ancestry, customer operations, healthcare administration, legal drafting, and data pipelines are deferred to a separate discussion paper. No conformance is claimed for any. The transfer boundary is decidability: where done cannot be written as an observable, these computations claim nothing, and the two-ledgers rule generalizes instead. --- ## 13 · Lineage and neighbors Closest ancestors, led honestly: **certifying algorithms**; **proof-carrying code and proof-carrying data**; **design by contract**; **in-toto layouts**, the nearest formal ancestor of the frozen plan; **authenticated data structures and transparency logs**; **RFC 3161** with the Haber and Stornetta line. The complexity-theoretic asymmetry is calibrated intuition, not a load-bearing claim: the checker does not trust the witness, it checks it. What this specification assembles, and as far as its author can determine no prior published methodology assembles, is that pattern applied to AI-agent development end to end, with the evaluator small, the computations separated, and the witness anchorable; contemporaneous preprints on evidence-sufficiency grading and oversight calibration are cited as neighbors, because I6 applies to specifications too. --- ## 14 · Versioning, stewardship, and companion machinery Versioned in the open; changes as successions with deltas stated; games met with published counters; the measure's integrity outranks its stability. **Companion machinery before any claim of implementable standard:** (1) canonical bundle and envelope schemas; (2) exact canonicalization specification; (3) full transition table for C; (4) predicate registry with evidence-shape and evidence_strength rules; (5) trust-policy schema; (6) valid and invalid test vectors; (7) minimal open reference evaluator; (8) conformance test suite; (9) independent formal and cryptographic review. **Per the stewardship record of this version: the companion machinery items (1) through (8) were produced and exercised through Trial 0; item (9), independent formal and cryptographic review, is the pending item. Until it completes, GAD is a ratified implementation specification, not an independently validated standard.** **Version history.** v0.1 (July 12, 2026): initial draft; single predicate; theorem labels. v0.2: first review round; predicate split; causation claims replaced by immutability and membership; explicit terminals; non-circular chain; signed verdicts; bound probes; observed scope closure; recorded versus bounded precedence; typed claims; trials. v0.3: second round; DEFENSIBLE(B, Q, Π); policy-scoped anchors; computed effective class and fail-closed export; attested mode; gated OUTCOME; three-level conformance; sequence-primary ordering; succession procedure; ladder-corpus relation; Trial 0; integrity-linked language. v0.4: third round; two-axis effective class; evidence-derived claim strength; corrected scope branch; Proposition and Claim split; export repair boundary; explicit GAD-1 payloads; issuer table; contiguous sequence; normative profile split; extended attestation; qualified complexity. v0.5 (July 12, 2026): fourth round, semantic changes enumerated: executor failure made first-class via executor_exit and mandatory engine-captured execution_result, so the GAD-1 record survives a vanished executor and absence is evidence, with claim demoted to optional testimony; touched surfaces and deltas made engine-computed from baseline and session monitor, removing the executor's authority over its own fence position; the checkpoint lifecycle made exact, ranges signing only their past, coverage required, final checkpoint after terminal, and a SEALING record phase added so terminal means terminal without contradiction; the bundle split into core and evidence envelope with anchors signing root_core, dissolving the anchor self-coverage recursion; a GAD-2 evidentiary floor added, completion-crediting done-tests at proxy or better, closing the verified-by-attestation loophole; test identity split into test_spec_digest and signal_artifact_digest with probes bound to the executed artifact; observation layers made a set over a base capture type, with exercised layers recorded in Q; the issuer table completed (probe, executor_exit, execution_result, revised_approval_request, nonconformance_notice, successor freeze, sealing) and claim strength generalized via evidence_strength over non-verdict evidence; the operator made a canonical record for independence evaluation; and prose expansion frozen in favor of Trial 0 and the reference evaluator. v0.6 (July 12, 2026): fifth-round triage, minimal corrective revision, semantic changes enumerated: INCOMPLETE made reachable via Model A, the SNAPSHOT_SEAL side operation emitting valid sealed snapshot artifacts with coverage through the head and no terminal entry, evaluating as VALID_RECORD with OUTCOME = INCOMPLETE; the envelope manifest defined non-recursively, M_envelope excluding itself with root_envelope and versioned envelope lineage E_{k+1} = E_k + Q_{k+1}; R6 restated as bundle-checkable mechanical derivation from the referenced engine-authenticated execution_result, with genuine computation assigned to constructor conformance per structure-is-not-history; replay made policy-deterministic via the trust policy's replay_policy with fail-closed execution of required replays, removing evaluator-dependence; the executor call restated as SUPERVISE_EXECUTOR with normative supervisor semantics deferred to the transition table (REG-1); a quiescence barrier added before surface and delta computation, with the operational definition owed by the profile (REG-2); checkpoint schema details routed to the specification register and test vectors (REG-3). No other sections altered; the prose freeze holds, and further revisions arrive only from implementation findings recorded in the register. Final consistency pass before freeze, three edits: the opening statuses normalized to their precise objects, VALID_RECORD, OUTCOME, and CONTRACT_SATISFIED over B_core and DEFENSIBLE over the envelope E; SNAPSHOT_SEAL restated as a side operation from RUNNING back to RUNNING emitting the immutable snapshot artifact S_k, so the live run has no undefined route back; and signed objects made uniformly self-reference-free, SIGN_x(obj) = {body: obj, signature: sig_x(canon(obj))}, with the evaluation attestation restated accordingly. **v0.6 is FROZEN as the Trial 0 specification candidate.** v0.7 (July 15, 2026): succession 1, performed under the ceremony Section 15 introduces (RUL-9, rested July 15, 2026), recorded in the signed sidecar delta beside this document and cited by the companion specification register. Semantic changes enumerated: Section 15 added, defining specification succession as an object distinct from plan succession, with its object this document's byte digest, its authority the named operator, and its signed delta carrying predecessor and successor digests, the register entries and rulings discharged, a section-level statement of what changed and why, a CONSEQUENCES section for the structural couplings the amendment severs, the invalidated downstream artifacts named by class against the cited digest of a manifest computed from the trees, and an explicit statement of what the successor does not claim; and the declared normative range amended so that Section 14's stewardship rule and Section 15's ceremony both fall inside it, the defect closed being that a change rule outside the normative range is decorative. Succession 1 is genesis, and Section 15 discloses it as such rather than claiming an authority v0.6 never gave. v0.8 (July 15, 2026): succession 2, recorded in the signed sidecar delta beside this document and cited by the companion specification register. **Succession 2 is the first specification succession performed under a rule that PREDATES it:** Section 15's ceremony was introduced by v0.7, not by this document, which is succession 1's genesis disclosure making good on what it promised. Semantic changes enumerated: executor_exit's node made NULLABLE under RUL-12, resting REG-28, mirroring execution_result under RUL-10 as amended rather than inventing a second mechanism, non-null when the session covered exactly one node (engine-observed, the one-session-per-node policy tier) and null when it covered many, the null a stated absence per I5, pairing by session_id, which is the only thing the engine observes at the exit moment, and per-node consequences of a multi-node exit, including which node routes to FAILED, derived through the single RUL-8 derived-attribution mechanism and classed proxy; the defect closed being that one session dies once, so a required scalar node on the exit record implied one exit per covered node and would have demanded of Atlas a node name no honest writer could supply, forcing the synthesis RUL-8 forbids. With it the triplet's philosophy becomes uniform: dispatch names the commissioned set; exit and result each name the session plus a node only when singularity was observed. Also added, discharging REG-29 and closing it: the blessing that an evaluator MAY read a scalar dispatch node in a pre-v0.7 record as the one-member set containing it, a spelling of a legal set and never a synthesized boundary, which preserves the historical invalid fixtures byte-identical and moves the concession out of one tool's source and into the normative text where it is judged; the invalid-fixture generator remains future work and is not claimed here. v0.7's and v0.6's history entries stand intact as fact, and succession 1's genesis disclosure is neither softened nor restated. v0.9 (July 16, 2026): succession 3, recorded in the signed sidecar delta beside this document and cited by the companion specification register. Four additive amendments, clarifications and definitions resting the register entries REG-14, REG-37, REG-38, and REG-39, with no existing normative sentence weakened: REG-14, the Profile One key lifecycle design (a key_id supersedes a prior one only through a signed lifecycle entry naming both ids and the effective boundary; revocation is forward-looking, a revoked principal's past signatures remaining valid for the records they signed; rotation and revocation events recorded as signed lifecycle entries in the succession record stream; a compromised key handled by succession until an implementation lands, which remains post-v1.0 work); REG-37, the ruling that verifying under a public key is a read of public material and does not cross a signing boundary, signing boundaries governing what keys sign; REG-38, the normative definition of key material (a value is key material iff it parses as a private key or derives a public key the tree trusts; pattern-matching on length or encoding is not a conforming check, because a secret scalar has no detectable shape); and REG-39, the probe-fired standard (a planted-defect probe counts as fired only if it really spawned, exited nonzero, and produced output; conforming tooling judges probes by all three). All earlier history entries stand intact as fact, and succession 1's genesis disclosure is neither softened nor restated. v1.0 (July 2026): succession 4, ratification and status transition, its signed record at succession/delta/succession-4.json: ratified by Trial 0, recorded in docs/trial-0/: the conformance matrix, the operator-signed ratification manifest, and the RFC 3161 anchor. Independent formal and cryptographic review pending (Phase 5). No normative text changes. v1.0 asserts ratification of Trial 0's record-level results, never general conformance; Section 1's results remain labeled Propositions and Claims, not Theorems, until independent review completes. v1.1 (July 2026): succession 5, status truth and the session-scoped Algorithm 1, its signed record at succession/delta/succession-5.json: three pre-Trial-0 status passages corrected to the post-ratification truth; Algorithm 1 made session-scoped, discharging REG-58; no conformance requirement weakened. v1.2 (July 2026): succession 6, the type-completeness amendment, its signed record at succession/delta/succession-6.json: C_s derivation made engine-derived and fail-closed, discharging REG-61; succession numbering made explicit in this history, each named entry citing its signed record file; bundle conformance narrowed, with constructor and operational conformance requiring their own inspection and audit; session construction, succession termination, and exit code semantics clarified; no conformance requirement weakened. v1.3 (July 2026): succession 7, the transition-completeness amendment, its signed record at succession/delta/succession-7.json: the U_s branch closing the fail-closed loop in the algorithm; candidacy made constructor-published under Profile One minimums; succession exits made labeled control flow into SEALING; the draft label retired; engine-log binding pinned; no conformance requirement weakened. --- ## 15 · Specification succession **This section is normative, and it defines the only ceremony by which this document changes.** Section 14 states the stewardship posture; this section states the procedure that posture requires. A change rule outside the declared normative range is decorative, which is why this section and Section 14 are inside it. **A specification succession is a distinct object from plan succession and borrows nothing from it.** SUCCEED(P), given in Section 1 and restated in Section 4, operates on a plan P = (N, D, meta) and appends plan_superseded to that plan's witness. **SUCCEED does not apply to this document, and a specification succession MUST NOT be performed by it, nor borrow its shape, its authority, or its record.** A specification has no witness to append to, no node set, no dependency edges, no fence, and no AuthorizedPrincipals(P) registry; SUCCEED's signed payload is typed to obligation_map, changed_class_floors, changed_fences, and changed_tests, not one of which is a thing a specification has. The two ceremonies share a name and nothing further. Plan succession terminates its predecessor as SUPERSEDED; specification succession supersedes a frozen document, which has no terminal state to enter. **Object.** The object of a specification succession is this document, identified by the byte digest of its frozen text. Predecessor and successor are named by digest and never by version label alone: a label is not an identity. **Authority.** The authority is the operator, named in the record. No other party MAY perform a specification succession; in particular the executor of a governed run MUST NOT perform one, and a ruling recorded in the companion register is not itself an amendment of this document. **The delta.** A specification succession's signature is over a spec-succession delta. The delta MUST carry, and a succession whose delta omits any of them is not a succession: 1. the predecessor spec digest; 2. the successor spec digest; 3. the register entries and rulings the amendment discharges, cited by identifier; 4. a section-level statement of what changed and why; 5. a CONSEQUENCES section naming the structural couplings the amendment severs. This is distinct from item 6 and MUST NOT be merged into it: a broken join is not a stale byte. An invalidated artifact is regenerated from its sources; a severed coupling must be re-derived by a decision, and listing it as though it were a stale byte hides that decision; 6. the identity of every downstream artifact whose bytes the amendment invalidates, named BY CLASS, with the cited digest of a manifest COMPUTED from the trees. The manifest MUST be computed and MUST NOT be a hand-typed list: such a list is stale the moment any of its members moves, and a recited figure is not a computed one; 7. an explicit statement of what the successor does not claim. **The record.** The record of a specification succession lives in gad-protocol as a signed sidecar beside this document, and the companion specification register cites it. The register remains the channel through which this document learns that it must change; the succession is how it changes. **Numbering.** Specification successions are NUMBERED in sequence from 1. **v0.6 to v0.7 is succession 1.** **Genesis disclosure for succession 1.** Succession 1 is performed under a ceremony that v0.7 itself introduces. v0.6 did not authorize its own amendment, and no artifact claims it did. This succession is the first act under a rule it also creates; every succession after it is governed by a rule that predates it. This disclosure is part of the record. It MUST NOT be softened, removed, or restated as though the predecessor had authorized what it did not authorize: the referee does not bless its own birth certificate. --- *End of v1.3.*