diff --git a/.githooks/pre-push b/.githooks/pre-push
index bb39df9..b83801a 100755
--- a/.githooks/pre-push
+++ b/.githooks/pre-push
@@ -1,11 +1,12 @@
 #!/usr/bin/env bash
 # agent-bridle pre-push hook — the local equivalent of CI gates.
 #
-# PIPELINE PARITY: this hook mirrors .github/workflows/ci.yml and the `check` /
-# `check-windows` / `publish-check` / `py-test` recipes in justfile. When editing the
-# lint/format/test/publish/python steps here, verify it still matches the CI
-# workflow and the justfile (HOOK PARITY rule). `check-windows` only does real work
-# on a Windows host (the AppContainer backend is Windows-only) and skips elsewhere.
+# PIPELINE PARITY: this hook mirrors .github/workflows/ci.yml and formal.yml,
+# plus the `check` / `check-formal` / `check-windows` / `publish-check` /
+# `py-test` recipes in justfile. When editing lint/format/test/proof/publish/
+# python steps here, verify they still match the owning CI workflow and the
+# justfile (HOOK PARITY rule). `check-windows` only does real work on a Windows
+# host (the AppContainer backend is Windows-only) and skips elsewhere.
 #
 # Do NOT bypass with --no-verify. If this fails, fix the issue.
 
@@ -14,6 +15,9 @@ set -euo pipefail
 echo "[pre-push] running 'just check' (fmt + clippy -D warnings + tests, full matrix)"
 just check
 
+echo "[pre-push] running 'just check-formal' (Lean proofs + integrity gate)"
+just check-formal
+
 echo "[pre-push] running 'just check-windows' (AppContainer backend + kernel proofs; skips off Windows)"
 just check-windows
 
diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml
new file mode 100644
index 0000000..2146ce1
--- /dev/null
+++ b/.github/workflows/formal.yml
@@ -0,0 +1,49 @@
+# Ceremony Suite formal proof gate.
+#
+# HOOK PARITY: `just check-formal` and `.githooks/pre-push` run the same
+# `lake build` plus `lake exe formalGate` locally. Keep all three in sync when
+# the proof command changes.
+
+name: Formal proofs
+
+on:
+  push:
+    paths:
+      - "formal/**"
+      - ".github/workflows/formal.yml"
+      - ".githooks/pre-push"
+      - "justfile"
+  pull_request:
+    paths:
+      - "formal/**"
+      - ".github/workflows/formal.yml"
+      - ".githooks/pre-push"
+      - "justfile"
+  workflow_dispatch: {}
+
+permissions:
+  contents: read
+
+jobs:
+  lean:
+    name: Lean (${{ matrix.os }})
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, windows-latest]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@v4
+      - name: Build P1 proofs and contract tests
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: true
+          lake-package-directory: formal
+          use-github-cache: false
+          use-mathlib-cache: false
+      - name: Reject proof escapes and omitted modules
+        working-directory: formal
+        shell: bash
+        run: |
+          "$HOME/.elan/bin/lake" exe formalGate
diff --git a/.gitignore b/.gitignore
index 2aa47d2..39edbfb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,6 +3,9 @@
 **/target
 Cargo.lock.orig
 
+# Lean / Lake
+**/.lake/
+
 # Coverage
 *.profraw
 /coverage
diff --git a/docs/TOOLCHAIN.md b/docs/TOOLCHAIN.md
index b2d8dee..d40c2f9 100644
--- a/docs/TOOLCHAIN.md
+++ b/docs/TOOLCHAIN.md
@@ -9,10 +9,11 @@ Package managers assumed: **apt** (Debian/Ubuntu) on Linux, **Homebrew** on
 macOS, **Chocolatey** on Windows. Anything not in a manager uses the tool's
 official installer script.
 
-**Verified state (2026-07-15):** §1 and the Lean/rustup halves of §2 are
-exercised on Linux. The macOS and Windows columns and the full Aeneas build
-follow upstream documentation and have not yet been executed here — trust,
-then verify, then update this line.
+**Verified state (2026-07-16):** §1 is exercised on Linux, macOS, and Windows.
+Lean `v4.31.0` and the P1 proof project have been exercised on native Windows;
+the formal workflow exercises the same build and proof-integrity gate on Linux
+and Windows. The full Aeneas/opam build and native macOS Lean remain unverified
+here; trust, then verify, then update this line.
 
 ---
 
@@ -53,14 +54,16 @@ Then, in the repository:
 ```sh
 just install-hooks   # mandatory — pre-push mirrors CI
 just check           # fmt + clippy (-D warnings, both feature configs) + tests
+just check-formal    # pinned build plus proof-escape/import-completeness gate
 ```
 
 `cargo-llvm-cov` is optional: the coverage recipe skips gracefully when it is
 absent and enforces the 75% floor when present.
 
-Windows note: `just` recipes assume a POSIX shell. Native builds work for the
-Rust workspace, but run `just` from Git Bash — or do everything in WSL2
-(Ubuntu) and follow the Linux column, which is the least-surprise path.
+Windows note: `just check-formal` and the direct Rust recipes run from native
+PowerShell. Recipes with embedded POSIX scripts (including the full hook) still
+require Git Bash, or run everything in WSL2 (Ubuntu) and follow the Linux
+column.
 
 ## 2. Formal-verification track (Lean · Charon · Aeneas)
 
@@ -131,9 +134,9 @@ cd aeneas && make                # Aeneas builds
 With §2 green, the Ceremony Contract's proof obligations (PO-1, PO-2 first)
 run as: carve the pure decision kernel in `agent-bridle-core` → Charon
 extracts LLBC → Aeneas emits Lean → theorems live in a `lake` project pinned
