diff --git a/.github/dependabot.yml b/.github/dependabot.yml
index 085c969..d5a6320 100644
--- a/.github/dependabot.yml
+++ b/.github/dependabot.yml
@@ -17,8 +17,8 @@
 #
 #   /                              root workspace (vcl-ut, fmt, lint, core)
 #   /src/interface/parse           parser + decider + vclt-gate  <- the real spine
-#   /src/interface/attest          depends on ../parse (in-repo)
-#   /src/interface/recompute-wasm  depends on ../parse (in-repo)
+#   /ffi/rust/attest               depends on src/interface/parse (in-repo)
+#   /ffi/rust/recompute-wasm       depends on src/interface/parse (in-repo)
 #
 # DELIBERATELY EXCLUDED: /src/interface/echidna-client. It depends on
 # ../../interface, which in turn carries an out-of-tree path dependency
@@ -66,13 +66,13 @@ updates:
     open-pull-requests-limit: 0
 
   - package-ecosystem: "cargo"
-    directory: "/src/interface/attest"
+    directory: "/ffi/rust/attest"
     schedule:
       interval: "weekly"
     open-pull-requests-limit: 0
 
   - package-ecosystem: "cargo"
-    directory: "/src/interface/recompute-wasm"
+    directory: "/ffi/rust/recompute-wasm"
     schedule:
       interval: "weekly"
     open-pull-requests-limit: 0
diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml
index 255ddea..7ce473e 100644
--- a/.github/workflows/rhodibot.yml
+++ b/.github/workflows/rhodibot.yml
@@ -1,5 +1,5 @@
-# This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
+# This workflow is managed by gh actions-lock.
 # rhodibot.yml — RSR compliance CANARY (report-only)
 #
 # Rhodibot does NOT mutate this repository. It never deletes, renames,
diff --git a/.github/workflows/satellite-crates-gate.yml b/.github/workflows/satellite-crates-gate.yml
index 43eeea1..00bbb4f 100644
--- a/.github/workflows/satellite-crates-gate.yml
+++ b/.github/workflows/satellite-crates-gate.yml
@@ -9,8 +9,8 @@
 #   /                              e2e.yml
 #   /src/interface/parse           parse-gate.yml
 #   /src/interface/echidna-client  backend-matrix.yml (needs echidna sibling)
-#   /src/interface/attest          NOTHING   <- gated here
-#   /src/interface/recompute-wasm  NOTHING   <- gated here
+#   /ffi/rust/attest               NOTHING   <- gated here
+#   /ffi/rust/recompute-wasm       NOTHING   <- gated here
 #
 # The cost of that gap was measured on 2026-07-21: both ungated crates had
 # stopped compiling. `ast::Statement` gained the S1 consonance field `verb`
@@ -76,10 +76,10 @@ jobs:
       - name: Clippy — warnings are errors
         run: |
           set -euo pipefail
-          cargo clippy --manifest-path src/interface/${{ matrix.crate }}/Cargo.toml \
+          cargo clippy --manifest-path ffi/rust/${{ matrix.crate }}/Cargo.toml \
             --all-targets -- -D warnings
 
       - name: Tests
         run: |
           set -euo pipefail
-          cargo test --manifest-path src/interface/${{ matrix.crate }}/Cargo.toml
+          cargo test --manifest-path ffi/rust/${{ matrix.crate }}/Cargo.toml
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 5f1313a..f0577ed 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -13,6 +13,16 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 ==== Changed
 
