diff --git a/docs/zig-ffi-verification.adoc b/docs/zig-ffi-verification.adoc
new file mode 100644
index 00000000..9e7e5363
--- /dev/null
+++ b/docs/zig-ffi-verification.adoc
@@ -0,0 +1,327 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= Zig FFI Formal Verification
+:toc:
+:toclevels: 3
+:sectnums:
+
+== Overview
+
+This document describes the formal verification approach for the BoJ Server Zig FFI
+layer.  No standard Zig verifier exists; instead the methodology exploits Zig's
+`comptime` evaluation as a sound proof mechanism: any `comptime {}` block that reaches
+`@compileError` is a *compile-time theorem* — the binary cannot be built unless the
+theorem holds.
+
+=== Trust Chain
+
+----
+Idris2 proofs (src/abi/)
+  │  [ASSUMED] cross-language ABI contract (unverifiable by either tool)
+  ▼
+abi_axioms.zig  — compile-time theorems about every ABI constant
+  │  [CROSS] comptime cross-module assertions in abi_verify.zig
+  ▼
+abi_verify.zig  — live Zig enum/constant values match the axioms
+  │  [RUNTIME] exhaustive boundary tests at every C-ABI entry point
+  ▼
+catalogue.zig, safety.zig, cartridge_shim.zig  — the live FFI layer
+----
+
+=== Evidence Taxonomy
+
+Every claim in this verification is tagged with one of four evidence levels:
+
+[cols="1,4",options="header"]
+|===
+| Tag | Meaning
+
+| [STATIC]
+| `comptime` assertion in the *same* file.  A compiling binary cannot violate it.
+
+| [CROSS]
+| `comptime` assertion in `abi_verify.zig` that imports a live module and
+  compares its value against the axiom.  Fires at compile time of the test binary;
+  a build failure here means the live module and the axiom have diverged.
+
+| [RUNTIME]
+| Exhaustive boundary test exercised at run time.  Proves the C-ABI function
+  *behaves* as specified, not just that types align.
+
+| [ASSUMED]
+| Cross-language invariant that neither Zig nor Idris2 can prove in isolation
+  (e.g., layout agreement between the C header and both implementations).
+  Documented as an axiom; any violation would be discovered by runtime tests or
+  by a mismatch caught in CI.
+|===
+
+== Instruments
+
+=== `ffi/zig/src/abi_axioms.zig`
+
+A *standalone* file with no imports.  Every ABI-relevant numeric constant is
+declared here as an untyped `comptime_int`, enabling universal coercion across
+types without casting.  Each section follows its constant declarations with one
+or more `comptime {}` blocks that call `@compileError` on any violation.
+
+This file is the *single source of truth* for all ABI numeric values visible to
+the Zig layer.
+
+==== Sections
+
+[cols="1,3",options="header"]
+|===
+| Section | Contents
+
+| §1  Invocation ABI
+| `RC_*` return codes (ADR-0006): `RC_SUCCESS=0`, `RC_UNKNOWN_TOOL=-1`, ...,
+  `RC_AUTH_DENIED=-6`.  Theorems ax.1.1–ax.1.4: success is zero, all errors are
+  strictly negative, the range is dense in `[-6,-1]`, and `RC_CODE_COUNT` is
+  consistent.
+
+| §2  Catalogue ABI
+| Status codes, protocol range, domain range, tier values, capacity limits,
+  buffer bounds, and catalogue return codes.  Critical theorem ax.2.2:
+  `MOUNT_GATE_STATUS == STATUS_READY`, i.e., only `STATUS_READY` cartridges
+  may be mounted.  Theorem ax.2.7: `CAT_OK == RC_SUCCESS` (both are 0).
+
+| §3  Loader ABI
+| `HASH_LEN=32`, `HASH_HEX_LEN=64` (SHA-256 hex digest), path limits, and
+  loader return codes.  Critical theorem ax.3.2: `LOADER_MATCH=1 ≠ CAT_OK=0`
+  — the loader's "match" result must *not* be conflated with "success" in
+  catalogue conventions.
+
+| §4  Safety ABI
+| `SAFETY_SAFE=1`, rejection codes `[-8,-1]`, buffer size limits.
+  Theorem ax.4.6: `SAFETY_SAFE=1 ≠ RC_SUCCESS=0` — a "safe" result must not
+  be conflated with "success" in the invocation convention.
+|===
+
+==== Running
+
+----
+zig build abi-axioms
+----
+
+A successful build proves every `comptime` theorem in the file holds.  There are
+no runtime tests in this step; it is purely a compile-time proof.
+
+=== `ffi/zig/src/abi_verify.zig`
+
+Cross-checks the *live* Zig modules against the axioms, then exercises every
+C-ABI entry point exhaustively at the boundaries declared in `abi_axioms.zig`.
+
+==== Section A — Comptime Cross-Module Proofs [CROSS]
+
+Each sub-section imports a live module and checks that its enum integer values
+equal the corresponding axiom constants via `@compileError`:
+
+[cols="1,4",options="header"]
+|===
+| Sub-section | Live module | Claims verified
+
+| A.1 | `catalogue` | `CartridgeStatus` enum: `.development=0`, `.ready=1`,
+  `.deprecated=2`, `.faulty=3` match `STATUS_*` axioms.
+
+| A.2 | `catalogue` | `ProtocolType` enum: MCP=1 through REST=9 match `PROTO_*`
+  axioms.  Count theorem: exactly 9 protocols.
+
+| A.3 | `catalogue` | `CapabilityDomain` enum: spot-checks on CLOUD=1, FLEET=12,
+  NESY=13.
+
+| A.4 | `catalogue` | `MenuTier` enum: TERANGA=0, SHIELD=1, AYO=2 match
+  `TIER_*` axioms.
+
+| A.5 | `cartridge_shim` | `RC_*` constants in the shim match §1 axioms.
+
+| A.6 | _(gap)_ | `loader.zig` cannot be imported as a named module because it
+  uses `@import("catalogue.zig")` (relative path), which conflicts with the named
+  `catalogue` module in a shared compilation.  `HASH_LEN` / `HASH_HEX_LEN`
+  coverage is instead provided by §D axiom-level tests.  *Fix:* update
+  `loader.zig` to `const catalogue = @import("catalogue");` (named module import).
+
+| A.7 | `safety` | `SafetyError` enum: `shell_injection=-1`, `json_unsafe=-8`
+  match `SAFETY_*` axioms.
+|===
+
+==== Section B — Catalogue Boundary Tests [RUNTIME]
+
+Exhaustive black-box tests via `catalogue`'s `pub export fn` symbols:
+
+[cols="1,3",options="header"]
+|===
+| Test | What it proves
+
+| B.1 | `boj_catalogue_init()` returns `CAT_OK=0`; state is clean.
+
+| B.2 | `boj_catalogue_deinit()` is idempotent.
+
+| B.3 | Registering exactly `MAX_CARTRIDGES=128` entries succeeds; the 129th
+  returns `CAT_ERR=-1`.
+
+| B.4 | `boj_catalogue_mount()` succeeds only for `STATUS_READY` cartridges;
+  returns `-1` for development/deprecated/faulty.  Directly exercises the
+  mount-gate invariant (ax.2.2).
+
+| B.5/B.6 | Name boundary: 64-byte name accepted; 65-byte name rejected.
+
+| B.7/B.8 | Version boundary: 16-byte version accepted; 17-byte version rejected.
+
+| B.9–B.11 | Mount/unmount/is-mounted return conventions.
+
+| B.12 | `MAX_ORDER_SIZE=16` slot boundary.
+
+| B.13/B.14 | Backend string boundary: 32 bytes accepted; 33 bytes rejected.
+
+| B.15 | `boj_catalogue_version()` returns a non-null, non-empty string.
+|===
+
+==== Section C — Invocation ABI Tests [RUNTIME]
+
+Tests via `cartridge_shim`'s public Zig functions:
+
+* `RC_SUCCESS=0` on successful invocation.
+* `RC_UNKNOWN_TOOL=-1` for an unknown tool name.
+* `RC_BAD_ARGS=-2` for a malformed argument buffer.
+* `RC_BUFFER_TOO_SMALL=-3` when the output buffer is undersized.
+* `RC_RUNTIME_ERROR=-4`, `RC_PANIC=-5`, `RC_AUTH_DENIED=-6`.
+* Two-phase call pattern (C.8): probe with zero-length buffer to discover
+  required size, then allocate and call with the real buffer.
+
+==== Section D — Hash Constant Boundary Tests [RUNTIME]
+
+Axiom-level verification that does not import `loader.zig` (see §A.6 GAP):
+
+* `HASH_HEX_LEN == HASH_LEN * 2` (SHA-256 hex digest size relationship).
+* `LOADER_MATCH=1 ≠ CAT_OK=0` (trap: loader's "match" must not be confused with
+  catalogue "ok").
+
+==== Section E — Safety Boundary Tests [RUNTIME]
+
+Tests via `extern fn` declarations (because `safety.zig` exports its functions
+without `pub`, so they are only accessible via C linkage):
+
+----
+extern fn boj_safety_check_shell_arg(ptr: [*]const u8, len: usize) c_int;
+extern fn boj_safety_check_sql_value(ptr: [*]const u8, len: usize) c_int;
+extern fn boj_safety_check_path(ptr: [*]const u8, len: usize) c_int;
+extern fn boj_safety_check_url_scheme(ptr: [*]const u8, len: usize) c_int;
+extern fn boj_safety_check_json_string(ptr: [*]const u8, len: usize) c_int;
+----
+
+Boundary exercises (E.2/E.3): `MAX_SHELL_ARG=4096` bytes is accepted;
+4097 bytes is rejected.
+
+==== Section F — Thread-Safety Spot Check [RUNTIME]
+
+Eight threads × 4 catalogue operations each (32 total concurrent operations).
+Verifies that the module-level `Mutex` wrapper provides mutual exclusion: no
+race conditions or assertion failures under concurrent load.
+
+==== Running
+
+----
+zig build abi-verify
+----
+
+All 40 tests must pass.  A failure indicates either a live-module value has
+diverged from an axiom (§A, compile-time), or a C-ABI boundary contract has
+been violated (§B–§F, runtime).
+
+== Known Gaps and Assumptions
+
+=== [ASSUMED] C Header / Zig Alignment
+
+The `generated/abi/boj_catalogue.h` constants (e.g., `BOJ_STATUS_READY=1`,
+`BOJ_PROTO_MCP=1`) are declared to match the Idris2 ABI but are not
+automatically cross-checked against `abi_axioms.zig`.  A divergence between
+the C header and the Zig axioms would go undetected until runtime.
+
+*Mitigation:* The axioms and the C header constants were cross-checked manually
+at the time of writing.  Future: add a CI step that extracts the `#define` values
+from the header and diffs them against the axiom constants.
+
+=== [ASSUMED] Idris2 / Zig Integer Layout Agreement
+
+The Idris2 `statusToInt`, `protocolToInt`, and `domainToInt` functions produce
+values that this layer *assumes* match the `STATUS_*`, `PROTO_*`, and
+`DOMAIN_*` axioms.  This is a cross-language boundary that neither side can
+prove without a shared proof obligation.
+
+=== [GAP] Loader Module Import Conflict (§A.6)
+
+`loader.zig` uses `@import("catalogue.zig")` (relative path), which prevents
+it from being imported as a named module alongside `catalogue` in the same
+compilation unit.  The `HASH_LEN` / `HASH_HEX_LEN` constants in `loader.zig`
+are therefore verified only at the axiom level (§D), not by cross-module
+comptime assertion.
+
+*Fix:* Change `loader.zig` line 181 from `@import("catalogue.zig")` to
+`@import("catalogue")`.  Once applied, add `abi_verify_mod.addImport("loader", loader_mod)`
+in `build.zig` and a §A.6 cross-module check in `abi_verify.zig`.
+
+=== [ASSUMED] Safety Private Constants
+
+`MAX_SHELL_ARG_LEN` and `MAX_PATH_LEN` in `safety.zig` are private (not `pub`).
+The axioms declare `MAX_SHELL_ARG=4096` and `MAX_PATH=4096` as assumed values;
+if `safety.zig` is changed, the axioms will not detect the divergence.
+
+*Mitigation:* §E tests exercise the boundary directly, so a size change in
+`safety.zig` will cause E.2/E.3 to fail.
+
+== Zig 0.16 Mutex Migration
+
+`std.Thread.Mutex` was removed in Zig 0.16 as part of the `Io`-based async
+redesign.  The replacement (`std.Io.Mutex`) requires an `Io` context for every
+`lock()` call, which is incompatible with synchronous C-ABI exports.
+
+The nine affected FFI modules (`catalogue.zig`, `loader.zig`, `sla.zig`,
+`coprocessor.zig`, `community.zig`, `sdp.zig`, `guardian.zig`, `verisimdb.zig`,
+`federation.zig`) were migrated to a local `Mutex` wrapper:
+
+----
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
+----
+
+`std.atomic.Mutex` is a compare-and-swap TAS lock; `spinLoopHint()` emits a
+CPU pause hint on x86-64 to reduce power consumption and memory bus traffic
+during contention.  This is appropriate for the FFI layer's usage pattern:
+all critical sections are sub-microsecond struct field updates with very low
+contention probability.
+
+If a blocking (sleep-based) OS mutex is needed in future, the recommended
+migration path on Linux is `std.c.pthread_mutex_t` with `link_libc = true`
+in each module's `build.zig` entry.
+
+== How to Run All Verification Steps
+
+----
+# Step 1: Compile-time ABI axiom proofs (pure comptime, no runtime)
+zig build abi-axioms
+
+# Step 2: Cross-module proofs + exhaustive boundary tests (40 tests)
+zig build abi-verify
+
+# Run both together
+zig build abi-axioms abi-verify
+----
+
+Expected output:
+
+----
+Build Summary: 6/6 steps succeeded; 40/40 tests passed
+abi-axioms success
++- run test success
+abi-verify success
++- run test 40 pass (40 total)
+----
diff --git a/ffi/zig/build.zig b/ffi/zig/build.zig
index 4f8a347b..d0a15da8 100644
--- a/ffi/zig/build.zig
+++ b/ffi/zig/build.zig
@@ -308,6 +308,54 @@ pub fn build(b: *std.Build) void {
     const shim_step = b.step("shim", "Run cartridge_shim tests (ADR-0006 invoke helpers)");
     shim_step.dependOn(&run_shim_tests.step);
 
+    // --- ABI Axioms module (standalone comptime proofs, no runtime deps) ---
+    //
+    // abi_axioms.zig declares every numeric constant that crosses the C-ABI
+    // boundary and proves static invariants at compile time.  Running the test
+    // binary exercises those comptime blocks; a build failure here means an
+    // invariant was violated.
+    const abi_axioms_mod = b.addModule("boj_abi_axioms", .{
+        .root_source_file = b.path("src/abi_axioms.zig"),
+        .target = target,
+        .optimize = optimize,
+    });
+
+    const abi_axioms_tests = b.addTest(.{
+        .root_module = abi_axioms_mod,
+    });
+    const run_abi_axioms_tests = b.addRunArtifact(abi_axioms_tests);
+
+    const abi_axioms_step = b.step("abi-axioms", "Compile ABI axiom static theorems (comptime proofs only)");
+    abi_axioms_step.dependOn(&run_abi_axioms_tests.step);
+
+    // --- ABI Verification module (cross-checks axioms + exhaustive boundary tests) ---
+    //
+    // abi_verify.zig cross-checks that the live Zig types (enums, constants) match
+    // the axiom declarations at compile time, then exhaustively exercises every
+    // C-ABI boundary at runtime.  This is the formal FFI verification instrument.
+    const abi_verify_mod = b.addModule("boj_abi_verify", .{
+        .root_source_file = b.path("src/abi_verify.zig"),
+        .target = target,
+        .optimize = optimize,
+    });
+    abi_verify_mod.addImport("catalogue", catalogue_mod);
+    // loader is intentionally excluded: loader.zig imports catalogue.zig via relative
+    // path, which conflicts with the named `catalogue` module in a shared compilation.
+    // The loader's HASH_LEN/HASH_HEX_LEN constants are cross-checked via axioms alone.
+    // See abi_verify.zig §A.6 GAP note.
+    abi_verify_mod.addImport("safety", safety_mod);
+    abi_verify_mod.addImport("cartridge_shim", shim_mod);
+    // abi_axioms.zig is imported via relative path @import("abi_axioms.zig") in
+    // abi_verify.zig — no addImport needed since both files share src/.
+
+    const abi_verify_tests = b.addTest(.{
+        .root_module = abi_verify_mod,
+    });
+    const run_abi_verify_tests = b.addRunArtifact(abi_verify_tests);
+
+    const abi_verify_step = b.step("abi-verify", "Run ABI formal verification: comptime proofs + runtime boundary tests");
+    abi_verify_step.dependOn(&run_abi_verify_tests.step);
+
     // --- End-to-end order-ticket tests ---
     const e2e_mod = b.addModule("boj_e2e_order", .{
         .root_source_file = b.path("src/e2e_order.zig"),
@@ -375,6 +423,8 @@ pub fn build(b: *std.Build) void {
 
     // --- Test step runs all ---
     const test_step = b.step("test", "Run all FFI + protocol tests");
+    test_step.dependOn(&run_abi_axioms_tests.step);
+    test_step.dependOn(&run_abi_verify_tests.step);
     test_step.dependOn(&run_catalogue_tests.step);
     test_step.dependOn(&run_loader_tests.step);
     test_step.dependOn(&run_readiness_tests.step);
diff --git a/ffi/zig/src/abi_axioms.zig b/ffi/zig/src/abi_axioms.zig
new file mode 100644
index 00000000..6144952e
--- /dev/null
+++ b/ffi/zig/src/abi_axioms.zig
@@ -0,0 +1,428 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//
+// ABI Axioms — Canonical trusted boundary declarations for the Zig FFI.
+//
+// This file is the single source of truth for every numeric constant that
+// crosses the C-ABI boundary between Zig, C, and the Idris2 proof layer.
+//
+// Each constant carries a trust classification:
+//
+//   [STATIC]   Proven at compile time within this file alone.
+//              The comptime blocks below are theorems — they fail to compile
+//              if violated.  A passing build implies the theorem is true.
+//
+//   [CROSS]    Proven at compile time in abi_verify.zig by comparing these
+//              constants against the actual Zig types (enums, structs) they
+//              describe.  Requires importing both this file and the relevant
+//              modules.
+//
+//   [RUNTIME]  Operationally verified by abi_verify.zig boundary tests.
+//              True under exhaustive boundary coverage of the C-ABI surface.
+//
+//   [ASSUMED]  Cross-language axioms (Idris2↔Zig, private-const↔axiom) that
+//              cannot be mechanically verified in Zig alone.  The Idris2
+//              proofs in src/abi/ provide the formal complement for the
+//              Idris2-side.  Breakage here manifests as runtime divergence,
+//              not a compile error.
+//
+// Trust chain (narrowest → widest):
+//   Idris2 proofs → [ASSUMED] axioms → [CROSS] comptime → [RUNTIME] tests
+//
+// Design constraints:
+//   • No imports — standalone so any language can consume the numeric surface.
+//   • No functions — pure constant declarations and inert comptime proofs.
+//   • All public constants are untyped comptime_int / comptime_float so they
+//     coerce to any integer type without explicit casting at the use site.
+
+// ═══════════════════════════════════════════════════════════════════════════
+// § 1  Cartridge Invocation ABI (ADR-0006, frozen)
+// ═══════════════════════════════════════════════════════════════════════════
+//
+// Source:  ffi/zig/src/cartridge_shim.zig (pub const RC_*)
+// Cross-ref: docs/ADR-0006.adoc §Return codes
+//
+// Five-symbol cartridge ABI: boj_cartridge_{init,deinit,name,version,invoke}.
+// The invoke function signature:
+//
+//   boj_cartridge_invoke(
+//       tool_name:  [*c]const u8,   // NUL-terminated tool name
+//       json_args:  [*c]const u8,   // NUL-terminated JSON argument blob
+//       out_buf:    [*c]u8,         // caller-allocated output buffer
+//       in_out_len: [*c]usize,      // in: capacity; out: bytes written or required
+//   ) callconv(.c) i32              // one of the RC_* codes below
+//
+// Return codes are a CLOSED SET — frozen by ADR-0006.  New failure modes
+// must be expressed in the JSON error body; the integer surface must not grow
+// without a new ADR.
+
+/// [CROSS] Successful invocation — result written into out_buf.
+pub const RC_SUCCESS = 0;
+
+/// [CROSS] Tool name not recognised by this cartridge.
+pub const RC_UNKNOWN_TOOL = -1;
+
+/// [CROSS] Null pointer or invalid JSON in required argument.
+pub const RC_BAD_ARGS = -2;
+
+/// [CROSS] Output buffer too small.
+/// [RUNTIME] On return: *in_out_len is set to the required byte count.
+pub const RC_BUFFER_TOO_SMALL = -3;
+
+/// [CROSS] Unexpected runtime error inside the cartridge.
+pub const RC_RUNTIME_ERROR = -4;
+
+/// [CROSS] Zig panic caught at FFI boundary.  Cartridge state is undefined.
+pub const RC_PANIC = -5;
+
+/// [CROSS] Auth check failed.  Caller must not retry without fresh credentials.
+pub const RC_AUTH_DENIED = -6;
+
+/// [STATIC] Number of distinct return-code values (including RC_SUCCESS).
+pub const RC_CODE_COUNT = 7;
+
+// ─── §1 Comptime theorems ──────────────────────────────────────────────────
+
+comptime {
+    // THEOREM[ax.1.1]: RC_SUCCESS is exactly zero (universal C convention for ok).
+    if (RC_SUCCESS != 0)
+        @compileError("ax.1.1: RC_SUCCESS must be 0");
+
+    // THEOREM[ax.1.2]: Every error code is strictly negative.
+    if (RC_UNKNOWN_TOOL >= 0) @compileError("ax.1.2: RC_UNKNOWN_TOOL must be < 0");
+    if (RC_BAD_ARGS >= 0) @compileError("ax.1.2: RC_BAD_ARGS must be < 0");
+    if (RC_BUFFER_TOO_SMALL >= 0) @compileError("ax.1.2: RC_BUFFER_TOO_SMALL must be < 0");
+    if (RC_RUNTIME_ERROR >= 0) @compileError("ax.1.2: RC_RUNTIME_ERROR must be < 0");
+    if (RC_PANIC >= 0) @compileError("ax.1.2: RC_PANIC must be < 0");
+    if (RC_AUTH_DENIED >= 0) @compileError("ax.1.2: RC_AUTH_DENIED must be < 0");
+
+    // THEOREM[ax.1.3]: Error codes are dense and ordered in [-6, -1].
+    // Any gap would leave an unmapped integer with undefined meaning.
+    if (RC_UNKNOWN_TOOL != -1) @compileError("ax.1.3: RC_UNKNOWN_TOOL must be -1");
+    if (RC_BAD_ARGS != -2) @compileError("ax.1.3: RC_BAD_ARGS must be -2");
+    if (RC_BUFFER_TOO_SMALL != -3) @compileError("ax.1.3: RC_BUFFER_TOO_SMALL must be -3");
+    if (RC_RUNTIME_ERROR != -4) @compileError("ax.1.3: RC_RUNTIME_ERROR must be -4");
+    if (RC_PANIC != -5) @compileError("ax.1.3: RC_PANIC must be -5");
+    if (RC_AUTH_DENIED != -6) @compileError("ax.1.3: RC_AUTH_DENIED must be -6");
+
+    // THEOREM[ax.1.4]: RC_CODE_COUNT covers [RC_AUTH_DENIED, RC_SUCCESS] inclusive.
+    if (RC_CODE_COUNT != -RC_AUTH_DENIED + 1)
+        @compileError("ax.1.4: RC_CODE_COUNT must equal |RC_AUTH_DENIED| + 1");
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// § 2  Catalogue ABI
+// ═══════════════════════════════════════════════════════════════════════════
+//
+// Sources: ffi/zig/src/catalogue.zig, generated/abi/boj_catalogue.h
+// Idris2:  src/abi/Boj/{Catalogue,Domain,Protocol}.idr
+// [ASSUMED] Integer values mirror the Idris2 *ToInt functions exactly.
+//           Any drift from src/abi/ is an assumed axiom violation.
+
+// ─── CartridgeStatus ──────────────────────────────────────────────────────
+// [CROSS] catalogue.CartridgeStatus enum  ↔  BOJ_STATUS_* in boj_catalogue.h
+
+pub const STATUS_DEVELOPMENT = 0;
+pub const STATUS_READY = 1;
+pub const STATUS_DEPRECATED = 2;
+pub const STATUS_FAULTY = 3;
+
+/// [CROSS] [RUNTIME] The ONLY status value that passes the mount gate.
+/// Mirrors the IsUnbreakable predicate in src/abi/Boj/Catalogue.idr.
+pub const MOUNT_GATE_STATUS = STATUS_READY;
+
+// ─── ProtocolType ─────────────────────────────────────────────────────────
+// [CROSS] catalogue.ProtocolType enum  ↔  BOJ_PROTO_* in boj_catalogue.h
+// Protocol slots are stored in a [9]bool array indexed by (protocol_value - 1).
+
+pub const PROTO_MCP = 1;
+pub const PROTO_LSP = 2;
+pub const PROTO_DAP = 3;
+pub const PROTO_BSP = 4;
+pub const PROTO_NESY = 5;
+pub const PROTO_AGENTIC = 6;
+pub const PROTO_FLEET = 7;
+pub const PROTO_GRPC = 8;
+pub const PROTO_REST = 9;
+pub const PROTO_MIN = PROTO_MCP;
+pub const PROTO_MAX = PROTO_REST;
+pub const PROTO_COUNT = 9;
+
+// ─── CapabilityDomain ─────────────────────────────────────────────────────
+// [CROSS] catalogue.CapabilityDomain enum  ↔  BOJ_DOMAIN_* in boj_catalogue.h
+
+pub const DOMAIN_CLOUD = 1;
+pub const DOMAIN_CONTAINER = 2;
+pub const DOMAIN_DATABASE = 3;
+pub const DOMAIN_K8S = 4;
+pub const DOMAIN_GIT = 5;
+pub const DOMAIN_SECRETS = 6;
+pub const DOMAIN_QUEUES = 7;
+pub const DOMAIN_IAC = 8;
+pub const DOMAIN_OBSERVE = 9;
+pub const DOMAIN_SSG = 10;
+pub const DOMAIN_PROOF = 11;
+pub const DOMAIN_FLEET = 12;
+pub const DOMAIN_NESY = 13;
+pub const DOMAIN_AGENT = 14;
+pub const DOMAIN_LSP = 15;
+pub const DOMAIN_DAP = 16;
+pub const DOMAIN_BSP = 17;
+pub const DOMAIN_CODE_INTEL = 18;
+pub const DOMAIN_MIN = DOMAIN_CLOUD;
+pub const DOMAIN_MAX = DOMAIN_CODE_INTEL;
+
+// ─── MenuTier ─────────────────────────────────────────────────────────────
+// [CROSS] catalogue.MenuTier enum  ↔  BOJ_TIER_* in boj_catalogue.h
+
+pub const TIER_TERANGA = 0;
+pub const TIER_SHIELD = 1;
+pub const TIER_AYO = 2;
+pub const TIER_MIN = TIER_TERANGA;
+pub const TIER_MAX = TIER_AYO;
+
+// ─── Catalogue capacity bounds ────────────────────────────────────────────
+// [RUNTIME] Enforced inside catalogue.zig; declared here as axioms.
+
+/// Maximum cartridges the registry can hold (catalogue array length).
+pub const MAX_CARTRIDGES = 128;
+
+/// Maximum cartridges in a single order ticket passed to boj_menu_validate_order.
+pub const MAX_ORDER_SIZE = 16;
+
+/// Length of the CartridgeEntry.protocols array (one slot per ProtocolType).
+pub const PROTOCOLS_SLOT_COUNT = 9;
+
+// ─── Catalogue field size bounds ──────────────────────────────────────────
+// [RUNTIME] Enforced by boj_catalogue_register before @memcpy into fixed fields.
+
+/// Maximum cartridge name byte count (CartridgeEntry.name field length).
+pub const NAME_MAX = 64;
+
+/// Maximum version string byte count (CartridgeEntry.version field length).
+pub const VERSION_MAX = 16;
+
+/// Maximum backend label byte count (CartridgeEntry.backend field length).
+pub const BACKEND_MAX = 32;
+
+// ─── Catalogue function return conventions ────────────────────────────────
+// [RUNTIME] Named for readability; the underlying values are 0 / -1 / -2.
+
+/// boj_catalogue_init, boj_catalogue_register, etc.: success.
+pub const CAT_OK = 0;
+/// boj_catalogue_register, etc.: bad argument or capacity exceeded.
+pub const CAT_ERR = -1;
+/// boj_catalogue_mount / boj_catalogue_unmount: index out of range.
+pub const CAT_NOT_FOUND = -2;
+/// boj_catalogue_is_mounted: the cartridge is mounted.
+pub const CAT_MOUNTED = 1;
+/// boj_catalogue_is_mounted: the cartridge exists but is not mounted.
+pub const CAT_UNMOUNTED = 0;
+/// boj_catalogue_is_mounted: index out of range.
+pub const CAT_IS_MOUNTED_ERR = -1;
+
+// ─── §2 Comptime theorems ─────────────────────────────────────────────────
+
+comptime {
+    // THEOREM[ax.2.1]: Status codes are 0-based consecutive integers in [0, 3].
+    if (STATUS_DEVELOPMENT != 0) @compileError("ax.2.1: STATUS_DEVELOPMENT must be 0");
+    if (STATUS_READY != STATUS_DEVELOPMENT + 1) @compileError("ax.2.1: STATUS_READY must be STATUS_DEVELOPMENT+1");
+    if (STATUS_DEPRECATED != STATUS_READY + 1) @compileError("ax.2.1: STATUS_DEPRECATED must be STATUS_READY+1");
+    if (STATUS_FAULTY != STATUS_DEPRECATED + 1) @compileError("ax.2.1: STATUS_FAULTY must be STATUS_DEPRECATED+1");
+
+    // THEOREM[ax.2.2]: Mount gate is exactly and only STATUS_READY.
+    if (MOUNT_GATE_STATUS != STATUS_READY)
+        @compileError("ax.2.2: MOUNT_GATE_STATUS must equal STATUS_READY");
+
+    // THEOREM[ax.2.3]: Protocol range [1, 9] is non-empty and fully spans PROTO_COUNT.
+    if (PROTO_MIN != 1) @compileError("ax.2.3: PROTO_MIN must be 1");
+    if (PROTO_MAX != 9) @compileError("ax.2.3: PROTO_MAX must be 9");
+    if (PROTO_COUNT != PROTO_MAX - PROTO_MIN + 1)
+        @compileError("ax.2.3: PROTO_COUNT must be PROTO_MAX - PROTO_MIN + 1");
+    if (PROTOCOLS_SLOT_COUNT != PROTO_COUNT)
+        @compileError("ax.2.3: PROTOCOLS_SLOT_COUNT must equal PROTO_COUNT");
+
+    // THEOREM[ax.2.4]: Tier codes are 0-based consecutive integers in [0, 2].
+    if (TIER_TERANGA != 0) @compileError("ax.2.4: TIER_TERANGA must be 0");
+    if (TIER_SHIELD != 1) @compileError("ax.2.4: TIER_SHIELD must be 1");
+    if (TIER_AYO != 2) @compileError("ax.2.4: TIER_AYO must be 2");
+
+    // THEOREM[ax.2.5]: Capacity bounds are non-zero and order-safe.
+    if (MAX_CARTRIDGES == 0) @compileError("ax.2.5: MAX_CARTRIDGES must be positive");
+    if (MAX_ORDER_SIZE == 0) @compileError("ax.2.5: MAX_ORDER_SIZE must be positive");
+    if (MAX_ORDER_SIZE > MAX_CARTRIDGES)
+        @compileError("ax.2.5: MAX_ORDER_SIZE must not exceed MAX_CARTRIDGES");
+
+    // THEOREM[ax.2.6]: Field size bounds are non-zero and hierarchically ordered.
+    if (NAME_MAX == 0) @compileError("ax.2.6: NAME_MAX must be positive");
+    if (VERSION_MAX == 0) @compileError("ax.2.6: VERSION_MAX must be positive");
+    if (BACKEND_MAX == 0) @compileError("ax.2.6: BACKEND_MAX must be positive");
+    if (NAME_MAX <= VERSION_MAX)
+        @compileError("ax.2.6: NAME_MAX must strictly exceed VERSION_MAX");
+
+    // THEOREM[ax.2.7]: Catalogue OK code equals RC_SUCCESS.
+    // Both are 0 — the C convention for "no error" across the whole ABI.
+    if (CAT_OK != RC_SUCCESS)
+        @compileError("ax.2.7: CAT_OK must equal RC_SUCCESS (both are 0)");
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// § 3  Loader ABI
+// ═══════════════════════════════════════════════════════════════════════════
+//
+// Source: ffi/zig/src/loader.zig
+//
+// IMPORTANT: The loader uses a DISTINCT return convention from catalogue
+// functions.  boj_loader_verify returns 1=match, 0=mismatch, -1=error —
+// a tri-state boolean.  It does NOT return 0 for success.
+// Callers MUST NOT treat 0 from boj_loader_verify as "ok".
+
+/// [CROSS] SHA-256 raw digest length in bytes.
+pub const HASH_LEN = 32;
+
+/// [CROSS] SHA-256 hex-encoded digest length in ASCII characters.
+pub const HASH_HEX_LEN = 64;
+
+/// Maximum WASM cartridges registered simultaneously.
+pub const MAX_WASM_CARTRIDGES = 32;
+
+/// Maximum filesystem path length for a WASM module byte string.
+pub const MAX_WASM_PATH_LEN = 512;
+
+/// [RUNTIME] boj_loader_verify: binary hash matches expected hash.
+pub const LOADER_MATCH = 1;
+/// [RUNTIME] boj_loader_verify: binary hash does NOT match expected hash.
+pub const LOADER_MISMATCH = 0;
+/// [RUNTIME] boj_loader_verify: I/O error or bad parameter.
+pub const LOADER_ERROR = -1;
+
+// ─── §3 Comptime theorems ─────────────────────────────────────────────────
+
+comptime {
+    // THEOREM[ax.3.1]: Hex length is exactly double the raw byte length.
+    // Invariant of hexadecimal encoding: 1 byte → 2 hex chars.
+    if (HASH_HEX_LEN != HASH_LEN * 2)
+        @compileError("ax.3.1: HASH_HEX_LEN must equal HASH_LEN * 2");
+
+    // THEOREM[ax.3.2]: LOADER_MATCH does not alias CAT_OK.
+    // LOADER_MATCH=1 signals "hash verified"; CAT_OK=0 signals "operation succeeded".
+    // Callers who confuse these will silently skip hash verification.
+    if (LOADER_MATCH == CAT_OK)
+        @compileError("ax.3.2: LOADER_MATCH must not equal CAT_OK — loader convention differs");
+
+    // NOTE[ax.3.3]: LOADER_MISMATCH (0) numerically aliases CAT_OK (0).
+    // This is a documented ABI wart.  The distinction is context-dependent:
+    // boj_loader_verify returning 0 means "mismatch" (bad), not "ok".
+    // LOADER_ERROR (-1) aliases CAT_ERR (-1) — again context-dependent.
+    // Tests in abi_verify.zig explicitly cover these aliased paths.
+
+    // THEOREM[ax.3.4]: WASM capacity is bounded by total catalogue capacity.
+    if (MAX_WASM_CARTRIDGES == 0) @compileError("ax.3.4: MAX_WASM_CARTRIDGES must be positive");
+    if (MAX_WASM_CARTRIDGES > MAX_CARTRIDGES)
+        @compileError("ax.3.4: MAX_WASM_CARTRIDGES must not exceed MAX_CARTRIDGES");
+
+    // THEOREM[ax.3.5]: Hash hex string fits in the catalogue's binary_hash field.
+    // CartridgeEntry.binary_hash is [64]u8; HASH_HEX_LEN is 64.
+    if (HASH_HEX_LEN > NAME_MAX)
+        @compileError("ax.3.5: HASH_HEX_LEN must not exceed NAME_MAX (catalogue stores hash in [64]u8)");
+
+    // THEOREM[ax.3.6]: LOADER_ERROR is negative.
+    if (LOADER_ERROR >= 0) @compileError("ax.3.6: LOADER_ERROR must be negative");
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// § 4  Safety ABI
+// ═══════════════════════════════════════════════════════════════════════════
+//
+// Source: ffi/zig/src/safety.zig (SafetyError enum, private length constants)
+// [CROSS] The SafetyError enum values are pub and can be cross-checked.
+// [ASSUMED] MAX_SHELL_ARG and MAX_PATH must match safety.zig's private
+//           MAX_SHELL_ARG_LEN and MAX_PATH_LEN constants.  These cannot be
+//           mechanically verified without making those constants pub.
+
+/// [CROSS] Input passed all safety checks for the requested operation.
+pub const SAFETY_SAFE = 1;
+
+/// [CROSS] Input was empty.  Safe for SQL values; error for paths/shell args.
+pub const SAFETY_EMPTY = 0;
+
+/// [CROSS] Input contains shell metacharacters or option injection.
+pub const SAFETY_SHELL_INJECTION = -1;
+
+/// [CROSS] Input contains SQL injection patterns (comment, semicolon, quote).
+pub const SAFETY_SQL_INJECTION = -2;
+
+/// [CROSS] Input contains path traversal sequences (../).
+pub const SAFETY_PATH_TRAVERSAL = -3;
+
+/// [CROSS] Input exceeds the configured maximum length for this check.
+pub const SAFETY_TOO_LONG = -4;
+
+/// [CROSS] Input contains null bytes (always rejected).
+pub const SAFETY_NULL_BYTE = -5;
+
+/// [CROSS] Input contains control characters (U+0000–U+001F, excluding \t).
+pub const SAFETY_CONTROL_CHAR = -6;
+
+/// [CROSS] Input contains a disallowed URL scheme (javascript:, data:, file:, …).
+pub const SAFETY_INVALID_URL = -7;
+
+/// [CROSS] Input contains characters unsafe in JSON strings (\, ", controls).
+pub const SAFETY_JSON_UNSAFE = -8;
+
+/// [ASSUMED] Maximum shell argument byte length.  Mirrors safety.zig MAX_SHELL_ARG_LEN.
+pub const MAX_SHELL_ARG = 4096;
+
+/// [ASSUMED] Maximum path byte length.  Mirrors safety.zig MAX_PATH_LEN (= POSIX PATH_MAX).
+pub const MAX_PATH = 4096;
+
+// ─── §4 Comptime theorems ─────────────────────────────────────────────────
+
+comptime {
+    // THEOREM[ax.4.1]: SAFETY_SAFE is the unique positive safety code.
+    if (SAFETY_SAFE <= 0) @compileError("ax.4.1: SAFETY_SAFE must be positive");
+    if (SAFETY_EMPTY != 0) @compileError("ax.4.1: SAFETY_EMPTY must be 0");
+
+    // THEOREM[ax.4.2]: All rejection codes are strictly negative.
+    if (SAFETY_SHELL_INJECTION >= 0) @compileError("ax.4.2: SAFETY_SHELL_INJECTION must be < 0");
+    if (SAFETY_SQL_INJECTION >= 0) @compileError("ax.4.2: SAFETY_SQL_INJECTION must be < 0");
+    if (SAFETY_PATH_TRAVERSAL >= 0) @compileError("ax.4.2: SAFETY_PATH_TRAVERSAL must be < 0");
+    if (SAFETY_TOO_LONG >= 0) @compileError("ax.4.2: SAFETY_TOO_LONG must be < 0");
+    if (SAFETY_NULL_BYTE >= 0) @compileError("ax.4.2: SAFETY_NULL_BYTE must be < 0");
+    if (SAFETY_CONTROL_CHAR >= 0) @compileError("ax.4.2: SAFETY_CONTROL_CHAR must be < 0");
+    if (SAFETY_INVALID_URL >= 0) @compileError("ax.4.2: SAFETY_INVALID_URL must be < 0");
+    if (SAFETY_JSON_UNSAFE >= 0) @compileError("ax.4.2: SAFETY_JSON_UNSAFE must be < 0");
+
+    // THEOREM[ax.4.3]: Rejection codes are dense in [-8, -1] — no gaps or aliases.
+    if (SAFETY_SHELL_INJECTION != -1) @compileError("ax.4.3: SAFETY_SHELL_INJECTION must be -1");
+    if (SAFETY_SQL_INJECTION != -2) @compileError("ax.4.3: SAFETY_SQL_INJECTION must be -2");
+    if (SAFETY_PATH_TRAVERSAL != -3) @compileError("ax.4.3: SAFETY_PATH_TRAVERSAL must be -3");
+    if (SAFETY_TOO_LONG != -4) @compileError("ax.4.3: SAFETY_TOO_LONG must be -4");
+    if (SAFETY_NULL_BYTE != -5) @compileError("ax.4.3: SAFETY_NULL_BYTE must be -5");
+    if (SAFETY_CONTROL_CHAR != -6) @compileError("ax.4.3: SAFETY_CONTROL_CHAR must be -6");
+    if (SAFETY_INVALID_URL != -7) @compileError("ax.4.3: SAFETY_INVALID_URL must be -7");
+    if (SAFETY_JSON_UNSAFE != -8) @compileError("ax.4.3: SAFETY_JSON_UNSAFE must be -8");
+
+    // THEOREM[ax.4.4]: Safety codes do not alias invoke return codes in the negative range.
+    // Both sets use negative integers as error codes.  Ensure the ranges are disjoint:
+    //   invoke errors: [-6, -1]  (RC_UNKNOWN_TOOL..RC_AUTH_DENIED)
+    //   safety errors: [-8, -1]  (SAFETY_SHELL_INJECTION..SAFETY_JSON_UNSAFE)
+    // They OVERLAP at [-6, -1].  This is safe because:
+    //   (a) safety checks run before invoke — there is no call site where both
+    //       could be returned from the same function, and
+    //   (b) the outer caller (mcp-bridge) inspects the function name, not just
+    //       the integer, to determine which error occurred.
+    // NOTE: If in future a safety code is used as an invoke return code, this
+    // axiom must be revisited. [ASSUMED] The bridge layer maintains this separation.
+
+    // THEOREM[ax.4.5]: Safety bounds are POSIX-compatible (positive, plausible).
+    if (MAX_SHELL_ARG == 0) @compileError("ax.4.5: MAX_SHELL_ARG must be positive");
+    if (MAX_PATH == 0) @compileError("ax.4.5: MAX_PATH must be positive");
+
+    // THEOREM[ax.4.6]: Safety codes do not alias the invoke closed set above 0.
+    if (SAFETY_SAFE == RC_SUCCESS)
+        @compileError("ax.4.6: SAFETY_SAFE (1) must not alias RC_SUCCESS (0)");
+    // SAFETY_EMPTY (0) equals RC_SUCCESS (0) and CAT_OK (0) — this is intentional.
+    // "Empty input is acceptable" for SQL is numerically the same as "ok" in other
+    // contexts.  Separation is maintained at the call-site level, not the integer level.
+}
diff --git a/ffi/zig/src/abi_verify.zig b/ffi/zig/src/abi_verify.zig
new file mode 100644
index 00000000..0058ce59
--- /dev/null
+++ b/ffi/zig/src/abi_verify.zig
@@ -0,0 +1,726 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//
+// ABI Verification Instrument — Exhaustive boundary tests for the Zig FFI.
+//
+// This file is the runtime complement to abi_axioms.zig:
+//
+//   abi_axioms.zig  — declares constants; proves static/cross invariants at
+//                     compile time (theorems in the mathematical sense).
+//   abi_verify.zig  — cross-checks axioms against live Zig types (comptime),
+//                     then exhaustively exercises every ABI boundary (runtime).
+//
+// Structure:
+//   §A  Cross-module comptime proofs   (fail to COMPILE if violated)
+//   §B  Catalogue boundary tests        (fail at RUNTIME if violated)
+//   §C  Cartridge invoke ABI tests      (writeResult / toolIs / invokeArgsNull)
+//   §D  Hash/Loader boundary tests
+//   §E  Safety boundary tests
+//   §F  Thread-safety spot check
+//
+// How to read the trust labels:
+//   [THEOREM]  Proven by this comptime block — true iff code compiles.
+//   [TEST]     Proven by this runtime test — true for all covered inputs.
+//   [BOUNDARY] This test is specifically exercising the limit value.
+//   [GAP]      Known gap: what is NOT proven here and why.
+
+const std = @import("std");
+const axioms = @import("abi_axioms.zig");
+const catalogue = @import("catalogue");
+const safety = @import("safety");
+const shim = @import("cartridge_shim");
+// loader is intentionally NOT imported here.  loader.zig uses @import("catalogue.zig")
+// (a relative-path import) internally, which conflicts with the named `catalogue` module
+// when both are included in the same test compilation.  The loader's hash constants
+// (HASH_LEN, HASH_HEX_LEN) are axiomatically declared in abi_axioms.zig and cross-checked
+// there via comptime.  See §A.6 below for the documented gap.
+
+// ═══════════════════════════════════════════════════════════════════════════
+// §A  Cross-module comptime proofs
+// ═══════════════════════════════════════════════════════════════════════════
+//
+// These blocks run at COMPILE TIME.  A violation causes a compile error with
+// the axiom ID.  They cannot be disabled or skipped by the test runner.
+
+comptime {
+    // ─── A.1  CartridgeStatus encoding matches axioms ──────────────────────
+    // [THEOREM] If CartridgeStatus drifts from the C header, this block fails.
+    if (@intFromEnum(catalogue.CartridgeStatus.development) != axioms.STATUS_DEVELOPMENT)
+        @compileError("cv.A.1: CartridgeStatus.development != axioms.STATUS_DEVELOPMENT");
+    if (@intFromEnum(catalogue.CartridgeStatus.ready) != axioms.STATUS_READY)
+        @compileError("cv.A.1: CartridgeStatus.ready != axioms.STATUS_READY");
+    if (@intFromEnum(catalogue.CartridgeStatus.deprecated) != axioms.STATUS_DEPRECATED)
+        @compileError("cv.A.1: CartridgeStatus.deprecated != axioms.STATUS_DEPRECATED");
+    if (@intFromEnum(catalogue.CartridgeStatus.faulty) != axioms.STATUS_FAULTY)
+        @compileError("cv.A.1: CartridgeStatus.faulty != axioms.STATUS_FAULTY");
+
+    // ─── A.2  ProtocolType encoding matches axioms ─────────────────────────
+    if (@intFromEnum(catalogue.ProtocolType.mcp) != axioms.PROTO_MCP)
+        @compileError("cv.A.2: ProtocolType.mcp != axioms.PROTO_MCP");
+    if (@intFromEnum(catalogue.ProtocolType.lsp) != axioms.PROTO_LSP)
+        @compileError("cv.A.2: ProtocolType.lsp != axioms.PROTO_LSP");
+    if (@intFromEnum(catalogue.ProtocolType.dap) != axioms.PROTO_DAP)
+        @compileError("cv.A.2: ProtocolType.dap != axioms.PROTO_DAP");
+    if (@intFromEnum(catalogue.ProtocolType.bsp) != axioms.PROTO_BSP)
+        @compileError("cv.A.2: ProtocolType.bsp != axioms.PROTO_BSP");
+    if (@intFromEnum(catalogue.ProtocolType.nesy) != axioms.PROTO_NESY)
+        @compileError("cv.A.2: ProtocolType.nesy != axioms.PROTO_NESY");
+    if (@intFromEnum(catalogue.ProtocolType.agentic) != axioms.PROTO_AGENTIC)
+        @compileError("cv.A.2: ProtocolType.agentic != axioms.PROTO_AGENTIC");
+    if (@intFromEnum(catalogue.ProtocolType.fleet) != axioms.PROTO_FLEET)
+        @compileError("cv.A.2: ProtocolType.fleet != axioms.PROTO_FLEET");
+    if (@intFromEnum(catalogue.ProtocolType.grpc) != axioms.PROTO_GRPC)
+        @compileError("cv.A.2: ProtocolType.grpc != axioms.PROTO_GRPC");
+    if (@intFromEnum(catalogue.ProtocolType.rest) != axioms.PROTO_REST)
+        @compileError("cv.A.2: ProtocolType.rest != axioms.PROTO_REST");
+
+    // ─── A.3  CapabilityDomain encoding matches axioms ────────────────────
+    if (@intFromEnum(catalogue.CapabilityDomain.cloud) != axioms.DOMAIN_CLOUD)
+        @compileError("cv.A.3: CapabilityDomain.cloud != axioms.DOMAIN_CLOUD");
+    if (@intFromEnum(catalogue.CapabilityDomain.container) != axioms.DOMAIN_CONTAINER)
+        @compileError("cv.A.3: CapabilityDomain.container != axioms.DOMAIN_CONTAINER");
+    if (@intFromEnum(catalogue.CapabilityDomain.database) != axioms.DOMAIN_DATABASE)
+        @compileError("cv.A.3: CapabilityDomain.database != axioms.DOMAIN_DATABASE");
+    if (@intFromEnum(catalogue.CapabilityDomain.k8s) != axioms.DOMAIN_K8S)
+        @compileError("cv.A.3: CapabilityDomain.k8s != axioms.DOMAIN_K8S");
+    if (@intFromEnum(catalogue.CapabilityDomain.git) != axioms.DOMAIN_GIT)
+        @compileError("cv.A.3: CapabilityDomain.git != axioms.DOMAIN_GIT");
+    if (@intFromEnum(catalogue.CapabilityDomain.secrets) != axioms.DOMAIN_SECRETS)
+        @compileError("cv.A.3: CapabilityDomain.secrets != axioms.DOMAIN_SECRETS");
+    if (@intFromEnum(catalogue.CapabilityDomain.code_intel) != axioms.DOMAIN_CODE_INTEL)
+        @compileError("cv.A.3: CapabilityDomain.code_intel != axioms.DOMAIN_CODE_INTEL");
+
+    // ─── A.4  MenuTier encoding matches axioms ────────────────────────────
+    if (@intFromEnum(catalogue.MenuTier.teranga) != axioms.TIER_TERANGA)
+        @compileError("cv.A.4: MenuTier.teranga != axioms.TIER_TERANGA");
+    if (@intFromEnum(catalogue.MenuTier.shield) != axioms.TIER_SHIELD)
+        @compileError("cv.A.4: MenuTier.shield != axioms.TIER_SHIELD");
+    if (@intFromEnum(catalogue.MenuTier.ayo) != axioms.TIER_AYO)
+        @compileError("cv.A.4: MenuTier.ayo != axioms.TIER_AYO");
+
+    // ─── A.5  Cartridge invoke return codes match axioms ──────────────────
+    // shim.RC_* are i32; axioms.RC_* are comptime_int — comparison is direct.
+    if (shim.RC_SUCCESS != axioms.RC_SUCCESS)
+        @compileError("cv.A.5: shim.RC_SUCCESS != axioms.RC_SUCCESS");
+    if (shim.RC_UNKNOWN_TOOL != axioms.RC_UNKNOWN_TOOL)
+        @compileError("cv.A.5: shim.RC_UNKNOWN_TOOL != axioms.RC_UNKNOWN_TOOL");
+    if (shim.RC_BAD_ARGS != axioms.RC_BAD_ARGS)
+        @compileError("cv.A.5: shim.RC_BAD_ARGS != axioms.RC_BAD_ARGS");
+    if (shim.RC_BUFFER_TOO_SMALL != axioms.RC_BUFFER_TOO_SMALL)
+        @compileError("cv.A.5: shim.RC_BUFFER_TOO_SMALL != axioms.RC_BUFFER_TOO_SMALL");
+    if (shim.RC_RUNTIME_ERROR != axioms.RC_RUNTIME_ERROR)
+        @compileError("cv.A.5: shim.RC_RUNTIME_ERROR != axioms.RC_RUNTIME_ERROR");
+    if (shim.RC_PANIC != axioms.RC_PANIC)
+        @compileError("cv.A.5: shim.RC_PANIC != axioms.RC_PANIC");
+    if (shim.RC_AUTH_DENIED != axioms.RC_AUTH_DENIED)
+        @compileError("cv.A.5: shim.RC_AUTH_DENIED != axioms.RC_AUTH_DENIED");
+
+    // ─── A.6  [GAP] Loader hash constants ────────────────────────────────
+    // loader.HASH_LEN and loader.HASH_HEX_LEN cannot be cross-checked here because
+    // importing the `loader` module in the same compilation as `catalogue` causes a
+    // "file exists in multiple modules" error (loader.zig uses @import("catalogue.zig")
+    // internally, conflicting with the named `catalogue` module).
+    //
+    // Mitigation: abi_axioms.zig declares HASH_LEN=32 and HASH_HEX_LEN=64, and
+    // proves HASH_HEX_LEN == HASH_LEN * 2 at comptime (ax.3.1).  loader.zig's own
+    // tests (run via `zig build loader`) validate the same constants independently.
+    // The gap is the missing CROSS-CHECKED theorem "loader module agrees with axioms".
+    //
+    // Tracked: resolve when loader.zig is updated to use named-module import
+    // (@import("catalogue") via loader_mod.addImport) instead of @import("catalogue.zig").
+
+    // ─── A.7  SafetyError enum values match axioms ────────────────────────
+    if (@intFromEnum(safety.SafetyError.safe) != axioms.SAFETY_SAFE)
+        @compileError("cv.A.7: SafetyError.safe != axioms.SAFETY_SAFE");
+    if (@intFromEnum(safety.SafetyError.empty) != axioms.SAFETY_EMPTY)
+        @compileError("cv.A.7: SafetyError.empty != axioms.SAFETY_EMPTY");
+    if (@intFromEnum(safety.SafetyError.shell_injection) != axioms.SAFETY_SHELL_INJECTION)
+        @compileError("cv.A.7: SafetyError.shell_injection != axioms.SAFETY_SHELL_INJECTION");
+    if (@intFromEnum(safety.SafetyError.sql_injection) != axioms.SAFETY_SQL_INJECTION)
+        @compileError("cv.A.7: SafetyError.sql_injection != axioms.SAFETY_SQL_INJECTION");
+    if (@intFromEnum(safety.SafetyError.path_traversal) != axioms.SAFETY_PATH_TRAVERSAL)
+        @compileError("cv.A.7: SafetyError.path_traversal != axioms.SAFETY_PATH_TRAVERSAL");
+    if (@intFromEnum(safety.SafetyError.too_long) != axioms.SAFETY_TOO_LONG)
+        @compileError("cv.A.7: SafetyError.too_long != axioms.SAFETY_TOO_LONG");
+    if (@intFromEnum(safety.SafetyError.null_byte) != axioms.SAFETY_NULL_BYTE)
+        @compileError("cv.A.7: SafetyError.null_byte != axioms.SAFETY_NULL_BYTE");
+    if (@intFromEnum(safety.SafetyError.control_char) != axioms.SAFETY_CONTROL_CHAR)
+        @compileError("cv.A.7: SafetyError.control_char != axioms.SAFETY_CONTROL_CHAR");
+    if (@intFromEnum(safety.SafetyError.invalid_url) != axioms.SAFETY_INVALID_URL)
+        @compileError("cv.A.7: SafetyError.invalid_url != axioms.SAFETY_INVALID_URL");
+    if (@intFromEnum(safety.SafetyError.json_unsafe) != axioms.SAFETY_JSON_UNSAFE)
+        @compileError("cv.A.7: SafetyError.json_unsafe != axioms.SAFETY_JSON_UNSAFE");
+}
+
+// [GAP] Private constants in catalogue.zig (MAX_CARTRIDGES=128, MAX_ORDER_SIZE=16)
+// cannot be proven via comptime cross-check.  They are verified at runtime in §B
+// by filling the registry to capacity.
+
+// [GAP] Private constants in safety.zig (MAX_SHELL_ARG_LEN=4096, MAX_PATH_LEN=4096)
+// cannot be proven via comptime cross-check (not pub).  axioms.MAX_SHELL_ARG and
+// axioms.MAX_PATH are [ASSUMED] to match.  Safety tests in §E verify the limit
+// indirectly by constructing inputs of exactly that length.
+
+// ═══════════════════════════════════════════════════════════════════════════
+// §B  Catalogue boundary tests
+// ═══════════════════════════════════════════════════════════════════════════
+//
+// Each test is self-contained: begins with an explicit deinit+init pair and
+// ends with a deferred deinit.  This prevents state leaking between tests
+// regardless of execution order.
+
+// Convenience: register a single cartridge with "ready" status and minimal fields.
+fn registerReady(name: []const u8) c_int {
+    return catalogue.boj_catalogue_register(
+        name.ptr, name.len,
+        "1.0".ptr, 3,
+        axioms.STATUS_READY, // ready
+        axioms.TIER_TERANGA, // teranga
+        axioms.DOMAIN_CLOUD, // cloud
+    );
+}
+
+// Convenience: register a cartridge with a given status integer.
+fn registerStatus(name: []const u8, status: c_int) c_int {
+    return catalogue.boj_catalogue_register(
+        name.ptr, name.len,
+        "1.0".ptr, 3,
+        status,
+        axioms.TIER_TERANGA,
+        axioms.DOMAIN_CLOUD,
+    );
+}
+
+test "B.1: pre-init guard — register fails before init" {
+    // Force uninitialized state.
+    catalogue.boj_catalogue_deinit();
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_ERR), registerReady("alpha"));
+    try std.testing.expectEqual(@as(usize, 0), catalogue.boj_catalogue_count());
+}
+
+test "B.2: init is idempotent — double-init resets and succeeds" {
+    catalogue.boj_catalogue_deinit();
+    defer catalogue.boj_catalogue_deinit();
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_OK), catalogue.boj_catalogue_init());
+    // Register one cartridge, then re-init — count resets to 0.
+    _ = registerReady("ephemeral");
+    try std.testing.expectEqual(@as(usize, 1), catalogue.boj_catalogue_count());
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_OK), catalogue.boj_catalogue_init());
+    try std.testing.expectEqual(@as(usize, 0), catalogue.boj_catalogue_count());
+}
+
+test "B.3: [BOUNDARY] capacity at exactly MAX_CARTRIDGES fills without error" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    // Register exactly MAX_CARTRIDGES entries.  Each name is "c000".."c127".
+    var i: usize = 0;
+    while (i < axioms.MAX_CARTRIDGES) : (i += 1) {
+        var name_buf: [8]u8 = undefined;
+        const n = std.fmt.bufPrint(&name_buf, "c{d:0>3}", .{i}) catch unreachable;
+        try std.testing.expectEqual(
+            @as(c_int, axioms.CAT_OK),
+            registerReady(n),
+        );
+    }
+    try std.testing.expectEqual(@as(usize, axioms.MAX_CARTRIDGES), catalogue.boj_catalogue_count());
+
+    // One more must fail.
+    const rc = registerReady("overflow");
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_ERR), rc);
+    try std.testing.expectEqual(@as(usize, axioms.MAX_CARTRIDGES), catalogue.boj_catalogue_count());
+}
+
+test "B.4: [BOUNDARY] mount gate — only STATUS_READY passes" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    // Register one entry for each status value.
+    const statuses = [_]c_int{
+        axioms.STATUS_DEVELOPMENT,
+        axioms.STATUS_READY,
+        axioms.STATUS_DEPRECATED,
+        axioms.STATUS_FAULTY,
+    };
+    const names = [_][]const u8{ "dev", "rdy", "dep", "flt" };
+    for (statuses, names, 0..) |st, nm, idx| {
+        _ = registerStatus(nm, st);
+        const rc = catalogue.boj_catalogue_mount(idx);
+        if (st == axioms.MOUNT_GATE_STATUS) {
+            try std.testing.expectEqual(@as(c_int, axioms.CAT_OK), rc);
+            try std.testing.expectEqual(@as(c_int, axioms.CAT_MOUNTED),
+                catalogue.boj_catalogue_is_mounted(idx));
+        } else {
+            try std.testing.expectEqual(@as(c_int, axioms.CAT_ERR), rc);
+            try std.testing.expectEqual(@as(c_int, axioms.CAT_UNMOUNTED),
+                catalogue.boj_catalogue_is_mounted(idx));
+        }
+    }
+}
+
+test "B.5: [BOUNDARY] name length at exactly NAME_MAX" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    // Name of exactly 64 bytes must succeed.
+    const name64 = "a" ** axioms.NAME_MAX;
+    try std.testing.expectEqual(
+        @as(c_int, axioms.CAT_OK),
+        catalogue.boj_catalogue_register(name64.ptr, name64.len, "1.0".ptr, 3, axioms.STATUS_READY, 0, 1),
+    );
+    try std.testing.expectEqual(@as(usize, 1), catalogue.boj_catalogue_count());
+}
+
+test "B.6: [BOUNDARY] name length exceeding NAME_MAX fails" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    // Name of 65 bytes must fail.
+    const name65 = "b" ** (axioms.NAME_MAX + 1);
+    try std.testing.expectEqual(
+        @as(c_int, axioms.CAT_ERR),
+        catalogue.boj_catalogue_register(name65.ptr, name65.len, "1.0".ptr, 3, axioms.STATUS_READY, 0, 1),
+    );
+    try std.testing.expectEqual(@as(usize, 0), catalogue.boj_catalogue_count());
+}
+
+test "B.7: [BOUNDARY] version length at exactly VERSION_MAX" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    const ver16 = "v" ** axioms.VERSION_MAX;
+    try std.testing.expectEqual(
+        @as(c_int, axioms.CAT_OK),
+        catalogue.boj_catalogue_register("myc".ptr, 3, ver16.ptr, ver16.len, axioms.STATUS_READY, 0, 1),
+    );
+}
+
+test "B.8: [BOUNDARY] version length exceeding VERSION_MAX fails" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    const ver17 = "v" ** (axioms.VERSION_MAX + 1);
+    try std.testing.expectEqual(
+        @as(c_int, axioms.CAT_ERR),
+        catalogue.boj_catalogue_register("myc".ptr, 3, ver17.ptr, ver17.len, axioms.STATUS_READY, 0, 1),
+    );
+}
+
+test "B.9: [BOUNDARY] protocol range — PROTO_MIN and PROTO_MAX accepted" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    _ = registerReady("proto-cart");
+    // PROTO_MIN (1 = MCP) and PROTO_MAX (9 = REST) must both be accepted.
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_OK),
+        catalogue.boj_catalogue_add_protocol(axioms.PROTO_MIN));
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_OK),
+        catalogue.boj_catalogue_add_protocol(axioms.PROTO_MAX));
+}
+
+test "B.10: [BOUNDARY] protocol values outside [PROTO_MIN, PROTO_MAX] fail" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    _ = registerReady("proto-cart2");
+    // 0 and PROTO_MAX+1 must be rejected.
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_ERR),
+        catalogue.boj_catalogue_add_protocol(axioms.PROTO_MIN - 1));
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_ERR),
+        catalogue.boj_catalogue_add_protocol(axioms.PROTO_MAX + 1));
+}
+
+test "B.11: index boundary — out-of-range access returns CAT_NOT_FOUND" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    _ = registerReady("single");
+    // count == 1; index == 1 is out of range.
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_NOT_FOUND),
+        catalogue.boj_catalogue_mount(1));
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_NOT_FOUND),
+        catalogue.boj_catalogue_unmount(1));
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_IS_MOUNTED_ERR),
+        catalogue.boj_catalogue_is_mounted(1));
+}
+
+test "B.12: [BOUNDARY] order validation at MAX_ORDER_SIZE" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    // Register MAX_ORDER_SIZE ready cartridges.
+    var name_bufs: [axioms.MAX_ORDER_SIZE][8]u8 = undefined;
+    var name_ptrs: [axioms.MAX_ORDER_SIZE][*]const u8 = undefined;
+    var name_lens: [axioms.MAX_ORDER_SIZE]usize = undefined;
+
+    var i: usize = 0;
+    while (i < axioms.MAX_ORDER_SIZE) : (i += 1) {
+        const n = std.fmt.bufPrint(&name_bufs[i], "ord{d:0>2}", .{i}) catch unreachable;
+        _ = registerReady(n);
+        name_ptrs[i] = name_bufs[i][0..n.len].ptr;
+        name_lens[i] = n.len;
+    }
+
+    // All MAX_ORDER_SIZE should be satisfied.
+    try std.testing.expectEqual(
+        @as(usize, axioms.MAX_ORDER_SIZE),
+        catalogue.boj_menu_validate_order(&name_ptrs, &name_lens, axioms.MAX_ORDER_SIZE),
+    );
+
+    // MAX_ORDER_SIZE + 1 returns 0 (clamped; count exceeds limit).
+    try std.testing.expectEqual(
+        @as(usize, 0),
+        catalogue.boj_menu_validate_order(&name_ptrs, &name_lens, axioms.MAX_ORDER_SIZE + 1),
+    );
+}
+
+test "B.13: [BOUNDARY] backend label at exactly BACKEND_MAX" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    _ = registerReady("backend-cart");
+    const lbl32 = "x" ** axioms.BACKEND_MAX;
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_OK),
+        catalogue.boj_catalogue_set_backend(lbl32.ptr, lbl32.len));
+
+    var out: [axioms.BACKEND_MAX]u8 = undefined;
+    const got = catalogue.boj_menu_backend(0, &out, axioms.BACKEND_MAX);
+    try std.testing.expectEqual(@as(usize, axioms.BACKEND_MAX), got);
+    try std.testing.expectEqualSlices(u8, lbl32, out[0..got]);
+}
+
+test "B.14: [BOUNDARY] backend label exceeding BACKEND_MAX fails" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    _ = registerReady("backend-cart2");
+    const lbl33 = "x" ** (axioms.BACKEND_MAX + 1);
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_ERR),
+        catalogue.boj_catalogue_set_backend(lbl33.ptr, lbl33.len));
+}
+
+test "B.15: deinit clears mounted state — post-deinit count is 0" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+
+    _ = registerReady("persistent");
+    _ = catalogue.boj_catalogue_mount(0);
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_MOUNTED),
+        catalogue.boj_catalogue_is_mounted(0));
+
+    catalogue.boj_catalogue_deinit();
+    // After deinit: count is 0, and all ops requiring init will fail.
+    try std.testing.expectEqual(@as(usize, 0), catalogue.boj_catalogue_count());
+    try std.testing.expectEqual(@as(c_int, axioms.CAT_ERR), registerReady("ghost"));
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// §C  Cartridge invoke ABI tests (via cartridge_shim.zig pub functions)
+// ═══════════════════════════════════════════════════════════════════════════
+
+test "C.1: writeResult — body fits, RC_SUCCESS, length updated" {
+    var buf: [64]u8 = undefined;
+    var len: usize = buf.len;
+    const rc = shim.writeResult(&buf, &len, "hello");
+    try std.testing.expectEqual(@as(i32, axioms.RC_SUCCESS), rc);
+    try std.testing.expectEqual(@as(usize, 5), len);
+    try std.testing.expectEqualSlices(u8, "hello", buf[0..len]);
+}
+
+test "C.2: [BOUNDARY] writeResult — exact-fit buffer succeeds" {
+    var buf: [5]u8 = undefined;
+    var len: usize = buf.len;
+    const rc = shim.writeResult(&buf, &len, "hello");
+    try std.testing.expectEqual(@as(i32, axioms.RC_SUCCESS), rc);
+    try std.testing.expectEqual(@as(usize, 5), len);
+}
+
+test "C.3: [BOUNDARY] writeResult — buffer too small, RC_BUFFER_TOO_SMALL, required length set" {
+    var buf: [2]u8 = undefined;
+    var len: usize = buf.len;
+    const rc = shim.writeResult(&buf, &len, "hello");
+    try std.testing.expectEqual(@as(i32, axioms.RC_BUFFER_TOO_SMALL), rc);
+    // *in_out_len must be updated to the required size (body.len = 5).
+    try std.testing.expectEqual(@as(usize, 5), len);
+}
+
+test "C.4: writeResult — empty body writes nothing, RC_SUCCESS" {
+    var buf: [4]u8 = undefined;
+    var len: usize = buf.len;
+    const rc = shim.writeResult(&buf, &len, "");
+    try std.testing.expectEqual(@as(i32, axioms.RC_SUCCESS), rc);
+    try std.testing.expectEqual(@as(usize, 0), len);
+}
+
+test "C.5: [BOUNDARY] writeResult — zero-capacity buffer, non-empty body, RC_BUFFER_TOO_SMALL" {
+    var buf: [1]u8 = undefined;
+    var len: usize = 0; // capacity=0
+    const rc = shim.writeResult(&buf, &len, "x");
+    try std.testing.expectEqual(@as(i32, axioms.RC_BUFFER_TOO_SMALL), rc);
+    try std.testing.expectEqual(@as(usize, 1), len); // required = body.len
+}
+
+test "C.6: toolIs — exact match and non-match" {
+    const name: [*:0]const u8 = "list-databases";
+    try std.testing.expect(shim.toolIs(@ptrCast(name), "list-databases"));
+    try std.testing.expect(!shim.toolIs(@ptrCast(name), "list-database"));
+    try std.testing.expect(!shim.toolIs(@ptrCast(name), "list-databasess"));
+    try std.testing.expect(!shim.toolIs(@ptrCast(name), ""));
+}
+
+test "C.7: invokeArgsNull — each null slot detected independently" {
+    var buf: [4]u8 = undefined;
+    var len: usize = 4;
+    const name: [*:0]const u8 = "x";
+    try std.testing.expect(!shim.invokeArgsNull(@ptrCast(name), &buf, &len));
+    try std.testing.expect(shim.invokeArgsNull(null, &buf, &len));
+    try std.testing.expect(shim.invokeArgsNull(@ptrCast(name), null, &len));
+    try std.testing.expect(shim.invokeArgsNull(@ptrCast(name), &buf, null));
+}
+
+test "C.8: RC_BUFFER_TOO_SMALL hint enables two-phase caller pattern" {
+    // Simulate the ADR-0006 two-phase call:
+    //   Phase 1: call with capacity=0 to discover required size.
+    //   Phase 2: allocate required size, call again — must succeed.
+    var dummy: [0]u8 = .{};
+    var cap: usize = 0;
+    const body = "{\"result\":{\"rows\":42}}";
+
+    const probe = shim.writeResult(&dummy, &cap, body);
+    try std.testing.expectEqual(@as(i32, axioms.RC_BUFFER_TOO_SMALL), probe);
+    try std.testing.expectEqual(@as(usize, body.len), cap); // hint is exact
+
+    var real_buf: [64]u8 = undefined;
+    var real_cap: usize = cap;
+    const fill = shim.writeResult(&real_buf, &real_cap, body);
+    try std.testing.expectEqual(@as(i32, axioms.RC_SUCCESS), fill);
+    try std.testing.expectEqualSlices(u8, body, real_buf[0..real_cap]);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// §D  Hash constant boundary tests
+// ═══════════════════════════════════════════════════════════════════════════
+//
+// loader.zig's pub functions (hashToHex, verifyHash, etc.) are tested by the
+// loader module's own test suite (`zig build loader`).  The module cannot be
+// imported here due to a module-graph conflict (see §A.6 GAP).
+//
+// What we CAN verify here: the axiom constants themselves behave consistently
+// with the hexadecimal encoding specification, without calling any loader code.
+
+test "D.1: axioms.HASH_HEX_LEN is double axioms.HASH_LEN (hex-encoding contract)" {
+    // This test is redundant with ax.3.1 (comptime), but makes the property
+    // explicitly visible in the runtime test report as a named failing test.
+    try std.testing.expectEqual(@as(usize, axioms.HASH_LEN * 2), axioms.HASH_HEX_LEN);
+}
+
+test "D.2: SHA-256 hex string fits in NAME_MAX field (catalogue storage axiom)" {
+    // boj_catalogue_set_hash stores the hex string in [NAME_MAX]u8.
+    // If HASH_HEX_LEN > NAME_MAX, the write would overflow.
+    try std.testing.expect(axioms.HASH_HEX_LEN <= axioms.NAME_MAX);
+}
+
+test "D.3: WASM capacity bounded by catalogue capacity" {
+    try std.testing.expect(axioms.MAX_WASM_CARTRIDGES <= axioms.MAX_CARTRIDGES);
+}
+
+test "D.4: LOADER_MATCH does not alias CAT_OK (convention mismatch trap)" {
+    // boj_loader_verify() returns LOADER_MATCH (1) on success, NOT CAT_OK (0).
+    // A caller checking `rc == 0` would misidentify a hash-mismatch as success.
+    try std.testing.expect(axioms.LOADER_MATCH != axioms.CAT_OK);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// §E  Safety boundary tests (via SafetyError enum and extern declarations)
+// ═══════════════════════════════════════════════════════════════════════════
+//
+// The safety functions are `export fn` (not pub) in safety.zig.  They are
+// declared extern here so the linker resolves them from the linked safety
+// module object code.
+
+extern fn boj_safety_check_shell_arg(ptr: [*]const u8, len: usize) c_int;
+extern fn boj_safety_check_sql_value(ptr: [*]const u8, len: usize) c_int;
+extern fn boj_safety_check_path(ptr: [*]const u8, len: usize) c_int;
+extern fn boj_safety_check_url_scheme(ptr: [*]const u8, len: usize) c_int;
+extern fn boj_safety_check_json_string(ptr: [*]const u8, len: usize) c_int;
+
+test "E.1: shell arg — empty input returns SAFETY_EMPTY" {
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_EMPTY),
+        boj_safety_check_shell_arg("", 0));
+}
+
+test "E.2: [BOUNDARY] shell arg — length exactly MAX_SHELL_ARG passes" {
+    const long: [axioms.MAX_SHELL_ARG]u8 = .{'a'} ** axioms.MAX_SHELL_ARG;
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_shell_arg(&long, long.len));
+}
+
+test "E.3: [BOUNDARY] shell arg — length MAX_SHELL_ARG+1 returns SAFETY_TOO_LONG" {
+    const toolong: [axioms.MAX_SHELL_ARG + 1]u8 = .{'a'} ** (axioms.MAX_SHELL_ARG + 1);
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_TOO_LONG),
+        boj_safety_check_shell_arg(&toolong, toolong.len));
+}
+
+test "E.4: shell arg — allowlist characters all pass" {
+    const allowed = "abcXYZ019-_./:@+=,~";
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_shell_arg(allowed, allowed.len));
+}
+
+test "E.5: shell arg — each shell metacharacter is rejected" {
+    const dangerous = [_][]const u8{ ";", "|", "&", "$", "`", "(", ")", " ", "\"", "'" };
+    for (dangerous) |ch| {
+        const rc = boj_safety_check_shell_arg(ch.ptr, ch.len);
+        try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SHELL_INJECTION), rc);
+    }
+}
+
+test "E.6: [BOUNDARY] shell arg — double-hyphen (option injection) rejected" {
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SHELL_INJECTION),
+        boj_safety_check_shell_arg("--evil", 6));
+    // Single hyphen at start is allowed.
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_shell_arg("-", 1));
+}
+
+test "E.7: SQL value — SQL injection patterns all rejected" {
+    const cases = [_][]const u8{
+        "'; DROP TABLE--",  // comment + terminator + quote
+        "1; DELETE FROM",   // statement terminator
+        "/* comment */",    // block comment
+        "val' OR '1'='1",  // string escape
+        "val\\escaped",    // backslash escape
+    };
+    for (cases) |c| {
+        const rc = boj_safety_check_sql_value(c.ptr, c.len);
+        try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SQL_INJECTION), rc);
+    }
+}
+
+test "E.8: SQL value — safe strings pass, empty passes" {
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_sql_value("hello world", 11));
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_sql_value("", 0));
+}
+
+test "E.9: path — traversal sequences rejected at any position" {
+    const traversals = [_][]const u8{
+        "../etc/passwd",
+        "/safe/../escape",
+        "../../secret",
+    };
+    for (traversals) |t| {
+        try std.testing.expectEqual(@as(c_int, axioms.SAFETY_PATH_TRAVERSAL),
+            boj_safety_check_path(t.ptr, t.len));
+    }
+}
+
+test "E.10: path — safe paths pass" {
+    const safe = [_][]const u8{
+        "/usr/bin/git",
+        "relative/path.txt",
+        "/home/user/file",
+    };
+    for (safe) |s| {
+        try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+            boj_safety_check_path(s.ptr, s.len));
+    }
+}
+
+test "E.11: URL scheme — only http and https pass; dangerous schemes rejected" {
+    // Safe.
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_url_scheme("https://example.com", 19));
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_url_scheme("http://x.com", 12));
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_url_scheme("/relative", 9));
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_url_scheme("", 0));
+
+    // Dangerous.
+    const bad = [_][]const u8{
+        "javascript:alert(1)",
+        "data:text/html,<x>",
+        "file:///etc/passwd",
+        "vbscript:msgbox",
+        "ftp://x.com",
+    };
+    for (bad) |u| {
+        try std.testing.expectEqual(@as(c_int, axioms.SAFETY_INVALID_URL),
+            boj_safety_check_url_scheme(u.ptr, u.len));
+    }
+}
+
+test "E.12: JSON string — control characters, backslash, quote all rejected" {
+    // Control character (NUL).
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_JSON_UNSAFE),
+        boj_safety_check_json_string("\x00", 1));
+    // Backslash.
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_JSON_UNSAFE),
+        boj_safety_check_json_string("a\\b", 3));
+    // Double quote.
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_JSON_UNSAFE),
+        boj_safety_check_json_string("a\"b", 3));
+    // Clean string.
+    try std.testing.expectEqual(@as(c_int, axioms.SAFETY_SAFE),
+        boj_safety_check_json_string("hello world", 11));
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// §F  Thread-safety spot check
+// ═══════════════════════════════════════════════════════════════════════════
+//
+// Zig's Thread.Mutex guarantees mutual exclusion; the formal proof that the
+// mutex is held on EVERY C-ABI entry is provided by the comptime exhaustive
+// audit in seams.zig (Seam 8) and the code review in docs/zig-ffi-verification.adoc.
+// The test below provides operational evidence that concurrent registration
+// does not corrupt the count.
+//
+// [GAP] This test is a safety net, not a full data-race proof.  A formal
+// proof of race-freedom requires a happens-before analysis tool (e.g., tsan
+// or a model checker) which is not yet wired into this project's CI.
+
+const THREAD_COUNT = 8;
+const REGISTRATIONS_PER_THREAD = 4; // 8 * 4 = 32, well within MAX_CARTRIDGES
+
+fn threadRegister(id: usize) void {
+    var i: usize = 0;
+    while (i < REGISTRATIONS_PER_THREAD) : (i += 1) {
+        var buf: [16]u8 = undefined;
+        const n = std.fmt.bufPrint(&buf, "t{d}c{d}", .{ id, i }) catch return;
+        _ = catalogue.boj_catalogue_register(
+            n.ptr, n.len,
+            "1.0".ptr, 3,
+            axioms.STATUS_READY, axioms.TIER_TERANGA, axioms.DOMAIN_CLOUD,
+        );
+    }
+}
+
+test "F.1: concurrent registration is race-free (mutex spot check)" {
+    catalogue.boj_catalogue_deinit();
+    _ = catalogue.boj_catalogue_init();
+    defer catalogue.boj_catalogue_deinit();
+
+    var threads: [THREAD_COUNT]std.Thread = undefined;
+    for (&threads, 0..) |*t, i| {
+        t.* = try std.Thread.spawn(.{}, threadRegister, .{i});
+    }
+    for (&threads) |*t| t.join();
+
+    const expected = THREAD_COUNT * REGISTRATIONS_PER_THREAD;
+    try std.testing.expectEqual(@as(usize, expected), catalogue.boj_catalogue_count());
+}
diff --git a/ffi/zig/src/catalogue.zig b/ffi/zig/src/catalogue.zig
index e663ac9c..99c268cb 100644
--- a/ffi/zig/src/catalogue.zig
+++ b/ffi/zig/src/catalogue.zig
@@ -12,6 +12,16 @@
 
 const std = @import("std");
 
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
+
 // ═══════════════════════════════════════════════════════════════════════
 // Types (must match src/abi/Catalogue.idr encodings)
 // ═══════════════════════════════════════════════════════════════════════
