diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml
index b203334..a81237c 100644
--- a/.github/workflows/boj-build.yml
+++ b/.github/workflows/boj-build.yml
@@ -16,7 +16,11 @@ jobs:
   trigger-boj:
     runs-on: ubuntu-latest
     timeout-minutes: 15
-    if: ${{ vars.BOJ_SERVER_URL != '' || secrets.BOJ_SERVER_URL != '' }}
+    # No job-level `if:` gate here. The `secrets` context is not available in
+    # job-level conditions (only `github`, `inputs`, `needs`, `vars`), and a
+    # `vars`-only test would silently skip the secret-configured case. The step
+    # below reads both and exits 0 when neither is set, which is the documented
+    # no-op behaviour.
     steps:
       - name: Checkout
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
index 00790de..071270e 100644
--- a/.github/workflows/dogfood-gate.yml
+++ b/.github/workflows/dogfood-gate.yml
@@ -261,31 +261,40 @@ jobs:
 
           echo "has_manifest=true" >> "$GITHUB_OUTPUT"
 
-          # Validate TOML structure using Python 3.11+ tomllib
-          python3 -c "
-import tomllib, sys
-with open('eclexiaiser.toml', 'rb') as f:
-    data = tomllib.load(f)
-project = data.get('project', {})
-if not project.get('name', '').strip():
-    print('ERROR: project.name is required', file=sys.stderr)
-    sys.exit(1)
-functions = data.get('functions', [])
-if not functions:
-    print('ERROR: at least one [[functions]] entry is required', file=sys.stderr)
-    sys.exit(1)
-for fn in functions:
-    if not fn.get('name', '').strip():
-        print('ERROR: function name cannot be empty', file=sys.stderr)
-        sys.exit(1)
-    if not fn.get('source', '').strip():
-        print(f'ERROR: function {fn[\"name\"]} has no source path', file=sys.stderr)
-        sys.exit(1)
-print(f'Valid: {project[\"name\"]} ({len(functions)} function(s))')
-" || {
-            echo "::error file=eclexiaiser.toml::Invalid eclexiaiser.toml — see step output for details"
+          # Validate TOML structure using Python 3.11+ tomllib.
+          # Quoted heredoc: no shell expansion, so no backslash escaping is
+          # needed. Body is indented to the block scalar's level and is
+          # dedented back to column 0 by YAML before bash sees it.
+          if ! python3 <<'PY'
+          import tomllib, sys
+
+          with open('eclexiaiser.toml', 'rb') as f:
+              data = tomllib.load(f)
+
+          project = data.get('project', {})
+          if not project.get('name', '').strip():
+              print('ERROR: project.name is required', file=sys.stderr)
+              sys.exit(1)
+
+          functions = data.get('functions', [])
+          if not functions:
+              print('ERROR: at least one [[functions]] entry is required', file=sys.stderr)
+              sys.exit(1)
+
+          for fn in functions:
+              if not fn.get('name', '').strip():
+                  print('ERROR: function name cannot be empty', file=sys.stderr)
+                  sys.exit(1)
+              if not fn.get('source', '').strip():
+                  print(f"ERROR: function {fn['name']} has no source path", file=sys.stderr)
+                  sys.exit(1)
+
+          print(f"Valid: {project['name']} ({len(functions)} function(s))")
+          PY
+          then
+            echo "::error file=eclexiaiser.toml::Invalid eclexiaiser.toml - see step output for details"
             exit 1
-          }
+          fi
 
       - name: Write summary
         run: |
diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml
index fdb9ca1..58ca643 100644
--- a/.github/workflows/e2e.yml
+++ b/.github/workflows/e2e.yml
@@ -1,186 +1,87 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# RSR Standard E2E + Aspect + Benchmark Workflow Template
+# KRL — E2E, Aspect and Benchmark gates.
 #
