diff --git a/.devcontainer/Containerfile b/.devcontainer/Containerfile
new file mode 100644
index 0000000..ad46a6f
--- /dev/null
+++ b/.devcontainer/Containerfile
@@ -0,0 +1,33 @@
+# Dev container image for epistemic-types.
+#
+# Toolchain parity with .github/workflows/agda.yml: the same Debian 13 base
+# image digest as CI, with the same pinned Agda (agda-bin=2.6.4.3-1+b2), so a
+# first run inside this container reproduces the CI proof gates. ripgrep is
+# required by tests/check-rejections.sh; just is the task runner entry point.
+#
+# Build manually with:
+#   docker build -t epistemic-types-dev -f .devcontainer/Containerfile .
+# or let VS Code Dev Containers / Codespaces / the devcontainer CLI build it.
+
+FROM debian:13-slim@sha256:d7e12182ce18b85b93007c1dedf31f2d29e01ccf3182cc4017c709b6259bc132
+
+ENV LANG=C.UTF-8 \
+    LC_ALL=C.UTF-8 \
+    DEBIAN_FRONTEND=noninteractive
+
+RUN apt-get update \
+ && apt-get install --no-install-recommends -y \
+      bash \
+      ca-certificates \
+      git \
+      just \
+      make \
+      ripgrep \
+      agda-bin=2.6.4.3-1+b2 \
+ && rm -rf /var/lib/apt/lists/*
+
+RUN test "$(agda --version)" = 'Agda version 2.6.4.3'
+
+WORKDIR /workspaces/epistemic-types
+
+CMD ["bash"]
diff --git a/.devcontainer/README.adoc b/.devcontainer/README.adoc
new file mode 100644
index 0000000..a540001
--- /dev/null
+++ b/.devcontainer/README.adoc
@@ -0,0 +1,43 @@
+= Dev container — epistemic-types
+:revdate: 2026-10-04
+
+== What this is
+
+`.devcontainer/Containerfile` builds a Debian 13 image pinned to the same base
+digest as the repository's Proof Safety workflow, and installs the same Agda
+(`agda-bin=2.6.4.3-1+b2`) plus `bash`, `git`, `just`, `make` and `ripgrep`
+(`tests/check-rejections.sh` needs `rg`). `devcontainer.json` runs `just check`
+once, after creation, so a fresh container either reproduces the positive and
+expected-rejection proof gates or reports the failing gate.
+
+== Usage
+
+* *VS Code*: install the *Dev Containers* extension and choose
+  **Reopen in Container** from the command palette.
+* *Codespaces / GitHub web*: **Code > Codespaces > New codespace**.
+* *CLI*: run the standard devcontainer CLI against this repository, or build the
+  image directly:
+
+[source,sh]
+----
+docker build -t epistemic-types-dev -f .devcontainer/Containerfile .
+docker run --rm -it -v "$PWD":/workspaces/epistemic-types epistemic-types-dev
+# then inside the container:
+just check
+----
+
+== Toolchain parity
+
+The image digest in the `FROM` line is the digest used by
+`.github/workflows/agda.yml` for both of its jobs, and the Agda package version
+is the one CI asserts before running the gates. CI invokes the same
+`scripts/check.sh` entry point, so a passing container check and a passing CI
+check mean the same gate, on the same toolchain.
+
+== What is not verified here
+
+This container defines the first-run environment; it is not a claim about
+non-Linux hosts, other Agda versions, or the optional canonical-Echo gate
+(`just check-canonical`), which needs a reviewed `echo-types` checkout and a
+writable Agda standard-library source tree and is therefore not part of first
+run.
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
new file mode 100644
index 0000000..ccd4ce2
--- /dev/null
+++ b/.devcontainer/devcontainer.json
@@ -0,0 +1,23 @@
+{
+  "name": "epistemic-types (Agda 2.6.4.3, CI-matched)",
+  "build": {
+    "dockerfile": "Containerfile",
+    "context": "."
+  },
+  "postCreateCommand": "just check",
+  "containerEnv": {
+    "LANG": "C.UTF-8",
+    "LC_ALL": "C.UTF-8"
+  },
+  "customizations": {
+    "vscode": {
+      "extensions": [
+        "banacorn.agda-mode",
+        "asciidoctor.asciidoctor-vscode",
+        "timonwong.shellcheck",
+        "skellock.just"
+      ]
+    }
+  },
+  "shutdownAction": "stopContainer"
+}
diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml
index 7e924e7..8c814f0 100644
--- a/.github/workflows/agda.yml
+++ b/.github/workflows/agda.yml
@@ -40,8 +40,7 @@ jobs:
       - name: Verify toolchain and proof constructions
         run: |
           test "$(agda --version)" = 'Agda version 2.6.4.3'
-          bash tests/check-proofs.sh
-          bash tests/check-rejections.sh
+          bash scripts/check.sh
 
   echo:
     name: Canonical Echo correspondence
diff --git a/.machine_readable/descriptiles/META.a2ml b/.machine_readable/descriptiles/META.a2ml
index 4591f3d..2d064d8 100644
--- a/.machine_readable/descriptiles/META.a2ml
+++ b/.machine_readable/descriptiles/META.a2ml
@@ -3,7 +3,7 @@
 
 [metadata]
 version = "0.1.0"
-last-updated = "2026-06-15"
+last-updated = "2026-10-04"
 
 [project-info]
 name = "epistemic-types"
@@ -23,7 +23,8 @@ adrs = [
   { id = "ADR-003", title = "Compile under --safe --without-K", status = "accepted", date = "2026-06-15" },
   { id = "ADR-004", title = "No Agda standard library; build with agda --no-libraries", status = "accepted", date = "2026-06-15" },
   { id = "ADR-005", title = "Keep certified residues and resource bounds distinct from epistemic standpoints", status = "accepted", date = "2026-06-15" },
-  { id = "ADR-006", title = "ProofTransport: no smuggling by construction", status = "accepted", date = "2026-06-15" }
+  { id = "ADR-006", title = "ProofTransport: no smuggling by construction", status = "accepted", date = "2026-06-15" },
+  { id = "ADR-007", title = "Secret types and information-flow control are specified outside this repository", status = "accepted", date = "2026-10-04" }
 ]
 
 [architecture-decisions.ADR-001]
@@ -68,14 +69,21 @@ context = "When attestations cross trust boundaries, a naive design lets a sende
 decision = "`View : Agent -> Artifact -> Status -> Claim -> Set` is standpoint-indexed. `transmit` downgrades a sender's `Proof` to a receiver's `Receipt`; `verify` upgrades `Data -> Proof` only with the receiver's OWN checker and evidence (`proofNeedsChecker`). Public views are portable, designated views are receiver-bound, and receipt-only views never certify."
 consequence = "No-smuggling holds structurally rather than by side-condition. The engineering rendering for a2ml/k9 lives in `.machine_readable/proof-transport/`; the worked attestation is `ProofTransportExample` (issuer K9SVC, receiver Alice, third party Bob, claim ActionWasPerformed, artifact AttestationBlob)."
 
+[architecture-decisions.ADR-007]
+title = "Secret types and information-flow control are specified outside this repository"
+status = "accepted"
+context = "Issue #29 preserved a secret-types research note here; issue #32 then proposed an in-repository security model. On 2026-10-04 the owner ruled that hyperpolymath/secret-types is the standalone home, with D153 (a secret type is a value whose flow is constrained by a confidentiality label with explicit declassification, registered in the type-family map on that boundary) and D154 (reuse an existing lattice, two-point first then general; prove noninterference; declassify only at explicit audited points)."
+decision = "This repository adds no Secret API and no information-flow implementation. docs/secret-types.adoc is retained as the boundary/history note; the specification itself, lattice reuse, the noninterference theorem, and audited declassification belong to hyperpolymath/secret-types."
+consequence = "The epistemic core keeps its scope: no confidentiality claim attaches to BeliefModality, Echo grades, or Access. epistemic-types#29 stays closed; the move of issue #32 must not be duplicated."
+
 [development-practices]
 build-tool = "just"
 build-command = "just check"
-check-command = "agda --no-libraries -i src src/EpistemicTypes/All.agda"
+check-command = "bash scripts/check.sh (local Agda when present, otherwise 'guix shell -D -f build/guix.scm -- bash scripts/check.sh')"
 agda-version = "2.6.4.3"
-package-manager = "none (single agda-lib; no external Agda dependencies)"
-ci-platform = "none (billing wall; see AUDIT.adoc)"
-container-runtime = "none"
+package-manager = "none (single agda-lib; no external Agda dependencies); development environment in build/guix.scm"
+ci-platform = "GitHub Actions (Proof Safety, Governance, CodeQL, secret scan); see docs/ci-safety.adoc"
+container-runtime = "dev container in .devcontainer/ (Debian 13 base digest and agda-bin version matched to CI)"
 
 [design-rationale]
 posture = "Mathematical honesty over API size. The library is small on purpose: every law is either proved or an explicit obligation, and nothing is postulated."
diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml
index b80fa13..b8720a9 100644
--- a/.machine_readable/descriptiles/STATE.a2ml
+++ b/.machine_readable/descriptiles/STATE.a2ml
@@ -1,7 +1,7 @@
 [metadata]
 project = "epistemic-types"
 version = "0.1.0"
-last-updated = "2026-09-27"
+last-updated = "2026-10-04"
 status = "prototype"  # prototype | active | paused | archived
 
 [project-context]
@@ -19,10 +19,16 @@ maturity = "experimental"  # experimental | alpha | beta | production | lts
 discipline = "Constructive. Compiles under {-# OPTIONS --safe --without-K #-}. No postulates. No Agda standard library (built with 'agda --no-libraries'; only Agda.Builtin.* / Agda.Primitive)."
 honesty-rule = "Laws appear as explicit fields when not derivable; lawful instances are added only after proving or explicitly assuming the laws. No smuggling."
 
+[boundaries]
+secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153: label-constrained flow with explicit declassification and type-family-map registration; D154: reuse an existing lattice two-point-first, prove noninterference, declassify only at explicit audited points). This repository adds no Secret API and no information-flow implementation; docs/secret-types.adoc is retained as the boundary/history note. epistemic-types#29 is resolved and stays closed; the transfer of epistemic-types#32 to secret-types is pending GitHub issue-write access and must not be duplicated."
+
 [build]
-checker = "Agda 2.6.4.3"
+checker = "Agda 2.6.4.3 (CI-matched)"
 command = "just check"
+entry-point = "scripts/check.sh — local agda when present, else 'guix shell -D -f build/guix.scm -- bash scripts/check.sh'"
 expands-to = "bash tests/check-proofs.sh && bash tests/check-rejections.sh"
+dev-container = ".devcontainer/ — Debian 13 pinned to the same base image digest as CI, agda-bin=2.6.4.3-1+b2; postCreateCommand runs 'just check'"
+ci-entry-point = ".github/workflows/agda.yml asserts 'Agda version 2.6.4.3', then runs 'bash scripts/check.sh'"
 aggregator = "src/EpistemicTypes/All.agda re-exports every module."
 
 [modules]
diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
index a6ed4f8..0501a06 100644
--- a/0-AI-MANIFEST.a2ml
+++ b/0-AI-MANIFEST.a2ml
@@ -4,7 +4,7 @@ title = "epistemic-types — universal AI agent entry point"
 version = "0.1.0"
 format = "a2ml"
 status = "prototype"
-last-updated = "2026-09-07"
+last-updated = "2026-10-04"
 
 [project]
 name = "epistemic-types"
@@ -36,11 +36,17 @@ format = "AsciiDoc (.adoc) is the default; existing lowercase doc filenames are
 scm-files-location = ".machine_readable/ ONLY — a2ml and scm/Nickel/k9 files never live at repo root"
 license = "MPL-2.0"
 build = "just check"
-build-expansion = "bash tests/check-proofs.sh && bash tests/check-rejections.sh"
+build-expansion = "bash scripts/check.sh → bash tests/check-proofs.sh && bash tests/check-rejections.sh"
 agda-options = "{-# OPTIONS --safe --without-K #-} ; no postulates; no Agda standard library (only Agda.Builtin.* / Agda.Primitive)"
 agda-version = "2.6.4.3"
 echo-distinction = "Do not collapse Echo C y and E κ A. Echo retains certified residues; epistemic types are standpoint/warrant/access modalities. Their composition is meaningful; they are not the same modality."
 ci = "Proof and security workflows configured; required merge checks are described in docs/ci-safety.adoc"
+secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153/D154). Do not add a Secret API or information-flow implementation here; docs/secret-types.adoc is the boundary/history note. epistemic-types#29 stays closed."
+
+[first-run]
+dev-container = ".devcontainer/ — Debian 13 pinned to the same base image digest as CI, agda-bin=2.6.4.3-1+b2; postCreateCommand runs 'just check'."
+local = "just check → scripts/check.sh: local Agda when present, otherwise 'guix shell -D -f build/guix.scm -- bash scripts/check.sh'."
+ci = ".github/workflows/agda.yml asserts 'Agda version 2.6.4.3' and runs 'bash scripts/check.sh' in the pinned Debian 13 container."
 
 [source]
 root = "src/EpistemicTypes/"
@@ -91,7 +97,7 @@ step-3 = "Read .machine_readable/descriptiles/META.a2ml for architecture and des
 step-4 = "Read .machine_readable/descriptiles/ECOSYSTEM.a2ml for ecosystem position and sibling repos."
 step-5 = "Read .machine_readable/descriptiles/AGENTIC.a2ml, NEUROSYM.a2ml, and PLAYBOOK.a2ml for agent guidance."
 step-6 = "Read README.adoc and explainme.adoc for the human-facing overview."
-step-7 = "Run 'just check' to check every source module and semantic rejection fixture before and after changes."
+step-7 = "Run 'just check' (→ scripts/check.sh: local Agda or the Guix environment, or the dev container) to check every source module and semantic rejection fixture before and after changes."
 
 [policy]
 rules = [
@@ -101,6 +107,7 @@ rules = [
   "Keep a2ml / Nickel / k9 files under .machine_readable/ only.",
   "License and SPDX changes are owner-manual; do not add LICENSE files or SPDX headers.",
   "Maintain owner-authorized proof and security CI; do not bypass failing checks.",
+  "Secret types and information-flow control stay outside this repository (D153/D154, docs/secret-types.adoc); do not duplicate the move of issue #32.",
 ]
 
 [ecosystem]
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index ecbc81b..dd8bddd 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -12,6 +12,26 @@ the changelog records what is actually proved, not what is aspired to.
 
 === https://github.com/hyperpolymath/epistemic-types/compare/v0.1.0...HEAD[Unreleased]
 
+[[changed--2026-10-04]]
+==== Changed — 2026-10-04
+
+* First-run environment. `just check` now calls `scripts/check.sh`, which uses a
+  local Agda when one is on `PATH` and otherwise enters the checked-in Guix
+  environment (`build/guix.scm`). A dev container (`.devcontainer/`) pinned to
+  the same Debian 13 base image digest and the same Agda
+  (`agda-bin=2.6.4.3-1+b2`) as CI runs `just check` after creation, and the core
+  CI job now invokes `scripts/check.sh` after asserting the Agda version, so a
+  green container check and a green CI check are the same gate on the same
+  toolchain. `build/guix.scm` gains `ripgrep` and `findutils` (required by the
+  rejection-manifest check and the recursive module scan); README, the
+  documentation index, `docs/ci-safety.adoc` and the machine-readable state
+  describe the environment.
+* Boundary. Per the owner decision of 2026-10-04, `hyperpolymath/secret-types`
+  is the standalone home for secret types (D153, D154). `docs/secret-types.adoc`
+  is retained as the boundary/history note with the decision recorded and the
+  superseded placement section marked; no `Secret` API or information-flow
+  implementation is added here, and `epistemic-types#29` stays closed.
+
 [[added--2026-09-27]]
 ==== Added — 2026-09-27
 
diff --git a/Justfile b/Justfile
index ac8c924..ceb8e7a 100644
--- a/Justfile
+++ b/Justfile
@@ -1,5 +1,8 @@
-check: check-proofs check-rejections
+# Full proof gate through the first-run entry point: local Agda, else Guix.
+check:
+	bash scripts/check.sh
 
+# Individual gates (also invoked by scripts/check.sh and by CI).
 check-proofs:
 	bash tests/check-proofs.sh
 
diff --git a/README.adoc b/README.adoc
index 8863d67..e44a3c2 100644
--- a/README.adoc
+++ b/README.adoc
@@ -202,9 +202,11 @@ This is a prototype, not a complete epistemic logic. The following are **intenti
   transport that would lift the integer certificate to rational input
 * Cross-iteration reuse of a skip bound, and the row-insertion update that
   maintains the scan invariants (`Applications.RapidNJSkip.WeakeningObligation`)
-* Confidentiality labels, secret types, declassification, and noninterference;
-  see link:docs/secret-types.adoc[the information-flow proposal] for the
-  two-level baseline, non-claims, and repository boundary
+* Confidentiality labels, secret types, declassification, and noninterference —
+  out of scope for this repository. The standalone home is
+  link:https://github.com/hyperpolymath/secret-types[`hyperpolymath/secret-types`]
+  (D153/D154); link:docs/secret-types.adoc[the boundary/history note] records
+  the decision and the pointer. No `Secret` API exists here.
 
 == Build
 
@@ -213,7 +215,22 @@ This is a prototype, not a complete epistemic logic. The following are **intenti
 just check  # positive proofs and expected rejection controls
 ----
 
-Or directly:
+`just check` calls `scripts/check.sh`: it uses a local `agda` when one is on
+`PATH`, and otherwise enters the checked-in Guix environment. The explicit
+forms are:
+
+[source,bash]
+----
+bash scripts/check.sh
+guix shell -D -f build/guix.scm -- bash scripts/check.sh
+----
+
+The repository ships a dev container whose image is pinned to the same Debian 13
+base digest as CI and installs the same Agda (`agda-bin=2.6.4.3-1+b2`); its
+`postCreateCommand` runs `just check`, so a first run either reproduces both
+gates or reports the failing one. See link:.devcontainer/README.adoc[].
+
+To check a single module or the aggregate directly:
 
 [source,bash]
 ----
@@ -226,7 +243,7 @@ agda --no-libraries -i src src/EpistemicTypes/All.agda
 * link:docs/continuity-foundations.adoc[Continuity foundations] — store coherence, retained information, bounds, and next obligations
 * link:docs/proof-transport.adoc[Proof transport] — semantic verification across boundaries
 * link:docs/applications/rapidnj-q-criterion.adoc[Applications: the RapidNJ Q-criterion] — the bound, the skip warrant, the exact-arithmetic obligation
-* link:docs/secret-types.adoc[Secret types] — a proposed two-level information-flow model, its noninterference target, and the repository boundary; no API is implemented
+* link:docs/secret-types.adoc[Secret types — boundary and history] — why the two-level information-flow proposal is not implemented here; the standalone home is `hyperpolymath/secret-types` (D153/D154)
 
 == License
 
diff --git a/build/guix.scm b/build/guix.scm
index bbf41df..ba23992 100644
--- a/build/guix.scm
+++ b/build/guix.scm
@@ -9,14 +9,23 @@
              (gnu packages agda)
              (gnu packages haskell)
              (gnu packages base)
-             (gnu packages bash))
+             (gnu packages bash)
+             (gnu packages rust-apps))
 
+;; Development environment for the proof gates.
+;;
+;; Entry point:  guix shell -D -f build/guix.scm -- bash scripts/check.sh
+;;
+;; `scripts/check.sh` falls back to this environment when no Agda is on PATH.
+;; The Agda in Guix may differ from the version CI pins (2.6.4.3); the script
+;; reports the version it uses. ripgrep and findutils are required by
+;; tests/check-rejections.sh and tests/check-proofs.sh.
 (package
   (name "epistemic-types")
   (version "0.1.0")
   (source #f)
   (build-system gnu-build-system)
-  (inputs (list agda ghc coreutils bash make))
+  (inputs (list agda ghc coreutils findutils ripgrep bash make))
   (synopsis "epistemic-types")
   (description "epistemic-types — part of the hyperpolymath ecosystem.")
   (home-page "https://github.com/hyperpolymath/epistemic-types")
diff --git a/docs/README.adoc b/docs/README.adoc
index 28a88c3..8a21174 100644
--- a/docs/README.adoc
+++ b/docs/README.adoc
@@ -36,10 +36,11 @@ authority.
   public / designated / receipt distinctions.
 
 | `docs/secret-types.adoc`
-| Issue #32's proposed two-level information-flow model: label order, attacker
-  and observation boundary, target noninterference property, distinction from
-  existing interfaces, and an early repository-placement decision. No API or
-  security theorem is implemented.
+| Boundary and history for secret types: the 2026-10-04 owner decision that
+  `hyperpolymath/secret-types` is the standalone home (D153/D154), the retained
+  two-level information-flow proposal (label order, attacker and observation
+  boundary, noninterference target), and the reason no `Secret` API or security
+  theorem exists in this repository.
 |===
 
 == Continuity foundations
diff --git a/docs/ci-safety.adoc b/docs/ci-safety.adoc
index d6e5f2f..897df7d 100644
--- a/docs/ci-safety.adoc
+++ b/docs/ci-safety.adoc
@@ -49,6 +49,13 @@ or physical continuity.
 
 == Reproduce
 
+`just check` runs `scripts/check.sh`, the same entry point the core CI job uses:
+a local Agda when one is on `PATH`, otherwise the checked-in Guix environment
+(`build/guix.scm`). The dev container in `.devcontainer/` pins the same base
+image digest and Agda version as CI and runs `just check` on creation, so a
+green container check and a green CI check are the same gate on the same
+toolchain (see link:../.devcontainer/README.adoc[]).
+
 [source,sh]
 ----
 just check
diff --git a/docs/secret-types.adoc b/docs/secret-types.adoc
index 583017c..01dd2c2 100644
--- a/docs/secret-types.adoc
+++ b/docs/secret-types.adoc
@@ -16,6 +16,41 @@ declassification rule, or noninterference theorem in this repository today.
 
 toc::[]
 
+[[boundary_and_history]]
+== Boundary and history — 2026-10-04
+
+**Owner decision (2026-10-04): `hyperpolymath/secret-types` is the standalone
+home for secret types.** This note is retained in `epistemic-types` as the
+boundary/history record: it explains why this repository does not host a
+`Secret` API or an information-flow implementation, and it points to the
+standalone work. No `Secret` type, IFC calculus, declassification rule, or
+noninterference theorem is added here.
+
+Two rulings govern the standalone specification:
+
+* **D153** — A secret type is a value whose flow is constrained by a
+  confidentiality label with explicit declassification, registered in the
+  type-family map on that boundary.
+* **D154** — Reuse an existing lattice (two-point first, then general), prove
+  noninterference, and allow declassification only at explicit audited points.
+
+The proposal below (two labels `Public ⊑ Secret`, dependency join, low-observer
+attacker, termination-insensitive noninterference target) remains the starting
+point for the standalone specification, read in the light of D154: the two-point
+lattice comes first and generalises only if the typing rules require it, and
+declassification is admitted **only at explicit audited points** with a stated
+authority and policy. The baseline's blanket "no declassification" is the safe
+default for this note, not the final policy for the standalone design.
+
+Status of the related issues:
+
+* `epistemic-types#29` (preservation of the original note) is resolved and
+  stays closed.
+* `epistemic-types#32` ("Specify an in-repository security model for secret
+  types") is obsolete as titled: the work moves to `hyperpolymath/secret-types`
+  (D153/D154). Until that transfer lands, this note and issue #32 remain the
+  record; the replacement issue is the transferred #32 itself, not a duplicate.
+
 == Decision offered for issue #32
 
 Issue #31 landed this research direction here as documentation. Issue #32 asks
@@ -287,6 +322,14 @@ link:https://github.com/hyperpolymath/echo-types/blob/main/docs/adjacency/inform
 
 === Placement decision for the next step
 
+[NOTE]
+.Superseded 2026-10-04
+====
+This section records the 2026-09-27 recommendation ("no new repository yet").
+The owner decided on 2026-10-04 that `hyperpolymath/secret-types` is the
+standalone home; see <<boundary_and_history>> above.
+====
+
 **Do not create a new repository from issue #32 alone, and do not add a
 `Secret` module under `EpistemicTypes`.** Keep this specification here as the
 record of why the question arose. Before writing proof code, make one explicit
diff --git a/scripts/check.sh b/scripts/check.sh
new file mode 100755
index 0000000..a3678e1
--- /dev/null
+++ b/scripts/check.sh
@@ -0,0 +1,43 @@
+#!/usr/bin/env bash
+# First-run proof gate for epistemic-types.
+#
+# Uses a local Agda when one is on PATH; otherwise enters the checked-in Guix
+# environment (build/guix.scm). CI (.github/workflows/agda.yml) runs this same
+# script inside the pinned Debian 13 container, whose agda-bin version is
+# asserted to be 2.6.4.3 before the gates run.
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+
+required_agda=2.6.4.3
+
+run_gates() {
+  bash tests/check-proofs.sh
+  bash tests/check-rejections.sh
+}
+
+# Recursion guard: the Guix environment may resolve a differently named binary;
+# if it still lacks agda we fail rather than looping.
+if [[ "${EPISTEMIC_TYPES_IN_GUIX:-0}" == 1 ]]; then
+  run_gates
+  exit 0
+fi
+
+if command -v agda >/dev/null 2>&1; then
+  version=$(agda --version | sed -n 's/^Agda version //p')
+  printf 'INFO: local Agda %s (CI pins %s)\n' "${version:-unknown}" "$required_agda"
+  run_gates
+elif command -v guix >/dev/null 2>&1; then
+  printf 'INFO: no local agda; entering the checked-in Guix environment (build/guix.scm)\n'
+  export EPISTEMIC_TYPES_IN_GUIX=1
+  exec guix shell -D -f build/guix.scm -- bash scripts/check.sh
+else
+  cat >&2 <<'EOF'
+FAIL: no Agda toolchain found.
+
+Install Agda 2.6.4.3 (the CI-matched version), or run this repository's
+dev container (.devcontainer/), or install Guix and re-run:
+
+    guix shell -D -f build/guix.scm -- bash scripts/check.sh
+EOF
+  exit 1
+fi