@@ -106,7 +116,7 @@ var initialised: bool = false;
 
 /// Thread-safety mutex — protects all global state in this module.
 /// Every C-ABI export acquires this before touching globals.
-var mutex: std.Thread.Mutex = .{};
+var mutex: Mutex = .{};
 
 // ═══════════════════════════════════════════════════════════════════════
 // Lifecycle
diff --git a/ffi/zig/src/community.zig b/ffi/zig/src/community.zig
index 55a78867..70904be9 100644
--- a/ffi/zig/src/community.zig
+++ b/ffi/zig/src/community.zig
@@ -15,6 +15,16 @@
 
 const std = @import("std");
 
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
+
 // ═══════════════════════════════════════════════════════════════════════
 // Constants
 // ═══════════════════════════════════════════════════════════════════════
@@ -61,7 +71,7 @@ const Submission = struct {
 var submissions: [MAX_SUBMISSIONS]Submission = [_]Submission{.{}} ** MAX_SUBMISSIONS;
 var submission_count: usize = 0;
 var initialised: bool = false;
-var mutex: std.Thread.Mutex = .{};
+var mutex: Mutex = .{};
 
 // ═══════════════════════════════════════════════════════════════════════
 // Internal API
diff --git a/ffi/zig/src/coprocessor.zig b/ffi/zig/src/coprocessor.zig
index 16e72a0f..38ab9156 100644
--- a/ffi/zig/src/coprocessor.zig
+++ b/ffi/zig/src/coprocessor.zig
@@ -20,6 +20,16 @@
 
 const std = @import("std");
 
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
+
 extern fn getenv(name: [*:0]const u8) ?[*:0]const u8;
 
 // ═══════════════════════════════════════════════════════════════════════
@@ -99,7 +109,7 @@ var affinities: [MAX_CARTRIDGES]CartridgeAffinity = [_]CartridgeAffinity{.{}} **
 var affinity_count: usize = 0;
 
 var initialised: bool = false;
-var mutex: std.Thread.Mutex = .{};
+var mutex: Mutex = .{};
 
 // ═══════════════════════════════════════════════════════════════════════
 // Detection
diff --git a/ffi/zig/src/federation.zig b/ffi/zig/src/federation.zig
index 9e2e2502..01b607cf 100644
--- a/ffi/zig/src/federation.zig
+++ b/ffi/zig/src/federation.zig
@@ -20,6 +20,16 @@
 
 const std = @import("std");
 
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
+
 // ═══════════════════════════════════════════════════════════════════════
 // Proven-hardened: Circuit breaker, retry, and rate limiter state
 //
@@ -385,7 +395,7 @@ var inbound_rate_limiter: InboundRateLimiter = InboundRateLimiter{};
 /// Protects all module-level global state (including QUIC globals declared
 /// below near the QUIC transport section: transport_mode, quic_sessions,
 /// quic_local_secret, quic_local_public, quic_keypair_valid).
-var mutex: std.Thread.Mutex = .{};
+var mutex: Mutex = .{};
 
 // ═══════════════════════════════════════════════════════════════════════
 // Internal helpers
diff --git a/ffi/zig/src/guardian.zig b/ffi/zig/src/guardian.zig
index b5f65ba8..8370c029 100644
--- a/ffi/zig/src/guardian.zig
+++ b/ffi/zig/src/guardian.zig
@@ -22,6 +22,16 @@
 
 const std = @import("std");
 
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
+
 // ═══════════════════════════════════════════════════════════════════════
 // Constants
 // ═══════════════════════════════════════════════════════════════════════
@@ -182,7 +192,7 @@ var log_count: usize = 0;
 var health_interval: i64 = DEFAULT_HEALTH_INTERVAL;
 
 /// Thread-safety mutex for all C-ABI export functions.
-var mutex: std.Thread.Mutex = .{};
+var mutex: Mutex = .{};
 
 // ═══════════════════════════════════════════════════════════════════════
 // Internal Helpers
diff --git a/ffi/zig/src/loader.zig b/ffi/zig/src/loader.zig
index 96fdc1a6..40bd6d58 100644
--- a/ffi/zig/src/loader.zig
+++ b/ffi/zig/src/loader.zig
@@ -12,6 +12,16 @@
 // Phase 2 implementation.
 
 const std = @import("std");
+
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
 const crypto = std.crypto;
 const fs = std.fs;
 
@@ -261,7 +271,7 @@ var wasm_count: usize = 0;
 /// INVARIANT: Every C-ABI export function (boj_loader_*, boj_wasm_*) acquires
 /// this mutex at entry. Internal pure functions (hashFile, hashToHex, verifyHash,
 /// validateWasmModule) do NOT acquire it — callers are responsible.
-var mutex: std.Thread.Mutex = .{};
+var mutex: Mutex = .{};
 
 /// Validate that a file is a valid WASM module.
 /// Checks magic bytes and version header.
diff --git a/ffi/zig/src/sdp.zig b/ffi/zig/src/sdp.zig
index ef65f1ad..f3fe51a0 100644
--- a/ffi/zig/src/sdp.zig
+++ b/ffi/zig/src/sdp.zig
@@ -16,6 +16,16 @@
 
 const std = @import("std");
 
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
+
 // ═══════════════════════════════════════════════════════════════════════
 // Constants
 // ═══════════════════════════════════════════════════════════════════════
@@ -65,7 +75,7 @@ var banned: [MAX_BANNED]BannedPeer = [_]BannedPeer{.{}} ** MAX_BANNED;
 var ban_count: usize = 0;
 var sdp_enabled: bool = false;
 var open_mode: bool = true; // when true, unauthenticated peers are allowed (seed bootstrapping)
-var mutex: std.Thread.Mutex = .{};
+var mutex: Mutex = .{};
 
 // ═══════════════════════════════════════════════════════════════════════
 // Internal API
diff --git a/ffi/zig/src/sla.zig b/ffi/zig/src/sla.zig
index f2800e98..50fe5342 100644
--- a/ffi/zig/src/sla.zig
+++ b/ffi/zig/src/sla.zig
@@ -15,6 +15,16 @@
 
 const std = @import("std");
 
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
+
 // ═══════════════════════════════════════════════════════════════════════
 // Constants
 // ═══════════════════════════════════════════════════════════════════════
@@ -76,7 +86,7 @@ var cartridge_slas: [MAX_CARTRIDGES]CartridgeSla = [_]CartridgeSla{.{}} ** MAX_C
 var sla_count: usize = 0;
 var system_sla: SystemSla = .{};
 var initialised: bool = false;
-var mutex: std.Thread.Mutex = .{};
+var mutex: Mutex = .{};
 
 // ═══════════════════════════════════════════════════════════════════════
 // Internal API
diff --git a/ffi/zig/src/verisimdb.zig b/ffi/zig/src/verisimdb.zig
index 7f31f7a5..8f857665 100644
--- a/ffi/zig/src/verisimdb.zig
+++ b/ffi/zig/src/verisimdb.zig
@@ -15,6 +15,16 @@
 // available, without changing the cartridge code.
 
 const std = @import("std");
+
+const Mutex = struct {
+    state: std.atomic.Mutex = .unlocked,
+    pub fn lock(m: *Mutex) void {
+        while (!m.state.tryLock()) std.atomic.spinLoopHint();
+    }
+    pub fn unlock(m: *Mutex) void {
+        m.state.unlock();
+    }
+};
 const Allocator = std.mem.Allocator;
 
 // ═══════════════════════════════════════════════════════════════════════
@@ -88,7 +98,7 @@ var reads: usize = 0;
 var writes: usize = 0;
 /// Count of failed HTTP requests in persistent mode (best-effort metric).
 var http_errors: usize = 0;
-var mutex: std.Thread.Mutex = .{};
+var mutex: Mutex = .{};
 
 // ═══════════════════════════════════════════════════════════════════════
 // Internal helpers