From 7e758524ebfbba1acd0634fcbb2f1bb90cb9cb36 Mon Sep 17 00:00:00 2001
From: Shawn Hartsock <hartsock@users.noreply.github.com>
Date: Wed, 15 Jul 2026 21:07:17 -0400
Subject: [PATCH 1/3] docs(formal): design the ceremony proof kernel

Define the product lattice, trusted protocol state, explicit crypto assumptions, and the Rust-to-Lean refinement gate for the stacked formal-verification work.

Co-authored-by: OpenAI GPT-5 <codex@openai.com>
---
 ...026-07-15-formal-ceremony-kernel-design.md | 494 ++++++++++++++++++
 1 file changed, 494 insertions(+)
 create mode 100644 docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md

diff --git a/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md b/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md
new file mode 100644
index 0000000..d0475cf
--- /dev/null
+++ b/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md
@@ -0,0 +1,494 @@
+# Formal Ceremony Kernel Design
+
+**Status:** approved for a stacked implementation PR (2026-07-15)
+**Parent:** agent-bridle PR #229, `docs/spec/ceremony-contract.md`
+**Stacked branch:** `feat/formal-ceremony-kernel`
+**Scope:** a hand-written Lean specification, a pure Rust mirror extracted by
+Charon/Aeneas, and bridge proofs that the Rust implementation refines the
+specification.
+
+## 1. Purpose
+
+The Ceremony Contract currently states algebraic and protocol properties in
+prose. The formal kernel must prevent those properties from drifting back into
+claims that the implementation does not enforce.
+
+This design addresses two different questions:
+
+1. What behavior is correct?
+2. Does the Rust kernel implement that behavior?
+
+The hand-written Lean model answers the first question. Charon and Aeneas
+translate a pure Rust kernel into Lean, and bridge theorems answer the second.
+A proof suite is incomplete if either side is missing.
+
+The model is deliberately conditional at cryptographic boundaries. Lean can
+prove that the protocol uses a collision-resistant hash or an unforgeable
+signature in the right place; it does not prove that BLAKE3 or Ed25519 has
+those computational properties. Those properties remain explicit assumptions
+behind a small verified interface.
+
+## 2. Goals
+
+- Replace the flat verdict order with a product lattice whose independent axes
+  cannot be confused.
+- Prove meet resolution is associative, commutative, idempotent,
+  order-independent, and non-amplifying.
+- Make an accepted decision carry evidence that it belongs to the request it
+  answers and cannot exceed that request's ceiling.
+- Bind authorization to a canonical structured action, not display text.
+- Make attest and introduction challenges recipient-bound, generation-bound,
+  and single-use.
+- Model rollback protection around a trusted checkpoint outside the
+  attacker-controlled log.
+- Give every quorum signer one canonical unsigned revocation body.
+- Reject unsupported algorithms and unsupported authority-bearing wire data
+  before it enters the kernel.
+- Extract the Rust kernel with Charon/Aeneas and prove that the extracted
+  functions refine the hand-written Lean model.
+- Run the hand-written and bridge proofs on Linux and native Windows.
+
+## 3. Non-goals
+
+- Proving BLAKE3 collision resistance, Ed25519 unforgeability, WebAuthn
+  authenticator correctness, or OS secure-storage guarantees.
+- Formalizing JSON, TOML, DAG-CBOR, multicodec, or CID parsers in the first
+  increment. Their canonical behavior is covered by shared vectors and an
+  abstract injectivity contract at the kernel boundary.
+- Proving asynchronous transport, UI rendering, filesystem durability, or
+  network liveness.
+- Moving serde, IO, crypto implementations, or UI code into the pure kernel.
+- Treating a parent-linked log by itself as rollback-proof.
+
+## 4. PR And Commit Structure
+
+The implementation is a separate stacked PR:
+
+- Base branch: `docs/spec-ceremony-contract` (PR #229)
+- Head branch: `feat/formal-ceremony-kernel`
+- Proposed title: `formal: prove ceremony algebra and protocol safety kernel`
+
+Planned commits:
+
+1. `docs(formal): design the ceremony proof kernel`
+2. `formal(lean): prove the requirement algebra and protocol invariants`
+3. `formal(rust): add the pure extraction-oriented ceremony kernel`
+4. `formal(aeneas): prove the Rust kernel refines the Lean model`
+5. `ci(formal): enforce Lean proofs and generated-code freshness`
+
+The parent PR must be refreshed from `main` before the full verification gate.
+Its current head predates #219, so native Windows `cargo test --workspace`
+runs Unix-only `real_spawn` fixtures and fails before any stacked changes.
+
+## 5. Authority Algebra
+
+### 5.1 Why the flat verdict order is insufficient
+
+The order `deny < attest < ask < approve` combines several independent facts:
+
+- whether authority may be granted;
+- the maximum caveats of the grant;
+- what evidence is required before granting;
+- how long the grant may remain valid.
+
+Combining these axes into one enum makes semantically different states appear
+comparable and encourages callers to treat a rendering choice as authority.
+The formal model separates them.
+
+### 5.2 Product lattice
+
+The hand-written model defines:
+
+```lean
+inductive Permit
+  | deny
+  | allow
+
+inductive Evidence
+  | presence
+  | prompt
+  | none
+
+inductive Lifetime
+  | once
+  | generation
+  | durable
+
+structure Requirement (Caveats : Type) where
+  permit : Permit
+  ceiling : Caveats
+  evidence : Evidence
+  lifetime : Lifetime
+```
+
+The order means "no more authority than":
+
+- `deny <= allow`;
+- `presence <= prompt <= none` because stronger evidence is more restrictive;
+- `once <= generation <= durable`;
+- caveats use the existing attenuation order.
+
+`Requirement` receives the componentwise order and meet:
+
+```text
+meet(a, b).permit   = min(a.permit, b.permit)
+meet(a, b).ceiling  = meet(a.ceiling, b.ceiling)
+meet(a, b).evidence = min(a.evidence, b.evidence)
+meet(a, b).lifetime = min(a.lifetime, b.lifetime)
+```
+
+The first Lean proof set establishes:
+
+- `meet_assoc`;
+- `meet_comm`;
+- `meet_idem`;
+- `meet_le_left` and `meet_le_right`;
+- permutation invariance of list-fold resolution;
+- every resolved requirement is no more authoritative than every matching
+  input constraint;
+- headless degradation replaces an unmet evidence obligation with `deny` and
+  is therefore non-amplifying.
+
+The existing four verdict names remain wire and policy vocabulary. A total
+function maps each verdict into the product lattice. The rest of the kernel
+operates on `Requirement`, not on verdict precedence numbers.
+
+## 6. Requests, Decisions, And Effect Binding
+
+### 6.1 Structured actions
+
+Display strings are not authority. The model uses a structured action and an
+abstract canonical digest:
+
+```lean
+structure Action where
+  tool : ToolName
+  arguments : CanonicalArguments
+  resource : CanonicalResource
+
+structure Request where
+  requestId : RequestId
+  action : Action
+  actionId : Digest
+  ceiling : Requirement Caveats
+  options : Finset Choice
+```
+
+Request validation requires `actionId = digest(action)`. Display text is
+derived metadata and never participates in authorization except by being
+covered by the request's canonical wire record for auditability.
+
+### 6.2 Validated decisions
+
+Wire input first parses into `RawDecision`. It reaches the kernel only through:
+
+```lean
+validateDecision :
+  (request : Request) -> RawDecision -> Option (DecisionFor request)
+```
+
+`DecisionFor request` contains a choice plus proofs that:
+
+- the decision names `request.requestId`;
+- the decision names `request.actionId`;
+- the choice is a member of `request.options`;
+- the resulting requirement is below `request.ceiling`;
+- exactly one of grant and escalation was supplied.
+
+Authorization also receives the action that is about to execute and checks
+its digest against `request.actionId`. The soundness theorem states that any
+minted context is for the approved action and is no more authoritative than
+the request ceiling.
+
+Escalation is represented separately from `DecisionFor`; it cannot construct
+an effective grant.
+
+## 7. Challenges And Single Use
+
+Attestation and introduction use the same challenge algebra with different
+domain tags:
+
+```lean
+inductive Purpose
+  | attest
+  | introduce
+
+structure Challenge where
+  purpose : Purpose
+  issuer : Fingerprint
+  recipient : Fingerprint
+  requestId : Option RequestId
+  actionId : Option Digest
+  generation : Nat
+  nonce : Nonce
+```
+
+The signature input is domain-separated by protocol, object kind, and version.
+For introductions, the recipient issues the challenge; a nonce chosen only by
+the introduced party is not fresh evidence.
+
+The trusted state contains issued and consumed challenge identifiers. An
+accepting transition requires the challenge to be issued, unconsumed, valid
+for the current generation, and bound to the expected identities and action.
+It then consumes the challenge atomically.
+
+Theorems establish:
+
+- an accepted challenge was issued by the expected verifier;
+- an accepted attest challenge names the authorized action;
+- an accepted introduction names both enrolled identities;
+- no sequential execution can accept the same challenge twice;
+- a generation mismatch fails closed.
+
+Concurrency atomicity is a boundary obligation for the Rust adapter and is
+tested with the existing gate's concurrent single-use regression pattern.
+
+## 8. Trusted State And Protocol Transitions
+
+The protocol model is an inductive transition relation over a small world:
+
+```lean
+structure World where
+  policy : Policy
+  trustedHead : Checkpoint
+  generation : Nat
+  issued : Finset ChallengeId
+  consumed : Finset ChallengeId
+  loadBearing : Finset Fingerprint
+  profile : CryptoProfile
+
+inductive Step : Actor -> World -> Event -> World -> Prop
+```
+
+Events include restrictive policy additions, signed loosening entries, pinning,
+revocation, generation bumps, challenge consumption, and checkpoint advances.
+
+The main safety split is explicit:
+
+```lean
+theorem untrusted_step_safe
+  (h : Step .untrusted before event after) :
+  effective after <= effective before /\
+  after.loadBearing = before.loadBearing /\
+  after.trustedHead = before.trustedHead
+```
+
+An untrusted actor may add a restrictive nuisance entry, but cannot widen
+authority, add or remove trusted identities, or rewrite the trusted checkpoint.
+Any transition outside that class must carry the corresponding authorization
+witness: principal signature, accepted ceremony, or valid quorum.
+
+This is stronger and clearer than allowing the load-bearing set to grow under
+an untrusted transition. Adding a trusted identity is authority and requires a
+ceremony.
+
+## 9. Log Extension And Rollback
+
+A parent-linked log proves ancestry only relative to a known head. It does not
+make suffix truncation or presentation of an older fork detectable by itself.
+
+The formal model therefore separates:
+
+- `UntrustedLog`, which may be truncated, reordered, withheld, or replaced;
+- `World.trustedHead`, stored or witnessed outside that attacker's authority;
+- `Extends(candidate, trustedHead)`, a verified ancestry relation.
+
+A synchronization or reload transition may advance the checkpoint only when
+the candidate extends the existing trusted checkpoint. It may never replace
+the checkpoint with an ancestor or unrelated fork.
+
+Theorems establish:
+
+- accepted checkpoints are monotonic under `Extends`;
+- a strict ancestor of the trusted checkpoint is rejected;
+- an unrelated fork is rejected;
+- mutations confined to the untrusted log cannot alter trusted state;
+- rollback detection is conditional on the checkpoint remaining outside the
+  attacker's write authority.
+
+The concrete checkpoint adapter may use OS protected storage, a quorum-signed
+peer witness, hardware storage, or another mechanism. Each adapter must state
+which principal protects it. No theorem calls a chain rollback-proof without
+that premise.
+
+## 10. Canonical Revocation And Quorum
+
+Revocation has one unsigned body:
+
+```lean
+structure RevocationBody where
+  target : Fingerprint
+  reason : RevocationReason
+  succession : Option Fingerprint
+  tombstone : Bool
+  policyEpoch : Nat
+
+structure Endorsement where
+  signer : Fingerprint
+  signature : Signature
+
+structure Revocation where
+  body : RevocationBody
+  endorsements : Finset Endorsement
+```
+
+Every endorsement verifies over the same domain-separated digest of
+`RevocationBody`. Signatures are not part of the body they sign. The enclosing
+chain record has a separate append signature.
+
+Validation requires:
+
+- signer membership in the quorum policy selected by `policyEpoch`;
+- distinct signer identities;
+- every signature verifies over the same body digest;
+- the signer count reaches the threshold;
+- last-root removal carries either a valid successor or an explicit tombstone;
+- ceremony strength is at least the enrollment strength being revoked.
+
+The principal theorem is that fewer than the required distinct valid signers
+cannot produce a revocation transition.
+
+## 11. Wire And Crypto Boundary
+
+Signed inputs include a domain separator containing protocol, object kind, and
+version. Authority-bearing v1 records reject unknown fields. Future versions
+must be explicitly selected and validated; they are not silently interpreted
+as v1.
+
+Opaque extension data is permitted only in fields declared non-authoritative.
+It remains covered by the canonical content digest and must survive a round
+trip unchanged.
+
+`CryptoProfile` is trusted configuration, not attacker-selected input. Before
+dispatching on a multihash or multicodec code, validation proves that the code
+belongs to the active profile. Profile rotation is an authorized state
+transition.
+
+The Lean boundary exposes assumptions such as:
+
+```lean
+class CryptoAssumptions (Value Key Message Signature : Type) where
+  canonicalInjective : forall {x y : Value},
+    canonical x = canonical y -> x = y
+  digestBinding : forall {x y : Value},
+    digest x = digest y -> canonical x = canonical y
+  signatureOrigin : forall {key : Key} {msg : Message} {sig : Signature},
+    verifies key msg sig -> signedBy key msg sig
+```
+
+These are assumptions used by protocol theorems, not claims that Lean proved
+the underlying cryptographic algorithms. `signatureOrigin` proves only which
+key produced a signature. Whether that key is authorized is a separate kernel
+predicate over the active principal, quorum policy, role, and policy epoch.
+
+The concrete checkpoint adapter has a similarly explicit environmental
+obligation: attacker-controlled log writes cannot alter the trusted checkpoint.
+The protocol proof is conditional on that adapter property; it is not hidden as
+a consequence of hashing.
+
+## 12. Rust Kernel And Aeneas Refinement
+
+The Rust mirror lives in a pure module under `agent-bridle-core`. It contains
+only algebraic data, explicit loops, validation predicates, and transition
+functions. It contains no serde, IO, async, clocks, random generation, crypto
+implementation, trait objects, or UI code.
+
+Boundary adapters convert verified wire and cryptographic results into kernel
+values. Invalid or unsupported inputs never construct kernel types.
+
+Charon extracts the module to LLBC and Aeneas emits Lean under
+`formal/Generated/`. Generated files are checked in and never edited manually.
+`formal/Ceremony/Refinement.lean` proves, for each extracted operation:
+
+- Rust meet equals specification meet;
+- Rust resolution equals specification resolution;
+- Rust decision validation implies `DecisionFor`;
+- Rust transition acceptance implies the specification `Step` relation;
+- Rust authorization output satisfies action binding and attenuation.
+
+The bridge theorem is the release gate. Hand-written model proofs and extracted
+Rust proofs passing independently are insufficient.
+
+## 13. Lean Project Layout
+
+```text
+formal/
+  lakefile.toml
+  lean-toolchain
+  Ceremony/
+    Algebra.lean
+    Decision.lean
+    Challenge.lean
+    Log.lean
+    Revocation.lean
+    Protocol.lean
+    CryptoAssumptions.lean
+    Refinement.lean
+  Generated/
+    CeremonyKernel.lean
+  Tests/
+    Counterexamples.lean
+```
+
+The Lean version is pinned to the Aeneas backend's compatible toolchain.
+Dependencies are pinned in `lake-manifest.json`.
+
+`Counterexamples.lean` records negative examples for the traps found during
+review: suffix rollback without a trusted head, out-of-matrix grants, action
+display substitution, replayed challenges, circular quorum payloads, unknown
+authority fields, and attacker-selected hash algorithms. These examples make
+the missing premise or rejected construction visible to reviewers.
+
+## 14. Verification And CI
+
+The stacked PR adds:
+
+- `lake build` on Ubuntu and native Windows;
+- Rust unit and property tests for the pure mirror;
+- Linux-only Charon/Aeneas regeneration using pinned toolchains and caches;
+- a generated-code freshness check that fails on a diff;
+- `cargo fmt`, build, test, and clippy gates already required by the repo;
+- pre-push parity for every required CI command.
+
+Live services, network inference, hardware authenticators, and external peers
+are not used by automated tests. Crypto and storage adapters use deterministic
+mocks at this layer.
+
+Because PR #229 currently predates the Windows test gating in #219, its branch
+must first absorb current `main`; otherwise the unrelated Unix-command fixtures
+fail on native Windows before formal verification runs.
+
+## 15. Acceptance Criteria
+
+- The product lattice laws compile without `sorry`, `admit`, or new axioms
+  outside the named crypto/storage assumptions.
+- Resolution is proved permutation-invariant and non-amplifying.
+- A validated decision is proved request-bound, action-bound,
+  matrix-contained, and ceiling-bounded.
+- Attest and introduction challenges are proved single-use in the sequential
+  kernel and generation-bound.
+- Rollback rejection explicitly depends on an independently trusted
+  checkpoint.
+- Quorum validation uses distinct signers over one unsigned body.
+- Unsupported profiles and unsupported authority-bearing wire versions fail
+  closed.
+- Aeneas-generated Rust operations are connected to the hand model by bridge
+  theorems.
+- Lean builds on Windows and Linux; Aeneas regeneration is reproducible on
+  Linux/WSL.
+- The PR body lists any remaining unproved environmental assumptions.
+
+## 16. Review Guidance
+
+Reviewers should reject any change that:
+
+- moves rendering, serde, IO, or cryptographic implementation into the kernel;
+- treats a CID or parent link as freshness without trusted external state;
+- lets raw wire values bypass validated constructors;
+- lets display text identify an executable effect;
+- accepts a decision without checking request, action, matrix, and ceiling;
+- treats a nonce as fresh without issuer and consumption state;
+- lets quorum signers sign different payloads;
+- dispatches an attacker-selected algorithm outside the active profile;
+- adds a theorem using `sorry`, `admit`, or an unnamed axiom;
+- omits the refinement proof between extracted Rust and the specification.

From fd509b8e4bca62f9daa2b60b9dd9f899a39a1870 Mon Sep 17 00:00:00 2001
From: Shawn Hartsock <hartsock@users.noreply.github.com>
Date: Wed, 15 Jul 2026 22:07:39 -0400
Subject: [PATCH 2/3] docs(formal): align kernel plan with ceremony suite

Split the proof work by the P1 to P2 to P0 dependency order, place rollback state in P2's external anchor, and move enrollment freshness to the Tier-2 protocol track.

Co-Authored-By: OpenAI GPT-5 <codex@openai.com>
---
 ...26-07-16-p1-signed-object-formalization.md | 477 ++++++++++++++++++
 ...026-07-15-formal-ceremony-kernel-design.md | 127 ++---
 2 files changed, 547 insertions(+), 57 deletions(-)
 create mode 100644 docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md

diff --git a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md
new file mode 100644
index 0000000..f55fb9b
--- /dev/null
+++ b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md
@@ -0,0 +1,477 @@
+# P1 Signed-Object Formalization Implementation Plan
+
+> **For agentic workers:** REQUIRED SUB-SKILL: Use
+> superpowers:subagent-driven-development (recommended) or
+> superpowers:executing-plans to implement this plan task-by-task. Steps use
+> checkbox (`- [ ]`) syntax for tracking.
+
+**Goal:** Build and continuously verify the P1 Lean model that makes canonical
+encoding, sealed loading, strict version handling, and algorithm
+allowlist-before-dispatch explicit proof obligations.
+
+**Architecture:** A dependency-free Lean project models only P1. An abstract
+`CanonicalEncoding` interface carries the profile's injectivity premise;
+`VerifiedEnvelope` and `Sealed` make verify-before-parse structural; and the
+algorithm dispatcher can only receive an `AllowedAlgorithm` witness. Negative
+examples demonstrate why raw attacker-selected dispatch and reserialization
+after parsing are not admissible APIs.
+
+**Tech Stack:** Lean 4 `v4.31.0` via elan/lake, Rust workspace checks, GitHub
+Actions on Ubuntu and Windows, PowerShell-compatible local commands.
+
+## Global Constraints
+
+- P1 has no dependency on P0, P2, serde, IO, clocks, network services, or
+  concrete cryptographic implementations.
+- Cryptographic strength is a Tier-1 assumption; no theorem claims to prove
+  BLAKE3 collision resistance or Ed25519 unforgeability.
+- Proofs contain no `sorry`, `admit`, or unnamed axioms.
+- Verification must run on Linux and native Windows.
+- Automated tests are deterministic and use no live services.
+- Every commit is authored as Shawn Hartsock and includes
+  `Co-Authored-By: OpenAI GPT-5 <codex@openai.com>`.
+
+---
+
+### Task 1: Pin the standalone Lean project and write the failing contract test
+
+**Files:**
+- Create: `formal/lean-toolchain`
+- Create: `formal/lakefile.toml`
+- Create: `formal/Tests.lean`
+- Create: `formal/Tests/SignedObjectContracts.lean`
+
+**Interfaces:**
+- Consumes: Lean standard library only.
+- Produces: Lake library `CeremonyFormal` rooted at `formal/Ceremony` and test
+  import `Ceremony.P1.SignedObject`.
+
+- [ ] **Step 1: Add the toolchain and Lake configuration**
+
+```text
+leanprover/lean4:v4.31.0
+```
+
+```toml
+name = "ceremony-formal"
+version = "0.1.0"
+defaultTargets = ["CeremonyFormal", "CeremonyTests"]
+
+[[lean_lib]]
+name = "CeremonyFormal"
+srcDir = "."
+roots = ["Ceremony"]
+
+[[lean_lib]]
+name = "CeremonyTests"
+srcDir = "."
+roots = ["Tests"]
+```
+
+- [ ] **Step 2: Write a test importing the not-yet-created P1 module**
+
+```lean
+import Ceremony.P1.SignedObject
+
+open Ceremony.P1
+
+example : Profile.v1.allowsHash .blake3_256 := by decide
+example : Not (Profile.v1.allowsHash .sha1) := by decide
+```
+
+```lean
+import Tests.SignedObjectContracts
+```
+
+- [ ] **Step 3: Run the test and verify RED**
+
+Run: `Push-Location formal; lake build; Pop-Location`
+
+Expected: FAIL because `Ceremony.P1.SignedObject` does not exist.
+
+- [ ] **Step 4: Commit only after Task 2 reaches green**
+
+The scaffold, model, and tests land together in Task 2 so no commit leaves the
+default Lake target broken.
+
+### Task 2: Model canonical bytes, profile witnesses, and sealed values
+
+**Files:**
+- Create: `formal/Ceremony.lean`
+- Create: `formal/Ceremony/P1/SignedObject.lean`
+- Modify: `formal/Tests/SignedObjectContracts.lean`
+
+**Interfaces:**
+- Consumes: `ByteArray`, `Finset`, and decidable equality from Lean core.
+- Produces: `HashAlgorithm`, `SignatureAlgorithm`, `Codec`, `Profile`,
+  `AllowedHash`, `AllowedSignature`, `AllowedCodec`, `CanonicalEncoding`,
+  `VerifiedBytes`, `Sealed`, `seal`, and `sealed_eq_of_same_canonical`.
+
+- [ ] **Step 1: Extend the test with the wished-for sealing API**
+
+```lean
+def bytesEncoding : CanonicalEncoding ByteArray where
+  encode := id
+  injective := fun h => h
+
+example (a b : ByteArray) (h : bytesEncoding.encode a = bytesEncoding.encode b) :
+    a = b := bytesEncoding.injective h
+
+example (value : ByteArray) : (seal bytesEncoding value).value = value := rfl
+```
+
+- [ ] **Step 2: Run the test and verify RED**
+
+Run: `Push-Location formal; lake build; Pop-Location`
+
+Expected: FAIL with unknown identifiers such as `CanonicalEncoding` and
+`seal`.
+
+- [ ] **Step 3: Implement the minimal P1 model**
+
+Define finite algorithm enums, a v1 profile containing exactly BLAKE3-256,
+Ed25519, and DAG-CBOR, proof-carrying allowed-algorithm wrappers, an injective
+canonical encoder interface, and a `Sealed` value whose canonical bytes must be
+proved equal to the encoding of its value. Use this module shape:
+
+```lean
+namespace Ceremony.P1
+
+inductive HashAlgorithm | blake3_256 | sha1
+  deriving DecidableEq, Repr
+inductive SignatureAlgorithm | ed25519 | ecdsa
+  deriving DecidableEq, Repr
+inductive Codec | dagCbor | json
+  deriving DecidableEq, Repr
+
+structure Profile where
+  version : Nat
+  hashes : List HashAlgorithm
+  signatures : List SignatureAlgorithm
+  codecs : List Codec
+
+def Profile.v1 : Profile :=
+  { version := 1, hashes := [.blake3_256],
+    signatures := [.ed25519], codecs := [.dagCbor] }
+
+def Profile.allowsHash (profile : Profile) (algorithm : HashAlgorithm) : Prop :=
+  algorithm ∈ profile.hashes
+
+def Profile.allowsSignature
+    (profile : Profile) (algorithm : SignatureAlgorithm) : Prop :=
+  algorithm ∈ profile.signatures
+
+def Profile.allowsCodec (profile : Profile) (codec : Codec) : Prop :=
+  codec ∈ profile.codecs
+
+structure AllowedHash (profile : Profile) where
+  algorithm : HashAlgorithm
+  allowed : profile.allowsHash algorithm
+
+structure AllowedSignature (profile : Profile) where
+  algorithm : SignatureAlgorithm
+  allowed : profile.allowsSignature algorithm
+
+structure AllowedCodec (profile : Profile) where
+  codec : Codec
+  allowed : profile.allowsCodec codec
+
+structure CanonicalEncoding (Value : Type) where
+  encode : Value -> ByteArray
+  injective : Function.Injective encode
+
+structure Sealed {Value : Type} (encoding : CanonicalEncoding Value) where
+  value : Value
+  canonical : ByteArray
+  canonical_eq : canonical = encoding.encode value
+
+def seal (encoding : CanonicalEncoding Value) (value : Value) : Sealed encoding :=
+  { value, canonical := encoding.encode value, canonical_eq := rfl }
+```
+
+Parsing and concrete signature verification remain boundary parameters rather
+than hidden axioms.
+
+- [ ] **Step 4: Prove canonical identity and profile rejection**
+
+Add theorems with these exact signatures:
+
+```lean
+theorem sealed_eq_of_same_canonical
+    {encoding : CanonicalEncoding Value} {a b : Sealed encoding}
+    (h : a.canonical = b.canonical) : a = b
+
+theorem sha1_not_allowed : Not (Profile.v1.allowsHash .sha1)
+theorem blake3_allowed : Profile.v1.allowsHash .blake3_256
+theorem ecdsa_not_allowed : Not (Profile.v1.allowsSignature .ecdsa)
+theorem ed25519_allowed : Profile.v1.allowsSignature .ed25519
+theorem json_not_allowed : Not (Profile.v1.allowsCodec .json)
+theorem dag_cbor_allowed : Profile.v1.allowsCodec .dagCbor
+```
+
+- [ ] **Step 5: Run the focused proof build and verify GREEN**
+
+Run: `Push-Location formal; lake build; Pop-Location`
+
+Expected: PASS with both `CeremonyFormal` and `SignedObjectContracts` built.
+
+- [ ] **Step 6: Commit the P1 model**
+
+```text
+formal(lean): prove P1 signed-object contracts
+
+Co-Authored-By: OpenAI GPT-5 <codex@openai.com>
+```
+
+### Task 3: Encode verify-before-parse and allowlist-before-dispatch
+
+**Files:**
+- Modify: `formal/Ceremony/P1/SignedObject.lean`
+- Modify: `formal/Tests/SignedObjectContracts.lean`
+- Create: `formal/Tests/P1Counterexamples.lean`
+- Modify: `formal/lakefile.toml`
+
+**Interfaces:**
+- Consumes: P1 algorithm and canonicalization types from Task 2.
+- Produces: `RawEnvelope`, `SupportedVersion`, `VerifiedEnvelope`,
+  `verifyEnvelope`, `dispatchHash`, and rejection theorems for unsupported
+  versions, critical fields, and algorithms.
+
+- [ ] **Step 1: Write failing tests for hostile inputs**
+
+```lean
+def v1Envelope : RawEnvelope :=
+  { version := 1, hash := .blake3_256, signature := .ed25519,
+    codec := .dagCbor, receivedCanonical := ByteArray.mk #[],
+    unknownCritical := [] }
+
+def unsupportedVersionEnvelope : RawEnvelope := { v1Envelope with version := 2 }
+def sha1Envelope : RawEnvelope := { v1Envelope with hash := .sha1 }
+def unknownCriticalEnvelope : RawEnvelope :=
+  { v1Envelope with unknownCritical := ["future-authority"] }
+
+example : (verifyEnvelope Profile.v1 v1Envelope).isSome := by decide
+example : verifyEnvelope Profile.v1 unsupportedVersionEnvelope = none := by decide
+example : verifyEnvelope Profile.v1 sha1Envelope = none := by decide
+example : verifyEnvelope Profile.v1 unknownCriticalEnvelope = none := by decide
+```
+
+The counterexample module also defines an `unsafeDispatch` that accepts a raw
+`HashAlgorithm`; the safe `dispatchHash` requires an `AllowedHash` witness, so
+v1 cannot dispatch SHA-1:
+
+```lean
+inductive HashImplementation | blake3 | legacySha1 deriving DecidableEq
+
+def unsafeDispatch : HashAlgorithm -> HashImplementation
+  | .blake3_256 => .blake3
+  | .sha1 => .legacySha1
+
+def dispatchHash (allowed : AllowedHash profile) : HashImplementation :=
+  unsafeDispatch allowed.algorithm
+
+example : unsafeDispatch .sha1 = .legacySha1 := rfl
+
+theorem no_v1_sha1_witness
+    (allowed : AllowedHash Profile.v1) :
+    Not (allowed.algorithm = .sha1) := by
+  intro h
+  subst h
+  exact sha1_not_allowed allowed.allowed
+```
+
+- [ ] **Step 2: Run the test and verify RED**
+
+Run: `Push-Location formal; lake build; Pop-Location`
+
+Expected: FAIL because envelope verification and safe dispatch are undefined.
+
+- [ ] **Step 3: Implement staged verification**
+
+`verifyEnvelope` checks version, rejects non-empty critical unknown fields,
+checks profile membership, and only then constructs the proof witness passed to
+the abstract dispatch function. It retains received canonical bytes in
+`VerifiedEnvelope`; no theorem reserializes a typed value to recover signed
+bytes. Implement the boundary with this shape:
+
+```lean
+structure RawEnvelope where
+  version : Nat
+  hash : HashAlgorithm
+  signature : SignatureAlgorithm
+  codec : Codec
+  receivedCanonical : ByteArray
+  unknownCritical : List String
+  deriving DecidableEq
+
+structure VerifiedEnvelope (profile : Profile) where
+  raw : RawEnvelope
+  version_eq : raw.version = profile.version
+  critical_empty : raw.unknownCritical = []
+  allowedHash : AllowedHash profile
+  hash_eq : allowedHash.algorithm = raw.hash
+  allowedSignature : AllowedSignature profile
+  signature_eq : allowedSignature.algorithm = raw.signature
+  allowedCodec : AllowedCodec profile
+  codec_eq : allowedCodec.codec = raw.codec
+
+def verifyEnvelope (profile : Profile) (raw : RawEnvelope) :
+    Option (VerifiedEnvelope profile) :=
+  if hv : raw.version = profile.version then
+    if hc : raw.unknownCritical = [] then
+      if hh : profile.allowsHash raw.hash then
+        if hs : profile.allowsSignature raw.signature then
+          if hcodec : profile.allowsCodec raw.codec then
+            some { raw, version_eq := hv, critical_empty := hc,
+              allowedHash := { algorithm := raw.hash, allowed := hh },
+              hash_eq := rfl,
+              allowedSignature := { algorithm := raw.signature,
+                allowed := hs }, signature_eq := rfl,
+              allowedCodec := { codec := raw.codec, allowed := hcodec },
+              codec_eq := rfl }
+          else none
+        else none
+      else none
+    else none
+  else none
+```
+
+- [ ] **Step 4: Prove fail-closed behavior**
+
+Add theorems with these exact statements:
+
+```lean
+theorem verified_hash_allowed
+    (h : verifyEnvelope profile raw = some verified) :
+    profile.allowsHash verified.allowedHash.algorithm
+
+theorem verified_signature_allowed
+    (h : verifyEnvelope profile raw = some verified) :
+    profile.allowsSignature verified.allowedSignature.algorithm
+
+theorem verified_codec_allowed
+    (h : verifyEnvelope profile raw = some verified) :
+    profile.allowsCodec verified.allowedCodec.codec
+
+theorem unsupported_version_rejected
+    (h : Not (raw.version = profile.version)) :
+    verifyEnvelope profile raw = none
+
+theorem unknown_critical_rejected
+    (h : Not (raw.unknownCritical = [])) :
+    verifyEnvelope profile raw = none
+```
+
+- [ ] **Step 5: Run all Lean targets and verify GREEN**
+
+Run: `Push-Location formal; lake build; Pop-Location`
+
+Expected: PASS, including `P1Counterexamples`.
+
+- [ ] **Step 6: Commit the verification boundary**
+
+```text
+formal(lean): enforce allowlist-before-dispatch
+
+Co-Authored-By: OpenAI GPT-5 <codex@openai.com>
+```
+
+### Task 4: Add cross-platform proof gates and hook parity
+
+**Files:**
+- Modify: `.github/workflows/ci.yml`
+- Modify: `justfile`
+- Modify: `.githooks/pre-push`
+- Modify: `docs/TOOLCHAIN.md`
+
+**Interfaces:**
+- Consumes: the `formal` Lake project from Tasks 1-3.
+- Produces: `just check-formal`, Linux and Windows `lake build` jobs, and a
+  pre-push invocation matching the required CI proof gate.
+
+- [ ] **Step 1: Add a failing local gate check**
+
+Add `check-formal` to `justfile` with `lake build` executed from `formal`, then
+invoke it before installing elan to confirm the command fails clearly when the
+toolchain is absent.
+
+- [ ] **Step 2: Install/resolve the pinned Lean toolchain and verify the gate**
+
+Run: `elan toolchain install leanprover/lean4:v4.31.0`
+
+Run: `just check-formal`
+
+Expected: PASS.
+
+- [ ] **Step 3: Mirror the gate in CI and pre-push**
+
+Add a `formal` job with an Ubuntu/Windows matrix using `leanprover/lean-action`
+and `lake build`. Add `just check-formal` to `.githooks/pre-push`. Keep parity
+comments adjacent in all three files.
+
+- [ ] **Step 4: Update toolchain status accurately**
+
+Record native Windows `lake build` as verified only after the local run passes;
+leave native Aeneas/opam explicitly unverified and WSL2-recommended.
+
+- [ ] **Step 5: Run syntax and proof gates**
+
+Run: `just check-formal`
+
+Run: `cargo fmt --all -- --check`
+
+Run: `git diff --check`
+
+Expected: all PASS.
+
+- [ ] **Step 6: Commit CI enforcement**
+
+```text
+ci(formal): gate P1 proofs on Linux and Windows
+
+Co-Authored-By: OpenAI GPT-5 <codex@openai.com>
+```
+
+### Task 5: Run the repository gate and open the stacked PR
+
+**Files:**
+- Verify only; no planned source changes.
+
+**Interfaces:**
+- Consumes: all P1 commits.
+- Produces: a reviewable PR based on `feat/formal-ceremony-kernel`.
+
+- [ ] **Step 1: Scan for proof escapes**
+
+Run: `rg -n '\b(sorry|admit|axiom)\b' formal`
+
+Expected: no matches. Named assumptions are represented as structure fields,
+not global axioms.
+
+- [ ] **Step 2: Run the full native-Windows gate**
+
+Run: `just check-formal`
+
+Run: `just check`
+
+Run: `just check-windows`
+
+Run: `just publish-check`
+
+Expected: all PASS. Any environment-dependent kernel proof skip or failure is
+reported verbatim in the PR body rather than generalized away.
+
+- [ ] **Step 3: Verify branch shape and attribution**
+
+Run: `git log --format=full origin/feat/formal-ceremony-kernel..HEAD`
+
+Expected: every commit is authored by Shawn Hartsock and contains the OpenAI
+GPT-5 co-author trailer.
+
+- [ ] **Step 4: Push normally and open the PR**
+
+Push without bypassing hooks. Open a draft PR titled
+`formal: prove P1 signed-object contracts` with `What this PR does`, `Test
+plan`, and `Out of scope` sections. Base it on
+`feat/formal-ceremony-kernel`; identify the model and Codex desktop harness in
+the body.
diff --git a/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md b/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md
index d0475cf..7f8cf54 100644
--- a/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md
+++ b/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md
@@ -1,11 +1,12 @@
 # Formal Ceremony Kernel Design
 
-**Status:** approved for a stacked implementation PR (2026-07-15)
-**Parent:** agent-bridle PR #229, `docs/spec/ceremony-contract.md`
+**Status:** approved for an ordered stack of implementation PRs; reconciled
+with the Ceremony Suite on 2026-07-16
+**Parent:** agent-bridle PR #229, `docs/spec/README.md` and profiles P0-P5
 **Stacked branch:** `feat/formal-ceremony-kernel`
-**Scope:** a hand-written Lean specification, a pure Rust mirror extracted by
-Charon/Aeneas, and bridge proofs that the Rust implementation refines the
-specification.
+**Scope:** profile-ordered hand-written Lean specifications, a pure Rust mirror
+extracted by Charon/Aeneas, and bridge proofs that the Rust implementation
+refines the specifications.
 
 ## 1. Purpose
 
@@ -37,10 +38,12 @@ behind a small verified interface.
 - Make an accepted decision carry evidence that it belongs to the request it
   answers and cannot exceed that request's ceiling.
 - Bind authorization to a canonical structured action, not display text.
-- Make attest and introduction challenges recipient-bound, generation-bound,
-  and single-use.
-- Model rollback protection around a trusted checkpoint outside the
-  attacker-controlled log.
+- Make attest challenges verifier-bound, action-bound, generation-bound, and
+  single-use in the Tier-3 kernel. Enrollment and Introduction freshness are
+  proved separately as a Tier-2 symbolic protocol.
+- Model rollback protection around P2's external anti-rollback anchor, outside
+  the attacker-controlled log and represented as trusted state carried into
+  every verification.
 - Give every quorum signer one canonical unsigned revocation body.
 - Reject unsupported algorithms and unsupported authority-bearing wire data
   before it enters the kernel.
@@ -59,26 +62,32 @@ behind a small verified interface.
   network liveness.
 - Moving serde, IO, crypto implementations, or UI code into the pure kernel.
 - Treating a parent-linked log by itself as rollback-proof.
+- Proving SAS, proof-of-possession Introduction, MITM resistance, or
+  unknown-key-share resistance in Lean. Those are P3 protocol properties and
+  require Tamarin or ProVerif under a Dolev-Yao model.
 
 ## 4. PR And Commit Structure
 
-The implementation is a separate stacked PR:
-
-- Base branch: `docs/spec-ceremony-contract` (PR #229)
-- Head branch: `feat/formal-ceremony-kernel`
-- Proposed title: `formal: prove ceremony algebra and protocol safety kernel`
-
-Planned commits:
-
-1. `docs(formal): design the ceremony proof kernel`
-2. `formal(lean): prove the requirement algebra and protocol invariants`
-3. `formal(rust): add the pure extraction-oriented ceremony kernel`
-4. `formal(aeneas): prove the Rust kernel refines the Lean model`
-5. `ci(formal): enforce Lean proofs and generated-code freshness`
-
-The parent PR must be refreshed from `main` before the full verification gate.
-Its current head predates #219, so native Windows `cargo test --workspace`
-runs Unix-only `real_spawn` fixtures and fails before any stacked changes.
+Implementation follows the suite dependency DAG. Each proof boundary is a
+separate stacked PR so a reviewer can reject one profile without entangling
+its dependents:
+
+1. `formal: prove P1 signed-object contracts` -- Lean project, canonical
+   encoding contract, sealed-value boundary, version rejection, and
+   allowlist-before-dispatch.
+2. `formal: prove P2 chain-store monotonicity` -- external-anchor trusted
+   state, DAG extension, rollback/fork rejection, and untrusted-step safety.
+3. `formal: prove P0 authority resolution` -- product lattice, total
+   resolution, matrix/ceiling validation, and non-amplification.
+4. `formal: add the extraction-oriented ceremony kernel` -- pure Rust mirror
+   for the proven P0/P1/P2 slice, with property tests.
+5. `formal: prove Aeneas refinement of the ceremony kernel` -- checked-in
+   extraction and bridge theorems, followed by generated-code freshness gates.
+
+The design PR remains based directly on `docs/spec-ceremony-contract` (PR
+#229). Every implementation branch is based on the preceding formal branch.
+P3 enrollment gets a separate Tier-2 protocol-verification stack after the
+P0/P1/P2 waist is proven; P4 and P5 follow their profile dependencies.
 
 ## 5. Authority Algebra
 
@@ -203,15 +212,15 @@ the request ceiling.
 Escalation is represented separately from `DecisionFor`; it cannot construct
 an effective grant.
 
-## 7. Challenges And Single Use
+## 7. Attestation Challenges And Single Use
 
-Attestation and introduction use the same challenge algebra with different
-domain tags:
+The Tier-3 kernel models attestation challenges. P3 Introduction may reuse the
+wire shape, but its recipient-issued handshake and adversarial-channel claims
+belong to the Tier-2 symbolic model and are not discharged by these theorems:
 
 ```lean
 inductive Purpose
   | attest
-  | introduce
 
 structure Challenge where
   purpose : Purpose
@@ -224,9 +233,6 @@ structure Challenge where
 ```
 
 The signature input is domain-separated by protocol, object kind, and version.
-For introductions, the recipient issues the challenge; a nonce chosen only by
-the introduced party is not fresh evidence.
-
 The trusted state contains issued and consumed challenge identifiers. An
 accepting transition requires the challenge to be issued, unconsumed, valid
 for the current generation, and bound to the expected identities and action.
@@ -236,7 +242,6 @@ Theorems establish:
 
 - an accepted challenge was issued by the expected verifier;
 - an accepted attest challenge names the authorized action;
-- an accepted introduction names both enrolled identities;
 - no sequential execution can accept the same challenge twice;
 - a generation mismatch fails closed.
 
@@ -245,12 +250,12 @@ tested with the existing gate's concurrent single-use regression pattern.
 
 ## 8. Trusted State And Protocol Transitions
 
-The protocol model is an inductive transition relation over a small world:
+The P0/P2 kernel model is an inductive transition relation over a small world:
 
 ```lean
 structure World where
   policy : Policy
-  trustedHead : Checkpoint
+  anchor : ExternalAnchor
   generation : Nat
   issued : Finset ChallengeId
   consumed : Finset ChallengeId
@@ -270,11 +275,11 @@ theorem untrusted_step_safe
   (h : Step .untrusted before event after) :
   effective after <= effective before /\
   after.loadBearing = before.loadBearing /\
-  after.trustedHead = before.trustedHead
+  after.anchor = before.anchor
 ```
 
 An untrusted actor may add a restrictive nuisance entry, but cannot widen
-authority, add or remove trusted identities, or rewrite the trusted checkpoint.
+authority, add or remove trusted identities, or rewrite P2's external anchor.
 Any transition outside that class must carry the corresponding authorization
 witness: principal signature, accepted ceremony, or valid quorum.
 
@@ -290,8 +295,9 @@ make suffix truncation or presentation of an older fork detectable by itself.
 The formal model therefore separates:
 
 - `UntrustedLog`, which may be truncated, reordered, withheld, or replaced;
-- `World.trustedHead`, stored or witnessed outside that attacker's authority;
-- `Extends(candidate, trustedHead)`, a verified ancestry relation.
+- `World.anchor`, the P2 `ExternalAnchor` stored or witnessed outside that
+  attacker's authority;
+- `Extends(candidate, anchor.checkpoint)`, a verified ancestry relation.
 
 A synchronization or reload transition may advance the checkpoint only when
 the candidate extends the existing trusted checkpoint. It may never replace
@@ -416,12 +422,17 @@ formal/
   lakefile.toml
   lean-toolchain
   Ceremony/
-    Algebra.lean
-    Decision.lean
-    Challenge.lean
-    Log.lean
-    Revocation.lean
-    Protocol.lean
+    P1/
+      SignedObject.lean
+    P2/
+      ChainStore.lean
+    P0/
+      Algebra.lean
+      Decision.lean
+      Challenge.lean
+      Protocol.lean
+    P4/
+      Revocation.lean
     CryptoAssumptions.lean
     Refinement.lean
   Generated/
@@ -433,15 +444,16 @@ formal/
 The Lean version is pinned to the Aeneas backend's compatible toolchain.
 Dependencies are pinned in `lake-manifest.json`.
 
-`Counterexamples.lean` records negative examples for the traps found during
-review: suffix rollback without a trusted head, out-of-matrix grants, action
-display substitution, replayed challenges, circular quorum payloads, unknown
-authority fields, and attacker-selected hash algorithms. These examples make
-the missing premise or rejected construction visible to reviewers.
+Counterexample modules live beside the profile that owns the rejected
+construction. They record suffix rollback without an external anchor,
+out-of-matrix grants, action display substitution, replayed attest challenges,
+circular quorum payloads, unknown authority fields, and attacker-selected hash
+algorithms. These examples make the missing premise or rejected construction
+visible to reviewers without mixing profile dependencies.
 
 ## 14. Verification And CI
 
-The stacked PR adds:
+The formal stack adds these gates incrementally as their owning profile lands:
 
 - `lake build` on Ubuntu and native Windows;
 - Rust unit and property tests for the pure mirror;
@@ -454,9 +466,9 @@ Live services, network inference, hardware authenticators, and external peers
 are not used by automated tests. Crypto and storage adapters use deterministic
 mocks at this layer.
 
-Because PR #229 currently predates the Windows test gating in #219, its branch
-must first absorb current `main`; otherwise the unrelated Unix-command fixtures
-fail on native Windows before formal verification runs.
+PR #229 was rebased over #219 before this design was reconciled, and its current
+CI is green on Linux, macOS, and Windows. Each child branch must preserve that
+baseline while adding its profile-specific proof gate.
 
 ## 15. Acceptance Criteria
 
@@ -465,8 +477,9 @@ fail on native Windows before formal verification runs.
 - Resolution is proved permutation-invariant and non-amplifying.
 - A validated decision is proved request-bound, action-bound,
   matrix-contained, and ceiling-bounded.
-- Attest and introduction challenges are proved single-use in the sequential
-  kernel and generation-bound.
+- Attest challenges are proved single-use in the sequential kernel,
+  generation-bound, and action-bound. P3 Introduction claims are absent from
+  the Tier-3 acceptance gate and tracked in the Tier-2 protocol stack.
 - Rollback rejection explicitly depends on an independently trusted
   checkpoint.
 - Quorum validation uses distinct signers over one unsigned body.

From f9593d0271f6008a0b310a968a09ab11d4bc4d7e Mon Sep 17 00:00:00 2001
From: Shawn Hartsock <hartsock@users.noreply.github.com>
Date: Wed, 15 Jul 2026 23:16:09 -0400
Subject: [PATCH 3/3] docs(formal): bind P1 to signed envelope bytes

Reconcile the formal kernel with PR #229 OB-4 and OB-6: exact envelope recomposition, universal signature domains, named crypto soundness, private verified constructors, and trusted-profile dispatch.

Co-Authored-By: OpenAI GPT-5 <codex@openai.com>
---
 ...26-07-16-p1-signed-object-formalization.md | 33 ++++++--
 ...026-07-15-formal-ceremony-kernel-design.md | 80 +++++++++++++++----
 2 files changed, 93 insertions(+), 20 deletions(-)

diff --git a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md
index f55fb9b..53b1540 100644
--- a/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md
+++ b/docs/superpowers/plans/2026-07-16-p1-signed-object-formalization.md
@@ -9,12 +9,12 @@
 encoding, sealed loading, strict version handling, and algorithm
 allowlist-before-dispatch explicit proof obligations.
 
-**Architecture:** A dependency-free Lean project models only P1. An abstract
-`CanonicalEncoding` interface carries the profile's injectivity premise;
-`VerifiedEnvelope` and `Sealed` make verify-before-parse structural; and the
-algorithm dispatcher can only receive an `AllowedAlgorithm` witness. Negative
-examples demonstrate why raw attacker-selected dispatch and reserialization
-after parsing are not admissible APIs.
+**Architecture:** A dependency-free Lean project models only P1. A signed-byte
+envelope embeds the canonical body and universal signature domain. An abstract
+codec proves every decoded envelope recomposes to the exact received bytes;
+named cryptographic soundness contracts connect executable checks to digest
+binding and signature origin. Verified constructors are private, and algorithm
+dispatch requires the active `TrustedProfile` witness.
 
 **Tech Stack:** Lean 4 `v4.31.0` via elan/lake, Rust workspace checks, GitHub
 Actions on Ubuntu and Windows, PowerShell-compatible local commands.
@@ -31,6 +31,27 @@ Actions on Ubuntu and Windows, PowerShell-compatible local commands.
 - Every commit is authored as Shawn Hartsock and includes
   `Co-Authored-By: OpenAI GPT-5 <codex@openai.com>`.
 
+## Parent-Reconciliation Amendment
+
+PR #229 added OB-4 and OB-6 after the initial TDD outline below was written.
+These requirements supersede the earlier `RawEnvelope` and public `Sealed`
+snippets:
+
+- Transport is an explicit signed-bytes envelope. JSON/TOML carry an encoded
+  canonical body; authority never depends on their reserialization.
+- The codec contract requires `decode received = some envelope` to imply
+  `encode envelope = received`.
+- Every signature covers record type, store ID, causal thread or principal,
+  profile/version, codec, CID, signer, and canonical body.
+- Executable digest and signature checks carry soundness proofs into named
+  Tier-1 `DigestBinding` and `SignedBy` relations.
+- Verified and parsed-value constructors are private. The only production path
+  is decode, profile/field validation, CID/signature verification, then parse.
+- Cryptographic dispatch requires both an allowlist witness and the active
+  `TrustedProfile`; caller-created profiles cannot reach legacy dispatch.
+- The proof gate scans every Lean source in `formal/`, rejects proof escapes,
+  and rejects modules omitted from the root import graph.
+
 ---
 
 ### Task 1: Pin the standalone Lean project and write the failing contract test
diff --git a/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md b/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md
index 7f8cf54..4886c5b 100644
--- a/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md
+++ b/docs/superpowers/specs/2026-07-15-formal-ceremony-kernel-design.md
@@ -38,6 +38,10 @@ behind a small verified interface.
 - Make an accepted decision carry evidence that it belongs to the request it
   answers and cannot exceed that request's ceiling.
 - Bind authorization to a canonical structured action, not display text.
+- Bind every signed object to an explicit signed-bytes envelope whose canonical
+  body is transported unchanged through JSON/TOML views.
+- Domain-separate every signature by record type, store, causal thread or
+  principal, profile, and version.
 - Make attest challenges verifier-bound, action-bound, generation-bound, and
   single-use in the Tier-3 kernel. Enrollment and Introduction freshness are
   proved separately as a Tier-2 symbolic protocol.
@@ -72,9 +76,9 @@ Implementation follows the suite dependency DAG. Each proof boundary is a
 separate stacked PR so a reviewer can reject one profile without entangling
 its dependents:
 
-1. `formal: prove P1 signed-object contracts` -- Lean project, canonical
-   encoding contract, sealed-value boundary, version rejection, and
-   allowlist-before-dispatch.
+1. `formal: prove P1 signed-object contracts` -- Lean project, exact
+   signed-envelope decoding contract, universal signature domains, private
+   sealed-value boundary, version rejection, and trusted allowlist dispatch.
 2. `formal: prove P2 chain-store monotonicity` -- external-anchor trusted
    state, DAG extension, rollback/fork rejection, and untrusted-step safety.
 3. `formal: prove P0 authority resolution` -- product lattice, total
@@ -356,10 +360,39 @@ cannot produce a revocation transition.
 
 ## 11. Wire And Crypto Boundary
 
-Signed inputs include a domain separator containing protocol, object kind, and
-version. Authority-bearing v1 records reject unknown fields. Future versions
-must be explicitly selected and validated; they are not silently interpreted
-as v1.
+P1 resolves OB-4 with one authority-bearing transport shape. JSON and TOML are
+views over an embedded canonical byte string; they are never signed directly:
+
+```lean
+structure SignatureDomain where
+  recordType : RecordType
+  storeId : StoreId
+  threadOrPrincipal : ScopeId
+
+structure UnsignedEnvelope where
+  profile : ProfileId
+  codec : Codec
+  domain : SignatureDomain
+  body : ByteArray
+  cid : ContentId
+  signer : Fingerprint
+
+structure SignedEnvelope where
+  unsigned : UnsignedEnvelope
+  signatureAlgorithm : SignatureAlgorithm
+  signature : ByteArray
+```
+
+The signature input is the canonical encoding of the entire
+`UnsignedEnvelope`. Thus record type, store, causal thread or principal,
+profile, codec, body CID, and signer are universally domain-bound (OB-6).
+Authority-bearing v1 records reject unknown fields. Future versions must be
+explicitly selected and validated; they are not silently interpreted as v1.
+
+The parser remains outside the kernel, but its Tier-1 contract is exact: if
+`decode received = some envelope`, then `encode envelope = received`. The
+decoder cannot report invented security metadata for unrelated bytes. Shared
+vectors exercise the concrete DAG-CBOR and JSON/TOML envelope adapters.
 
 Opaque extension data is permitted only in fields declared non-authoritative.
 It remains covered by the canonical content digest and must survive a round
@@ -370,22 +403,33 @@ dispatching on a multihash or multicodec code, validation proves that the code
 belongs to the active profile. Profile rotation is an authorized state
 transition.
 
-The Lean boundary exposes assumptions such as:
+The Lean boundary exposes named assumptions such as:
 
 ```lean
-class CryptoAssumptions (Value Key Message Signature : Type) where
+class CryptoAssumptions (Value Key Message Signature Digest : Type) where
   canonicalInjective : forall {x y : Value},
     canonical x = canonical y -> x = y
-  digestBinding : forall {x y : Value},
-    digest x = digest y -> canonical x = canonical y
+  digestSound : forall {value : Value} {claimed : Digest},
+    digestMatches claimed (canonical value) -> claimed = digest (canonical value)
+  digestBinding : forall {left right : ByteArray},
+    digest left = digest right -> left = right
   signatureOrigin : forall {key : Key} {msg : Message} {sig : Signature},
     verifies key msg sig -> signedBy key msg sig
 ```
 
 These are assumptions used by protocol theorems, not claims that Lean proved
-the underlying cryptographic algorithms. `signatureOrigin` proves only which
-key produced a signature. Whether that key is authorized is a separate kernel
-predicate over the active principal, quorum policy, role, and policy epoch.
+the underlying cryptographic algorithms. The executable digest/signature
+predicates must carry proofs into these semantic relations; an arbitrary
+always-true callback is not an admissible boundary implementation.
+`signatureOrigin` proves only which key produced a signature. Whether that key
+is authorized is a separate kernel predicate over the active principal,
+quorum policy, role, and policy epoch.
+
+Verified and sealed types have private constructors. Production code obtains
+them only through the checked decoder/verifier path; the formal API exposes
+read-only evidence projections. Hash and signature dispatch additionally
+requires the active `TrustedProfile` witness, so a caller-created profile cannot
+manufacture a legacy algorithm path.
 
 The concrete checkpoint adapter has a similarly explicit environmental
 obligation: attacker-controlled log writes cannot alter the trusted checkpoint.
@@ -477,6 +521,11 @@ baseline while adding its profile-specific proof gate.
 - Resolution is proved permutation-invariant and non-amplifying.
 - A validated decision is proved request-bound, action-bound,
   matrix-contained, and ceiling-bounded.
+- A decoded signed envelope recomposes to the exact received bytes; its CID is
+  sound for the embedded canonical body and its signature is sound for the
+  universally domain-separated unsigned envelope.
+- Only a trusted active profile can dispatch cryptographic algorithms, and
+  verified/sealed constructors are private.
 - Attest challenges are proved single-use in the sequential kernel,
   generation-bound, and action-bound. P3 Introduction claims are absent from
   the Tier-3 acceptance gate and tracked in the Tier-2 protocol stack.
@@ -498,6 +547,9 @@ Reviewers should reject any change that:
 - moves rendering, serde, IO, or cryptographic implementation into the kernel;
 - treats a CID or parent link as freshness without trusted external state;
 - lets raw wire values bypass validated constructors;
+- accepts transport metadata that is not proved to recompose to the exact
+  received signed envelope;
+- signs a payload without record/store/thread-or-principal domain separation;
 - lets display text identify an executable effect;
 - accepts a decision without checking request, action, matrix, and ceiling;
 - treats a nonce as fresh without issuer and consumption state;