+* *SPARK-grade safe-source boundary* (vcl-ut#49): moved the Rust C-ABI
+  attestation crate and the `wasm32` host/guest recompute crate from
+  `src/interface/{attest,recompute-wasm}` to `ffi/rust/`, so every Rust
+  `unsafe` block in the repository lives under `ffi/`. The aspect gate
+  (`tests/aspect_tests.sh`) now requires: no unsafe Rust constructs anywhere
+  under `src/` (tests included); `#![forbid(unsafe_code)]` on every `src/`
+  crate root; and the SPDX identifier on the first line of every `src/` Rust
+  file. It keeps the fail-open check from vcl-ut#117 (`unwrap`/`expect`/
+  `panic!` family). Moved crates keep their own lockfiles; the Zig shim,
+  satellite gate, Dependabot, and audit classifications follow the new paths.
 * *Modality profiles distinguished from the fixed Octad schema* (vcl-ut#118):
   adopted `modality profile` for versioned, implementation-specific modality
   selections and `modality set` for membership alone. Clarified that VCL-UT's
@@ -123,7 +133,7 @@ the corpus decision core (`+Schema+`/`+Decide+`/`+Checker+`
 public deciders via `+WireConformance+` on shared golden bytes
 (find-dependent verdicts pinned Rust-side + input-value conformance,
 disclosed); P5c-5 (#32) the recompute *`+wasm32+`* artefact
-`+src/interface/recompute-wasm+` (`+vcl_recompute+`, fail-closed, one
+`+ffi/rust/recompute-wasm+` (`+vcl_recompute+`, fail-closed, one
 audited host/guest `+unsafe+` block; all logic in the forbid-unsafe
 crate); P5c-6 (this change) the `+OWED→RESOLVED+` stance flip + ADR
 `+docs/decisions/0002-ffi-attestation-trust-boundary.adoc+`. The
@@ -133,7 +143,7 @@ system not load-bearing under recompute); `+affinescriptiser+` N/A
 (resource-required + wasm-backend-pending; disclosed in
 `+AFFINESCRIPTISER-NA.adoc+`, not faked).
 * Phase 5 / vcl-ut#25 — *Tier-2 (P5d) RESOLVED*:
-`+src/interface/attest+` (`+vcltotal-attest+`) mints/verifies an Ed25519
+`+ffi/rust/attest+` (`+vcltotal-attest+`) mints/verifies an Ed25519
 attestation over
 `+DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level+` (level =
 the conformance-pinned `+certified_level+`, signed iff `+0..=10+`,
@@ -143,7 +153,7 @@ crate, linked into `+ffi/zig/src/lib.zig+` (`+vclut_verify_wire+`) by
 (roundtrip + 5 tamper variants + fail-closed + C-ABI tests).
 `+ed25519-dalek+`/`+sha2+` contained to the Tier-2 crate; zero-dep
 forbid-unsafe core untouched; one audited host/guest `+unsafe+` block.
-Spec `+src/interface/attest/ATTESTATION-FORMAT.adoc+`; ADR-0002 → both
+Spec `+ffi/rust/attest/ATTESTATION-FORMAT.adoc+`; ADR-0002 → both
 tiers RESOLVED. *The vcl-ut#25 boundary-reinforcement workstream is
 complete* (only the precisely-scoped disclosed limits remain — not
 gaps). A re-checkable proof is impossible _only_ over the C-ABI fallback
diff --git a/Cargo.lock b/Cargo.lock
index 618b19a..dbbe2bc 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -239,9 +239,9 @@ dependencies = [
 
 [[package]]
 name = "crossbeam-epoch"
-version = "0.9.18"
+version = "0.9.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5b82ac4a3c2ca9c3460964f020e1402edd5753411d7737aa39c3714ad1b5420e"
+checksum = "dc74980687109a3b14c72fd458107bf0baa1da1a1a805e178d15501ba9b86d9d"
 dependencies = [
  "crossbeam-utils",
 ]
diff --git a/REUSE.toml b/REUSE.toml
index 2e3ec50..026afa7 100644
--- a/REUSE.toml
+++ b/REUSE.toml
@@ -98,6 +98,7 @@ path = [
   "contractiles/**",
   "examples/**",
   "features/**",
+  "ffi/**",
   "src/**",
   "verification/**",
 ]
diff --git a/audits/assail-classifications.a2ml b/audits/assail-classifications.a2ml
index 3b6975e..47029f2 100644
--- a/audits/assail-classifications.a2ml
+++ b/audits/assail-classifications.a2ml
@@ -22,12 +22,12 @@
   ;; Mirrors the reference pattern in hyperpolymath/007
   ;; audits/assail-classifications.a2ml (zig_bridge.rs UnsafeCode).
   (classification
-    (file "src/interface/recompute-wasm/src/lib.rs")
+    (file "ffi/rust/recompute-wasm/src/lib.rs")
     (category "UnsafeCode")
     (audit "in-file UNSAFE POLICY (lib.rs:40-46) + deny(clippy::undocumented_unsafe_blocks)")
     (rationale "only unsafe is the documented host/guest memory-ABI block (alloc/dealloc pair); all decision logic lives in the forbid(unsafe_code) vcltotal-parse crate"))
   (classification
-    (file "src/interface/attest/src/lib.rs")
+    (file "ffi/rust/attest/src/lib.rs")
     (category "UnsafeCode")
     (audit "in-file UNSAFE POLICY (lib.rs:38-42) + deny(clippy::undocumented_unsafe_blocks)")
     (rationale "single documented C-ABI block in vclut_rs_verify with null/len checks and fail-closed -1 returns; decode logic in forbid(unsafe_code) crate"))
diff --git a/docs/2026-07-21-workup-consonance-and-verisim.adoc b/docs/2026-07-21-workup-consonance-and-verisim.adoc
index bde657b..f01a300 100644
--- a/docs/2026-07-21-workup-consonance-and-verisim.adoc
+++ b/docs/2026-07-21-workup-consonance-and-verisim.adoc
@@ -398,7 +398,7 @@ that preserves VeriSimDB's genuinely good UX work:
 
 === 3. Attestation
 
-`src/interface/attest` mints a signed attestation over `(statement, schema)`
+`ffi/rust/attest` mints a signed attestation over `(statement, schema)`
 carrying the certified level, verifiable independently. For a database whose
 selling point is maintained identity consonance, being able to prove *after
 the fact* that a transition was admitted at a stated level — and have a third
diff --git a/docs/decisions/0002-ffi-attestation-trust-boundary.adoc b/docs/decisions/0002-ffi-attestation-trust-boundary.adoc
index 8f55ddf..d4ba9d2 100644
--- a/docs/decisions/0002-ffi-attestation-trust-boundary.adoc
+++ b/docs/decisions/0002-ffi-attestation-trust-boundary.adoc
@@ -9,7 +9,7 @@ Date: 2026-05-19
 ## Status
 
 Accepted (**both tiers RESOLVED** — Tier-1 recompute-PCC over `wasm32`;
-Tier-2 / P5d C-ABI Ed25519 attestation fallback, `src/interface/attest`
+Tier-2 / P5d C-ABI Ed25519 attestation fallback, `ffi/rust/attest`
 linked into the Zig shim). Tracked: hyperpolymath/vcl-ut#25.
 Authoritative companion:
 `verification/proofs/VERIFICATION-STANCE.adoc` (canonical two-tier
@@ -41,7 +41,7 @@ Constraints established during Phase 5:
   verdict entry is a pure resource-free function (fabricating a
   resource to satisfy the tool would violate the verification-honesty
   doctrine), and its wasm backend is Phase-2-pending. (Disclosed:
-  `src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc`.)
+  `ffi/rust/recompute-wasm/AFFINESCRIPTISER-NA.adoc`.)
 
 ## Decision
 
@@ -49,7 +49,7 @@ Adopt a **two-tier boundary**:
 
 **Tier-1 — recompute-PCC over plain `wasm32` (the achieved tier).**
 The consumer is shipped the `wasm32` module
-`src/interface/recompute-wasm` (`vcl_recompute`) + the wire bytes of a
+`ffi/rust/recompute-wasm` (`vcl_recompute`) + the wire bytes of a
 `(Statement, OctadSchema)` + the producer's claimed level, and
 **re-runs the certified decision itself**, comparing its verdict to
 the claim. This is proof-carrying code by *recomputation*, not by
@@ -79,7 +79,7 @@ decode/decision logic in the `#![forbid(unsafe_code)]` crate.
 
 **Tier-2 — C-ABI trusted-certifier attestation (fallback, P5d,
 RESOLVED).** For consumers that cannot run the Tier-1 wasm:
-`src/interface/attest` (`vcltotal-attest`) mints an Ed25519 signature
+`ffi/rust/attest` (`vcltotal-attest`) mints an Ed25519 signature
 over `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level`, where
 `level` is the conformance-pinned `vcltotal_parse::certified_level`
 (signed iff `0..=10`, fail-closed); the consumer Ed25519-verifies
@@ -90,7 +90,7 @@ shim (`vclut_verify_wire`) by `build.zig`; `zig build test` exercises
 the boundary end-to-end. Strictly weaker than Tier-1 (pure trust in
 the minting certifier + that it ran the pinned decider), and labelled
 as such everywhere. Spec:
-`src/interface/attest/ATTESTATION-FORMAT.adoc`; crypto
+`ffi/rust/attest/ATTESTATION-FORMAT.adoc`; crypto
 (`ed25519-dalek`/`sha2`) contained to this Tier-2 crate, the
 zero-dep forbid-unsafe core untouched.
 
diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc
index 92ac97d..a96e799 100644
--- a/docs/developer/ABI-FFI-README.adoc
+++ b/docs/developer/ABI-FFI-README.adoc
@@ -68,13 +68,16 @@ vcl_total/
 │   │   ├── legacy/             # Pre-Phase-5 plumbing (DEPRECATED)
 │   │   │   └── Foreign.idr     # Legacy libvqlut bindings (Zig
 │   │   │                       # asserts level; no Idris certificate)
-│   │   ├── attest/             # Tier-2 Rust: signed attestation
-│   │   ├── recompute-wasm/     # Tier-1 Rust: consumer-side recompute
+│   │   ├── parse/              # Safe Rust parser + decider (forbid-unsafe)
 │   │   └── ffi/                # Legacy Zig multi-stage pipeline
 │   └── core/                   # Idris2 corpus (the certifier itself)
+│                               # No unsafe Rust anywhere under src/ (#49)
 │
 ├── ffi/
-│   └── zig/                    # FFI implementation (Zig)
+│   ├── rust/                   # Rust unsafe-boundary crates (only here)
+│   │   ├── attest/             # Tier-2 Rust: signed C-ABI attestation
+│   │   └── recompute-wasm/     # Tier-1 Rust: consumer-side wasm recompute
+│   └── zig/                    # Zig shim, links ffi/rust/attest
 │       ├── build.zig           # Build configuration
 │       ├── build.zig.zon       # Dependencies
 │       ├── src/
diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc
index 5b9e196..dc6fbfe 100644
--- a/docs/status/PROOF-NEEDS.adoc
+++ b/docs/status/PROOF-NEEDS.adoc
@@ -115,7 +115,7 @@ conformant with the Rust encoder by `+Refl+` in
 `+VclTotal.Interface.WireConformance+`. The marshalling seam’s _decode_
 side is machine-verified. *P5c — RESOLVED (Tier-1 recompute-PCC):* the
 consumer re-runs the certified decision itself from the fail-closed
-`+wasm32+` module `+src/interface/recompute-wasm+` (`+vcl_recompute+`);
+`+wasm32+` module `+ffi/rust/recompute-wasm+` (`+vcl_recompute+`);
 the decision core is a faithful Rust port of the corpus
 (`+Schema+`/`+Decide+`/`+Checker+`) machine-pinned via
 `+WireConformance+`. TCB = conformance-pinned decider image + wasm
@@ -123,7 +123,7 @@ runtime + the once-proved corpus (offline-re-checkable) — _not_ a
 trusted tag, _not_ a transported proof object. Plain `+wasm32+` suffices
 (type system not load-bearing under recompute); `+affinescriptiser+` N/A
 (disclosed). *P5d — RESOLVED (Tier-2 fallback):*
-`+src/interface/attest+` mints/verifies an Ed25519 attestation bound to
+`+ffi/rust/attest+` mints/verifies an Ed25519 attestation bound to
 `+(sha256(stmt_wire), sha256(schema_wire),   level)+` (fail-closed); the
 `+vclut_rs_verify+` backend is linked into `+ffi/zig+`
 (`+vclut_verify_wire+`, `+zig build test+` green end-to-end).
diff --git a/ffi/rust/README.adoc b/ffi/rust/README.adoc
new file mode 100644
index 0000000..588545b
--- /dev/null
+++ b/ffi/rust/README.adoc
@@ -0,0 +1,40 @@
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Rust FFI Boundary Crates
+:toc:
+
+This directory is the Rust host/guest and C-ABI boundary layer, and the
+*only* place in the repository where Rust `unsafe` is allowed (vcl-ut#49).
+Rust code under `src/` is safe Rust: every crate root there carries
+`#![forbid(unsafe_code)]`, and `tests/aspect_tests.sh` rejects any unsafe
+construct under `src/`, test code included.
+
+Each crate here keeps its unsafe surface to one audited block with a
+`// SAFETY:` justification (`#![deny(clippy::undocumented_unsafe_blocks)]`)
+and delegates all decoding and decision logic to the safe
+`src/interface/parse` (`vcltotal-parse`) crate.
+
+== Crates
+
+* `attest/` (`vcltotal-attest`): Tier-2 C-ABI Ed25519 trusted-certifier
+  attestation backend (`vclut_rs_verify`), linked into the Zig shim
+  `ffi/zig` by `ffi/zig/build.zig`. Spec: `attest/ATTESTATION-FORMAT.adoc`.
+* `recompute-wasm/` (`vcltotal-recompute-wasm`): Tier-1 `wasm32`
+  recompute-PCC entry point (`vcl_recompute`).
+
+Each crate is an independent Cargo workspace root with its own committed
+lockfile, so it builds without the repository's other workspace roots
+(one of which carries an external path dependency).
+
+== Validation
+
+[source,sh]
+----
+cargo clippy --manifest-path ffi/rust/attest/Cargo.toml --all-targets -- -D warnings
+cargo test   --manifest-path ffi/rust/attest/Cargo.toml --locked
+cargo clippy --manifest-path ffi/rust/recompute-wasm/Cargo.toml --all-targets -- -D warnings
+cargo test   --manifest-path ffi/rust/recompute-wasm/Cargo.toml --locked
+(cd ffi/zig && zig build test)   # links attest/ end to end
+----
+
+CI: `.github/workflows/satellite-crates-gate.yml`.
diff --git a/src/interface/attest/.gitignore b/ffi/rust/attest/.gitignore
similarity index 100%
rename from src/interface/attest/.gitignore
rename to ffi/rust/attest/.gitignore
diff --git a/src/interface/attest/ATTESTATION-FORMAT.adoc b/ffi/rust/attest/ATTESTATION-FORMAT.adoc
similarity index 96%
rename from src/interface/attest/ATTESTATION-FORMAT.adoc
rename to ffi/rust/attest/ATTESTATION-FORMAT.adoc
index 4796844..8ea5ccd 100644
--- a/src/interface/attest/ATTESTATION-FORMAT.adoc
+++ b/ffi/rust/attest/ATTESTATION-FORMAT.adoc
@@ -62,13 +62,13 @@ registry/trust). "query" in the issue-#25 phrasing
 
 A tampered `stmt_wire`, `schema_wire`, `level`, or `sig`, or a wrong
 public key, all fail verification (machine-tested:
-`src/interface/attest` — roundtrip + 5 tamper variants + fail-closed +
+`ffi/rust/attest` — roundtrip + 5 tamper variants + fail-closed +
 C-ABI).
 
 == C-ABI
 
 `vclut_rs_verify(stmt_ptr, stmt_len, schema_ptr, schema_len, sk_ptr,
-out_ptr, out_cap) -> i64` (Rust, `src/interface/attest`), linked into
+out_ptr, out_cap) -> i64` (Rust, `ffi/rust/attest`), linked into
 the Zig shim `ffi/zig/src/lib.zig` and exposed as
 `vclut_verify_wire(...)`. Returns the level `0..10` (and writes the
 65-byte token) or `-1` Rejected (writes nothing; `vclut_last_error`
diff --git a/src/interface/attest/Cargo.lock b/ffi/rust/attest/Cargo.lock
similarity index 100%
rename from src/interface/attest/Cargo.lock
rename to ffi/rust/attest/Cargo.lock
diff --git a/src/interface/attest/Cargo.toml b/ffi/rust/attest/Cargo.toml
similarity index 83%
rename from src/interface/attest/Cargo.toml
rename to ffi/rust/attest/Cargo.toml
index 6d20c25..a47e1a5 100644
--- a/src/interface/attest/Cargo.toml
+++ b/ffi/rust/attest/Cargo.toml
@@ -1,7 +1,8 @@
 # SPDX-License-Identifier: MPL-2.0
 
-# Standalone workspace root (same rationale as ../parse, ../recompute-wasm):
-# decoupled from the broken parent virtual workspace. This is the Tier-2
+# Standalone workspace root (same rationale as src/interface/parse and
+# ffi/rust/recompute-wasm): an FFI boundary crate that builds and gates in
+# isolation from the other workspace roots. This is the Tier-2
 # (C-ABI trusted-certifier attestation) FALLBACK crate — explicitly the
 # weaker boundary tier (see VERIFICATION-STANCE.adoc's two-tier model).
 # The crypto dependency is CONTAINED here and never touches the
@@ -23,7 +24,7 @@ crate-type = ["staticlib", "rlib"]
 path = "src/lib.rs"
 
 [dependencies]
-vcltotal-parse = { path = "../parse" }
+vcltotal-parse = { path = "../../../src/interface/parse" }
 # de-facto standard, widely audited (user decision 2026-05-19).
 # default-features off keeps the tree minimal; `std` for the host
 # staticlib; no rng feature (deterministic keys via from_bytes).
diff --git a/src/interface/attest/README.adoc b/ffi/rust/attest/README.adoc
similarity index 96%
rename from src/interface/attest/README.adoc
rename to ffi/rust/attest/README.adoc
index 59d88e1..098a270 100644
--- a/src/interface/attest/README.adoc
+++ b/ffi/rust/attest/README.adoc
@@ -13,7 +13,7 @@ attestation (the FALLBACK tier).** Authoritative model:
 == Role
 
 For consumers that **cannot run the Tier-1 recompute `wasm32` module**
-(`src/interface/recompute-wasm`). A C ABI cannot carry a re-checkable
+(`ffi/rust/recompute-wasm`). A C ABI cannot carry a re-checkable
 proof, so this mints an Ed25519 attestation binding
 `(sha256(stmt_wire), sha256(schema_wire), level)` — unforgeable and
 bound, but *trusted* (the consumer trusts the certifier that signed
diff --git a/src/interface/attest/src/lib.rs b/ffi/rust/attest/src/lib.rs
similarity index 99%
rename from src/interface/attest/src/lib.rs
rename to ffi/rust/attest/src/lib.rs
index 6e600f4..be3c68a 100644
--- a/src/interface/attest/src/lib.rs
+++ b/ffi/rust/attest/src/lib.rs
@@ -6,7 +6,7 @@
 //!
 //! See `verification/proofs/VERIFICATION-STANCE.adoc`'s canonical
 //! two-tier boundary model. Tier-1 (recompute-PCC over `wasm32`,
-//! `src/interface/recompute-wasm`) is the achieved tier: the consumer
+//! `ffi/rust/recompute-wasm`) is the achieved tier: the consumer
 //! re-validates. Tier-2 — *this crate* — is the explicit **weaker
 //! fallback** for consumers that cannot run the Tier-1 wasm. A C ABI
 //! erases types to machine words, so it cannot carry a re-checkable
diff --git a/src/interface/recompute-wasm/.gitignore b/ffi/rust/recompute-wasm/.gitignore
similarity index 100%
rename from src/interface/recompute-wasm/.gitignore
rename to ffi/rust/recompute-wasm/.gitignore
diff --git a/src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc b/ffi/rust/recompute-wasm/AFFINESCRIPTISER-NA.adoc
similarity index 99%
rename from src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc
rename to ffi/rust/recompute-wasm/AFFINESCRIPTISER-NA.adoc
index 11d9eb2..970ae78 100644
--- a/src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc
+++ b/ffi/rust/recompute-wasm/AFFINESCRIPTISER-NA.adoc
@@ -61,7 +61,7 @@ wasm's type system:
 
 [source,sh]
 ----
-cd src/interface/recompute-wasm
+cd ffi/rust/recompute-wasm
 cargo build --release --target wasm32-unknown-unknown
 # → target/wasm32-unknown-unknown/release/vcltotal_recompute_wasm.wasm
 ----
diff --git a/src/interface/recompute-wasm/Cargo.lock b/ffi/rust/recompute-wasm/Cargo.lock
similarity index 100%
rename from src/interface/recompute-wasm/Cargo.lock
rename to ffi/rust/recompute-wasm/Cargo.lock
diff --git a/src/interface/recompute-wasm/Cargo.toml b/ffi/rust/recompute-wasm/Cargo.toml
similarity index 67%
rename from src/interface/recompute-wasm/Cargo.toml
rename to ffi/rust/recompute-wasm/Cargo.toml
index 2cf33d4..701bd0f 100644
--- a/src/interface/recompute-wasm/Cargo.toml
+++ b/ffi/rust/recompute-wasm/Cargo.toml
@@ -1,11 +1,11 @@
 # SPDX-License-Identifier: MPL-2.0
 
-# Standalone workspace root (same rationale as ../parse/Cargo.toml): the
-# parent virtual workspace has a pre-existing unresolvable external
-# path-dep, so this boundary crate builds/gates in isolation. Its ONLY
-# dependency is the in-repo, forbid-unsafe `vcltotal-parse` (internal
-# path-dep — resolves in a standalone checkout, unlike the broken
-# `../../../echidna/...` member).
+# Standalone workspace root (same rationale as
+# src/interface/parse/Cargo.toml): this FFI boundary crate builds and gates
+# in isolation from the other workspace roots. Its ONLY dependency is the
+# in-repo, forbid-unsafe `vcltotal-parse` (`src/interface/parse`, an
+# internal path-dep that resolves in a standalone checkout, unlike the
+# external `../../../echidna/...` dependency of `src/interface`).
 [workspace]
 
 [package]
@@ -23,7 +23,7 @@ crate-type = ["cdylib", "rlib"]
 path = "src/lib.rs"
 
 [dependencies]
-vcltotal-parse = { path = "../parse" }
+vcltotal-parse = { path = "../../../src/interface/parse" }
 
 # Total/panic-free is inherited from `vcltotal-parse`'s static SPARK
 # lint set (the decoder/decider carry no panics). `panic = "abort"`
diff --git a/src/interface/recompute-wasm/README.adoc b/ffi/rust/recompute-wasm/README.adoc
similarity index 100%
rename from src/interface/recompute-wasm/README.adoc
rename to ffi/rust/recompute-wasm/README.adoc
diff --git a/src/interface/recompute-wasm/src/lib.rs b/ffi/rust/recompute-wasm/src/lib.rs
similarity index 99%
rename from src/interface/recompute-wasm/src/lib.rs
rename to ffi/rust/recompute-wasm/src/lib.rs
index be629a8..bf5ed72 100644
--- a/src/interface/recompute-wasm/src/lib.rs
+++ b/ffi/rust/recompute-wasm/src/lib.rs
@@ -35,7 +35,7 @@
 //! Phase-2-pending.) The recompute security argument does not need it:
 //! soundness is the corpus proof, faithfulness is the conformance pin,
 //! and the wasm is a deterministic `cargo build` of the pinned source.
-//! See `src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc`.
+//! See `ffi/rust/recompute-wasm/AFFINESCRIPTISER-NA.adoc`.
 //!
 //! UNSAFE POLICY. All decision/decoding logic lives in the
 //! `#![forbid(unsafe_code)]` `vcltotal-parse` crate. The ONLY `unsafe`
diff --git a/ffi/zig/build.zig b/ffi/zig/build.zig
index 83dd479..5ecd729 100644
--- a/ffi/zig/build.zig
+++ b/ffi/zig/build.zig
@@ -10,13 +10,16 @@
 //
 // P5d (vcl-ut#25): the Tier-2 attestation backend `vclut_rs_verify`
 // (previously declared-but-unlinked, NAMED OWED) is now the Rust
-// `vcltotal-attest` crate (`src/interface/attest`). build.zig compiles
+// `vcltotal-attest` crate (`ffi/rust/attest`). build.zig compiles
 // that staticlib via cargo and links it into every artefact (incl. the
 // test runner), so the shim's `vclut_verify_wire` calls a real,
 // conformance-pinned, fail-closed backend — not a stub.
 
 const std = @import("std");
 
+/// Configure installation of the shared and static FFI libraries and the `test`
+/// step. Each artefact links the Rust attestation backend, built by Cargo in
+/// release mode; the standard target and optimisation options apply to Zig.
 pub fn build(b: *std.Build) void {
     const target = b.standardTargetOptions(.{});
     const optimize = b.standardOptimizeOption(.{});
@@ -25,10 +28,10 @@ pub fn build(b: *std.Build) void {
     const cargo = b.addSystemCommand(&.{
         "cargo",                "build",
         "--release",            "--manifest-path",
-        "../../src/interface/attest/Cargo.toml",
+        "../../ffi/rust/attest/Cargo.toml",
     });
 
-    const attest_a = b.path("../../src/interface/attest/target/release/libvcltotal_attest.a");
+    const attest_a = b.path("../../ffi/rust/attest/target/release/libvcltotal_attest.a");
 
     const lib_mod = b.createModule(.{
         .root_source_file = b.path("src/lib.zig"),
diff --git a/ffi/zig/src/lib.zig b/ffi/zig/src/lib.zig
index 8d5344b..bbb69be 100644
--- a/ffi/zig/src/lib.zig
+++ b/ffi/zig/src/lib.zig
@@ -46,7 +46,7 @@ fn clearLastError() void {
 //
 // Previously NAMED OWED ("declared in intent but not linked"). Now
 // implemented by the Rust `vcltotal-attest` crate
-// (`src/interface/attest`) and linked by build.zig. It decodes the
+// (`ffi/rust/attest`) and linked by build.zig. It decodes the
 // wire `(Statement, OctadSchema)`, runs the conformance-pinned
 // `vcltotal_parse::certified_level` (the same faithful image of the
 // Idris corpus decision Tier-1 uses), and on a genuine level mints an
diff --git a/src/core/lib.rs b/src/core/lib.rs
index 2099420..9453f41 100644
--- a/src/core/lib.rs
+++ b/src/core/lib.rs
@@ -2,3 +2,5 @@
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 // Dummy lib.rs for Rust compatibility
 // Actual implementation is in Idris files
+
+#![forbid(unsafe_code)]
diff --git a/src/interface/abi/Tier2.idr b/src/interface/abi/Tier2.idr
index 5b89454..4a2b0d1 100644
--- a/src/interface/abi/Tier2.idr
+++ b/src/interface/abi/Tier2.idr
@@ -5,8 +5,8 @@
 |||
 ||| Idris-side bindings to the *honest* C ABI exposed by the Zig shim
 ||| `ffi/zig/src/lib.zig` (`vclut_verify_wire`), which calls into the
-||| Rust crate `src/interface/attest` (`vclut_rs_verify`) — see
-||| `src/interface/attest/ATTESTATION-FORMAT.adoc` for the wire
+||| Rust crate `ffi/rust/attest` (`vclut_rs_verify`) — see
+||| `ffi/rust/attest/ATTESTATION-FORMAT.adoc` for the wire
 ||| contract and `docs/decisions/0002-ffi-attestation-trust-boundary.adoc`
 ||| for the trust model rationale.
 |||
@@ -35,13 +35,13 @@
 |||   (3) the Ed25519-dalek + sha2 implementation in the Tier-2 crate.
 |||
 ||| **Strictly weaker than Tier-1** (recompute-PCC over `wasm32`,
-||| `src/interface/recompute-wasm`), which trusts neither (1) nor (2)
+||| `ffi/rust/recompute-wasm`), which trusts neither (1) nor (2)
 ||| because the consumer re-runs the decision itself. Prefer Tier-1
 ||| where wasm hosting is available; Tier-2 is the C-ABI fallback.
 |||
 ||| **No proofs.** Like all FFI plumbing, this module contains no
 ||| theorems — its safety properties live in the Tier-2 Rust crate's
-||| tests (`src/interface/attest/src/lib.rs::tests` — roundtrip + 5
+||| tests (`ffi/rust/attest/src/lib.rs::tests` — roundtrip + 5
 ||| tamper variants + fail-closed + C-ABI). It is *not* in the
 ||| Idris2 proof corpus (`vclut-core.ipkg`); see
 ||| `verification/proofs/VERIFICATION-STANCE.adoc` §"Boundary model"
@@ -88,7 +88,7 @@ ed25519SeedSize = 32
 
 ||| The honest Tier-2 entry point. Bound to the Zig shim
 ||| `vclut_verify_wire` in `ffi/zig/src/lib.zig`, which calls
-||| `vclut_rs_verify` (`src/interface/attest/src/lib.rs`).
+||| `vclut_rs_verify` (`ffi/rust/attest/src/lib.rs`).
 |||
 ||| ABI:
 |||
diff --git a/src/interface/dap/src/lib.rs b/src/interface/dap/src/lib.rs
index 44382c4..3d36f17 100644
--- a/src/interface/dap/src/lib.rs
+++ b/src/interface/dap/src/lib.rs
@@ -1,10 +1,12 @@
-#![forbid(unsafe_code)]
 // SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 //! VCL-total DAP (Debug Adapter Protocol) Library
 //!
 //! Provides DAP message types and VCL query execution simulation
 //! for the VCL-total debug adapter.
 
+#![forbid(unsafe_code)]
+
 use serde::{Deserialize, Serialize};
 
 /// A DAP request from the client (editor).
diff --git a/src/interface/dap/src/main.rs b/src/interface/dap/src/main.rs
index 22afacc..34c289c 100644
--- a/src/interface/dap/src/main.rs
+++ b/src/interface/dap/src/main.rs
@@ -3,6 +3,8 @@
 //!
 //! This server provides DAP support for debugging VCL-total queries.
 
+#![forbid(unsafe_code)]
+
 use std::io::{BufRead, BufReader, Write};
 use std::net::{TcpListener, TcpStream};
 use vcltotal_dap::{dispatch_request, DapRequest};
diff --git a/src/interface/echidna-client/src/lib.rs b/src/interface/echidna-client/src/lib.rs
index b0c412d..174a11f 100644
--- a/src/interface/echidna-client/src/lib.rs
+++ b/src/interface/echidna-client/src/lib.rs
@@ -31,6 +31,8 @@
 //! [`vcltotal_interface`] re-exports and are used by callers that want to
 //! work in structured form.
 
+#![forbid(unsafe_code)]
+
 use thiserror::Error;
 
 pub use vcltotal_interface::{core, types};
diff --git a/src/interface/fmt/src/lib.rs b/src/interface/fmt/src/lib.rs
index c9612dd..4194803 100644
--- a/src/interface/fmt/src/lib.rs
+++ b/src/interface/fmt/src/lib.rs
@@ -1,4 +1,3 @@
-#![forbid(unsafe_code)]
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 //! VCL-total Formatting Library
@@ -6,6 +5,8 @@
 //! Provides formatting capabilities for VCL-total query files.
 //! Keywords are indented with two spaces for readability.
 
+#![forbid(unsafe_code)]
+
 /// Format VCL-total content by indenting lines that start with recognised keywords.
 ///
 /// Keywords recognised: SELECT, FROM, WHERE, GROUP, ORDER, HAVING, LIMIT.
diff --git a/src/interface/fmt/src/main.rs b/src/interface/fmt/src/main.rs
index 3ce0114..a1e4f25 100644
--- a/src/interface/fmt/src/main.rs
+++ b/src/interface/fmt/src/main.rs
@@ -3,6 +3,8 @@
 //!
 //! This tool formats VCL-total query files.
 
+#![forbid(unsafe_code)]
+
 use clap::Parser;
 use std::fs;
 use std::path::PathBuf;
diff --git a/src/interface/legacy/Foreign.idr b/src/interface/legacy/Foreign.idr
index 2a96208..9a04202 100644
--- a/src/interface/legacy/Foreign.idr
+++ b/src/interface/legacy/Foreign.idr
@@ -20,7 +20,7 @@
 ||| Use the new honest paths instead:
 |||
 |||   * **Tier-1 (recompute-PCC over `wasm32`)** — consumer re-runs
-|||     the certified decision via `src/interface/recompute-wasm`
+|||     the certified decision via `ffi/rust/recompute-wasm`
 |||     (`vcl_recompute`), comparing its verdict against the
 |||     producer's claim. No trusted certifier. See
 |||     `verification/proofs/VERIFICATION-STANCE.adoc` §"Boundary
@@ -28,7 +28,7 @@
 |||
 |||   * **Tier-2 (C-ABI Ed25519 signed attestation, FALLBACK)** —
 |||     producer signs `(sha256(stmt_wire), sha256(schema_wire),
-|||     level)`; consumer Ed25519-verifies. See `src/interface/attest`
+|||     level)`; consumer Ed25519-verifies. See `ffi/rust/attest`
 |||     (`vclut_rs_verify`) and the Idris bindings in
 |||     `VclTotal.ABI.Tier2` (`src/interface/abi/Tier2.idr`).
 |||
diff --git a/src/interface/lib.rs b/src/interface/lib.rs
index a61b558..4dfb0c7 100644
--- a/src/interface/lib.rs
+++ b/src/interface/lib.rs
@@ -10,6 +10,8 @@
 //! echidna-client) use this crate as their single import point for both
 //! sides of the vcl-ut ↔ echidna interface.
 
+#![forbid(unsafe_code)]
+
 /// Re-export echidna's canonical proof-surface types so callers don't need
 /// a direct dep on `echidna-core`. Covers Term, Goal, ProofState, Tactic,
 /// Hypothesis, Context, Theorem, Definition, Variable, Pattern,
diff --git a/src/interface/lint/src/lib.rs b/src/interface/lint/src/lib.rs
index c3c284e..7eed558 100644
--- a/src/interface/lint/src/lib.rs
+++ b/src/interface/lint/src/lib.rs
@@ -1,4 +1,3 @@
-#![forbid(unsafe_code)]
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 //! VCL-total Linting Library
@@ -6,6 +5,8 @@
 //! Provides linting capabilities for VCL-total query files.
 //! Checks for missing semicolons, lowercase keywords, SELECT *, and OFFSET without LIMIT.
 
+#![forbid(unsafe_code)]
+
 /// A single lint issue found in VCL-total content.
 #[derive(Debug)]
 pub struct LintIssue {
diff --git a/src/interface/lint/src/main.rs b/src/interface/lint/src/main.rs
index af8ee03..d056d25 100644
--- a/src/interface/lint/src/main.rs
+++ b/src/interface/lint/src/main.rs
@@ -3,6 +3,8 @@
 //!
 //! This tool lints VCL-total query files for syntax and style issues.
 
+#![forbid(unsafe_code)]
+
 use clap::Parser;
 use std::fs;
 use std::path::PathBuf;
diff --git a/src/interface/lsp/src/lib.rs b/src/interface/lsp/src/lib.rs
index 5b70ee9..51f67ca 100644
--- a/src/interface/lsp/src/lib.rs
+++ b/src/interface/lsp/src/lib.rs
@@ -1,9 +1,11 @@
-#![forbid(unsafe_code)]
 // SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 //! VCL-total LSP Library
 //!
 //! This library provides LSP support for VCL-total.
 
+#![forbid(unsafe_code)]
+
 use lsp_types::*;
 use std::collections::HashMap;
 
diff --git a/src/interface/lsp/src/main.rs b/src/interface/lsp/src/main.rs
index 6cace39..fa71a6b 100644
--- a/src/interface/lsp/src/main.rs
+++ b/src/interface/lsp/src/main.rs
@@ -6,6 +6,9 @@
 
 // Binary-side mirror of the `vclt-gate` posture: the server must report
 // failures to the client, never crash on them.
+
+#![forbid(unsafe_code)]
+
 #![deny(clippy::unwrap_used, clippy::expect_used)]
 
 use lsp_server::{Connection, Message, RequestId, Response};
diff --git a/src/interface/parse/src/ast.rs b/src/interface/parse/src/ast.rs
index 2a2365c..faab76f 100644
--- a/src/interface/parse/src/ast.rs
+++ b/src/interface/parse/src/ast.rs
@@ -290,10 +290,22 @@ pub enum RepairJustification {
 pub enum Transition {
     /// `TMerge left right into evidence level`: two DISTINCT inputs → one
     /// identity.
-    Merge(SubjectRef, SubjectRef, SubjectRef, Option<Expr>, SafetyLevel),
+    Merge(
+        SubjectRef,
+        SubjectRef,
+        SubjectRef,
+        Option<Expr>,
+        SafetyLevel,
+    ),
     /// `TSplit from outL outR evidence level`: one identity → two DISTINCT
     /// outputs.
-    Split(SubjectRef, SubjectRef, SubjectRef, Option<Expr>, SafetyLevel),
+    Split(
+        SubjectRef,
+        SubjectRef,
+        SubjectRef,
+        Option<Expr>,
+        SafetyLevel,
+    ),
     /// `TNormalise subject justification level`: repair transition, NO result
     /// set, justified.
     Normalise(SubjectRef, RepairJustification, SafetyLevel),
diff --git a/src/interface/parse/src/bin/vclt-gate.rs b/src/interface/parse/src/bin/vclt-gate.rs
index 673b16b..d239f31 100644
--- a/src/interface/parse/src/bin/vclt-gate.rs
+++ b/src/interface/parse/src/bin/vclt-gate.rs
@@ -15,6 +15,7 @@
 //! Pure function of (statement, schema): no network, no filesystem,
 //! no clock, no env-dependent behaviour beyond stdin/stdout/stderr.
 
+#![forbid(unsafe_code)]
 #![deny(clippy::unwrap_used, clippy::expect_used)]
 
 use serde_json::{json, Value};
diff --git a/src/interface/parse/src/decider.rs b/src/interface/parse/src/decider.rs
index ec9e706..494e503 100644
--- a/src/interface/parse/src/decider.rs
+++ b/src/interface/parse/src/decider.rs
@@ -611,14 +611,19 @@ fn evidence_injection_safe(t: &Transition) -> bool {
 /// `Transition.evidenceTypeCompat` — reuses the single-source-of-truth
 /// `whereComparisonsCompatible` decider on the evidence `Expr`. `None`
 /// evidence is vacuously compatible.
+///
+/// Returns whether every comparison in the evidence has compatible operand
+/// types resolved against `schema`; unresolved (`TAny`) types are compatible.
+/// Subquery contents are not checked. Evidence without comparisons returns `true`.
 fn evidence_type_compat(t: &Transition, schema: &OctadSchema) -> bool {
     match transition_evidence(t) {
         None => true,
         Some(e) => {
             let mut cs = Vec::new();
             extract_comparisons(e, &mut cs);
-            cs.iter()
-                .all(|(l, r)| types_compatible(&resolve_expr_type(l, schema), &resolve_expr_type(r, schema)))
+            cs.iter().all(|(l, r)| {
+                types_compatible(&resolve_expr_type(l, schema), &resolve_expr_type(r, schema))
+            })
         }
     }
 }
diff --git a/src/interface/parse/tests/conformance_emit.rs b/src/interface/parse/tests/conformance_emit.rs
index 4ce9ae6..bd531a3 100644
--- a/src/interface/parse/tests/conformance_emit.rs
+++ b/src/interface/parse/tests/conformance_emit.rs
@@ -214,7 +214,10 @@ fn emit() {
     // Transition recompute-tier verdicts (schema-independent for these
     // evidence-free fixtures): both admissible ⇒ InjectionProof = 4.
     println!("ctl1 = {}", certified_transition_level(&t_merge(), &sch1()));
-    println!("ctl2 = {}", certified_transition_level(&t_normalise(), &sch1()));
+    println!(
+        "ctl2 = {}",
+        certified_transition_level(&t_normalise(), &sch1())
+    );
 }
 
 /// Self-check: every fixture round-trips through the Rust codec, so the
diff --git a/src/interface/parse/tests/gate.rs b/src/interface/parse/tests/gate.rs
index fb89148..3b98850 100644
--- a/src/interface/parse/tests/gate.rs
+++ b/src/interface/parse/tests/gate.rs
@@ -77,7 +77,11 @@ fn fixture_admitted_assert_with_limit() {
     // Expr::Param (schema-unresolved) — passes L1 vacuously.
     let stmt = parse("ASSERT GRAPH.knows FROM HEXAD 'e-1' WHERE depth < 3 LIMIT 10")
         .expect("fixture 1 must parse");
-    assert_eq!(stmt.verb, Verb::Assert, "the ASSERT verb tag must be captured");
+    assert_eq!(
+        stmt.verb,
+        Verb::Assert,
+        "the ASSERT verb tag must be captured"
+    );
     let cert = certified_level(&stmt, &schema);
     assert_eq!(
         cert, 6,
@@ -183,8 +187,8 @@ fn s1_verb_tags_and_query_only_parse() {
         ("DECLARE", Verb::Declare),
         ("RETRACT", Verb::Retract),
     ] {
-        let stmt = parse(&format!("{kw} {body}"))
-            .unwrap_or_else(|e| panic!("{kw} should parse: {e:?}"));
+        let stmt =
+            parse(&format!("{kw} {body}")).unwrap_or_else(|e| panic!("{kw} should parse: {e:?}"));
         assert_eq!(stmt.verb, want, "{kw} must carry the {want:?} tag");
     }
     for kw in ["MERGE", "SPLIT", "NORMALISE"] {
diff --git a/src/interface/parse/tests/parse.rs b/src/interface/parse/tests/parse.rs
index b55a8c0..cb07dad 100644
--- a/src/interface/parse/tests/parse.rs
+++ b/src/interface/parse/tests/parse.rs
@@ -111,7 +111,10 @@ fn deep_parens_are_typed_error_not_overflow() {
 #[test]
 fn deep_not_chain_is_typed_error_not_overflow() {
     let msg = parse_on_gate_stack(|| {
-        let q = format!("SELECT * FROM STORE s WHERE {}GRAPH.x", "NOT ".repeat(100_000));
+        let q = format!(
+            "SELECT * FROM STORE s WHERE {}GRAPH.x",
+            "NOT ".repeat(100_000)
+        );
         parse(&q).err().map(|e| e.msg)
     });
     assert_eq!(
diff --git a/src/interface/parse/tests/wire.rs b/src/interface/parse/tests/wire.rs
index 897dbac..f83574d 100644
--- a/src/interface/parse/tests/wire.rs
+++ b/src/interface/parse/tests/wire.rs
@@ -413,6 +413,7 @@ fn decoder_rejects_deep_nesting_without_overflow() {
     schema.push(0); // graph modality = Graph
     schema.extend_from_slice(&1u32.to_le_bytes()); // one field
     schema.extend_from_slice(&0u32.to_le_bytes()); // field name ""
+
     // 200k nested TList tags (VqlType::TList == 8).
     schema.extend(std::iter::repeat_n(8u8, 200_000));
     // Hits the depth cap long before consuming the rest of the stream.
diff --git a/src/lib.rs b/src/lib.rs
index 6f45d76..ad8a96e 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -5,6 +5,8 @@
 //! This top-level crate re-exports the formatter and linter libraries
 //! for use in integration tests and downstream consumers.
 
+#![forbid(unsafe_code)]
+
 /// Re-export the VCL-total formatter.
 pub use vcltotal_fmt as fmt;
 
diff --git a/tests/aspect_tests.sh b/tests/aspect_tests.sh
index 5bcb14b..760ac9c 100644
--- a/tests/aspect_tests.sh
+++ b/tests/aspect_tests.sh
@@ -4,28 +4,30 @@
 #
 # tests/aspect_tests.sh — Aspect tests for vql-ut (VCL-total).
 #
-# Validates cross-cutting concerns over PRODUCTION source. The gate's
-# remit is *non-test* code: idiomatic test code legitimately uses
-# unwrap/expect (and a test harness' own `testing.expect`-style helpers),
-# so those are out of scope by design — see checks 2 and 3.
+# Validates cross-cutting concerns and the safe-source boundary
+# (vcl-ut#49). Rust code under src/ is safe Rust: the unsafe host/guest
+# (wasm) and C-ABI boundary crates live under ffi/rust/, never under src/.
 #
-#   1. SPDX licence headers on all src/ Rust files
-#   2. No UNDOCUMENTED unsafe in production src/. Audited FFI/WASM trust
-#      boundaries are permitted to contain `unsafe` (a cdylib's
-#      `#[no_mangle] extern "C"` entry *cannot* be written without it),
-#      but every `unsafe {` must carry a contiguous `// SAFETY:`
-#      justification — mirroring `clippy::undocumented_unsafe_blocks`.
-#   3. No .unwrap()/.expect()/panic!/unreachable!/todo!/unimplemented!
+#   1. SPDX licence header on the FIRST line of every src/ Rust file
+#   2. No unsafe Rust constructs anywhere under src/ (tests included):
+#      `unsafe {`, `unsafe fn|impl|trait|extern`, `#[unsafe(...)]`,
+#      `static mut`. FFI is isolated under ffi/rust/.
+#   3. Every Rust crate root under src/ (lib.rs, main.rs, bin/*.rs)
+#      carries `#![forbid(unsafe_code)]` — the compiler-level guard
+#      behind the lexical check 2.
+#   4. No .unwrap()/.expect()/panic!/unreachable!/todo!/unimplemented!
 #      in production (non-test) Rust src/ — the SPARK-grade fail-closed
 #      posture (cf. vcltotal-parse's deny lint-set, the estate pattern).
-#   4. HTTPS-only URLs
-#   5. No hardcoded secrets
-#   6. Totality marker: Cargo.lock committed (reproducible builds)
+#   5. HTTPS-only URLs
+#   6. No hardcoded secrets
+#   7. Totality marker: Cargo.lock committed (reproducible builds)
 #
-# "Production source" = *.rs under src/, EXCLUDING integration tests
-# (any path under a tests/ directory) and EXCLUDING #[cfg(test)] modules
-# (stripped below by brace depth). Non-Rust files (e.g. the Zig FFI shim)
-# are out of scope for the Rust-pattern checks 2 and 3.
+# "Production source" (check 4 only) = *.rs under src/, EXCLUDING
+# integration tests (any path under a tests/ directory) and EXCLUDING
+# #[cfg(test)] modules (stripped below by brace depth): idiomatic test code
+# legitimately uses unwrap/expect. Checks 1-3 cover test code too. Cargo
+# target/ directories are pruned everywhere. Non-Rust files (e.g. the Zig
+# FFI shim under ffi/zig) are out of scope for the Rust-pattern checks.
 
 set -euo pipefail
 
@@ -69,32 +71,81 @@ strip_cfg_test() {
         }'
 }
 
-# Production Rust sources: *.rs under src/, excluding integration tests.
-prod_rs_files() { find src/ -name '*.rs' 2>/dev/null | grep -v '/tests/' | sort; }
+# List every Rust source file under src/, tests included, skipping Cargo
+# target/ build output (which holds generated Rust).
+all_src_rs_files() {
+    find src/ -type d -name target -prune -o -type f -name '*.rs' -print | sort
+}
+
+# List the production Rust source files under src/: all_src_rs_files
+# minus integration tests (any path under a tests/ directory).
+prod_rs_files() { all_src_rs_files | grep -v '/tests/' || true; }
+
+# List the Rust crate roots under src/ (lib.rs, main.rs, src/bin/*.rs),
+# skipping Cargo target/ build output.
+crate_root_files() {
+    find src/ -type d -name target -prune -o -type f \
+        \( -name lib.rs -o -name main.rs -o -path '*/src/bin/*.rs' \) -print | sort
+}
 
 echo "=== VCL-total Aspect Tests ==="
 echo ""
 
-# 1. SPDX headers
-missing_spdx=$(find src/ -name '*.rs' 2>/dev/null \
-    | xargs grep -rL "SPDX-License-Identifier" 2>/dev/null | wc -l)
-check "SPDX headers on all src/ Rust files" "$([ "$missing_spdx" -eq 0 ] && echo 0 || echo 1)"
+# 1. SPDX header must be the first line, not merely present somewhere in
+#    the file (which let misplaced headers silently pass this gate). The
+#    expected string is split so REUSE does not read it as this file's own
+#    licence declaration.
+expected_spdx='// SPDX-License-'
+expected_spdx+='Identifier: MPL-2.0'
+missing_spdx=0
+while IFS= read -r f; do
+    if [ "$(head -n 1 "$f")" != "$expected_spdx" ]; then
+        echo "    missing/misplaced SPDX: $f"
+        missing_spdx=$((missing_spdx + 1))
+    fi
+done < <(all_src_rs_files)
+check "SPDX header on the first line of all src/ Rust files" \
+    "$([ "$missing_spdx" -eq 0 ] && echo 0 || echo 1)"
 
-# 2. No UNDOCUMENTED unsafe in production src/. Every `unsafe {` must be
-#    immediately preceded by a contiguous `// SAFETY:` justification.
-undoc_unsafe=0
+# 2. No unsafe Rust constructs anywhere under src/, tests included. The
+#    unsafe host/guest and C-ABI boundaries live under ffi/rust/.
+#    Carry a trailing unsafe token across blank/comment lines so the
+#    opening brace or declaration keyword can be on the following line.
+unsafe_hits=0
 while IFS= read -r f; do
-    n=$(strip_cfg_test < "$f" | awk '
-        /\/\/[[:space:]]*SAFETY/ { armed=1 }
-        /unsafe[[:space:]]*\{/   { if (!armed) bad++; armed=0; next }
-        ($0 !~ /^[[:space:]]*\/\//) && ($0 !~ /^[[:space:]]*$/) { armed=0 }
-        END { print bad+0 }')
-    undoc_unsafe=$((undoc_unsafe + n))
-done < <(prod_rs_files)
-check "No undocumented unsafe in production src/ (// SAFETY: required)" \
-    "$([ "$undoc_unsafe" -eq 0 ] && echo 0 || echo 1)"
+    n=$(awk -v f="$f" '
+        /^[[:space:]]*\/\// { next }
+        /^[[:space:]]*$/ { next }
+        {
+            line = pending_unsafe ? pending_unsafe : FNR
+            if (pending_unsafe) $0 = "unsafe " $0
+            pending_unsafe = ($0 ~ /(^|[^[:alnum:]_])unsafe[[:space:]]*$/) ? line : 0
+        }
+        /(^|[^[:alnum:]_])unsafe[[:space:]]*(\{|fn([^[:alnum:]_]|$)|extern([^[:alnum:]_]|$)|impl([^[:alnum:]_]|$)|trait([^[:alnum:]_]|$))/ \
+            { print "    unsafe: " f ":" line > "/dev/stderr"; bad++; next }
+        /#!?\[[[:space:]]*unsafe[[:space:]]*\(/ \
+            { print "    unsafe attribute: " f ":" FNR > "/dev/stderr"; bad++; next }
+        /(^|[^[:alnum:]_])static[[:space:]]+mut([^[:alnum:]_]|$)/ \
+            { print "    static mut: " f ":" FNR > "/dev/stderr"; bad++; next }
+        END { print bad+0 }' "$f")
+    unsafe_hits=$((unsafe_hits + n))
+done < <(all_src_rs_files)
+check "No unsafe Rust in src/ (FFI isolated under ffi/rust/)" \
+    "$([ "$unsafe_hits" -eq 0 ] && echo 0 || echo 1)"
+
+# 3. Every crate root under src/ forbids unsafe code at compile time, in
+#    addition to the lexical check above.
+missing_forbid=0
+while IFS= read -r f; do
+    if ! grep -q '^#!\[forbid(unsafe_code)\]' "$f"; then
+        echo "    missing #![forbid(unsafe_code)]: $f"
+        missing_forbid=$((missing_forbid + 1))
+    fi
+done < <(crate_root_files)
+check "All src/ Rust crate roots #![forbid(unsafe_code)]" \
+    "$([ "$missing_forbid" -eq 0 ] && echo 0 || echo 1)"
 
-# 3. No fail-open helpers in production (non-test) Rust src/: neither
+# 4. No fail-open helpers in production (non-test) Rust src/: neither
 #    .unwrap()/.expect() nor the panic family (`panic!`, `unreachable!`,
 #    `todo!`, `unimplemented!`). Mirrors the vcltotal-parse deny
 #    lint-set (the estate's SPARK-grade pattern).
@@ -106,16 +157,16 @@ done < <(prod_rs_files)
 check "No .unwrap()/.expect()/panic! in production src/" \
     "$([ "$failopen_hits" -eq 0 ] && echo 0 || echo 1)"
 
-# 4. HTTPS-only URLs
+# 5. HTTPS-only URLs
 http_hits=$(grep -rn 'http://[^l]' src/ 2>/dev/null | grep -v '#\|//' | wc -l || true)
 check "HTTPS-only URLs in source (no plain http://)" "$([ "$http_hits" -eq 0 ] && echo 0 || echo 1)"
 
-# 5. No hardcoded secrets
+# 6. No hardcoded secrets
 secret_hits=$(grep -rn 'password\s*=\s*["\x27][^"\x27]\|secret\s*=\s*["\x27][^"\x27]' \
     src/ 2>/dev/null | grep -iv 'test\|example\|placeholder' | wc -l || true)
 check "No hardcoded secrets in source" "$([ "$secret_hits" -eq 0 ] && echo 0 || echo 1)"
 
-# 6. Cargo.lock committed (reproducible builds)
+# 7. Cargo.lock committed (reproducible builds)
 check "Cargo.lock committed" "$([ -f Cargo.lock ] && echo 0 || echo 1)"
 
 echo ""
diff --git a/verification/proofs/VERIFICATION-STANCE.adoc b/verification/proofs/VERIFICATION-STANCE.adoc
index 96b49be..053e735 100644
--- a/verification/proofs/VERIFICATION-STANCE.adoc
+++ b/verification/proofs/VERIFICATION-STANCE.adoc
@@ -48,7 +48,7 @@ corpus compiles (**12 modules**: Phase 4 = `LayoutProofs` + L6–L10
 decoder + cross-language `Refl` conformance, the faithful Rust
 decision port, the recompute-`wasm32` artefact (**Tier-1
 recompute-PCC**), and the Ed25519 C-ABI attestation fallback
-(**Tier-2**, `src/interface/attest`, linked into the Zig shim) — both
+(**Tier-2**, `ffi/rust/attest`, linked into the Zig shim) — both
 **RESOLVED**, PRs #26/#28/#29/#30/#31/#32/#33 + P5d; see the canonical
 two-tier boundary model under "What is NOT proven").
 **Phase 2** de-vacuized L2/L3/L5
@@ -307,7 +307,7 @@ here.
   OWED: the *honest* Idris-side path is now
   **`VclTotal.ABI.Tier2`** at `src/interface/abi/Tier2.idr`, which
   binds `vclut_verify_wire` (Zig shim → `vclut_rs_verify` in
-  `src/interface/attest`) and returns a 65-byte Ed25519-signed
+  `ffi/rust/attest`) and returns a 65-byte Ed25519-signed
   attestation `[level:1][sig:64]` over `DOMAIN ‖ sha256(stmt_wire)
   ‖ sha256(schema_wire) ‖ level`. Trust-model ceiling is the same
   Tier-2 ceiling described under the boundary model below
@@ -315,7 +315,7 @@ here.
   than the deprecated asserted-integer path). The `Tier2.idr`
   module typechecks under idris2 0.8.0 (`--check` green) and
   carries no proofs (it is plumbing); the safety properties live
-  in `src/interface/attest/src/lib.rs::tests`.
+  in `ffi/rust/attest/src/lib.rs::tests`.
 . *(Phase 2 — RESOLVED) L2/L3/L5 predicates de-vacuized.* The
   content-free constructors (`ExprTypeSafe`/`WhereTypeSafe`,
   `AllNullableFieldsGuarded`'s `GuardedNull`, `AllSelectItemsTyped`'s
@@ -407,7 +407,7 @@ here.
 +
   ** *Tier-1 — recompute-PCC over `wasm32` (RESOLVED, the achieved
      tier).* The consumer is shipped the `wasm32` module
-     (`src/interface/recompute-wasm`, `vcl_recompute`) + the wire
+     (`ffi/rust/recompute-wasm`, `vcl_recompute`) + the wire
      bytes of a `(Statement, OctadSchema)` + the producer's claimed
      level, and **re-runs the certified decision itself**, comparing
      its verdict to the claim. This is proof-carrying code by
@@ -432,7 +432,7 @@ here.
      load-bearing only for a *proof-term-transport* design, which was
      **rejected** (Idris2 ships no embeddable verified core kernel;
      building one is its own subproject). `affinescriptiser` is *not*
-     used (disclosed, not an oversight — `src/interface/recompute-wasm/
+     used (disclosed, not an oversight — `ffi/rust/recompute-wasm/
      AFFINESCRIPTISER-NA.adoc`): it structurally requires ≥1
      `[[resources]]` and the entry is a pure resource-free verdict
      function (fabricating a resource to satisfy the tool would be the
@@ -444,7 +444,7 @@ here.
      RESOLVED).* A C ABI erases types to machine words, so it cannot
      transport a re-checkable dependent `SafetyCertificate`; over a C
      ABI the honest ceiling is *trusted-certifier attestation*, and
-     that ceiling is now reached. `src/interface/attest`
+     that ceiling is now reached. `ffi/rust/attest`
      (`vcltotal-attest`) mints an Ed25519 signature over
      `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level`, where
      `level` is the conformance-pinned `vcltotal_parse::certified_level`
@@ -462,7 +462,7 @@ here.
      (b) the certifier ran the pinned decider before signing —
      strictly weaker than Tier-1 (which trusts neither; it
      recomputes). Real key provisioning is deployment (estate token
-     vault). Spec: `src/interface/attest/ATTESTATION-FORMAT.adoc`;
+     vault). Spec: `ffi/rust/attest/ATTESTATION-FORMAT.adoc`;
      crypto (`ed25519-dalek`/`sha2`) is contained to this Tier-2 crate
      and never touches the zero-dep forbid-unsafe core.
 +
@@ -492,7 +492,7 @@ here.
   (P5c-5 #32) with the faithful Rust decision port machine-pinned to
   the corpus (P5c-2/3/4 #31). (4) *RESOLVED:* the P5d C-ABI
   signed-attestation *fallback* + `vclut_rs_verify` linkage (Tier-2,
-  `src/interface/attest`, linked into the Zig shim). **Nothing under
+  `ffi/rust/attest`, linked into the Zig shim). **Nothing under
   this issue's NAMED-OWED list remains** — what remains are the
   precisely-scoped *disclosed limitations* below, not gaps.
   *Disclosed limitations, not hidden gaps:* (i) the certified decoder
@@ -549,10 +549,10 @@ here.
   ceiling), but cryptographically bound and tamper-evident, with the
   Rust crate's test suite enforcing the fail-closed contract. For
   the strongest guarantee, use Tier-1 recompute-PCC over `wasm32`
-  (`src/interface/recompute-wasm`).
+  (`ffi/rust/recompute-wasm`).
 * *Transport (DELIVERED — Tier-1 recompute-PCC, P5c, vcl-ut#25).* The
   guarantee is **not** "trust our attestation". You are shipped the
-  `wasm32` module `src/interface/recompute-wasm` (`vcl_recompute`) +
+  `wasm32` module `ffi/rust/recompute-wasm` (`vcl_recompute`) +
   the `(Statement, OctadSchema)` wire bytes + the claimed level. **Run
   it and compare**: a match means *you* have independently
   re-established the corpus-proved verdict — your TCB is the
@@ -665,7 +665,7 @@ here.
   machine-pinned to the corpus's public deciders via `WireConformance`
   on shared golden bytes (find-dependent verdicts pinned Rust-side +
   by input-value conformance, disclosed). *P5c-5 (#32):* the
-  recompute **`wasm32` artefact** `src/interface/recompute-wasm`
+  recompute **`wasm32` artefact** `ffi/rust/recompute-wasm`
   (`vcl_recompute`, fail-closed, one audited host/guest unsafe block;
   all logic stays in the `#![forbid(unsafe_code)]` crate). Together
   these are **Tier-1 (recompute-PCC over `wasm32`), now RESOLVED** —
@@ -682,14 +682,14 @@ here.
   disclosed in `AFFINESCRIPTISER-NA.adoc`, not faked) and plain
   `wasm32` is sufficient because the wasm type system is not
   load-bearing under recompute.
-  *P5d (Tier-2 fallback) — RESOLVED:* `src/interface/attest`
+  *P5d (Tier-2 fallback) — RESOLVED:* `ffi/rust/attest`
   (`vcltotal-attest`) mints/verifies an Ed25519 attestation over
   `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level` (level =
   the pinned `certified_level`, signed iff `0..=10`, fail-closed); the
   previously-OWED `vclut_rs_verify` is this crate, linked into the
   `ffi/zig` shim (`vclut_verify_wire`) by `build.zig` with `zig build
   test` exercising the boundary end-to-end. Spec
-  `src/interface/attest/ATTESTATION-FORMAT.adoc`; crypto contained,
+  `ffi/rust/attest/ATTESTATION-FORMAT.adoc`; crypto contained,
   core untouched. The only remaining disclosed item is the *encode*
   direction (Idris→wire), which is **not a gap**: it is not required
   by either tier (the producer encodes from the trusted Rust side; the
@@ -717,11 +717,11 @@ P5a trusted Rust parser (#26); P5b-1 wire codec (#28); P5b-2
 decoder + `Refl` conformance (#29); P5c-1 certified `OctadSchema`
 codec (#30); P5c-2/3/4 `vcltotal_parse::decider` faithful Rust port
 of the corpus decision core, machine-pinned via `WireConformance`
-(#31); P5c-5 recompute `wasm32` artefact `src/interface/recompute-wasm`
+(#31); P5c-5 recompute `wasm32` artefact `ffi/rust/recompute-wasm`
 (fail-closed, one audited host/guest unsafe block) (#32); P5c-6 (#33)
 the Tier-1 `OWED→RESOLVED` stance flip + ADR
 `docs/decisions/0002-ffi-attestation-trust-boundary.adoc`. **P5d (this
-PR):** Tier-2 — `src/interface/attest` (`vcltotal-attest`) Ed25519
+PR):** Tier-2 — `ffi/rust/attest` (`vcltotal-attest`) Ed25519
 attestation mint/verify + the `vclut_rs_verify` backend linked into
 the `ffi/zig` shim (`vclut_verify_wire`, `zig build test` green
 end-to-end); ADR-0002 updated to Tier-2 RESOLVED. **Both tiers
@@ -763,7 +763,7 @@ total/zero-escape, `WireConformance` `Refl`-pinned to the Rust
 encoder); the decision core is a faithful Rust port machine-pinned to
 the corpus; the consumer re-runs it from a fail-closed `wasm32` module
 — *you re-validate, you do not trust a tag*. *Tier-2 (C-ABI
-attestation fallback, P5d):* `src/interface/attest` mints/verifies an
+attestation fallback, P5d):* `ffi/rust/attest` mints/verifies an
 Ed25519 token bound to `(sha256(stmt_wire), sha256(schema_wire),
 level)` (level = the pinned `certified_level`, fail-closed), with
 `vclut_rs_verify` linked into the Zig shim — for consumers that cannot