diff --git a/.gitignore b/.gitignore
index a9f1039..a9040e6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -46,3 +46,6 @@ dist/
 # Zig (FFI) build artifacts
 .zig-cache/
 zig-out/
+
+# Cross-compiled package binaries (just pkg-build-hello)
+examples/packages/hello.zpkg/binaries/
diff --git a/.tool-versions b/.tool-versions
index 2f5d885..a1268cd 100644
--- a/.tool-versions
+++ b/.tool-versions
@@ -1,3 +1,4 @@
 # SPDX-License-Identifier: MPL-2.0
 # asdf version manager configuration
 ocaml 5.1.1
+zig 0.13.0
diff --git a/docs/TOOLCHAIN.adoc b/docs/TOOLCHAIN.adoc
new file mode 100644
index 0000000..9b7eb66
--- /dev/null
+++ b/docs/TOOLCHAIN.adoc
@@ -0,0 +1,48 @@
+// SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.8
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+= Local toolchain setup
+
+Everything the CI gate runs (`.github/workflows/ci.yml`) can be reproduced
+locally with `just ci` plus `just proofs`. The pins live in `.tool-versions`.
+
+== Idris2 (>= 0.7.0) — the ABI proof layer
+
+Not packaged on most distros; bootstrap from source with Chez Scheme:
+
+[source,bash]
+----
+sudo apt-get install -y chezscheme libgmp-dev
+git clone --depth 1 -b v0.7.0 https://github.com/idris-lang/Idris2
+cd Idris2 && make bootstrap SCHEME=chezscheme && sudo make install
+----
+
+== OCaml (>= 4.14, pinned 5.1.1) with dune + menhir
+
+Via apt:
+
+[source,bash]
+----
+sudo apt-get install -y ocaml ocaml-dune menhir libmenhir-ocaml-dev \
+  libyojson-ocaml-dev libsedlex-ocaml-dev libppx-deriving-ocaml-dev \
+  libppx-deriving-yojson-ocaml-dev libalcotest-ocaml-dev ocaml-findlib
+----
+
+...or via opam:
+
+[source,bash]
+----
+opam install dune menhir sedlex yojson ppx_deriving ppx_deriving_yojson alcotest
+----
+
+== Zig (0.13 verified) — the FFI layer
+
+`just zig-ffi-check` compile-checks every FFI source without linking.
+A full `zig build` link requires system liboqs + libsodium
+(see `ffi/zig/build.zig` and `Containerfile.liboqs`).
+
+== The gate itself
+
+* `just proofs` — `idris2 --build src/abi/oblibeny-abi.ipkg`
+* `just ci` — dune lint + conformance suite + Zig FFI compile-check +
+  escape-hatch guard (no `believe_me` / `postulate` / `assert_total` /
+  `partial` / `idris_crash` / holes in the ABI proofs)
diff --git a/justfile b/justfile
index 5cd1119..285570d 100644
--- a/justfile
+++ b/justfile
@@ -46,13 +46,22 @@ proofs:
 zig-ffi-check:
     @if command -v zig >/dev/null 2>&1; then \
         for f in ffi/zig/src/*.zig ffi/zig/src/packages/*.zig; do \
-            [ -f "$$f" ] && echo "ast-check $$f" && zig ast-check "$$f"; \
+            [ -f "$f" ] && echo "ast-check $f" && zig ast-check "$f"; \
         done; \
         echo "✓ Zig FFI sources compile-checked"; \
     else \
         echo "zig not installed — skipping (see ffi/zig/build.zig; Zig 0.13 verified in PR #56)"; \
     fi
 
+# Fail if any soundness escape hatch appears in the ABI proofs — same gate as ci.yml
+guard-escape-hatches:
+    @if grep -rnE 'believe_me|assert_total|\bpostulate\b|\bpartial\b|idris_crash|\?[A-Za-z_][A-Za-z0-9_]*' \
+         src/abi/Crypto.idr src/abi/Packages; then \
+        echo "ERROR: soundness escape hatch found in ABI proofs"; \
+        exit 1; \
+    fi
+    @echo "no escape hatches"
+
 # ============================================================================
 # RUN
 # ============================================================================
@@ -105,8 +114,8 @@ doc:
 # RELEASE
 # ============================================================================
 
-# Run all checks (lint + test)
-ci: lint test
+# Run all checks (lint + test + FFI compile-check + escape-hatch guard)
+ci: lint test zig-ffi-check guard-escape-hatches
     @echo "All checks passed."
 
 # Prepare a release
@@ -125,8 +134,8 @@ release VERSION:
 validate-spec:
     @echo "Validating specification files..."
     @for f in ANCHOR*.scm SPEC*.scm AUTHORITY*.scm; do \
-        if [ -f "$$f" ]; then \
-            echo "  ✓ $$f exists"; \
+        if [ -f "$f" ]; then \
+            echo "  ✓ $f exists"; \
         fi; \
     done
 
@@ -139,31 +148,35 @@ golden-path:
 # DISTRIBUTION PROOF-OF-CONCEPT
 # ============================================================================
 
-# Verify Idris2 ABI proofs for hello package
+# Verify Idris2 ABI proofs for hello package (ipkg-level; per-file --check is a fake gate)
 abi-check-hello:
-    @echo "Checking Idris2 ABI proofs..."
-    idris2 --check src/abi/packages/hello/Interface.idr
+    @echo "Checking Idris2 ABI proofs (via oblibeny-abi.ipkg)..."
+    cd src/abi && idris2 --build oblibeny-abi.ipkg
 
-# Generate C headers from Idris2 ABI
+# Generate C code from the Idris2 ABI interface (module root = src/abi)
 abi-gen-hello:
-    @echo "Generating C headers from Idris2..."
+    @echo "Generating C from Idris2..."
     mkdir -p generated/abi/hello
-    idris2 --codegen c src/abi/packages/hello/Interface.idr
-    @echo "Headers generated in generated/abi/"
+    cd src/abi && idris2 --codegen c Packages/Hello/Interface.idr
+    @echo "Generated under src/abi/build/ (C backend)"
 
 # Build Zig FFI library for hello package
 ffi-build-hello:
     @echo "Building Zig FFI for hello package..."
+    mkdir -p dist/ffi
     cd ffi/zig && zig build-lib src/packages/hello.zig \
         -dynamic \
         -target x86_64-linux-musl \
         -O ReleaseSafe \
-        -femit-bin=../../lib/libhello.so
-    @echo "Built: lib/libhello.so"
+        -femit-bin=../../dist/ffi/libhello.so
+    @echo "Built: dist/ffi/libhello.so"
 
 # Build hello package for all architectures
 pkg-build-hello:
     @echo "Cross-compiling hello for all architectures..."
+    @mkdir -p examples/packages/hello.zpkg/binaries/x86_64 \
+        examples/packages/hello.zpkg/binaries/aarch64 \
+        examples/packages/hello.zpkg/binaries/riscv64
     @echo "  x86_64..."
     @cd examples/packages/hello.zpkg && \
         echo 'const std = @import("std"); pub fn main() !void { std.debug.print("Hello, Oblibeny Distribution!\\n", .{}); }' > hello.zig && \
@@ -177,7 +190,7 @@ pkg-build-hello:
     @cd examples/packages/hello.zpkg && \
         zig build-exe hello.zig -target riscv64-linux-musl -O ReleaseSafe && \
         mv hello binaries/riscv64/ && \
-        rm hello.zig hello.o || true
+        rm -f hello.zig hello.o
     @echo "✓ Cross-compilation complete"
 
 # Package hello.zpkg archive
diff --git a/mise.toml b/mise.toml
deleted file mode 100644
index 6dd983f..0000000
--- a/mise.toml
+++ /dev/null
@@ -1,57 +0,0 @@
-[tools]
-# Language runtimes
-node = "latest"
-python = "latest"
-rust = "latest"
-go = "latest"
-zig = "latest"
-java = "latest"
-bun = "latest"
-denojs = "latest"
-
-# Package managers
-npm = "latest"
-yarn = "latest"
-pnpm = "latest"
-pip = "latest"
-cargo = "latest"
-go-task = "latest"
-
-# Formatting & Linting
-gofmt = "latest"
-black = "latest"
-isort = "latest"
-ruff = "latest"
-prettier = "latest"
-shfmt = "latest"
-stylua = "latest"
-
-# Build tools
-cmake = "latest"
-make = "latest"
-ninja = "latest"
-
-# Shell tools
-git = "latest"
-gnu-sed = "latest"
-gnu-tar = "latest"
-gnu-grep = "latest"
-
-# Testing
-vitest = "latest"
-pytest = "latest"
-jest = "latest"
-
-[env]
-# Common environment variables
-NODE_ENV = "development"
-PYTHONDONTWRITEBYTECODE = "1"
-PYTHONUNBUFFERED = "1"
-
-# Task runner alias
-[alias]
-task = "go-task"
-build = "cargo build --release || npm run build || go build"
-test = "cargo test || npm test || go test ./..."
-lint = "ruff check . || prettier --check . || black --check ."
-fmt = "ruff format . || prettier --write . || black ."
diff --git a/scripts/check-proofs.sh b/scripts/check-proofs.sh
deleted file mode 100755
index dd68026..0000000
--- a/scripts/check-proofs.sh
+++ /dev/null
@@ -1,53 +0,0 @@
-#!/usr/bin/env bash
-# SPDX-License-Identifier: MPL-2.0
-# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
-#
-# Reproducible verification of Oblíbený's proof + type-safety claims.
-#
-# Runs, and fails on the first problem:
-#   1. the Idris2 ABI proof layer  (src/abi/oblibeny-abi.ipkg)
-#   2. the OCaml language build + conformance suite (dune)
-#   3. a guard that no soundness escape hatch has crept into the ABI proofs
-#
-# Toolchain (install if missing):
-#   * Idris2 >= 0.7.0.  Not packaged on most distros; bootstrap from source with
-#     Chez Scheme:
-#       sudo apt-get install -y chezscheme libgmp-dev
-#       git clone --depth 1 -b v0.7.0 https://github.com/idris-lang/Idris2
-#       cd Idris2 && make bootstrap SCHEME=chezscheme && sudo make install
-#   * OCaml >= 4.14 with dune + menhir + the libs in dune-project.  Via apt:
-#       sudo apt-get install -y ocaml ocaml-dune menhir libmenhir-ocaml-dev \
-#         libyojson-ocaml-dev libsedlex-ocaml-dev libppx-deriving-ocaml-dev \
-#         libppx-deriving-yojson-ocaml-dev libalcotest-ocaml-dev ocaml-findlib
-#     ...or via opam: opam install dune menhir sedlex yojson ppx_deriving \
-#         ppx_deriving_yojson alcotest
-
-set -euo pipefail
-
-repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
-cd "$repo_root"
-
-fail() { printf '\nFAIL: %s\n' "$1" >&2; exit 1; }
-
-# ---------------------------------------------------------------------------
-echo "==> [1/3] Idris2 ABI proof layer"
-command -v idris2 >/dev/null 2>&1 || fail "idris2 not found on PATH (see header for install)"
-idris2 --build src/abi/oblibeny-abi.ipkg
-
-# ---------------------------------------------------------------------------
-echo "==> [2/3] OCaml build + conformance suite"
-command -v dune >/dev/null 2>&1 || fail "dune not found on PATH (see header for install)"
-dune build
-dune runtest
-
-# ---------------------------------------------------------------------------
-echo "==> [3/3] escape-hatch guard (no believe_me / postulate / assert_total / partial / holes)"
-if grep -rnE 'believe_me|assert_total|\bpostulate\b|\bpartial\b|idris_crash|\?[A-Za-z_][A-Za-z0-9_]*' \
-     src/abi/Crypto.idr src/abi/Packages >/dev/null 2>&1; then
-  grep -rnE 'believe_me|assert_total|\bpostulate\b|\bpartial\b|idris_crash|\?[A-Za-z_][A-Za-z0-9_]*' \
-     src/abi/Crypto.idr src/abi/Packages
-  fail "soundness escape hatch found in ABI proofs"
-fi
-
-echo
-echo "OK: all proofs build, conformance suite passes, no escape hatches."