diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
new file mode 100644
index 0000000..b6ca674
--- /dev/null
+++ b/.github/CODEOWNERS
@@ -0,0 +1,13 @@
+# Code owners for hyperpolymath/gnpl.
+#
+# NB: an earlier unmerged sweep proposed this file naming @metadatastician, which owns
+# other repositories in the estate but not this one. Ownership here is @hyperpolymath.
+
+* @hyperpolymath
+
+# The proof surface and the FFI boundary carry the load-bearing correctness claims;
+# call them out so changes there are never merged unreviewed.
+/src/GqlDt/       @hyperpolymath
+/src/GQLdt/ABI/   @hyperpolymath
+/bridge/          @hyperpolymath
+/docs/proof-debt.md @hyperpolymath
diff --git a/.github/funding.yml b/.github/funding.yml
new file mode 100644
index 0000000..10176ef
--- /dev/null
+++ b/.github/funding.yml
@@ -0,0 +1,2 @@
+# https://docs.github.com/en/repositories/managing-your-repositorys-custom-fields/displaying-a-sponsor-button-in-your-repository
+github: hyperpolymath
diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md
new file mode 100644
index 0000000..015f1a3
--- /dev/null
+++ b/ARCHITECTURE.md
@@ -0,0 +1,78 @@
+<!--
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
+# Architecture
+
+> An earlier unmerged sweep proposed a generic `ARCHITECTURE.md` describing a
+> `src/ tests/ config/` layout with "modular, maintainable architecture designed for
+> clarity, scalability and long-term sustainability". This repository has none of those
+> directories and that text described nothing. What follows is the actual structure.
+
+## Two layers, one repository
+
+```
+GNPL          narration: "what account does this evidence support?"   <-- design only
+  │  lowers to
+GQLdt         query: "what is in the store?"                          <-- built, tested
+  │  FFI (liblith_bridge.a)
+Form.Bridge   Zig, C ABI                                              <-- built, tested
+  │
+Lithoglyph    Form.Model / Form.Blocks (Forth, append-only journal)   <-- separate repo
+```
+
+This is why a repository named `gnpl` contains sources namespaced `GqlDt`: GQLdt is not
+a leftover, it is GNPL's compilation target. See `README.adoc`, and `docs/THEORY.adoc`
+for why the narration layer is the point.
+
+## Layout
+
+| Path | Language | Role |
+|---|---|---|
+| `src/GqlDt/` | Lean 4 | the query core — types, lexer, parser, IR, pipeline |
+| `src/GqlDt/Types/` | Lean 4 | refinement types: `BoundedNat`, `NonEmptyString`, `Confidence` |
+| `src/GqlDt/Provenance/` | Lean 4 | `ActorId`, `Rationale`, `Tracked` — the warrant substrate |
+| `src/GqlDt/Prompt/` | Lean 4 | PROMPT six-dimension source scoring |
+| `src/GQLdt/ABI/` | Idris2 | ABI definitions + memory-layout proofs |
+| `bridge/` | Zig | FFI implementation; emits `zig-out/lib/liblith_bridge.a` |
+| `test/` | Lean 4 | executable suites, run by `lake test` |
+| `spec/` | Markdown/EBNF | the normative grammar and lexical specification |
+| `docs/` | AsciiDoc/Markdown | design rationale and proof debt |
+
+Per the estate standard, **ABI is Idris2 and FFI is Zig** — no hand-written C.
+`bridge/` is the only Zig tree; two pre-0.15-API skeletons were removed in #7.
+
+## Build order (it matters)
+
+`lakefile.lean` links against `bridge/zig-out/lib/liblith_bridge.a`, so the Zig archive
+must exist *before* the Lean executables link:
+
+```sh
+cd bridge && zig build && zig build test   # produces liblith_bridge.a
+cd ..     && lake build && lake test
+```
+
+Getting this backwards is why the `Containerfile` used to mask both steps with
+`|| echo`, which meant a wholly broken build still produced a "successful" image.
+
+## Verification posture
+
+The claims this repository makes about itself are gated, and the gates are tested:
+
+| Gate | What it establishes |
+|---|---|
+| `lake build` | the Lean core typechecks |
+| `lake test` | 163 executable checks across Lexer / Parser / TypeSafety |
+| `scripts/check-lean-proofs.sh --build-log` | Lean reports no *incomplete* proof (`sorry`) |
+| estate `check-trusted-base.sh` | every `axiom` is enumerated in `docs/proof-debt.md` |
+| `cd bridge && zig build test` | the FFI bridge builds and its unit tests pass |
+
+**A green proof gate means "nothing is admitted mid-proof", not "nothing is assumed".**
+Lean's `sorry` warning does not fire on `axiom`, and 16 axioms remain — five of them in
+*executable* position, so those functions have no implementation at all. Read
+`docs/proof-debt.md` before relying on any verification claim here.
+
+New gates are only accepted once they have been shown to go red on a seeded fault. The
+test driver and the proof gate were both canary-tested this way; the repository has a
+history of gates that could not fail, and the remedy is evidence, not intent.
diff --git a/GOVERNANCE.md b/GOVERNANCE.md
new file mode 100644
index 0000000..17f9cc3
--- /dev/null
+++ b/GOVERNANCE.md
@@ -0,0 +1,62 @@
+<!--
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
+# Governance
+
+`hyperpolymath/gnpl` is maintained by @hyperpolymath (see `MAINTAINERS`). Decisions are
+made by the maintainer; this document records *how* they are made and what a change has to
+clear, so the bar is legible rather than tacit.
+
+## Scope of decisions
+
+| Kind | Who decides | Evidence expected |
+|---|---|---|
+| Bug fix, doc correction, gate repair | maintainer or contributor PR | the gate that now fails, or the measurement |
+| Grammar / lexical behaviour | maintainer, against `spec/GQL-DT-*.md` | the spec clause being conformed to |
+| ABI or FFI surface | maintainer | layout proof in `src/GQLdt/ABI/`, both sides updated together |
+| Adding or discharging an `axiom` | maintainer | `docs/proof-debt.md` updated in the same change |
+| Semantics of PROMPT scoring | maintainer | affects a proof field — see below |
+
+## The rules a change must clear
+
+These are not style preferences; each exists because it was violated and cost something.
+
+1. **No handwaving.** A claim in a README, a manifest or a commit message must be
+   verifiable by running something. "Verified" without a command that verifies it is a
+   defect.
+2. **Gates must be able to fail.** A new or repaired gate is not accepted until it has been
+   shown to go red on a deliberately seeded fault, and green when removed. This repository
+   has shipped a naming gate that compared a string to itself, a `lake test` step that
+   swallowed real failures, test suites whose `main : IO Unit` always exited 0, and a
+   container build that masked both its steps with `|| echo`.
+3. **Specs are normative.** Where `spec/GQL-DT-Lexical.md` and the implementation disagree,
+   the implementation is wrong until the spec is deliberately amended.
+4. **The trusted base is enumerated.** Every `axiom` appears in `docs/proof-debt.md` with
+   `file:line` and a disposition. Nothing may be recorded as "budgeted" without a stated
+   refutation budget — untested assurance is unfalsifiable.
+5. **Foundation before depth.** Work that makes the codebase *verifiable* precedes work
+   that deepens any one strand. The 19 lexer defects found in July 2026 were invisible for
+   as long as they were because nothing could run and fail.
+
+## Cross-cutting changes
+
+Two areas cannot be changed on one side only:
+
+- **The FFI boundary.** `bridge/lith_types.zig` and the Lean types must agree. A change to
+  one without the other silently breaks the proofs that cross it.
+- **PROMPT scoring.** `PromptScores` carries a proof field,
+  `overall_correct : overall.val = (…sum…) / 6`. The averaging rule is welded into the
+  type, so changing it is a proof obligation change on every value, in Lean and in Zig
+  simultaneously — not an edit to one function.
+
+## Estate context
+
+This repository consumes shared workflows from `hyperpolymath/standards`. Faults in those
+are reported upstream rather than patched around locally; where a local shim is
+unavoidable it carries a comment naming the upstream issue.
+
+## Contributing
+
+See `CONTRIBUTING.md`. Code is MPL-2.0, documentation is CC-BY-SA-4.0.
diff --git a/MAINTAINERS b/MAINTAINERS
new file mode 100644
index 0000000..9d97072
--- /dev/null
+++ b/MAINTAINERS
@@ -0,0 +1,23 @@
+# Maintainers — hyperpolymath/gnpl
+
+## Active
+
+| Name                    | GitHub          | Role    |
+|-------------------------|-----------------|---------|
+| Jonathan D.A. Jewell    | @hyperpolymath  | Primary |
+
+## Scope
+
+GNPL (the narration/projection layer) and GQLdt (the query layer it lowers to) live in
+this repository together — see `README.adoc`. The Zig FFI bridge under `bridge/` and the
+Idris2 ABI under `src/GQLdt/ABI/` are maintained here too; the Lithoglyph data store they
+talk to is maintained separately.
+
+## Expectations
+
+- Changes touching `src/GqlDt/`, `src/GQLdt/ABI/` or `bridge/` need review — they carry the
+  correctness claims.
+- `docs/proof-debt.md` must be updated in the same change as any axiom added or discharged.
+  The estate trusted-base policy enforces this in CI.
+- Gates must be able to fail. A new gate is not accepted until it has been shown to go red
+  on a seeded fault.
diff --git a/README.adoc b/README.adoc
index 73cb46e..91765d7 100644
--- a/README.adoc
+++ b/README.adoc
@@ -76,7 +76,8 @@ Lithoglyph-as-a-database is the second. See the design documents below.
   no incomplete proofs — but see the trusted-base caveat below
 | Proof obligations | *16 axioms outstanding* | all stubs, none necessary; enumerated in
   link:docs/proof-debt.md[`docs/proof-debt.md`]