-# Covers ALL merge requirement test categories:
-#   - E2E (end-to-end pipeline tests)
-#   - Aspect (cross-cutting concern validation)
-#   - Benchmarks (performance regression detection)
-#   - Readiness (Component Readiness Grade: D/C/B)
-#
-# INSTRUCTIONS: Uncomment and customise the section matching your stack.
-# Delete sections that don't apply. See examples in each job.
-
+# These run the checked-in scripts under tests/ and benches/. Each script is
+# expected to exit non-zero on failure; none of them are permitted to report
+# success without having executed at least one assertion.
 name: E2E + Aspect + Bench
 on:
   push:
     branches: [main, master, develop]
     paths:
       - 'src/**'
-      - 'ffi/**'
       - 'tests/**'
+      - 'benches/**'
+      - 'spec/**'
+      - 'examples/**'
       - '.github/workflows/e2e.yml'
   pull_request:
     branches: [main, master]
     paths:
       - 'src/**'
-      - 'ffi/**'
       - 'tests/**'
+      - 'benches/**'
+      - 'spec/**'
+      - 'examples/**'
+      - '.github/workflows/e2e.yml'
   workflow_dispatch:
 permissions: read-all
 concurrency:
   group: e2e-${{ github.ref }}
   cancel-in-progress: true
-jobs:
-# ─── End-to-End Tests ──────────────────────────────────────────────
-# Uncomment ONE of the following e2e job blocks matching your stack.
-
-## === RUST E2E ===
-# e2e:
-#   name: E2E — Full Pipeline
-#   runs-on: ubuntu-latest
-#   timeout-minutes: 15
-#   steps:
-#     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-#     - uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7  # stable
-#     - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5  # v2
-#     - run: cargo build --release
-#     - run: bash tests/e2e.sh
-#       # OR: cargo test --test end_to_end -- --nocapture
-
-  ## === ZIG FFI E2E ===
-  # e2e:
-  #   name: E2E — FFI Pipeline
-  #   runs-on: ubuntu-latest
-  #   timeout-minutes: 15
-  #   steps:
-  #     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-  #     - uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406  # v2.2.1
-  #       with:
-  #         version: 0.15.0
-  #     - run: cd ffi/zig && zig build test
-  #     - run: bash tests/e2e.sh
-
-  ## === ELIXIR E2E ===
-  # e2e:
-  #   name: E2E — Full Pipeline
-  #   runs-on: ubuntu-latest
-  #   timeout-minutes: 15
-  #   steps:
-  #     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-  #     - uses: erlef/setup-beam@fc68ffb90438ef2936bbb3251622353b3dcb2f93  # v1.24.0
-  #       with:
-  #         otp-version: '27.0'
-  #         elixir-version: '1.17'
-  #     - run: mix deps.get && mix compile --warnings-as-errors
-  #     - run: mix test test/integration/e2e_test.exs --trace
 
-  ## === DENO/RESCRIPT E2E ===
-  # e2e:
-  #   name: E2E — Full Pipeline
-  #   runs-on: ubuntu-latest
-  #   timeout-minutes: 15
-  #   steps:
-  #     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-  #     - uses: denoland/setup-deno@667a34cdef165d8d2b2e98dde39547c9daac7282  # v2.0.4
-  #       with:
-  #         deno-version: v2.x
-  #     - run: deno install --node-modules-dir=auto
-  #     - run: deno task res:build  # ReScript compile
-  #     - run: deno test tests/e2e/
+env:
+  ZIG_VERSION: 0.16.0
 
