@@ -0,0 +1,34 @@
+# SPDX-License-Identifier: MPL-2.0
+# Proof Gate — type-checks the Idris 2 ABI proof modules on every push
+# and PR. Pattern imported from kategoria.
+#
+# Until 2026-07-21 these modules had NEVER been run through idris2:
+# 5 of 6 failed --check (and one carried a silent hole). The gate
+# hard-fails when the prover is missing (scripts/check-idris2-proofs.sh
+# refuses to skip) and rejects postulate/believe_me/%hint/holes in the
+# pass-required set. Layout.idr is quarantined — see PROOF-STATUS.adoc.
+#
+# Verified locally under Idris 2 0.7.0 (system) and 0.8.0 (nixpkgs):
+# 5/5 required modules PASS.
+name: Proof Gate
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  idris2-proofs:
+    name: idris2 --check (ABI proof modules)
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - uses: cachix/install-nix-action@a49548c11d9846ad46ecc0115273879b045f001c # v31.10.7
+
+      - name: Run proof gate
+        run: nix shell nixpkgs#idris2 -c ./scripts/check-idris2-proofs.sh
@@ -6,7 +6,7 @@
 [metadata]
 project = "typell"
 version = "0.1.0-alpha"
-last-updated = "2026-03-14"
+last-updated = "2026-07-27"
 status = "active"
 
 [project-context]
@@ -23,13 +23,24 @@ maturity = "early-alpha"
 crates = 14
 kernel-modules = 11
 bridge-crates = 13
-total-tests = 221
-kernel-tests = 87
+total-tests = 447   # 422 workspace + 25 kategoria conformance (2026-07-27, cargo test --workspace)
+kernel-tests = 225
 bridge-tests = 134
-idris2-abi-files = 3
+idris2-abi-files = 6
 zig-ffi-files = 1
 languages = ["Rust", "Idris2", "Zig"]
 