-| Tests | *none* | `lake test` reports `no test driver configured`
+| Tests | *163 checks, green* | `lake test` runs Lexer/Parser/TypeSafety suites. The gate is
+  canary-tested: a seeded false check turns it red
 | Zig FFI bridge (`bridge/`) | *builds* | produces `zig-out/lib/liblith_bridge.a`, the
   artifact `lakefile.lean` links; `zig build test` passes
 | GNPL narration layer | *design* | `docs/THEORY.adoc` + `docs/LITHOGLYPH.adoc`; no code yet
diff --git a/README.md b/README.md
index e106912..98a145f 100644
--- a/README.md
+++ b/README.md
@@ -78,7 +78,10 @@ GQLdt extends [Lithoglyph](https://github.com/hyperpolymath/nextgen-databases/tr
 - 🟡 M6: GQL-DT/GQL Parser (substantially complete - see below)
 
 **M6 Parser Status** (Substantially Complete):
-- ✅ Lexer: Hand-rolled 540-line implementation (80+ keywords, operators, literals, comments)
+- ✅ Lexer: Hand-rolled 540-line implementation (80+ keywords, operators, literals,
+  comments) — verified by 163 executable checks (`lake test`), not asserted. Two-character
+  lookahead was off by one until 2026-07-27, so `<=`/`>=`/`!=`/`<>` never lexed as single
+  tokens, `:` lexed as `::`, and block comments were skipped entirely; fixed and covered.
 - ✅ Parser: Combinator-based parser for INSERT/SELECT/UPDATE/DELETE
 - ✅ Type System: Refinement types, PROMPT scores, provenance tracking
 - ✅ Pipeline: 6-stage compilation (tokenize → parse → type check → IR → validate → serialize)
diff --git a/lakefile.lean b/lakefile.lean
index d0a4d83..bd649dd 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -22,6 +22,13 @@ lean_lib GqlDt where
   srcDir := "src"
   roots := #[`GqlDt]
 
+-- Shared test support (failure counter + exit-code summary).
+-- Declared as a library so the individual test executables can `import TestHarness`;
+-- a bare file under a target's srcDir is not otherwise resolvable as a module.
+lean_lib TestSupport where
+  srcDir := "test"
+  roots := #[`TestHarness]
+
 -- FFI Test executable (requires Zig library to be built first)
 -- Build Zig lib: cd bridge && zig build
 lean_exe ffi_test where
@@ -33,16 +40,62 @@ lean_exe ffi_test where
     "-llith_bridge"
   ]
 