-  ## === PLAYWRIGHT (Browser E2E) ===
-  # e2e-playwright:
-  #   name: Playwright — ${{ matrix.project }}
-  #   runs-on: ubuntu-latest
-  #   timeout-minutes: 20
-  #   strategy:
-  #     fail-fast: false
-  #     matrix:
-  #       project: [chromium-1080p, firefox-1080p, webkit-1080p]
-  #   steps:
-  #     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-  #     - uses: denoland/setup-deno@667a34cdef165d8d2b2e98dde39547c9daac7282  # v2.0.4
-  #       with:
-  #         deno-version: v2.x
-  #     - run: deno install --node-modules-dir=auto
-  #     - run: npx playwright install --with-deps
-  #     - run: npx playwright test --project=${{ matrix.project }}
-  #     - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02  # v4
-  #       if: failure()
-  #       with:
-  #         name: playwright-traces-${{ matrix.project }}
-  #         path: test-results/**/trace.zip
-  #         retention-days: 7
-
-  ## === HASKELL E2E ===
-  # e2e:
-  #   name: E2E — Full Pipeline
-  #   runs-on: ubuntu-latest
-  #   timeout-minutes: 15
-  #   steps:
-  #     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-  #     - uses: haskell-actions/setup@cd0d9bdd65b20557f41bea4dbe43d0b5fbbfe553  # v2.11.0
-  #       with:
-  #         ghc-version: '9.6'
-  #         cabal-version: '3.10'
-  #     - run: cabal build all
-  #     - run: bash tests/integration-test.sh
-
-# ─── Aspect Tests ──────────────────────────────────────────────────
-# Cross-cutting concerns: thread safety, ABI contracts, SPDX, dangerous patterns
-# Uncomment and customise:
-
-# aspect-tests:
-#   name: Aspect — Architectural Invariants
-#   runs-on: ubuntu-latest
-#   timeout-minutes: 10
-#   steps:
-#     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-#     - run: bash tests/aspect_tests.sh
-
-# ─── Benchmarks ────────────────────────────────────────────────────
-# Performance regression detection. Uncomment matching stack:
-
-## === RUST BENCH ===
-# benchmarks:
-#   name: Bench — Performance Regression
-#   runs-on: ubuntu-latest
-#   timeout-minutes: 15
-#   steps:
-#     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-#     - uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7  # stable
-#     - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5  # v2
-#     - run: cargo bench 2>&1 | tee /tmp/bench-results.txt
-#     - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02  # v4
-#       if: always()
-#       with:
-#         name: benchmark-results
-#         path: /tmp/bench-results.txt
-#         retention-days: 30
+jobs:
+  e2e:
+    name: E2E — FFI build, ABI correspondence, grammar smoke
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - name: Set up Zig
+        uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1
+        with:
+          version: ${{ env.ZIG_VERSION }}
+      - name: Run E2E suite
+        run: bash tests/e2e.sh
 
-  ## === ZIG BENCH ===
-  # benchmarks:
-  #   name: Bench — Performance Regression
-  #   runs-on: ubuntu-latest
-  #   timeout-minutes: 15
-  #   steps:
-  #     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-  #     - uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406  # v2.2.1
-  #       with:
-  #         version: 0.15.0
-  #     - run: cd ffi/zig && zig build bench
+  aspect:
+    name: Aspect — architectural invariants
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - name: Run aspect tests
+        run: bash tests/aspect_tests.sh
 
-# ─── Readiness (CRG) ──────────────────────────────────────────────
-# Component Readiness Grade: D (runs) → C (correct) → B (edge cases)
+  smoke:
+    name: Smoke — KRL grammar and examples
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - name: Run grammar smoke suite
+        run: bash tests/smoke/grammar_smoke.sh
 
-# readiness:
-#   name: Readiness — Grade D/C/B
-#   runs-on: ubuntu-latest
-#   timeout-minutes: 10
-#   steps:
-#     - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5  # v4
-#     - uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7  # stable
-#     - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5  # v2
-#     - run: cargo test --test readiness -- --nocapture
+  ffi-unit:
+    name: FFI — Zig unit tests
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - name: Set up Zig
+        uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1
+        with:
+          version: ${{ env.ZIG_VERSION }}
+      - name: zig build test
+        run: cd src/interface/ffi && zig build test
+      - name: zig build
+        run: cd src/interface/ffi && zig build
diff --git a/.gitignore b/.gitignore
index 1244f65..50dac54 100644
--- a/.gitignore
+++ b/.gitignore
@@ -104,6 +104,7 @@ sync_report*.txt
 # Hypatia scan cache (local-only)
 .hypatia/
 .zig-cache/