+[verification]
+# Enforced by scripts/check-idris2-proofs.sh (Proof Gate workflow) —
+# hard-fails when idris2 is absent; rejects postulate/believe_me/%hint/holes.
+# History: before 2026-07-21 the ABI proof modules had NEVER been checked
+# (5/6 failed; one silent hole). See PROOF-STATUS.adoc.
+idris2-proof-modules-passing = 5
+idris2-proof-modules-quarantined = ["Layout.idr"]
+provers-verified = ["Idris 2 0.7.0", "Idris 2 0.8.0 (nixpkgs)"]
+kategoria-conformance = "crates/typell-core/tests/kategoria_conformance.rs: 25 pass, 3 honest-ignore (type classes, GADTs, cubical absent)"
+last-verified = "2026-07-27"
+
 [kernel-modules]
 modules = [
   { name = "types.rs", lines = 920, purpose = "Unified type representation (HM + dependent + linear + effects + sessions + dimensional + refinement)" },
 
@@ -263,14 +263,7 @@ init:
 
 # Build the project (debug mode)
 build *args:
-    @echo "Building typell (debug)..."
-    # TODO: Replace with your build command
-    # Examples:
-    #   cargo build {{args}}                    # Rust
-    #   mix compile {{args}}                    # Elixir
-    #   zig build {{args}}                      # Zig
-    #   deno task build {{args}}                # Deno/ReScript
-    @echo "Build complete"
+    cargo build --workspace --locked {{args}}
 
 # Build in release mode with optimizations
 build-release *args:
@@ -305,16 +298,16 @@ clean-all: clean
 # TEST & QUALITY
 # ═══════════════════════════════════════════════════════════════════════════════
 
-# Run all tests
-test *args:
-    @echo "Running tests..."
-    # TODO: Replace with your test command
-    # Examples:
-    #   cargo test {{args}}
-    #   mix test {{args}}
-    #   zig build test {{args}}
-    #   deno test {{args}}
-    @echo "Tests passed!"
+# Run all tests: the Rust workspace (incl. the kategoria conformance
+# suite) and the Idris 2 ABI proof gate.
+test *args: proof-check
+    cargo test --workspace --locked {{args}}
+
+# Type-check the Idris 2 ABI proof modules (5 required + Layout
+# quarantined). Hard-fails when idris2 is absent — a gate that skips is
+# not a gate. See PROOF-STATUS.adoc.
+proof-check:
+    ./scripts/check-idris2-proofs.sh
 
 # Run tests with verbose output
 test-verbose:
 
@@ -0,0 +1,88 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= Proof Status — typell Idris 2 ABI modules
+:toc:
+
+*Measured 2026-07-27 under Idris 2 0.7.0 (system) and 0.8.0 (nixpkgs).
+Format and discipline imported from kategoria's PROOF-STATUS.adoc: this
+file records what `idris2 --check` actually says, not what comments
+claim.*
+
+== Verified modules (5 / 5 required PASS)
+
+[cols="2,1,4",options="header"]
+|===
+| Module (src/abi/) | Status | What it proves
+
+| Soundness.idr | PASS
+| Progress + preservation + type safety for the STLC core modelling
+  check.rs/infer.rs/unify.rs. Renaming and PARALLEL-substitution lemmas
+  fully proven — no holes.
+
+| InferenceSoundness.idr | PASS
+| Occurs-check/substitution lemmas, unifier soundness statements,
+  substitution idempotence for the inference model of unify.rs.
+
+| LevelMonotonicity.idr | PASS
+| The safety-level hierarchy (initial set L1–L10) is monotone:
+  `featNMono`/`featureMonotonicity` — higher levels' feature sets
+  subsume lower levels' — now proven for ALL level pairs.
+
+| Types.idr | PASS
+| ABI type definitions; decidable equality for Result; So-guarded
+  non-null handles; computable C-type sizes over a closed universe with
+  definitional layout lemmas.
+
+| Foreign.idr | PASS
+| FFI surface declarations matching ffi/zig.
+|===
+
+Gate: `just proof-check` → `scripts/check-idris2-proofs.sh` (also run in
+CI by `.github/workflows/proof-gate.yml`). The gate HARD-FAILS when
+idris2 is absent and rejects `postulate` / `believe_me` / `assert_total`
+/ `%hint` / holes (`?name`) outside comments in the required modules.
+
+== Quarantined (1)
+
+`Layout.idr` — RSR-template scaffolding, excluded from the pass-required
+set and reported by the gate on every run. Why: three named holes
+(`?fieldsAlignedProof`, `?exampleFieldsAligned`, `?offsetInBoundsProof`),
+a divisibility "proof" attempted via `Refl` on abstract arithmetic
+(unprovable as stated), `verifyAllPlatforms` returning `Right ()` while
+checking nothing, and `Nat` subtraction/`Divides` machinery that does not
+compile. No module imports it. Disposition (owner): rewrite honestly
+against real mod/div lemmas, or delete.
+
+== History — read this before trusting old claims
+
+Until 2026-07-21 these modules had NEVER been run through idris2:
+
+- 5 of 6 failed `--check` outright. `Soundness.idr` referenced `Step`
+  before its definition, returned erased implicits relevantly in its
+  canonical-forms lemmas, hid two NAMED HOLES in the substitution lemma
+  behind a comment insisting they were "not believe_me or postulate" —
+  and its `subst` function was semantically WRONG under binders
+  (substituted the lambda's own bound variable; the de Bruijn bug is why
+  the original proof could not be completed). `LevelMonotonicity.idr`
+  had a `Fin 11`-vs-`Fin 10` off-by-one in the `SafeUp` constructor of
+  the monotonicity model itself, a circular (uninhabitable) `SafeL1`
+  base case, and stdlib lemma names that no longer exist.
+- The one thing `--check` DID accept silently was a hole:
+  `?featureMonoGeneral` — the central feature-subsumption theorem was
+  only proven for L1. Holes pass `idris2 --check`; that is exactly why
+  the gate scans for them.
+- `applySubst` in InferenceSoundness.idr recursed through the
+  substitution's range and was non-terminating on cyclic substitutions;
+  it is now single-pass, modelling idempotent (MGU-form) substitutions,
+  with the invariant documented.
+
+== Reproduce
+
+[source,sh]
+----
+just proof-check
+# or directly:
+./scripts/check-idris2-proofs.sh
+# or with the same prover CI uses:
+nix shell nixpkgs#idris2 -c ./scripts/check-idris2-proofs.sh
+----
@@ -6,7 +6,7 @@
 
 == Overview
 
-TypeLL is the unified type system verification kernel for the hyperpolymath ecosystem. It is to PanLL what LLVM is to Clang: the formal verification substrate that multiple language frontends compile _types_ into. TypeLL is an *open-ended progressive* type safety framework: it works through increasingly strong type properties with no fixed upper bound. New levels are added as the theory demands. The initial progression (L1-L10) is defined below and used by VCL-total, 007, Kategoria, PanLL, and the nextgen-languages suite; this is a starting point, not a ceiling.
+TypeLL is the unified type system verification kernel for the hyperpolymath ecosystem. It is to PanLL what LLVM is to Clang: the formal verification substrate that multiple language frontends compile _types_ into. TypeLL is an *open-ended progressive* type safety framework: it works through increasingly strong type properties with no fixed upper bound. New levels are added as the theory demands. The initial progression (L1-L10) is defined below and used by VCL-total, 007, PanLL, and the nextgen-languages suite; this is a starting point, not a ceiling. (Correction 2026-07-27: Kategoria does NOT use this progression — its L1-L10 are language-FEATURE levels, a different hierarchy that happens to share the numbering. The mapping between the two is enablement, not identity: see docs/KATEGORIA-BRIDGE.adoc.)
 
 == Current State (2026-03-29)
 
@@ -115,7 +115,11 @@ new levels are added as the type theory demands.  L1-L10 is a starting point, no
 * **007** — Agent meta-language type system (tropical types, Five Facets);
   Isabelle foundation complete in `tropical-resource-typing` (2026-04-11):
   star equation, Floyd-Warshall, least prefixpoint, CNO — all proved, zero sorry.
-* **Kategoria** — Category theory verification; Route alpha achieved L9 (session types via Brady indexed monad);
+* **Kategoria** — The Type Safety Challenge (its OWN feature-level L1-L10
+  hierarchy; route α has 9/10 verified in Idris 2, L10 cubical documented
+  as its wall). Bridged 2026-07-21: kategoria's levels run here as
+  `crates/typell-core/tests/kategoria_conformance.rs` and its proof
+  discipline became this repo's Proof Gate — see docs/KATEGORIA-BRIDGE.adoc;
   `research/tropical/` research prototype added referencing `tropical-resource-typing` proofs.
 * **PanLL** — Cross-panel type intelligence (TypeLLService + TypeLLEngine in src/core/)
 * **typed-wasm** — TypeLL progressive type safety applied to WASM memory (current application: L1-L10), multi-module convergence infrastructure for AffineScript + Ephapax