-by its `lean-toolchain`. CI integration for the proofs is future work and
-will be mirrored in the pre-push hook per the HOOK/PIPELINE PARITY rule when
-it lands.
+by its `lean-toolchain`. The P1 Lean project is built on Linux and Windows in
+`formal.yml`; `formalGate` and the pre-push hook mirror its proof-integrity
+checks per the HOOK/PIPELINE PARITY rule.
 
 Refs: #225 (formal-track thread), `docs/spec/ceremony-contract.md` (the
 obligations this toolchain discharges).
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 53b1540..bf69d0a 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
@@ -67,7 +67,7 @@ snippets:
 - Produces: Lake library `CeremonyFormal` rooted at `formal/Ceremony` and test
   import `Ceremony.P1.SignedObject`.
 
-- [ ] **Step 1: Add the toolchain and Lake configuration**
+- [x] **Step 1: Add the toolchain and Lake configuration**
 
 ```text
 leanprover/lean4:v4.31.0
@@ -89,7 +89,7 @@ srcDir = "."
 roots = ["Tests"]
 ```
 
-- [ ] **Step 2: Write a test importing the not-yet-created P1 module**
+- [x] **Step 2: Write a test importing the not-yet-created P1 module**
 
 ```lean
 import Ceremony.P1.SignedObject
@@ -104,13 +104,13 @@ example : Not (Profile.v1.allowsHash .sha1) := by decide
 import Tests.SignedObjectContracts
 ```
 
-- [ ] **Step 3: Run the test and verify RED**
+- [x] **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**
+- [x] **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.
@@ -126,29 +126,32 @@ default Lake target broken.
 - 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`.
+  `VerifiedEnvelope`, `Sealed`, `sealValue`, and
+  `sealed_eq_of_same_canonical`.
 
-- [ ] **Step 1: Extend the test with the wished-for sealing API**
+- [x] **Step 1: Extend the test with the wished-for sealing API**
 
 ```lean
 def bytesEncoding : CanonicalEncoding ByteArray where
   encode := id
-  injective := fun h => h
+  injective := by
+    intro left right h
+    exact 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
+example (value : ByteArray) : (sealValue bytesEncoding value).value = value := rfl
 ```
 
-- [ ] **Step 2: Run the test and verify RED**
+- [x] **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`.
+`sealValue`.
 
-- [ ] **Step 3: Implement the minimal P1 model**
+- [x] **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
@@ -206,14 +209,14 @@ structure Sealed {Value : Type} (encoding : CanonicalEncoding Value) where
   canonical : ByteArray
   canonical_eq : canonical = encoding.encode value
 