+zig-out/
 target/
 node_modules/
 _build/
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
index d04e23e..fc32f5b 100644
--- a/.pre-commit-config.yaml
+++ b/.pre-commit-config.yaml
@@ -9,8 +9,14 @@ repos:
   - repo: https://github.com/pre-commit/pre-commit-hooks
     rev: v5.0.0
     hooks:
+      # LICENSES/ holds verbatim licence texts that must match the canonical
+      # SPDX wording byte for byte (CC-BY-SA-4.0 and MPL-2.0 both contain
+      # significant trailing whitespace). Reformatting them silently
+      # invalidates REUSE conformance, so they are excluded here.
       - id: trailing-whitespace
+        exclude: '^LICENSES/'
       - id: end-of-file-fixer
+        exclude: '^LICENSES/'
       - id: check-yaml
       - id: check-json
       - id: check-toml
@@ -47,5 +53,7 @@ repos:
         exclude: '(\.git|node_modules|target|_build|deps|\.deno|external_corpora|\.lake)/'
 
   # --- Secret detection ---
+  - repo: https://github.com/gitleaks/gitleaks
     rev: v8.24.3
     hooks:
+      - id: gitleaks
diff --git a/.tool-versions b/.tool-versions
index ce60c32..4a13be7 100644
--- a/.tool-versions
+++ b/.tool-versions
@@ -1,10 +1,10 @@
-# Uncomment and customize for your project
-# rust nightly
-# just 1.40.0
-# nickel 1.10.0
-# gleam 1.8.0
-# elixir 1.18.0
-# erlang 27.2
-# zig 0.14.0
-# idris2 0.7.0
+# Toolchains this repository actually uses.
+#   zig     — the C-ABI FFI shim under src/interface/ffi (verified against 0.16.0)
+#   idris2  — the ABI declarations under src/interface/Abi
+#
+# NOTE: `rust nightly` is retained only because .github/workflows/rust-ci.yml
+# still calls the shared Rust reusable. There is no Cargo.toml in this repo,
+# so that workflow currently gates nothing — see issue #38.
+zig 0.16.0
+idris2 0.7.0
 rust nightly
diff --git a/LICENSES/MPL-2.0.txt b/LICENSES/MPL-2.0.txt
index 14e2f77..ee6256c 100644
--- a/LICENSES/MPL-2.0.txt
+++ b/LICENSES/MPL-2.0.txt
@@ -357,7 +357,7 @@ Exhibit A - Source Code Form License Notice
 
   This Source Code Form is subject to the terms of the Mozilla Public
   License, v. 2.0. If a copy of the MPL was not distributed with this