--- Parser test executable
+-- Parser test executable.
+-- The three pure-Lean suites are @[default_target] so a plain `lake build` compiles them.
+-- Without that, `lake build` built only the GqlDt library, the test executables were never
+-- compiled by CI or locally, and two of them silently rotted until they no longer compiled
+-- at all. "Declared but built by nothing" is the failure mode this whole change exists to
+-- close, so the suites must not reintroduce it.
+@[default_target]
 lean_exe parser_test where
   srcDir := "test"
   root := `ParserTest
 
 -- Lexer test executable
+@[default_target]
 lean_exe lexer_test where
   srcDir := "test"
   root := `LexerTest
 
+-- Type-safety test executable.
+-- test/TypeSafetyTests.lean existed but was declared by no target, so it was never
+-- built and never run — it could not even fail to compile.
+@[default_target]
+lean_exe type_safety_test where
+  srcDir := "test"
+  root := `TypeSafetyTests
+
+-- Test driver: `lake test`.
+--
+-- Without this, `lake test` reported "no test driver configured" and exited non-zero,
+-- so CI had to tolerate that failure — which meant CI also tolerated genuine test
+-- failures. The suites below now return a real exit code (see test/TestHarness.lean).
+--
+-- ffi_test is deliberately excluded: it links against bridge/zig-out/lib/liblith_bridge.a,
+-- which requires `cd bridge && zig build` first. It is run separately by the zig-ffi CI
+-- job, where that artifact is guaranteed to exist. Including it here would make `lake test`
+-- fail on a clean checkout for a reason unrelated to Lean.
+@[test_driver]
+script test do
+  let suites := #["lexer_test", "parser_test", "type_safety_test"]
+  let mut failed : Array String := #[]
+  for suite in suites do
+    let bin := System.mkFilePath [".lake", "build", "bin", suite]
+    if !(← System.FilePath.pathExists bin) then
+      IO.eprintln s!"✗ {suite}: binary not found at {bin} — run `lake build` first"
+      failed := failed.push suite
+      continue
+    IO.println s!"\n▶ {suite}"
+    let child ← IO.Process.spawn { cmd := bin.toString }
+    if (← child.wait) != 0 then
+      failed := failed.push suite
+  if failed.isEmpty then
+    IO.println s!"\n✅ all {suites.size} Lean suite(s) passed"
+    return 0
+  else
+    IO.eprintln s!"\n❌ FAILED: {String.intercalate ", " failed.toList}"
+    return 1
+
 -- GQLdt CLI/REPL (with FFI persistence backend)
 lean_exe gqldt where
   srcDir := "src"
diff --git a/src/GqlDt/Lexer.lean b/src/GqlDt/Lexer.lean
index 34b90af..59e8cb2 100644
--- a/src/GqlDt/Lexer.lean
+++ b/src/GqlDt/Lexer.lean
@@ -263,14 +263,14 @@ partial def skipLineComment (s : LexerState) : LexerState :=
   | some _ => skipLineComment s.advance
 
 partial def skipBlockComment (s : LexerState) : LexerState :=
-  match s.curr, s.peek 0 with
+  match s.curr, s.peek 1 with
   | some '*', some '/' => s.advance.advance
   | none, _ => s
   | _, _ => skipBlockComment s.advance
 
 partial def skipWhitespaceAndComments (s : LexerState) : LexerState :=
   let s' := skipWhitespace s
-  match s'.curr, s'.peek 0 with
+  match s'.curr, s'.peek 1 with
   | some '-', some '-' => skipWhitespaceAndComments (skipLineComment (s'.advance.advance))
   | some '/', some '*' => skipWhitespaceAndComments (skipBlockComment (s'.advance.advance))
   | _, _ => s'
@@ -295,7 +295,7 @@ partial def parseString (s : LexerState) (quote : Char) : LexerState × String :
       if c = quote then
         (state.advance, acc)
       else if c = '\\' then
-        match state.peek 0 with
+        match state.peek 1 with
         | some 'n' => loop (state.advance.advance) (acc ++ "\n")
         | some 't' => loop (state.advance.advance) (acc ++ "\t")
         | some 'r' => loop (state.advance.advance) (acc ++ "\r")
@@ -357,21 +357,21 @@ def tokenizeOne (s : LexerState) : Option (Token × LexerState) :=
       else if c = '^' then some ({ type := .opCaret, line := line, column := column, lexeme := "^" }, s'.advance)
       else if c = '=' then some ({ type := .opEq, line := line, column := column, lexeme := "=" }, s'.advance)
       else if c = '<' then
-        match s'.peek 0 with
+        match s'.peek 1 with
         | some '=' => some ({ type := .opLe, line := line, column := column, lexeme := "<=" }, s'.advance.advance)
         | some '>' => some ({ type := .opNeq, line := line, column := column, lexeme := "<>" }, s'.advance.advance)
         | _ => some ({ type := .opLt, line := line, column := column, lexeme := "<" }, s'.advance)
       else if c = '>' then
-        match s'.peek 0 with
+        match s'.peek 1 with
         | some '=' => some ({ type := .opGe, line := line, column := column, lexeme := ">=" }, s'.advance.advance)
         | _ => some ({ type := .opGt, line := line, column := column, lexeme := ">" }, s'.advance)
       else if c = '!' then
-        match s'.peek 0 with
+        match s'.peek 1 with
         | some '=' => some ({ type := .opNeq, line := line, column := column, lexeme := "!=" }, s'.advance.advance)
         | _ => some ({ type := .opNot, line := line, column := column, lexeme := "!" }, s'.advance)
       else if c = '.' then some ({ type := .opDot, line := line, column := column, lexeme := "." }, s'.advance)
       else if c = ':' then
-        match s'.peek 0 with
+        match s'.peek 1 with
         | some ':' => some ({ type := .opDoubleColon, line := line, column := column, lexeme := "::" }, s'.advance.advance)
         | _ => some ({ type := .opColon, line := line, column := column, lexeme := ":" }, s'.advance)
       else if c = '(' then some ({ type := .leftParen, line := line, column := column, lexeme := "(" }, s'.advance)
diff --git a/test/FFITest.lean b/test/FFITest.lean
index db8ddb8..b6df2fc 100644
--- a/test/FFITest.lean
+++ b/test/FFITest.lean
@@ -11,6 +11,7 @@
 -- 3. Run: .lake/build/bin/ffi_test
 
 import GqlDt.FFI.Bridge
+import TestHarness
 import GqlDt.Types.BoundedNat
 import GqlDt.Prompt.PromptScores
 
@@ -118,7 +119,7 @@ def testIntegration : IO Unit := do
   IO.println "✓ Integration tests passed"
 
 /-- Main test runner -/
-def main : IO Unit := do
+def main : IO UInt32 := do
   IO.println "═══════════════════════════════════════════════"
   IO.println "  GqlDt FFI Integration Tests"
   IO.println "═══════════════════════════════════════════════"
@@ -137,5 +138,6 @@ def main : IO Unit := do
   IO.println ""
 
   IO.println "═══════════════════════════════════════════════"
-  IO.println "  All tests passed!"
+  IO.println "  FFI tests completed"
   IO.println "═══════════════════════════════════════════════"
+  GnplTest.summarise "FFI"
diff --git a/test/LexerTest.lean b/test/LexerTest.lean
index 580d4dd..041a38c 100644
--- a/test/LexerTest.lean
+++ b/test/LexerTest.lean
@@ -10,6 +10,7 @@
 -- Run with: lake build lexer_test && lake env lean --run test/LexerTest.lean
 
 import GqlDt.Lexer
+import TestHarness
 
 open GqlDt.Lexer
 
@@ -17,12 +18,15 @@ open GqlDt.Lexer
 -- Test Helpers
 -- ============================================================================
 
-/-- Count of test failures, tracked via IO.Ref -/
-def runTest (name : String) (passed : Bool) : IO Unit := do
-  if passed then
-    IO.println s!"  PASS: {name}"
-  else
-    IO.eprintln s!"  FAIL: {name}"
+/--
+Run one named check, recording the outcome in the shared failure counter.
+
+Previously this printed `FAIL` and returned `Unit`, so a failing check left no trace the
+process could act on — despite the doc comment claiming a counter. It now delegates to
+`GnplTest.check`, and `main` turns the tally into an exit code.
+-/
+def runTest (name : String) (passed : Bool) : IO Unit :=
+  GnplTest.check name passed
 
 /-- Extract token types from a tokenization result, excluding EOF -/
 def tokenTypes (result : Except String (List Token)) : List TokenType :=
@@ -259,19 +263,19 @@ def testStringLiterals : IO Unit := do
   -- Escape sequences
   runTest "'line\\nbreak'" (
     match firstType "'line\\nbreak'" with
-    | some (.litString s) => s.containsSubstr "\n"
+    | some (.litString s) => s.contains '\n'
     | _ => false
   )
 
   runTest "'tab\\there'" (
     match firstType "'tab\\there'" with
-    | some (.litString s) => s.containsSubstr "\t"
+    | some (.litString s) => s.contains '\t'
     | _ => false
   )
 
   runTest "'escaped\\\\backslash'" (
     match firstType "'escaped\\\\backslash'" with
-    | some (.litString s) => s.containsSubstr "\\"
+    | some (.litString s) => s.contains '\\'
     | _ => false
   )
 
@@ -312,8 +316,15 @@ def testIdentifiers : IO Unit := do
   )
 
   -- Qualified identifier via double colon
-  runTest "schema::table tokenizes" (
-    expectTypes "schema::table" [.identifier "schema", .opDoubleColon, .identifier "table"]
+  -- NB: the operand must not be a reserved word. `schema::table` does NOT produce three
+  -- identifiers, because SQL keywords are case-insensitive and `table` therefore lexes as
+  -- `.kwTable` — as this same suite asserts under "SQL Keywords". That is correct
+  -- behaviour, so the qualified-identifier case is tested with a non-reserved name.
+  runTest "schema::customers tokenizes" (
+    expectTypes "schema::customers" [.identifier "schema", .opDoubleColon, .identifier "customers"]
+  )
+  runTest "schema::table — `table` stays a keyword" (
+    expectTypes "schema::table" [.identifier "schema", .opDoubleColon, .kwTable]
   )
 
 -- ============================================================================
@@ -586,7 +597,7 @@ def testEdgeCases : IO Unit := do
 -- Main Test Runner
 -- ============================================================================
 
-def main : IO Unit := do
+def main : IO UInt32 := do
   IO.println "==============================================="
   IO.println "  GQL-DT Lexer Unit Tests"
   IO.println "==============================================="
@@ -611,3 +622,4 @@ def main : IO Unit := do
   IO.println "==============================================="
   IO.println "  Lexer tests completed"
   IO.println "==============================================="
+  GnplTest.summarise "Lexer"
diff --git a/test/ParserTest.lean b/test/ParserTest.lean
index 5465595..dc74b0c 100644
--- a/test/ParserTest.lean
+++ b/test/ParserTest.lean
@@ -6,6 +6,7 @@
 -- Run with: lake build && lean --run test/ParserTest.lean
 
 import GqlDt.Query
+import TestHarness
 
 open GqlDt.Query
 open GqlDt.Query.Parser
@@ -17,7 +18,7 @@ def testSelectAll : IO Unit := do
   | .ok q =>
     IO.println s!"  ✓ Parsed: table = {q.from.name}, projection = all"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test SELECT with columns -/
 def testSelectColumns : IO Unit := do
@@ -31,7 +32,7 @@ def testSelectColumns : IO Unit := do
     | _ =>
       IO.println "    (unexpected projection type)"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test SELECT with WHERE clause -/
 def testSelectWhere : IO Unit := do
@@ -45,7 +46,7 @@ def testSelectWhere : IO Unit := do
     | none =>
       IO.println "    where = none"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test INSERT statement -/
 def testInsert : IO Unit := do
@@ -57,9 +58,9 @@ def testInsert : IO Unit := do
       IO.println s!"  ✓ Parsed INSERT: table = {i.table.name}"
       IO.println s!"    values count = {i.values.length}"
     | _ =>
-      IO.println "  ✗ Got wrong statement type"
+      GnplTest.fail "✗ Got wrong statement type"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test INSERT with provenance -/
 def testInsertProvenance : IO Unit := do
@@ -73,9 +74,9 @@ def testInsertProvenance : IO Unit := do
       IO.println s!"    actor = {repr i.actor}"
       IO.println s!"    rationale = {repr i.rationale}"
     | _ =>
-      IO.println "  ✗ Got wrong statement type"
+      GnplTest.fail "✗ Got wrong statement type"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test UPDATE statement -/
 def testUpdate : IO Unit := do
@@ -88,9 +89,9 @@ def testUpdate : IO Unit := do
       IO.println s!"    set count = {u.set.length}"
       IO.println s!"    has where = {u.whereClause.isSome}"
     | _ =>
-      IO.println "  ✗ Got wrong statement type"
+      GnplTest.fail "✗ Got wrong statement type"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test DELETE statement -/
 def testDelete : IO Unit := do
@@ -102,9 +103,9 @@ def testDelete : IO Unit := do
       IO.println s!"  ✓ Parsed DELETE: table = {d.table.name}"
       IO.println s!"    has where = {d.whereClause.isSome}"
     | _ =>
-      IO.println "  ✗ Got wrong statement type"
+      GnplTest.fail "✗ Got wrong statement type"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test expression parsing -/
 def testExpressions : IO Unit := do
@@ -113,31 +114,31 @@ def testExpressions : IO Unit := do
   -- Simple comparison
   match parseExpr "x = 1" with
   | .ok _ => IO.println "  ✓ x = 1"
-  | .error e => IO.println s!"  ✗ x = 1: {e}"
+  | .error e => GnplTest.fail s!"✗ x = 1: {e}"
 
   -- String comparison
   match parseExpr "name = \"Alice\"" with
   | .ok _ => IO.println "  ✓ name = \"Alice\""
-  | .error e => IO.println s!"  ✗ name = \"Alice\": {e}"
+  | .error e => GnplTest.fail s!"✗ name = \"Alice\": {e}"
 
   -- AND expression
   match parseExpr "a = 1 AND b = 2" with
   | .ok _ => IO.println "  ✓ a = 1 AND b = 2"
-  | .error e => IO.println s!"  ✗ a = 1 AND b = 2: {e}"
+  | .error e => GnplTest.fail s!"✗ a = 1 AND b = 2: {e}"
 
   -- OR expression
   match parseExpr "a = 1 OR b = 2" with
   | .ok _ => IO.println "  ✓ a = 1 OR b = 2"
-  | .error e => IO.println s!"  ✗ a = 1 OR b = 2: {e}"
+  | .error e => GnplTest.fail s!"✗ a = 1 OR b = 2: {e}"
 
   -- Comparison operators
   match parseExpr "x > 10" with
   | .ok _ => IO.println "  ✓ x > 10"
-  | .error e => IO.println s!"  ✗ x > 10: {e}"
+  | .error e => GnplTest.fail s!"✗ x > 10: {e}"
 
   match parseExpr "x <= 100" with
   | .ok _ => IO.println "  ✓ x <= 100"
-  | .error e => IO.println s!"  ✗ x <= 100: {e}"
+  | .error e => GnplTest.fail s!"✗ x <= 100: {e}"
 
 /-- Test SELECT with ORDER BY and LIMIT -/
 def testSelectAdvanced : IO Unit := do
@@ -148,10 +149,10 @@ def testSelectAdvanced : IO Unit := do
     IO.println s!"    orderBy count = {q.orderBy.length}"
     IO.println s!"    limit = {repr q.limit}"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Main test runner -/
-def main : IO Unit := do
+def main : IO UInt32 := do
   IO.println "═══════════════════════════════════════════════"
   IO.println "  GQL Parser Tests"
   IO.println "═══════════════════════════════════════════════"
@@ -187,3 +188,4 @@ def main : IO Unit := do
   IO.println "═══════════════════════════════════════════════"
   IO.println "  Parser tests completed"
   IO.println "═══════════════════════════════════════════════"
+  GnplTest.summarise "Parser"
diff --git a/test/TestHarness.lean b/test/TestHarness.lean
new file mode 100644
index 0000000..bc79514
--- /dev/null
+++ b/test/TestHarness.lean
@@ -0,0 +1,53 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+--
+-- TestHarness.lean — shared failure accounting for the GQLdt test suites.
+--
+-- Why this exists: every suite in test/ previously printed "FAIL"/"✗" to stdout and
+-- then carried on to print "All tests passed!" unconditionally, with `main : IO Unit`
+-- so the process always exited 0. A failing test was therefore invisible to `lake test`,
+-- to CI, and to a human skim-reading the tail of the log.
+--
+-- LexerTest even documented a failure counter — "Count of test failures, tracked via
+-- IO.Ref" — that was never implemented.
+--
+-- This module supplies the counter that comment promised, and `summarise` turns it into
+-- a process exit code. A suite is only honest if a failing check can turn it red.
+
+namespace GnplTest
+
+/-- Number of failed checks recorded so far, across every suite in this process. -/
+initialize failureCount : IO.Ref Nat ← IO.mkRef 0
+
+/-- Record a passing check. -/
+def pass (name : String) : IO Unit :=
+  IO.println s!"  PASS: {name}"
+
+/-- Record a failing check. Increments the counter that `summarise` reads. -/
+def fail (name : String) (detail : String := "") : IO Unit := do
+  failureCount.modify (· + 1)
+  if detail.isEmpty then
+    IO.eprintln s!"  FAIL: {name}"
+  else
+    IO.eprintln s!"  FAIL: {name} — {detail}"
+
+/-- Assert a boolean condition, recording the outcome either way. -/
+def check (name : String) (passed : Bool) : IO Unit :=
+  if passed then pass name else fail name
+
+/--
+Print the suite verdict and yield the process exit code: `0` iff nothing failed.
+
+Use as the last line of `main`, whose type must be `IO UInt32` for the code to reach
+the operating system.
+-/
+def summarise (suite : String) : IO UInt32 := do
+  let n ← failureCount.get
+  if n == 0 then
+    IO.println s!"✅ {suite}: all checks passed"
+    return 0
+  else
+    IO.eprintln s!"❌ {suite}: {n} check(s) FAILED"
+    return 1
+
+end GnplTest
diff --git a/test/TypeSafetyTests.lean b/test/TypeSafetyTests.lean
index 055e5ff..165c5d9 100644
--- a/test/TypeSafetyTests.lean
+++ b/test/TypeSafetyTests.lean
@@ -5,6 +5,7 @@
 -- Demonstrate type safety enforcement at compile time
 
 import GqlDt.TypeSafe
+import TestHarness
 import GqlDt.TypeChecker
 import GqlDt.Types.BoundedNat
 import GqlDt.Types.NonEmptyString
@@ -12,19 +13,28 @@ import GqlDt.Prompt
 
 namespace GqlDt.Tests.TypeSafety
 
-open TypeSafe TypeChecker AST Types
+-- `Prompt` and `Provenance` are needed for PromptScores.create and Rationale respectively.
+-- Their absence is why this file stopped compiling: it was declared by no Lake target, so
+-- nothing ever built it and the rot went unnoticed.
+open TypeSafe TypeChecker AST Types Prompt Provenance
 
 -- Test 1: Valid insertion compiles
 def test_valid_insert : InsertStmt evidenceSchema :=
   let title := NonEmptyString.mk "Test Evidence" (by decide)
+  -- `min`/`max` are structure *parameters* of BoundedNat, not fields — the old
+  -- `BoundedNat.mk 0 100 100 …` passed them as data, which is why this stopped
+  -- elaborating. The anonymous constructor lets the expected type (PromptDimension,
+  -- i.e. BoundedNat 0 100) supply them, leaving val + the two bound proofs.
   let scores := PromptScores.create
-    (BoundedNat.mk 0 100 100 (by omega) (by omega))
-    (BoundedNat.mk 0 100 100 (by omega) (by omega))
-    (BoundedNat.mk 0 100 95 (by omega) (by omega))
-    (BoundedNat.mk 0 100 95 (by omega) (by omega))
-    (BoundedNat.mk 0 100 100 (by omega) (by omega))
-    (BoundedNat.mk 0 100 95 (by omega) (by omega))
-  let rationale := NonEmptyString.mk "Test rationale" (by decide)
+    ⟨100, by omega, by omega⟩
+    ⟨100, by omega, by omega⟩
+    ⟨95,  by omega, by omega⟩
+    ⟨95,  by omega, by omega⟩
+    ⟨100, by omega, by omega⟩
+    ⟨95,  by omega, by omega⟩
+  -- insertEvidence takes a Provenance.Rationale, not a bare NonEmptyString — the whole
+  -- point of the type is that a rationale cannot be confused with any other string.
+  let rationale := Rationale.fromString "Test rationale"
 
   insertEvidence title scores rationale
 
@@ -130,7 +140,7 @@ theorem typeSafeQueriesPreserveInvariants {schema : Schema} (stmt : InsertStmt s
   exact valueInvariant_holds (stmt.values.get i)
 
 -- Run all tests
-def main : IO Unit := do
+def main : IO UInt32 := do
   IO.println "=== GQLdt Type Safety Tests ==="
   IO.println ""
 
@@ -151,6 +161,11 @@ def main : IO Unit := do
   test_execution_safety
   IO.println ""
 
-  IO.println "=== All tests passed! ==="
+  IO.println "=== Type-safety tests completed ==="
+  GnplTest.summarise "TypeSafety"
 
 end GqlDt.Tests.TypeSafety
+
+/-- Top-level entry point. The suite's `main` lives inside `GqlDt.Tests.TypeSafety`, so
+    without this alias the linker finds no `main` symbol and the executable fails to link. -/
+def main : IO UInt32 := GqlDt.Tests.TypeSafety.main