-def seal (encoding : CanonicalEncoding Value) (value : Value) : Sealed encoding :=
+def sealValue (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**
+- [x] **Step 4: Prove canonical identity and profile rejection**
 
 Add theorems with these exact signatures:
 
@@ -230,13 +233,13 @@ 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**
+- [x] **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**
+- [x] **Step 6: Commit the P1 model**
 
 ```text
 formal(lean): prove P1 signed-object contracts
@@ -258,7 +261,7 @@ Co-Authored-By: OpenAI GPT-5 <codex@openai.com>
   `verifyEnvelope`, `dispatchHash`, and rejection theorems for unsupported
   versions, critical fields, and algorithms.
 
-- [ ] **Step 1: Write failing tests for hostile inputs**
+- [x] **Step 1: Write failing tests for hostile inputs**
 
 ```lean
 def v1Envelope : RawEnvelope :=
@@ -301,13 +304,13 @@ theorem no_v1_sha1_witness
   exact sha1_not_allowed allowed.allowed
 ```
 
-- [ ] **Step 2: Run the test and verify RED**
+- [x] **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**
+- [x] **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
@@ -325,8 +328,7 @@ structure RawEnvelope where
   unknownCritical : List String
   deriving DecidableEq
 
-structure VerifiedEnvelope (profile : Profile) where
-  raw : RawEnvelope
+structure VerifiedEnvelope (profile : Profile) (raw : RawEnvelope) where
   version_eq : raw.version = profile.version
   critical_empty : raw.unknownCritical = []
   allowedHash : AllowedHash profile
@@ -337,13 +339,13 @@ structure VerifiedEnvelope (profile : Profile) where
   codec_eq : allowedCodec.codec = raw.codec
 
 def verifyEnvelope (profile : Profile) (raw : RawEnvelope) :
-    Option (VerifiedEnvelope profile) :=
+    Option (VerifiedEnvelope profile raw) :=
   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,
+            some { version_eq := hv, critical_empty := hc,
               allowedHash := { algorithm := raw.hash, allowed := hh },
               hash_eq := rfl,
               allowedSignature := { algorithm := raw.signature,
@@ -357,7 +359,7 @@ def verifyEnvelope (profile : Profile) (raw : RawEnvelope) :
   else none
 ```
 
-- [ ] **Step 4: Prove fail-closed behavior**
+- [x] **Step 4: Prove fail-closed behavior**
 
 Add theorems with these exact statements:
 
@@ -383,13 +385,13 @@ theorem unknown_critical_rejected
     verifyEnvelope profile raw = none
 ```
 
-- [ ] **Step 5: Run all Lean targets and verify GREEN**
+- [x] **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**
+- [x] **Step 6: Commit the verification boundary**
 
 ```text
 formal(lean): enforce allowlist-before-dispatch
@@ -400,23 +402,24 @@ 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`
+- Create: `.github/workflows/formal.yml`
+- Create: `formal/Gate.lean`
 - 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.
+- Produces: `just check-formal`, Linux and Windows `lake build` plus
+  `formalGate` jobs, and a pre-push invocation matching the required CI gate.
 
-- [ ] **Step 1: Add a failing local gate check**
+- [x] **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.
+Invoke the not-yet-defined `just check-formal` first and confirm Just rejects
+the missing recipe. Add `check-formal` with a per-recipe `formal` working
+directory so native Windows elan resolves the nested toolchain pin.
 
-- [ ] **Step 2: Install/resolve the pinned Lean toolchain and verify the gate**
+- [x] **Step 2: Install/resolve the pinned Lean toolchain and verify the gate**
 
 Run: `elan toolchain install leanprover/lean4:v4.31.0`
 
@@ -424,18 +427,20 @@ Run: `just check-formal`
 
 Expected: PASS.
 
-- [ ] **Step 3: Mirror the gate in CI and pre-push**
+- [x] **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.
+Add a dedicated formal workflow with an Ubuntu/Windows matrix using
+`leanprover/lean-action@v1`, `lake build`, and `lake exe formalGate`. Trigger
+it on formal-path pushes so stacked PR heads are checked before their base
+contains the workflow. Add `just check-formal` to `.githooks/pre-push`. Keep
+parity comments adjacent in all three files.
 
-- [ ] **Step 4: Update toolchain status accurately**
+- [x] **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**
+- [x] **Step 5: Run syntax and proof gates**
 
 Run: `just check-formal`
 
@@ -445,7 +450,7 @@ Run: `git diff --check`
 
 Expected: all PASS.
 
-- [ ] **Step 6: Commit CI enforcement**
+- [x] **Step 6: Commit CI enforcement**
 
 ```text
 ci(formal): gate P1 proofs on Linux and Windows
@@ -462,14 +467,15 @@ Co-Authored-By: OpenAI GPT-5 <codex@openai.com>
 - Consumes: all P1 commits.
 - Produces: a reviewable PR based on `feat/formal-ceremony-kernel`.
 
-- [ ] **Step 1: Scan for proof escapes**
+- [x] **Step 1: Execute the proof-integrity gate**
 
-Run: `rg -n '\b(sorry|admit|axiom)\b' formal`
+Run: `just check-formal`
 
-Expected: no matches. Named assumptions are represented as structure fields,
-not global axioms.
+Expected: the Lake build passes, `formalGate` reports that every Lean source
+and root import is verified, and deliberate escape/unimported-module probes
+fail with independent diagnostics.
 
-- [ ] **Step 2: Run the full native-Windows gate**
+- [x] **Step 2: Run the full native-Windows gate**
 
 Run: `just check-formal`
 
@@ -479,19 +485,24 @@ 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.
+Expected: P1's formal gate, Windows gate, formatting, workflow lint, and
+publishability gate pass. Any pre-existing parent-branch failures in broader
+feature-matrix or coverage commands are reproduced and reported verbatim in
+the PR body rather than generalized away.
 
-- [ ] **Step 3: Verify branch shape and attribution**
+- [x] **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**
+- [x] **Step 4: Push normally and open the PR**
 
-Push without bypassing hooks. Open a draft PR titled
+Attempt a normal push first. If the unchanged parent branch still fails the
+repository hook after all P1-owned gates pass, use only the author's explicit
+one-time bypass authorization and document the exact parent failures. 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
diff --git a/formal/Ceremony.lean b/formal/Ceremony.lean
new file mode 100644
index 0000000..cd68152
--- /dev/null
+++ b/formal/Ceremony.lean
@@ -0,0 +1 @@
+import Ceremony.P1.SignedObject
diff --git a/formal/Ceremony/P1/SignedObject.lean b/formal/Ceremony/P1/SignedObject.lean
new file mode 100644
index 0000000..b395946
--- /dev/null
+++ b/formal/Ceremony/P1/SignedObject.lean
@@ -0,0 +1,377 @@
+namespace Ceremony.P1
+
+inductive HashAlgorithm
+  | blake3_256
+  | sha1
+  deriving DecidableEq, Repr
+
+inductive SignatureAlgorithm
+  | ed25519
+  | ecdsa
+  deriving DecidableEq, Repr
+
+def SignatureAlgorithm.isDeterministic : SignatureAlgorithm -> Prop
+  | .ed25519 => True
+  | .ecdsa => False
+
+instance (algorithm : SignatureAlgorithm) :
+    Decidable algorithm.isDeterministic := by
+  cases algorithm <;> unfold SignatureAlgorithm.isDeterministic <;>
+    exact inferInstance
+
+inductive Codec
+  | dagCbor
+  | json
+  deriving DecidableEq, Repr
+
+structure Profile where
+  version : Nat
+  hashes : List HashAlgorithm
+  signatures : List SignatureAlgorithm
+  codecs : List Codec
+
+namespace Profile
+
+def v1 : Profile :=
+  { version := 1
+    hashes := [.blake3_256]
+    signatures := [.ed25519]
+    codecs := [.dagCbor] }
+
+def allowsHash (profile : Profile) (algorithm : HashAlgorithm) : Prop :=
+  algorithm ∈ profile.hashes
+
+instance (profile : Profile) (algorithm : HashAlgorithm) :
+    Decidable (allowsHash profile algorithm) := by
+  unfold allowsHash
+  infer_instance
+
+def allowsSignature (profile : Profile) (algorithm : SignatureAlgorithm) : Prop :=
+  algorithm ∈ profile.signatures
+
+instance (profile : Profile) (algorithm : SignatureAlgorithm) :
+    Decidable (allowsSignature profile algorithm) := by
+  unfold allowsSignature
+  infer_instance
+
+def allowsCodec (profile : Profile) (codec : Codec) : Prop :=
+  codec ∈ profile.codecs
+
+instance (profile : Profile) (codec : Codec) :
+    Decidable (allowsCodec profile codec) := by
+  unfold allowsCodec
+  infer_instance
+
+end Profile
+
+inductive TrustedProfile : Profile -> Type
+  | v1 : TrustedProfile Profile.v1
+
+theorem trusted_profile_is_v1
+    {profile : Profile} (_trusted : TrustedProfile profile) :
+    profile = Profile.v1 := by
+  cases _trusted
+  rfl
+
+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 CanonicalPayloadDecoder
+    (Value : Type) (encoding : CanonicalEncoding Value) where
+  parse : ByteArray -> Option Value
+  parse_exact : forall bytes value, parse bytes = some value ->
+    bytes = encoding.encode value
+
+structure SignatureDomain where
+  recordType : String
+  storeId : ByteArray
+  threadOrPrincipal : ByteArray
+  deriving DecidableEq
+
+structure SignaturePreimage where
+  canonicalUnsigned : ByteArray
+  profileVersion : Nat
+  hashAlgorithm : HashAlgorithm
+  signatureAlgorithm : SignatureAlgorithm
+  codec : Codec
+  domain : SignatureDomain
+  body : ByteArray
+  claimedCid : ByteArray
+  signer : ByteArray
+  unknownCritical : List String
+  deriving DecidableEq
+
+structure SignedEnvelopeCodec where
+  Envelope : Type
+  Unsigned : Type
+  encode : Envelope -> ByteArray
+  encode_injective : Function.Injective encode
+  decode : ByteArray -> Option Envelope
+  decode_exact : forall received envelope, decode received = some envelope ->
+    encode envelope = received
+  unsigned : Envelope -> Unsigned
+  encodeUnsigned : Unsigned -> ByteArray
+  unsigned_injective : Function.Injective encodeUnsigned
+  version : Unsigned -> Nat
+  hash : Unsigned -> HashAlgorithm
+  signatureAlgorithm : Unsigned -> SignatureAlgorithm
+  codec : Unsigned -> Codec
+  domain : Unsigned -> SignatureDomain
+  body : Unsigned -> ByteArray
+  claimedCid : Unsigned -> ByteArray
+  signer : Unsigned -> ByteArray
+  signatureBytes : Envelope -> ByteArray
+  unknownCritical : Unsigned -> List String
+
+def SignedEnvelopeCodec.signaturePreimage
+    (envelopeCodec : SignedEnvelopeCodec)
+    (unsigned : envelopeCodec.Unsigned) : SignaturePreimage :=
+  { canonicalUnsigned := envelopeCodec.encodeUnsigned unsigned
+    profileVersion := envelopeCodec.version unsigned
+    hashAlgorithm := envelopeCodec.hash unsigned
+    signatureAlgorithm := envelopeCodec.signatureAlgorithm unsigned
+    codec := envelopeCodec.codec unsigned
+    domain := envelopeCodec.domain unsigned
+    body := envelopeCodec.body unsigned
+    claimedCid := envelopeCodec.claimedCid unsigned
+    signer := envelopeCodec.signer unsigned
+    unknownCritical := envelopeCodec.unknownCritical unsigned }
+
+structure CryptoBoundary (profile : Profile) where
+  digest : AllowedHash profile -> ByteArray -> ByteArray
+  digest_binding : forall leftAllowed rightAllowed left right,
+    digest leftAllowed left = digest rightAllowed right ->
+      leftAllowed.algorithm = rightAllowed.algorithm /\ left = right
+  SignedBy : AllowedSignature profile -> SignaturePreimage -> ByteArray -> Prop
+  signatureMatches : AllowedSignature profile -> SignaturePreimage -> ByteArray -> Bool
+  signature_sound : forall allowed preimage signature,
+    signatureMatches allowed preimage signature = true ->
+      SignedBy allowed preimage signature
+  signature_binding : forall leftAllowed rightAllowed left right signature,
+    SignedBy leftAllowed left signature ->
+      SignedBy rightAllowed right signature ->
+        leftAllowed.algorithm = rightAllowed.algorithm /\ left = right
+  signature_deterministic : forall allowed preimage left right,
+    SignedBy allowed preimage left ->
+      SignedBy allowed preimage right -> left = right
+
+structure VerifiedEnvelope
+    (profile : Profile)
+    (envelopeCodec : SignedEnvelopeCodec)
+    (crypto : CryptoBoundary profile)
+    (received : ByteArray) where
+  private verified ::
+  envelope : envelopeCodec.Envelope
+  decoded_eq : envelopeCodec.decode received = some envelope
+  received_exact : envelopeCodec.encode envelope = received
+  trustedProfile : TrustedProfile profile
+  version_eq :
+    envelopeCodec.version (envelopeCodec.unsigned envelope) = profile.version
+  critical_empty :
+    envelopeCodec.unknownCritical (envelopeCodec.unsigned envelope) = []
+  allowedHash : AllowedHash profile
+  hash_eq :
+    allowedHash.algorithm = envelopeCodec.hash (envelopeCodec.unsigned envelope)
+  allowedSignature : AllowedSignature profile
+  signature_eq : allowedSignature.algorithm =
+    envelopeCodec.signatureAlgorithm (envelopeCodec.unsigned envelope)
+  allowedCodec : AllowedCodec profile
+  codec_eq :
+    allowedCodec.codec = envelopeCodec.codec (envelopeCodec.unsigned envelope)
+  digestEvidence :
+    envelopeCodec.claimedCid (envelopeCodec.unsigned envelope) =
+      crypto.digest allowedHash
+        (envelopeCodec.body (envelopeCodec.unsigned envelope))
+  signatureEvidence : crypto.SignedBy allowedSignature
+    (envelopeCodec.signaturePreimage (envelopeCodec.unsigned envelope))
+    (envelopeCodec.signatureBytes envelope)
+
+def verifyEnvelope
+    {profile : Profile}
+    (trustedProfile : TrustedProfile profile)
+    (envelopeCodec : SignedEnvelopeCodec)
+    (crypto : CryptoBoundary profile)
+    (received : ByteArray) :
+    Option (VerifiedEnvelope profile envelopeCodec crypto received) :=
+  match decodedEq : envelopeCodec.decode received with
+  | none => none
+  | some envelope =>
+      let unsigned := envelopeCodec.unsigned envelope
+      if versionEq : envelopeCodec.version unsigned = profile.version then
+        if criticalEmpty : envelopeCodec.unknownCritical unsigned = [] then
+          if hashAllowed : profile.allowsHash (envelopeCodec.hash unsigned) then
+            let allowedHash : AllowedHash profile :=
+              { algorithm := envelopeCodec.hash unsigned
+                allowed := hashAllowed }
+            if signatureAllowed :
+                profile.allowsSignature (envelopeCodec.signatureAlgorithm unsigned) then
+              let allowedSignature : AllowedSignature profile :=
+                { algorithm := envelopeCodec.signatureAlgorithm unsigned
+                  allowed := signatureAllowed }
+              if codecAllowed : profile.allowsCodec (envelopeCodec.codec unsigned) then
+                let allowedCodec : AllowedCodec profile :=
+                  { codec := envelopeCodec.codec unsigned
+                    allowed := codecAllowed }
+                if digestValid : envelopeCodec.claimedCid unsigned =
+                    crypto.digest allowedHash (envelopeCodec.body unsigned) then
+                  if signatureValid : crypto.signatureMatches allowedSignature
+                      (envelopeCodec.signaturePreimage unsigned)
+                      (envelopeCodec.signatureBytes envelope) = true then
+                    some
+                      { envelope
+                        decoded_eq := decodedEq
+                        received_exact :=
+                          envelopeCodec.decode_exact received envelope decodedEq
+                        trustedProfile
+                        version_eq := versionEq
+                        critical_empty := criticalEmpty
+                        allowedHash
+                        hash_eq := rfl
+                        allowedSignature
+                        signature_eq := rfl
+                        allowedCodec
+                        codec_eq := rfl
+                        digestEvidence := digestValid
+                        signatureEvidence :=
+                          crypto.signature_sound _ _ _ signatureValid }
+                  else none
+                else none
+              else none
+            else none
+          else none
+        else none
+      else none
+
+structure Sealed
+    {Value : Type}
+    (encoding : CanonicalEncoding Value)
+    (profile : Profile)
+    (envelopeCodec : SignedEnvelopeCodec)
+    (crypto : CryptoBoundary profile)
+    (received : ByteArray) where
+  private sealed ::
+  verified : VerifiedEnvelope profile envelopeCodec crypto received
+  value : Value
+  canonical_eq :
+    envelopeCodec.body (envelopeCodec.unsigned verified.envelope) =
+      encoding.encode value
+
+def parseVerified
+    {Value : Type}
+    {encoding : CanonicalEncoding Value}
+    (decoder : CanonicalPayloadDecoder Value encoding)
+    {profile : Profile}
+    {envelopeCodec : SignedEnvelopeCodec}
+    {crypto : CryptoBoundary profile}
+    {received : ByteArray}
+    (verified : VerifiedEnvelope profile envelopeCodec crypto received) :
+    Option (Sealed encoding profile envelopeCodec crypto received) :=
+  let body := envelopeCodec.body (envelopeCodec.unsigned verified.envelope)
+  match parsedEq : decoder.parse body with
+  | none => none
+  | some value =>
+      some
+        { verified
+          value
+          canonical_eq := decoder.parse_exact body value parsedEq }
+
+def loadEnvelope
+    {Value : Type}
+    {encoding : CanonicalEncoding Value}
+    (decoder : CanonicalPayloadDecoder Value encoding)
+    {profile : Profile}
+    (trustedProfile : TrustedProfile profile)
+    (envelopeCodec : SignedEnvelopeCodec)
+    (crypto : CryptoBoundary profile)
+    (received : ByteArray) :
+    Option (Sealed encoding profile envelopeCodec crypto received) :=
+  match verifyEnvelope trustedProfile envelopeCodec crypto received with
+  | none => none
+  | some verified => parseVerified decoder verified
+
+theorem sealed_value_unique
+    {Value : Type}
+    {encoding : CanonicalEncoding Value}
+    {profile : Profile}
+    {envelopeCodec : SignedEnvelopeCodec}
+    {crypto : CryptoBoundary profile}
+    {received : ByteArray}
+    (left right : Sealed encoding profile envelopeCodec crypto received) :
+    left.value = right.value := by
+  have envelopeEq : left.verified.envelope = right.verified.envelope :=
+    envelopeCodec.encode_injective <|
+      left.verified.received_exact.trans right.verified.received_exact.symm
+  have bodyEq :
+      envelopeCodec.body (envelopeCodec.unsigned left.verified.envelope) =
+        envelopeCodec.body (envelopeCodec.unsigned right.verified.envelope) :=
+    congrArg (fun envelope =>
+      envelopeCodec.body (envelopeCodec.unsigned envelope)) envelopeEq
+  apply encoding.injective
+  exact left.canonical_eq.symm.trans (bodyEq.trans right.canonical_eq)
+
+theorem blake3_allowed : Profile.v1.allowsHash .blake3_256 := by decide
+
+theorem sha1_not_allowed : Not (Profile.v1.allowsHash .sha1) := by decide
+
+theorem ed25519_allowed : Profile.v1.allowsSignature .ed25519 := by decide
+
+theorem ecdsa_not_allowed : Not (Profile.v1.allowsSignature .ecdsa) := by decide
+
+theorem v1_signature_is_deterministic
+    (allowed : AllowedSignature Profile.v1) :
+    allowed.algorithm.isDeterministic := by
+  rcases allowed with ⟨algorithm, algorithmAllowed⟩
+  cases algorithm with
+  | ed25519 => trivial
+  | ecdsa => exact False.elim (ecdsa_not_allowed algorithmAllowed)
+
+theorem dag_cbor_allowed : Profile.v1.allowsCodec .dagCbor := by decide
+
+theorem json_not_allowed : Not (Profile.v1.allowsCodec .json) := by decide
+
+inductive HashImplementation
+  | blake3
+  | legacySha1
+  deriving DecidableEq, Repr
+
+theorem trusted_hash_is_blake3
+    {profile : Profile}
+    (trusted : TrustedProfile profile)
+    (allowed : AllowedHash profile) :
+    allowed.algorithm = .blake3_256 := by
+  have profileEq := trusted_profile_is_v1 trusted
+  subst profile
+  cases algorithmEq : allowed.algorithm with
+  | blake3_256 => rfl
+  | sha1 =>
+      exfalso
+      apply sha1_not_allowed
+      simpa [algorithmEq] using allowed.allowed
+
+theorem no_v1_sha1_witness (allowed : AllowedHash Profile.v1) :
+    Not (allowed.algorithm = .sha1) := by
+  intro algorithmEq
+  have trustedEq := trusted_hash_is_blake3 TrustedProfile.v1 allowed
+  simp [algorithmEq] at trustedEq
+
+def dispatchHash
+    {profile : Profile}
+    (trusted : TrustedProfile profile)
+    (allowed : AllowedHash profile) : HashImplementation :=
+  match trusted_hash_is_blake3 trusted allowed with
+  | _ => .blake3
+
+end Ceremony.P1
diff --git a/formal/Gate.lean b/formal/Gate.lean
new file mode 100644
index 0000000..d622d6f
--- /dev/null
+++ b/formal/Gate.lean
@@ -0,0 +1,43 @@
+def moduleName (path : System.FilePath) : String :=
+  let components := path.components.filter fun component => component != "."
+  String.intercalate "." <| components.map fun component =>
+    if component.endsWith ".lean" then (component.dropEnd 5).copy else component
+
+def hasDirectImport (rootSource module : String) : Bool :=
+  (rootSource.splitOn "\n").any fun line =>
+    line.trimAscii.copy == s!"import {module}"
+
+def proofEscapeErrors
+    (path : System.FilePath) (source : String) : Array String := Id.run do
+  let forbidden := #["sor" ++ "ry", "ad" ++ "mit", "ax" ++ "iom"]
+  let mut errors := #[]
+  for word in forbidden do
+    if source.contains word then
+      errors := errors.push s!"{path}: forbidden proof escape `{word}`"
+  return errors
+
+def isFormalRoot (module : String) : Bool :=
+  module == "Ceremony" || module == "Tests" || module == "Gate"
+
+def main : IO Unit := do
+  let ceremonyRoot <- IO.FS.readFile "Ceremony.lean"
+  let testsRoot <- IO.FS.readFile "Tests.lean"
+  let mut errors := #[]
+  let paths <- (System.FilePath.mk ".").walkDir fun path =>
+    pure (!path.components.contains ".lake")
+  for path in paths do
+    if path.extension == some "lean" && !path.components.contains ".lake" then
+      let source <- IO.FS.readFile path
+      errors := errors ++ proofEscapeErrors path source
+      let module := moduleName path
+      if !isFormalRoot module &&
+          !hasDirectImport ceremonyRoot module &&
+          !hasDirectImport testsRoot module then
+        errors := errors.push
+          s!"{path}: `{module}` is absent from Ceremony.lean and Tests.lean"
+  if errors.isEmpty then
+    IO.println "formal gate: all Lean sources and root imports verified"
+  else
+    for error in errors do
+      IO.eprintln s!"formal gate: {error}"
+    throw <| IO.userError s!"formal gate rejected {errors.size} violation(s)"
diff --git a/formal/Tests.lean b/formal/Tests.lean
new file mode 100644
index 0000000..d8124b1
--- /dev/null
+++ b/formal/Tests.lean
@@ -0,0 +1,2 @@
+import Tests.SignedObjectContracts
+import Tests.P1Counterexamples
diff --git a/formal/Tests/P1Counterexamples.lean b/formal/Tests/P1Counterexamples.lean
new file mode 100644
index 0000000..a305118
--- /dev/null
+++ b/formal/Tests/P1Counterexamples.lean
@@ -0,0 +1,18 @@
+import Ceremony.P1.SignedObject
+
+open Ceremony.P1
+
+def unsafeDispatch : HashAlgorithm -> HashImplementation
+  | .blake3_256 => .blake3
+  | .sha1 => .legacySha1
+
+example : unsafeDispatch .sha1 = .legacySha1 := rfl
+
+example (allowed : AllowedHash Profile.v1) :
+    Not (allowed.algorithm = .sha1) :=
+  no_v1_sha1_witness allowed
+
+example : dispatchHash
+    TrustedProfile.v1
+    ({ algorithm := .blake3_256, allowed := blake3_allowed } :
+      AllowedHash Profile.v1) = .blake3 := rfl
diff --git a/formal/Tests/SignedObjectContracts.lean b/formal/Tests/SignedObjectContracts.lean
new file mode 100644
index 0000000..1d14d92
--- /dev/null
+++ b/formal/Tests/SignedObjectContracts.lean
@@ -0,0 +1,282 @@
+import Ceremony.P1.SignedObject
+
+open Ceremony.P1
+
+example : Profile.v1.allowsHash .blake3_256 := by decide
+
+example : Not (Profile.v1.allowsHash .sha1) := by decide
+
+example : Profile.v1.allowsSignature .ed25519 := by decide
+
+example : Not (Profile.v1.allowsSignature .ecdsa) := by decide
+
+example (allowed : AllowedSignature Profile.v1) :
+    allowed.algorithm.isDeterministic :=
+  v1_signature_is_deterministic allowed
+
+example : Profile.v1.allowsCodec .dagCbor := by decide
+
+example : Not (Profile.v1.allowsCodec .json) := by decide
+
+def attackerProfile : Profile :=
+  { Profile.v1 with hashes := [.sha1] }
+
+example (trusted : TrustedProfile attackerProfile) : False := by
+  cases trusted
+
+def bytesEncoding : CanonicalEncoding ByteArray where
+  encode := id
+  injective := by
+    intro left right h
+    exact h
+
+def bytesDecoder : CanonicalPayloadDecoder ByteArray bytesEncoding where
+  parse := some
+  parse_exact := by
+    intro bytes value parsed
+    cases parsed
+    rfl
+
+def goodReceived : ByteArray := ByteArray.mk #[1]
+
+def alteredBodyReceived : ByteArray := ByteArray.mk #[2]
+
+def alteredDomainReceived : ByteArray := ByteArray.mk #[3]
+
+def alteredSignatureReceived : ByteArray := ByteArray.mk #[4]
+
+def unsupportedVersionReceived : ByteArray := ByteArray.mk #[5]
+
+def sha1Received : ByteArray := ByteArray.mk #[6]
+
+def ecdsaReceived : ByteArray := ByteArray.mk #[7]
+
+def jsonReceived : ByteArray := ByteArray.mk #[8]
+
+def unknownCriticalReceived : ByteArray := ByteArray.mk #[9]
+
+def unrelatedReceived : ByteArray := ByteArray.mk #[10]
+
+def alteredCidReceived : ByteArray := ByteArray.mk #[11]
+
+def alteredRecordTypeReceived : ByteArray := ByteArray.mk #[12]
+
+def alteredStoreReceived : ByteArray := ByteArray.mk #[13]
+
+def alteredSignerReceived : ByteArray := ByteArray.mk #[14]
+
+def goodBody : ByteArray := ByteArray.mk #[20, 21]
+
+def alteredBody : ByteArray := ByteArray.mk #[20, 22]
+
+def goodCid : ByteArray := goodBody
+
+def goodSigner : ByteArray := ByteArray.mk #[40, 41]
+
+def alteredSigner : ByteArray := ByteArray.mk #[40, 42]
+
+def goodSignature : ByteArray := ByteArray.mk #[50, 51]
+
+def alteredSignature : ByteArray := ByteArray.mk #[50, 52]
+
+def goodDomain : SignatureDomain :=
+  { recordType := "grant-record"
+    storeId := ByteArray.mk #[60]
+    threadOrPrincipal := ByteArray.mk #[61] }
+
+def alteredDomain : SignatureDomain :=
+  { goodDomain with threadOrPrincipal := ByteArray.mk #[62] }
+
+def alteredRecordTypeDomain : SignatureDomain :=
+  { goodDomain with recordType := "decision-record" }
+
+def alteredStoreDomain : SignatureDomain :=
+  { goodDomain with storeId := ByteArray.mk #[63] }
+
+def testUnsigned (envelope : ByteArray) : ByteArray :=
+  if envelope = alteredSignatureReceived then goodReceived else envelope
+
+def testEnvelopeCodec : SignedEnvelopeCodec where
+  Envelope := ByteArray
+  Unsigned := ByteArray
+  encode := id
+  encode_injective := by
+    intro left right h
+    exact h
+  decode := some
+  decode_exact := by
+    intro received envelope decoded
+    cases decoded
+    rfl
+  unsigned := testUnsigned
+  encodeUnsigned := id
+  unsigned_injective := by
+    intro left right h
+    exact h
+  version := fun unsigned =>
+    if unsigned = unsupportedVersionReceived then 2 else 1
+  hash := fun unsigned =>
+    if unsigned = sha1Received then .sha1 else .blake3_256
+  signatureAlgorithm := fun unsigned =>
+    if unsigned = ecdsaReceived then .ecdsa else .ed25519
+  codec := fun unsigned =>
+    if unsigned = jsonReceived then .json else .dagCbor
+  domain := fun unsigned =>
+    if unsigned = alteredDomainReceived then alteredDomain
+    else if unsigned = alteredRecordTypeReceived then alteredRecordTypeDomain
+    else if unsigned = alteredStoreReceived then alteredStoreDomain
+    else goodDomain
+  body := fun unsigned =>
+    if unsigned = alteredBodyReceived then alteredBody else goodBody
+  claimedCid := fun unsigned =>
+    if unsigned = alteredCidReceived then alteredBody else goodCid
+  signer := fun unsigned =>
+    if unsigned = alteredSignerReceived then alteredSigner else goodSigner
+  signatureBytes := fun envelope =>
+    if envelope = alteredSignatureReceived then alteredSignature else goodSignature
+  unknownCritical := fun unsigned =>
+    if unsigned = unknownCriticalReceived then ["future-authority"] else []
+
+def crossCodecReplay : SignedEnvelopeCodec :=
+  { testEnvelopeCodec with
+    domain := fun (unsigned : ByteArray) =>
+      if unsigned = goodReceived then alteredRecordTypeDomain
+      else testEnvelopeCodec.domain unsigned }
+
+def goodPreimage : SignaturePreimage :=
+  { canonicalUnsigned := goodReceived
+    profileVersion := 1
+    hashAlgorithm := .blake3_256
+    signatureAlgorithm := .ed25519
+    codec := .dagCbor
+    domain := goodDomain
+    body := goodBody
+    claimedCid := goodCid
+    signer := goodSigner
+    unknownCritical := [] }
+
+def exactCrypto : CryptoBoundary Profile.v1 where
+  digest := fun _allowed body => body
+  digest_binding := by
+    intro leftAllowed rightAllowed left right sameDigest
+    exact
+      ⟨(trusted_hash_is_blake3 TrustedProfile.v1 leftAllowed).trans
+          (trusted_hash_is_blake3 TrustedProfile.v1 rightAllowed).symm,
+        sameDigest⟩
+  SignedBy := fun allowed preimage signature =>
+    allowed.algorithm = .ed25519 /\ preimage = goodPreimage /\
+      signature = goodSignature
+  signatureMatches := fun allowed preimage signature =>
+    decide (allowed.algorithm = .ed25519 /\ preimage = goodPreimage /\
+      signature = goodSignature)
+  signature_sound := by
+    intro allowed preimage signature valid
+    exact of_decide_eq_true valid
+  signature_binding := by
+    intro leftAllowed rightAllowed left right _signature leftValid rightValid
+    exact
+      ⟨leftValid.1.trans rightValid.1.symm,
+        leftValid.2.1.trans rightValid.2.1.symm⟩
+  signature_deterministic := by
+    intro _allowed _preimage left right leftValid rightValid
+    exact leftValid.2.2.trans rightValid.2.2.symm
+
+example {received envelope}
+    (decoded : testEnvelopeCodec.decode received = some envelope) :
+    testEnvelopeCodec.encode envelope = received :=
+  testEnvelopeCodec.decode_exact received envelope decoded
+
+example : testEnvelopeCodec.signaturePreimage goodReceived = goodPreimage := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      goodReceived).isSome := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      alteredBodyReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      alteredDomainReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      alteredRecordTypeReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      alteredStoreReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      alteredSignerReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      alteredCidReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 crossCodecReplay exactCrypto
+      goodReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      alteredSignatureReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      unsupportedVersionReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      sha1Received).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      ecdsaReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      jsonReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      unknownCriticalReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      unrelatedReceived).isNone := by
+  decide
+
+example :
+    (verifyEnvelope TrustedProfile.v1 testEnvelopeCodec exactCrypto goodReceived).map
+      (fun verified => testEnvelopeCodec.encode verified.envelope) =
+        some goodReceived := by
+  decide
+
+example :
+    (loadEnvelope bytesDecoder TrustedProfile.v1 testEnvelopeCodec exactCrypto
+      goodReceived).map (fun sealed => sealed.value) = some goodBody := by
+  decide
+
+example
+    (left right :
+      Sealed bytesEncoding Profile.v1 testEnvelopeCodec exactCrypto goodReceived) :
+    left.value = right.value :=
+  sealed_value_unique left right
diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json
new file mode 100644
index 0000000..a3ecba2
--- /dev/null
+++ b/formal/lake-manifest.json
@@ -0,0 +1,6 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "«ceremony-formal»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/formal/lakefile.toml b/formal/lakefile.toml
new file mode 100644
index 0000000..0fda4e9
--- /dev/null
+++ b/formal/lakefile.toml
@@ -0,0 +1,21 @@
+name = "ceremony-formal"
+version = "0.1.0"
+defaultTargets = ["CeremonyFormal", "CeremonyTests"]
+
+[[lean_lib]]
+name = "CeremonyFormal"
+srcDir = "."
+roots = ["Ceremony"]
+moreLeanArgs = ["-DwarningAsError=true"]
+
+[[lean_lib]]
+name = "CeremonyTests"
+srcDir = "."
+roots = ["Tests"]
+moreLeanArgs = ["-DwarningAsError=true"]
+
+[[lean_exe]]
+name = "formalGate"
+srcDir = "."
+root = "Gate"
+moreLeanArgs = ["-DwarningAsError=true"]
diff --git a/formal/lean-toolchain b/formal/lean-toolchain
new file mode 100644
index 0000000..18640c8
--- /dev/null
+++ b/formal/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.31.0
diff --git a/justfile b/justfile
index 243b811..d62046a 100644
--- a/justfile
+++ b/justfile
@@ -1,8 +1,13 @@
 # agent-bridle build recipes.
 #
 # PIPELINE PARITY: these recipes mirror .githooks/pre-push and
-# .github/workflows/ci.yml. When editing the lint/format/test steps here,
-# update the push hook AND the CI workflow to match (HOOK PARITY rule).
+# .github/workflows/ci.yml plus formal.yml. When editing the
+# lint/format/test/proof steps here, update the push hook AND the owning CI
+# workflow to match (HOOK PARITY rule).
+
+# `windows-shell` keeps native Windows compatible with just 1.46; newer just
+# versions also accept the `[windows] set shell` spelling.
+set windows-shell := ["powershell.exe", "-NoLogo", "-NoProfile", "-Command"]
 
 # Default: list recipes.
 default:
@@ -29,6 +34,14 @@ check:
     cargo test --workspace --all-features
     cargo test --workspace --no-default-features
 
+# Lean proof gate. Mirrors `.github/workflows/formal.yml` and is run by the
+# pre-push hook on every platform. Lake reads `formal/lean-toolchain`;
+# warning-as-error and `formalGate` reject proof escapes and omitted modules.
+[working-directory: 'formal']
+check-formal:
+    lake build
+    lake exe formalGate
+
 # Windows AppContainer L3 backend checks — the local mirror of the `check-windows`
 # job in .github/workflows/ci.yml (and nightly-windows.yml). The `appcontainer_impl`
 # module and the `agent-bridle-aclaunch` launcher only compile on Windows, so this