-  file, You can obtain one at http://mozilla.org/MPL/2.0/.
+  file, You can obtain one at https://mozilla.org/MPL/2.0/.
 
 If it is not possible or desirable to put the notice in a particular
 file, then You may include the notice in a location (such as a LICENSE
diff --git a/src/interface/ffi/build.zig b/src/interface/ffi/build.zig
index 2607c11..cdb31a4 100644
--- a/src/interface/ffi/build.zig
+++ b/src/interface/ffi/build.zig
@@ -1,19 +1,35 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 //
-// Template FFI Build Configuration (Zig 0.15.2+)
-// Note: This is a minimal build file that demonstrates Zig integration
+// KRL FFI build configuration.
+//
+// Exposes two steps:
+//   zig build        — build the static library consumed over the C ABI
+//   zig build test   — run the FFI unit tests in src/main.zig
 
 const std = @import("std");
 
 pub fn build(b: *std.Build) void {
-    _ = b.standardTargetOptions(.{});
-    _ = b.standardOptimizeOption(.{});
+    const target = b.standardTargetOptions(.{});
+    const optimize = b.standardOptimizeOption(.{});
+
+    const ffi_mod = b.createModule(.{
+        .root_source_file = b.path("src/main.zig"),
+        .target = target,
+        .optimize = optimize,
+        .link_libc = true,
+    });
+
+    const lib = b.addLibrary(.{
+        .name = "krl",
+        .linkage = .static,
+        .root_module = ffi_mod,
+    });
+    b.installArtifact(lib);
+
+    const ffi_tests = b.addTest(.{ .root_module = ffi_mod });
+    const run_ffi_tests = b.addRunArtifact(ffi_tests);
 
-    // In Zig 0.15+, tests are run directly with:
-    //   zig build-exe -ftest-runner src/main.zig
-    //   zig build-exe -ftest-runner test/integration_test.zig
-    //
-    // This minimal build file provides scaffolding for future expansion.
-    // Tests can be invoked via command line without explicit build.zig configuration.
+    const test_step = b.step("test", "Run FFI unit tests");
+    test_step.dependOn(&run_ffi_tests.step);
 }
diff --git a/src/interface/ffi/src/main.zig b/src/interface/ffi/src/main.zig
index eaa6ea4..02909d4 100644
--- a/src/interface/ffi/src/main.zig
+++ b/src/interface/ffi/src/main.zig
@@ -38,12 +38,14 @@ pub const Result = enum(c_int) {
     null_pointer = 4,
 };
 
-/// Library handle (opaque to prevent direct access)
-pub const Handle = opaque {
+/// Library handle. A regular struct used as the backing type; C consumers only
+/// ever hold a `*Handle` and never see the layout, so it is effectively opaque
+/// across the ABI. (Zig `opaque {}` types cannot carry fields, which the
+/// internal state below requires.)
+pub const Handle = struct {
     // Internal state hidden from C
     allocator: std.mem.Allocator,
     initialized: bool,
-    // Add your fields here
 };
 
 //==============================================================================
@@ -210,7 +212,7 @@ export fn krl_build_info() [*:0]const u8 {
 //==============================================================================
 
 /// Callback function type (C ABI)
-pub const Callback = *const fn (u64, u32) callconv(.C) u32;
+pub const Callback = *const fn (u64, u32) callconv(.c) u32;
 
 /// Register a callback
 export fn krl_register_callback(
diff --git a/tests/aspect_tests.sh b/tests/aspect_tests.sh
index 3cd1eb5..82db15a 100755
--- a/tests/aspect_tests.sh
+++ b/tests/aspect_tests.sh
@@ -54,7 +54,8 @@ while IFS= read -r -d '' f; do
         warn "Missing SPDX header: $f"
         MISSING_SPDX=$((MISSING_SPDX + 1))
     fi
-done < <(find src/ -type f \( -name "*.rs" -o -name "*.zig" -o -name "*.res" -o -name "*.ex" -o -name "*.exs" -o -name "*.gleam" -o -name "*.idr" -o -name "*.sh" \) -print0 2>/dev/null)
+done < <(find src/ \( -name ".zig-cache" -o -name "zig-out" -o -name "build" \) -prune -o \
+    -type f \( -name "*.rs" -o -name "*.zig" -o -name "*.res" -o -name "*.ex" -o -name "*.exs" -o -name "*.gleam" -o -name "*.idr" -o -name "*.sh" \) -print0 2>/dev/null)
 
 if [ "$MISSING_SPDX" -eq 0 ]; then
     pass "All source files have SPDX headers"
@@ -67,42 +68,67 @@ fi
 # ═══════════════════════════════════════════════════════════════════════
 bold "Aspect 2: Dangerous patterns"
 
-# Idris2 dangerous patterns
-DANGEROUS_IDRIS=$(grep -rn 'believe_me\|assert_total\|really_believe_me' src/abi/ 2>/dev/null | grep -v "^Binary" | grep -v "test" || true)
-if [ -n "$DANGEROUS_IDRIS" ]; then
-    fail "Dangerous Idris2 patterns found:"
-    echo "$DANGEROUS_IDRIS" | head -5
-else
-    pass "No dangerous Idris2 patterns (believe_me, assert_total)"
-fi
+# Source files only. Prose files (.adoc/.md) legitimately *name* the banned
+# constructs in order to ban them; scanning them yields false positives.
+SOURCE_FILES=()
+while IFS= read -r -d '' f; do
+    SOURCE_FILES+=("$f")
+done < <(find src/ verification/ \( -name ".zig-cache" -o -name "zig-out" -o -name "build" \) -prune -o \
+    -type f \( -name "*.idr" -o -name "*.zig" -o -name "*.lean" -o -name "*.v" \
+       -o -name "*.hs" -o -name "*.rs" -o -name "*.ml" \) -print0 2>/dev/null)
 
-# Coq/Lean dangerous patterns
-DANGEROUS_PROOF=$(grep -rn '\bAdmitted\b\|\bsorry\b\|\bunsafeCoerce\b\|\bObj\.magic\b' src/ verification/ 2>/dev/null | grep -v "test" | grep -v "comment" || true)
-if [ -n "$DANGEROUS_PROOF" ]; then
-    fail "Dangerous proof patterns found:"
-    echo "$DANGEROUS_PROOF" | head -5
+# Comment lines legitimately *name* the banned constructs in order to ban them.
+# Strip `file:line:` then any leading comment marker before judging a hit.
+strip_comments() { grep -vE ':[0-9]+:[[:space:]]*(--|//|#|\(\*|\*)' || true; }
+
+if [ "${#SOURCE_FILES[@]}" -eq 0 ]; then
+    fail "No source files found under src/ or verification/ — aspect scan would be vacuous"
 else
-    pass "No dangerous proof patterns (Admitted, sorry, unsafeCoerce)"
+    # Idris2 dangerous patterns
+    DANGEROUS_IDRIS=$({ grep -n 'believe_me\|assert_total\|really_believe_me' "${SOURCE_FILES[@]}" 2>/dev/null || true; } | strip_comments)
+    if [ -n "$DANGEROUS_IDRIS" ]; then
+        fail "Dangerous Idris2 patterns found:"
+        echo "$DANGEROUS_IDRIS" | head -5
+    else
+        pass "No dangerous Idris2 patterns (believe_me, assert_total) in ${#SOURCE_FILES[@]} source files"
+    fi
+
+    # Coq/Lean/Haskell dangerous patterns
+    DANGEROUS_PROOF=$({ grep -n '\bAdmitted\b\|\bsorry\b\|\bunsafeCoerce\b\|\bObj\.magic\b' "${SOURCE_FILES[@]}" 2>/dev/null || true; } | strip_comments)
+    if [ -n "$DANGEROUS_PROOF" ]; then
+        fail "Dangerous proof patterns found:"
+        echo "$DANGEROUS_PROOF" | head -5
+    else
+        pass "No dangerous proof patterns (Admitted, sorry, unsafeCoerce) in ${#SOURCE_FILES[@]} source files"
+    fi
 fi
 
 # ═══════════════════════════════════════════════════════════════════════
 # Aspect 3: ABI/FFI Contract (if applicable)
 # ═══════════════════════════════════════════════════════════════════════
-# Uncomment if your project has Idris2 ABI + Zig FFI:
-
-# bold "Aspect 3: ABI/FFI contract"
-# if [ -d "src/abi" ] && [ -d "ffi/zig" ]; then
-#     # Check that every exported function in Idris2 ABI has a Zig FFI implementation
-#     ABI_EXPORTS=$(grep -h 'export' src/abi/*.idr 2>/dev/null | wc -l)
-#     FFI_EXPORTS=$(grep -h 'pub export fn' ffi/zig/src/*.zig 2>/dev/null | wc -l)
-#     if [ "$ABI_EXPORTS" -gt 0 ] && [ "$FFI_EXPORTS" -gt 0 ]; then
-#         pass "ABI ($ABI_EXPORTS exports) and FFI ($FFI_EXPORTS exports) both present"
-#     else
-#         fail "ABI/FFI mismatch: $ABI_EXPORTS ABI exports, $FFI_EXPORTS FFI exports"
-#     fi
-# else
-#     pass "ABI/FFI not applicable (no src/abi or ffi/zig)"
-# fi
+bold "Aspect 3: ABI/FFI contract"
+
+ABI_DIR="src/interface/Abi"
+FFI_DIR="src/interface/ffi"
+
+if [ -d "$ABI_DIR" ] && [ -d "$FFI_DIR" ]; then
+    # Idris2 declares the ABI surface; Zig implements it over the C ABI.
+    # Zig uses bare `export fn` (not `pub export fn`) for C-ABI exports.
+    ABI_FOREIGN=$(grep -h '%foreign' "$ABI_DIR"/*.idr 2>/dev/null | wc -l)
+    FFI_EXPORTS=$(grep -h '^export fn' "$FFI_DIR"/src/*.zig 2>/dev/null | wc -l)
+
+    if [ "${ABI_FOREIGN:-0}" -eq 0 ]; then
+        fail "No %foreign declarations found in $ABI_DIR — ABI surface is empty"
+    elif [ "$FFI_EXPORTS" -eq 0 ]; then
+        fail "No 'export fn' found in $FFI_DIR/src — FFI implementation is empty"
+    elif [ "$FFI_EXPORTS" -lt "$ABI_FOREIGN" ]; then
+        fail "ABI/FFI mismatch: $ABI_FOREIGN %foreign declarations but only $FFI_EXPORTS Zig exports"
+    else
+        pass "ABI ($ABI_FOREIGN %foreign decls) covered by FFI ($FFI_EXPORTS exports)"
+    fi
+else
+    fail "Expected ABI at $ABI_DIR and FFI at $FFI_DIR — one or both missing"
+fi
 
 # ═══════════════════════════════════════════════════════════════════════
 # Aspect 4: Error Handling (no raw panic in production code)
diff --git a/tests/e2e.sh b/tests/e2e.sh
index 4d6777c..7e7b2e9 100755
--- a/tests/e2e.sh
+++ b/tests/e2e.sh
@@ -69,62 +69,66 @@ echo ""
 # ─── Preflight ───────────────────────────────────────────────────────
 bold "Preflight checks"
 
-# TODO: Check that your binary/server is built
-# Example:
-# BINARY="$PROJECT_DIR/target/release/my-tool"
-# if [ ! -f "$BINARY" ]; then
-#     red "Binary not found at $BINARY — run 'just build' first"
-#     exit 1
-# fi
-# green "  Binary found: $BINARY"
-
-# TODO: Check dependencies
-# command -v curl >/dev/null 2>&1 || { red "curl not found"; exit 1; }
-# command -v jq >/dev/null 2>&1   || { red "jq not found"; exit 1; }
+FFI_DIR="$PROJECT_DIR/src/interface/ffi"
+ABI_DIR="$PROJECT_DIR/src/interface/Abi"
+
+command -v zig >/dev/null 2>&1 || { red "zig not found — required to build the KRL FFI"; exit 1; }
+green "  zig found: $(zig version)"
+
+[ -f "$FFI_DIR/build.zig" ] || { red "missing $FFI_DIR/build.zig"; exit 1; }
+green "  FFI build definition present"
 
 echo ""
 
-# ═══════════════════════════════════════════════════════════════════════
-# TODO: Add your E2E test sections below. Examples:
-# ═══════════════════════════════════════════════════════════════════════
+# ─── Section 1: FFI builds and its unit tests pass ───────────────────
+bold "Section 1: Zig FFI pipeline"
+
+if (cd "$FFI_DIR" && zig build test) >/dev/null 2>&1; then
+    green "  PASS: zig build test"
+    PASS=$((PASS + 1))
+else
+    red "  FAIL: zig build test"
+    FAIL=$((FAIL + 1))
+fi
+
+if (cd "$FFI_DIR" && zig build) >/dev/null 2>&1 && [ -f "$FFI_DIR/zig-out/lib/libkrl.a" ]; then
+    green "  PASS: static library libkrl.a produced"
+    PASS=$((PASS + 1))
+else
+    red "  FAIL: static library libkrl.a not produced"
+    FAIL=$((FAIL + 1))
+fi
 
-# ─── Example: CLI tool E2E ───────────────────────────────────────────
-# bold "Section 1: CLI happy path"
-# OUTPUT=$($BINARY --help 2>&1)
-# check "help flag works" "Usage:" "$OUTPUT"
-#
-# OUTPUT=$($BINARY process input.txt --output /tmp/e2e-output.json 2>&1)
-# check "process command succeeds" "complete" "$OUTPUT"
-#
-# OUTPUT=$(cat /tmp/e2e-output.json)
-# check "output is valid JSON" '"status"' "$OUTPUT"
-
-# ─── Example: Server E2E ────────────────────────────────────────────
-# bold "Section 2: Server lifecycle"
-# $BINARY serve --port 9999 &
-# SERVER_PID=$!
-# trap "kill $SERVER_PID 2>/dev/null" EXIT
-# sleep 2
-#
-# STATUS=$(curl -s -o /dev/null -w "%{http_code}" http://localhost:9999/health)
-# check_status "health endpoint" "200" "$STATUS"
-#
-# BODY=$(curl -s http://localhost:9999/health)
-# check "health response" '"status":"ok"' "$BODY"
-#
-# kill $SERVER_PID 2>/dev/null
-
-# ─── Example: VeriSimDB integration ─────────────────────────────────
-# bold "Section 3: VeriSimDB persistence"
-# VERISIM_URL="${VERISIM_API_URL:-http://localhost:9090}"
-# if ! curl -sf "$VERISIM_URL/health" >/dev/null 2>&1; then
-#     skip_test "VeriSimDB integration" "gateway not available"
-# else
-#     STATUS=$(curl -s -o /dev/null -w "%{http_code}" -X POST "$VERISIM_URL/api/v1/hexads" \
-#         -H "Content-Type: application/json" \
-#         -d '{"tool":"KRL","modality":"document","content":"e2e test"}')
-#     check_status "hexad POST" "201" "$STATUS"
-# fi
+echo ""
+
+# ─── Section 2: ABI surface is covered by the FFI ────────────────────
+bold "Section 2: ABI/FFI correspondence"
+
+ABI_FOREIGN=$(grep -h '%foreign' "$ABI_DIR"/*.idr 2>/dev/null | wc -l)
+FFI_EXPORTS=$(grep -h '^export fn' "$FFI_DIR"/src/*.zig 2>/dev/null | wc -l)
+
+if [ "$ABI_FOREIGN" -gt 0 ] && [ "$FFI_EXPORTS" -ge "$ABI_FOREIGN" ]; then
+    green "  PASS: $ABI_FOREIGN %foreign declarations covered by $FFI_EXPORTS Zig exports"
+    PASS=$((PASS + 1))
+else
+    red "  FAIL: ABI/FFI mismatch ($ABI_FOREIGN %foreign vs $FFI_EXPORTS exports)"
+    FAIL=$((FAIL + 1))
+fi
+
+echo ""
+
+# ─── Section 3: grammar smoke suite ──────────────────────────────────
+bold "Section 3: KRL grammar smoke suite"
+
+if bash "$PROJECT_DIR/tests/smoke/grammar_smoke.sh" >/dev/null 2>&1; then
+    green "  PASS: grammar smoke suite"
+    PASS=$((PASS + 1))
+else
+    red "  FAIL: grammar smoke suite"
+    FAIL=$((FAIL + 1))
+fi
+
+echo ""
 
 # ═══════════════════════════════════════════════════════════════════════
 # Summary