diff --git a/AGENTS.md b/AGENTS.md
index 2060575..25f4155 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -9,8 +9,8 @@
 This project uses **Rivet** for SDLC artifact traceability.
 - Config: `rivet.yaml`
 - Schemas: common, stpa, aspice, dev
-- Artifacts: 231 across 17 types
-- Validation: `rivet validate` (current status: 47 errors)
+- Artifacts: 252 across 17 types
+- Validation: `rivet validate` (current status: 95 errors)
 
 ## Available Commands
 
@@ -41,12 +41,12 @@ This project uses **Rivet** for SDLC artifact traceability.
 | `stakeholder-req` | 4 | Stakeholder requirement (SYS.1) |
 | `sub-hazard` | 3 | A refinement of a hazard into a more specific unsafe condition. |
 | `sw-arch-component` | 11 | Software architectural element (SWE.2) |
-| `sw-req` | 21 | Software requirement (SWE.1) |
+| `sw-req` | 26 | Software requirement (SWE.1) |
 | `sw-verification` | 12 | Software verification measure against SW requirements (SWE.6 — Software Verification) |
-| `sys-verification` | 27 | System verification measure against system requirements (SYS.5 — System Verification) |
+| `sys-verification` | 29 | System verification measure against system requirements (SYS.5 — System Verification) |
 | `system-arch-component` | 6 | System architectural element (SYS.3) |
 | `system-constraint` | 10 | A condition or behavior that must be satisfied to prevent a hazard. Each constraint is the inversion of a hazard. |
-| `system-req` | 54 | System requirement derived from stakeholder needs (SYS.2) |
+| `system-req` | 68 | System requirement derived from stakeholder needs (SYS.2) |
 | `uca` | 18 | An Unsafe Control Action — a control action that, in a particular context and worst-case environment, leads to a hazard. Four types (provably complete): 1. Not providing the control action leads to a hazard 2. Providing the control action leads to a hazard 3. Providing too early, too late, or in the wrong order 4. Control action stopped too soon or applied too long |
 | `design-decision` | 0 | An architectural or design decision with rationale |
 | `feature` | 0 | A user-visible capability or feature |
diff --git a/artifacts/cross-compilation.yaml b/artifacts/cross-compilation.yaml
new file mode 100644
index 0000000..079b784
--- /dev/null
+++ b/artifacts/cross-compilation.yaml
@@ -0,0 +1,375 @@
+# Cross-Compilation Toolchain Requirements (ASPICE SYS.2 / SWE.1)
+#
+# System: Synth -- WebAssembly-to-ARM Cortex-M AOT compiler
+#
+# Defines the cross-compilation toolchain requirements for producing
+# runnable firmware from synth-compiled relocatable objects. Covers
+# toolchain detection, kiln-builtins stub provisioning, Bazel hermetic
+# build integration, and the testing progression from emulation to
+# real hardware.
+#
+# Addresses issue #27 (ARM cross-compilation toolchain).
+# Extends: SL-001..SL-007 (static linking), CC-001..CC-008 (compilation chain).
+#
+# Format: rivet generic-yaml
+
+artifacts:
+  # ---------------------------------------------------------------------------
+  # System-level: cross-compilation toolchain
+  # ---------------------------------------------------------------------------
+
+  - id: XC-001
+    type: system-req
+    title: Minimal kiln-builtins stub for bare-metal Phase 1
+    description: >
+      A minimal kiln-builtins-stub.a shall be provided that resolves the
+      three undefined symbols emitted by synth-compiled objects:
+      __meld_dispatch_import (returns trap/-1 for all imports),
+      __meld_get_memory_base (returns pointer to static 64KB buffer in
+      .wasm_linear_memory), and cabi_realloc (bump allocator within
+      linear memory). This stub enables Phase 1 bare-metal testing
+      without requiring the full kiln runtime. The stub is cross-compiled
+      for thumbv7em-none-eabihf using arm-none-eabi-gcc or Rust
+      no_std with panic=abort.
+    status: draft
+    tags: [cross-compilation, kiln-builtins, stub, bare-metal, phase-1]
+    links:
+      - type: derives-from
+        target: CC-004
+      - type: derives-from
+        target: SL-003
+      - type: refines
+        target: KB-001
+      - type: refines
+        target: KB-003
+      - type: refines
+        target: KB-004
+    fields:
+      req-type: interface
+      priority: must
+      github-issue: 27
+      verification-criteria: >
+        arm-none-eabi-nm kiln-builtins-stub.a shows T (defined text)
+        for __meld_dispatch_import, __meld_get_memory_base, cabi_realloc;
+        linking with synth-compiled module.o produces firmware.elf with
+        no unresolved symbols.
+
+  - id: XC-002
+    type: system-req
+    title: Bazel-hermetic kiln-builtins stub build
+    description: >
+      The kiln-builtins-stub.a shall be buildable via Bazel as a
+      hermetic target using the ARM cross-compilation toolchain from
+      the Bazel toolchain registry. The Bazel rule shall produce a
+      static archive (.a) containing the stub symbols for the configured
+      ARM target triple. This enables CI to build and link firmware.elf
+      without requiring a locally installed arm-none-eabi-gcc.
+    status: draft
+    tags: [cross-compilation, bazel, hermetic, kiln-builtins]
+    links:
+      - type: derives-from
+        target: XC-001
+      - type: refines
+        target: CC-005
+    fields:
+      req-type: functional
+      priority: should
+      github-issue: 27
+      verification-criteria: >
+        bazel build //tests/compilation-chain:kiln-builtins-stub produces
+        a .a file; no local arm-none-eabi-gcc required.
+
+  - id: XC-003
+    type: system-req
+    title: ARM cross-linker auto-detection and invocation
+    description: >
+      synth-cli shall auto-detect the ARM cross-linker on the host system
+      and invoke it as a subprocess when the --link flag is provided. The
+      detection priority is: (1) --linker CLI flag, (2) SYNTH_LINKER
+      environment variable, (3) PATH search for arm-none-eabi-ld,
+      (4) PATH search for arm-zephyr-eabi-ld (Zephyr SDK), (5) PATH
+      search for ld.lld (LLVM linker with --target). If no linker is
+      found, synth shall emit a clear error message listing installation
+      options (brew install arm-none-eabi-gcc for macOS, apt install
+      gcc-arm-none-eabi for Linux).
+    status: draft
+    tags: [cross-compilation, linker, detection, cli]
+    links:
+      - type: derives-from
+        target: SL-001
+      - type: refines
+        target: CC-005
+      - type: refines
+        target: SL-TR-002
+    fields:
+      req-type: functional
+      priority: must
+      github-issue: 27
+      crate: synth-cli
+      verification-criteria: >
+        synth compile --link succeeds when arm-none-eabi-ld is on PATH;
+        clear error message when no linker found; --linker flag overrides
+        auto-detection.
+
+  - id: XC-004
+    type: system-req
+    title: "synth compile --link single-command firmware production"
+    description: >
+      synth-cli shall support a --link flag that orchestrates the
+      complete pipeline from WASM input to firmware.elf output in a
+      single invocation. When --link is provided, synth: (1) compiles
+      WASM to ARM producing module.o in a temp directory, (2) generates
+      a linker script for the target board, (3) invokes the ARM
+      cross-linker with module.o + kiln-builtins.a (from --builtins
+      flag) + linker script, (4) produces firmware.elf at the -o path.
+      This reduces the three-step manual process to one command.
+    status: draft
+    tags: [cross-compilation, cli, pipeline, single-command]
+    links:
+      - type: derives-from
+        target: CC-007
+      - type: derives-from
+        target: SL-TR-002
+      - type: refines
+        target: TR-003
+    fields:
+      req-type: functional
+      priority: should
+      github-issue: 27
+      crate: synth-cli
+      verification-criteria: >
+        synth compile module.wasm --link --builtins kiln-builtins.a
+        --target cortex-m4 -o firmware.elf produces a valid ET_EXEC ELF;
+        equivalent to manual synth compile + arm-none-eabi-ld.
+
+  - id: XC-005
+    type: system-req
+    title: Board-specific linker script generation via --board flag
+    description: >
+      synth-cli shall accept a --board flag (stm32f407, nrf52840, generic)
+      that selects the appropriate memory map for linker script generation.
+      When combined with --link, the generated linker script uses the
+      board's flash base/size and RAM base/size from the target platform
+      profiles (TP-002, TP-003, TP-008). Custom memory maps can be
+      provided via --flash-origin, --flash-size, --ram-origin, --ram-size
+      flags that override board defaults.
+    status: draft
+    tags: [cross-compilation, linker-script, board-profile]
+    links:
+      - type: derives-from
+        target: SL-002
+      - type: derives-from
+        target: TP-002
+      - type: derives-from
+        target: TP-003
+      - type: refines
+        target: SL-TR-001
+    fields:
+      req-type: functional
+      priority: should
+      crate: synth-cli
+      verification-criteria: >
+        synth compile --link --board stm32f407 generates linker script
+        with flash at 0x08000000; --board nrf52840 uses flash at 0x00000000;
+        --flash-origin overrides board default.
+
+  # ---------------------------------------------------------------------------
+  # Testing progression requirements
+  # ---------------------------------------------------------------------------
+
+  - id: XC-006
+    type: system-req
+    title: "Phase 1 testing: bare-metal Renode e2e test in CI"
+    description: >
+      The CI pipeline shall include a bare-metal end-to-end test that
+      exercises the complete Phase 1 pipeline: synth compile a WASM
+      module with one import, link with kiln-builtins-stub.a, and
+      execute on Renode Cortex-M4 emulator. The test validates: (1)
+      firmware.elf boots (Reset_Handler reaches user code), (2) WASM
+      function executes and produces correct result, (3) import dispatch
+      invokes the stub (trap/no-op). This test runs in Bazel CI via
+      rules_renode on every PR.
+    status: draft
+    tags: [cross-compilation, testing, renode, ci, phase-1]
+    links:
+      - type: derives-from
+        target: CC-006
+      - type: refines
+        target: E2E-VER-001
+      - type: refines
+        target: VER-005
+    fields:
+      req-type: functional
+      priority: must
+      github-issue: 27
+      verification-criteria: >
+        bazel test //tests/compilation-chain:bare_metal_e2e passes;
+        Renode log shows correct function result; no HardFault.
+
+  - id: XC-007
+    type: system-req
+    title: "Phase 2 testing: Zephyr QEMU integration test"
+    description: >
+      The CI pipeline shall include a Zephyr integration test that
+      builds a Zephyr application with synth-compiled assembly, runs
+      it on QEMU Cortex-M3, and verifies UART output. This validates
+      the Zephyr CMake integration path (ZI-001) with the actual Zephyr
+      build system. The test may run in a Zephyr Docker container if
+      the Zephyr SDK is not available on the CI host.
+    status: draft
+    tags: [cross-compilation, testing, zephyr, qemu, phase-2]
+    links:
+      - type: derives-from
+        target: ZI-001
+      - type: derives-from
+        target: ZI-005
+      - type: refines
+        target: VER-005
+    fields:
+      req-type: functional
+      priority: should
+      verification-criteria: >
+        west build -b qemu_cortex_m3 succeeds for examples/zephyr-poc;
+        QEMU output shows correct synth_add results.
+
+  - id: XC-008
+    type: system-req
+    title: "Phase 3 testing: STM32F4-Discovery hardware validation"
+    description: >
+      Firmware produced by the cross-compilation pipeline shall be
+      validated on a physical STM32F4-Discovery board. The test flashes
+      firmware.elf via OpenOCD or J-Link, monitors UART output at
+      115200 baud, and verifies that synth-compiled WASM functions
+      produce correct results on real silicon. This is a manual gate
+      test triggered before release milestones.
+    status: draft
+    tags: [cross-compilation, testing, hardware, stm32, phase-3]
+    links:
+      - type: derives-from
+        target: TP-002
+      - type: derives-from
+        target: ZI-006
+      - type: refines
+        target: VER-005
+    fields:
+      req-type: functional
+      priority: should
+      verification-criteria: >
+        OpenOCD flash succeeds; UART output matches expected results;
+        no HardFault on real STM32F407VG silicon.
+
+  - id: XC-009
+    type: system-req
+    title: "Phase 3 testing: nRF52840-DK hardware validation"
+    description: >
+      Firmware produced by the cross-compilation pipeline shall be
+      validated on a physical nRF52840-DK board. The test flashes via
+      J-Link (nRF52840-DK has onboard SEGGER), monitors UART output,
+      and verifies correct execution. The nRF52840 has a different
+      flash base (0x00000000 vs STM32's 0x08000000), validating that
+      the linker script generation correctly adapts to board profiles.
+    status: draft
+    tags: [cross-compilation, testing, hardware, nrf52840, phase-3]
+    links:
+      - type: derives-from
+        target: TP-003
+      - type: derives-from
+        target: ZI-006
+      - type: refines
+        target: VER-005
+    fields:
+      req-type: functional
+      priority: should
+      verification-criteria: >
+        J-Link flash succeeds; UART output correct; linker script uses
+        flash base 0x00000000 (not 0x08000000).
+
+  # ---------------------------------------------------------------------------
+  # SW-level requirements for cross-compilation in synth
+  # ---------------------------------------------------------------------------
+
+  - id: XC-TR-001
+    type: sw-req
+    title: ARM cross-linker subprocess invocation
+    description: >
+      synth-cli shall invoke the ARM cross-linker as a subprocess using
+      std::process::Command. The invocation shall pass: (1) -T <linker_script>
+      for the generated or user-provided linker script, (2) -o <output>
+      for the firmware.elf output path, (3) all input objects (module.o),
+      (4) all input libraries (kiln-builtins.a via --builtins), (5)
+      --gc-sections for dead code elimination. Linker stdout/stderr
+      shall be captured and re-emitted with synth context (which symbol
+      is unresolved, which object needs it). Non-zero exit codes from
+      the linker shall propagate as synth errors.
+    status: planned
+    tags: [cross-compilation, cli, subprocess, linker]
+    links:
+      - type: derives-from
+        target: XC-003
+      - type: derives-from
+        target: XC-004
+      - type: refines
+        target: SL-TR-002
+    fields:
+      req-type: functional
+      priority: must
+      crate: synth-cli
+      verification-criteria: >
+        synth compile --link invokes arm-none-eabi-ld with correct
+        arguments; linker errors reported with context; exit code
+        propagated.
+
+  - id: XC-TR-002
+    type: sw-req
+    title: Weak symbol fallback for __meld_get_memory_base
+    description: >
+      synth-backend shall emit a weak symbol definition for
+      __meld_get_memory_base that returns 0x20000000 (default SRAM base
+      for Cortex-M). This allows bare-metal firmware to link and boot
+      without kiln-builtins.a by using the weak default. When
+      kiln-builtins.a is linked, its strong symbol definition overrides
+      the weak default. The weak symbol shall be emitted in a separate
+      .text.synth.defaults section that can be gc-collected when not
+      needed.
+    status: planned
+    tags: [cross-compilation, weak-symbol, memory-base, bare-metal]
+    links:
+      - type: derives-from
+        target: KB-TR-005
+      - type: derives-from
+        target: SL-003
+    fields:
+      req-type: functional
+      priority: must
+      crate: synth-backend
+      verification-criteria: >
+        nm module.o shows W (weak) for __meld_get_memory_base;
+        linking without kiln-builtins.a uses weak default (0x20000000);
+        linking with kiln-builtins.a uses strong definition.
+
+  - id: XC-TR-003
+    type: sw-req
+    title: Target triple to linker flag mapping
+    description: >
+      synth-cli shall map target profiles to correct linker flags:
+      cortex-m4 -> arm-none-eabi-ld (no special flags, Thumb-2 default),
+      cortex-m4f -> arm-none-eabi-ld with -mfloat-abi=hard linkage,
+      cortex-m7dp -> arm-none-eabi-ld with double-precision FP linkage.
+      When using ld.lld, the mapping adds --target=thumbv7em-none-eabihf
+      for Cortex-M4F targets. The mapping is configured via the
+      TargetSpec and HardwareCapabilities structs.
+    status: planned
+    tags: [cross-compilation, target-triple, linker-flags]
+    links:
+      - type: derives-from
+        target: SL-001
+      - type: derives-from
+        target: TP-001
+    fields:
+      req-type: functional
+      priority: must
+      crate: synth-cli
+      verification-criteria: >
+        cortex-m4f target invokes linker with hard-float flags;
+        cortex-m3 target does not include FPU flags; ld.lld path
+        adds --target flag.
diff --git a/artifacts/gale-integration.yaml b/artifacts/gale-integration.yaml
new file mode 100644
index 0000000..84bb8c6
--- /dev/null
+++ b/artifacts/gale-integration.yaml
@@ -0,0 +1,326 @@
+# Gale Integration Requirements (ASPICE SYS.2 / SWE.1)
+#
+# System: Synth -- WebAssembly-to-ARM Cortex-M AOT compiler
+#
+# Defines how synth-compiled WASM modules integrate with gale's formally
+# verified kernel primitives for safety-critical embedded applications.
+# Covers both the Zephyr module path (Phase 1: C FFI shim) and the
+# Kiln host function path (Phase 2: direct Rust calls).
+#
+# Cross-repo references use gale: prefix for gale artifacts.
+#
+# Format: rivet generic-yaml
+
+artifacts:
+  # ---------------------------------------------------------------------------
+  # System-level: gale integration architecture
+  # ---------------------------------------------------------------------------
+
+  - id: GI-001
+    type: system-req
+    title: Gale Zephyr module co-deployment with synth-compiled modules
+    description: >
+      Synth-compiled WASM modules shall be deployable alongside gale's
+      formally verified kernel primitives in a single Zephyr application.
+      The Zephyr build system (west build) shall compile both: (1) synth
+      output (.s assembly files) via target_sources, and (2) gale's
+      libgale_ffi.a via the Zephyr module system (zephyr/module.yml,
+      CONFIG_GALE_KERNEL_SEM=y, etc.). The Zephyr C application code
+      serves as the integration layer, calling synth-compiled WASM
+      functions for application logic and using Zephyr kernel APIs
+      (which delegate to gale for verified arithmetic) for synchronization.
+      Both synth and gale target the same ARM triple
+      (thumbv7em-none-eabihf for Cortex-M4F).
+    status: draft
+    tags: [gale, zephyr, co-deployment, integration]
+    links:
+      - type: derives-from
+        target: ZI-001
+      - type: derives-from
+        target: BR-001
+      - type: derives-from
+        target: BR-003
+      - type: traces-to
+        target: gale:SYSREQ-SEM-001
+      - type: traces-to
+        target: gale:SYSREQ-MUT-001
+    fields:
+      req-type: interface
+      priority: must
+      verification-criteria: >
+        Zephyr application builds with both synth .s files and gale
+        Zephyr module enabled; application calls synth-compiled WASM
+        function and gale-verified semaphore in the same main().
+
+  - id: GI-002
+    type: system-req
+    title: Gale CMake Rust target triple compatibility with synth
+    description: >
+      Gale's Zephyr CMakeLists.txt and synth shall use compatible Rust
+      target triple selection logic for ARM Cortex-M. Both projects use
+      the same mapping: Cortex-M0 -> thumbv6m-none-eabi, Cortex-M3 ->
+      thumbv7m-none-eabi, Cortex-M4/M7 without FPU -> thumbv7em-none-eabi,
+      Cortex-M4/M7 with FPU -> thumbv7em-none-eabihf, Cortex-M33 ->
+      thumbv8m.main-none-eabi[hf]. The target profile definitions in
+      synth (TargetSpec, HardwareCapabilities) shall produce triples
+      that match gale's CMakeLists.txt RUST_TARGET variable for the
+      same Zephyr CONFIG_CPU_* selection.
+    status: draft
+    tags: [gale, target-triple, compatibility, cortex-m]
+    links:
+      - type: derives-from
+        target: TP-001
+      - type: derives-from
+        target: TP-004
+      - type: derives-from
+        target: TP-005
+      - type: traces-to
+        target: gale:STKH-001
+    fields:
+      req-type: interface
+      priority: must
+      verification-criteria: >
+        For each supported Cortex-M variant, synth's TargetSpec::triple()
+        matches gale's CMakeLists.txt RUST_TARGET for the same
+        CONFIG_CPU_* / CONFIG_FPU combination.
+
+  - id: GI-003
+    type: system-req
+    title: WASM task isolation via gale kernel primitives
+    description: >
+      Multi-component WASM applications compiled by synth shall use
+      gale kernel primitives for inter-component synchronization and
+      communication. Each WASM component instance runs in its own
+      Zephyr thread with an MPU-isolated linear memory region. Gale
+      provides the synchronization primitives: semaphores for producer-
+      consumer signaling, mutexes for shared resource protection,
+      message queues for typed inter-component messages, and pipes for
+      byte-stream communication. The synth-compiled code accesses these
+      primitives via kiln-builtins import dispatch, which routes to
+      gale's Rust implementation (Phase 2) or via Zephyr C APIs that
+      delegate to gale (Phase 1).
+    status: draft
+    tags: [gale, isolation, multi-component, wasm-tasks]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: derives-from
+        target: FR-008
+      - type: derives-from
+        target: ZI-003
+      - type: traces-to
+        target: CM-005
+      - type: traces-to
+        target: gale:STKH-002
+      - type: traces-to
+        target: gale:SYSREQ-KILN-001
+    fields:
+      req-type: functional
+      priority: should
+      verification-criteria: >
+        Two synth-compiled WASM components communicate via gale message
+        queue on Renode Cortex-M4; MPU regions isolate each component's
+        linear memory; semaphore coordinates execution order.
+
+  - id: GI-004
+    type: system-req
+    title: Gale WIT interfaces for kernel object imports (Phase 2)
+    description: >
+      WIT interface definitions shall be created for gale kernel objects
+      enabling WASM components to import kernel primitives as typed
+      resources. The WIT interfaces define: resource sem (init, give,
+      take, reset, count-get), resource mutex (lock, unlock),
+      resource condvar (signal, broadcast, wait), resource msgq (put,
+      get, peek), resource pipe (write, read), and resource stack (push,
+      pop). These WIT definitions are consumed by meld for component
+      lowering and by synth for canonical ABI stub generation. The WIT
+      definitions match gale's Rust API signatures as specified in
+      gale:SWREQ-KILN-001.
+    status: draft
+    tags: [gale, wit, component-model, kernel-objects, phase-2]
+    links:
+      - type: derives-from
+        target: CM-002
+      - type: derives-from
+        target: FR-001
+      - type: traces-to
+        target: gale:SWREQ-KILN-001
+      - type: traces-to
+        target: gale:SWREQ-KILN-002
+    fields:
+      req-type: interface
+      priority: should
+      verification-criteria: >
+        WIT interfaces compile with wit-bindgen; canonical ABI lowering
+        for each operation matches gale's Rust function signature;
+        synth generates correct import stubs for each WIT operation.
+
+  - id: GI-005
+    type: system-req
+    title: End-to-end verified compilation chain with gale
+    description: >
+      The end-to-end compilation chain shall maintain verified
+      correctness from gale source through to ARM binary execution.
+      The chain is: gale Rust source (Verus SMT proofs for functional
+      correctness) -> gale plain/ (Rocq proofs for refinement properties)
+      -> WASM (via Kiln host function registration) -> synth AOT
+      compilation (Rocq proofs for ARM codegen correctness). Each link
+      in the chain has formal verification: gale proves the kernel
+      primitive is correct, synth proves the compilation preserves
+      semantics. The gap is the Kiln host function boundary, which is
+      covered by ABI compatibility tests (CM-001, CM-VER-002).
+    status: draft
+    tags: [gale, verified-pipeline, end-to-end, safety-critical]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: derives-from
+        target: FR-006
+      - type: traces-to
+        target: gale:SYSREQ-KILN-002
+      - type: traces-to
+        target: gale:SWREQ-KILN-004
+      - type: traces-to
+        target: VER-001
+    fields:
+      req-type: safety
+      priority: must
+      verification-criteria: >
+        Gale Verus proofs pass (all kernel primitives verified); synth
+        Rocq proofs pass (all i32 operations T1-verified); ABI
+        compatibility tests pass between synth-abi and kiln canonical
+        ABI; no Admitted lemmas in critical path.
+
+  # ---------------------------------------------------------------------------
+  # SW-level requirements for gale integration in synth
+  # ---------------------------------------------------------------------------
+
+  - id: GI-TR-001
+    type: sw-req
+    title: Kernel object import stub generation for gale WIT interfaces
+    description: >
+      synth-synthesis shall generate ARM call stubs for gale kernel
+      object WIT imports. Each kernel object operation (e.g., sem.give,
+      mutex.lock) generates a BL to the corresponding kiln dispatch
+      index. The stub handles canonical ABI lowering of the resource
+      handle (u32 index) and operation-specific parameters. For Phase 1,
+      the stubs target __meld_dispatch_import with the appropriate import
+      index. For Phase 2 (per-import direct dispatch), the stubs target
+      __meld_import_N with arguments directly in R0-R3.
+    status: planned
+    tags: [gale, codegen, import-stub, wit]
+    links:
+      - type: derives-from
+        target: GI-004
+      - type: derives-from
+        target: KB-TR-001
+      - type: derives-from
+        target: KB-TR-002
+    fields:
+      req-type: functional
+      priority: should
+      crate: synth-synthesis
+      verification-criteria: >
+        Synth compiles a WASM module importing sem.give to ARM code
+        containing BL __meld_dispatch_import with correct import index;
+        resource handle passed in R0 per AAPCS.
+
+  - id: GI-TR-002
+    type: sw-req
+    title: Zephyr prj.conf generation with gale Kconfig
+    description: >
+      synth-cli shall support generating Zephyr project configuration
+      (prj.conf) that includes gale Kconfig options alongside synth's
+      requirements. When --gale-primitives=sem,mutex is specified, the
+      generated prj.conf includes CONFIG_GALE_KERNEL_SEM=y and
+      CONFIG_GALE_KERNEL_MUTEX=y in addition to CONFIG_PRINTK=y and
+      CONFIG_CONSOLE=y. This simplifies the Zephyr project setup for
+      applications using both synth and gale.
+    status: planned
+    tags: [gale, zephyr, kconfig, cli]
+    links:
+      - type: derives-from
+        target: GI-001
+      - type: derives-from
+        target: ZI-004
+    fields:
+      req-type: functional
+      priority: could
+      crate: synth-cli
+      verification-criteria: >
+        synth init-zephyr --gale-primitives=sem,mutex generates prj.conf
+        with correct Kconfig settings; west build succeeds with the
+        generated configuration.
+
+  # ---------------------------------------------------------------------------
+  # Verification for gale integration
+  # ---------------------------------------------------------------------------
+
+  - id: GI-VER-001
+    type: sys-verification
+    title: "Zephyr + synth + gale co-deployment test"
+    description: >
+      Integration test verifying that a Zephyr application can
+      simultaneously use synth-compiled WASM functions and gale-verified
+      kernel primitives. The test application: (1) calls a synth-compiled
+      add function, (2) initializes a gale semaphore via Zephyr k_sem_init,
+      (3) gives the semaphore, (4) takes the semaphore, (5) prints
+      results via printk. This validates that libgale_ffi.a and synth
+      assembly link without symbol conflicts and execute correctly
+      together.
+    status: planned
+    tags: [gale, integration-test, zephyr, co-deployment]
+    links:
+      - type: verifies
+        target: GI-001
+      - type: verifies
+        target: GI-002
+    fields:
+      method: simulation
+      preconditions:
+        - Zephyr SDK available
+        - Gale checkout at known path
+        - synth-compiled .s file for test module
+      steps:
+        - "west build -b qemu_cortex_m3 with both synth and gale"
+        - "Verify UART output: add result correct + sem give/take succeeds"
+      pass-criteria: >
+        Application builds with no linker errors; UART shows correct
+        add result; k_sem_give and k_sem_take succeed using gale's
+        verified implementation.
+
+  - id: GI-VER-002
+    type: sys-verification
+    title: "Multi-component WASM isolation test with gale primitives"
+    description: >
+      End-to-end test verifying that two synth-compiled WASM components
+      communicate via a gale message queue with MPU-isolated linear
+      memories. Component A produces values and enqueues them via
+      k_msgq_put (verified by gale MQ1-MQ13). Component B dequeues
+      and processes values. Each component's linear memory is in a
+      separate MPU region. The test validates: (1) message queue
+      operations use gale-verified index arithmetic, (2) MPU fault
+      occurs if one component accesses the other's memory, (3) correct
+      values are transferred end-to-end.
+    status: planned
+    tags: [gale, integration-test, isolation, multi-component]
+    links:
+      - type: verifies
+        target: GI-003
+      - type: verifies
+        target: GI-005
+    fields:
+      method: simulation
+      preconditions:
+        - Renode with MPU emulation
+        - Two synth-compiled WASM components
+        - Gale message queue enabled
+      steps:
+        - "Build Zephyr application with two synth components + gale msgq"
+        - "Run on Renode with MPU region monitoring"
+        - "Verify values transfer correctly via message queue"
+        - "Verify MPU fault on cross-component memory access"
+      pass-criteria: >
+        Messages transfer correctly via gale-verified msgq; MPU fault
+        triggered on cross-component access; gale MQ index arithmetic
+        proven correct via Verus proofs.
diff --git a/crates/synth-backend/src/arm_encoder.rs b/crates/synth-backend/src/arm_encoder.rs
index 08ac65b..d2f2c6c 100644
--- a/crates/synth-backend/src/arm_encoder.rs
+++ b/crates/synth-backend/src/arm_encoder.rs
@@ -2407,14 +2407,23 @@ impl ArmEncoder {
                     // Total offset = SignExtend(S:I1:I2:imm10:imm11:0)
                     // where I1 = NOT(J1 XOR S), I2 = NOT(J2 XOR S)
 
-                    let offset = halfword_offset >> 1; // Convert to word offset for encoding
-                    let s = if offset < 0 { 1u32 } else { 0u32 };
-                    let imm10 = ((offset >> 11) as u32) & 0x3FF;
-                    let imm11 = (offset as u32) & 0x7FF;
-                    let i1 = if s == 0 { 1 } else { 0 }; // J1 when S=0: I1=1, so J1=0
-                    let i2 = if s == 0 { 1 } else { 0 }; // J2 when S=0: I2=1, so J2=0
-                    let j1 = if s == 1 { i1 } else { 1 - i1 };
-                    let j2 = if s == 1 { i2 } else { 1 - i2 };
+                    // The B.W (T4) encoding packs the signed offset as:
+                    //   S:I1:I2:imm10:imm11:0  (25-bit signed, halfword-aligned)
+                    // where J1 = NOT(I1 XOR S), J2 = NOT(I2 XOR S)
+                    // Input halfword_offset already equals (target - PC - 4) / 2,
+                    // so the full byte offset = halfword_offset << 1.
+                    // The encoding fields split that 25-bit signed value (including the
+                    // implicit trailing zero) as: S | imm10 | imm11
+                    // with I1 = bit 23 and I2 = bit 22 of the signed offset.
+                    let signed_offset = halfword_offset << 1; // byte offset
+                    let s = if signed_offset < 0 { 1u32 } else { 0u32 };
+                    let uoffset = signed_offset as u32;
+                    let imm10 = (uoffset >> 12) & 0x3FF; // bits [21:12]
+                    let imm11 = (uoffset >> 1) & 0x7FF; // bits [11:1]
+                    let i1 = (uoffset >> 23) & 1; // bit 23
+                    let i2 = (uoffset >> 22) & 1; // bit 22
+                    let j1 = (!(i1 ^ s)) & 1; // J1 = NOT(I1 XOR S)
+                    let j2 = (!(i2 ^ s)) & 1; // J2 = NOT(I2 XOR S)
 
                     let hw1: u16 = (0xF000 | (s << 10) | imm10) as u16;
                     let hw2: u16 = (0x9000 | (j1 << 13) | (j2 << 11) | imm11) as u16;
diff --git a/crates/synth-backend/src/cortex_m.rs b/crates/synth-backend/src/cortex_m.rs
index 679b05c..7d89712 100644
--- a/crates/synth-backend/src/cortex_m.rs
+++ b/crates/synth-backend/src/cortex_m.rs
@@ -72,6 +72,8 @@ pub struct StartupCode {
     pub bss_end: u32,
     /// Enable FPU (set CPACR for CP10+CP11 full access)
     pub enable_fpu: bool,
+    /// Linear memory size in bytes (stored in R10 for memory.size)
+    pub memory_size: u32,
 }
 
 impl StartupCode {
@@ -86,6 +88,7 @@ impl StartupCode {
             bss_start: 0,
             bss_end: 0,
             enable_fpu: false,
+            memory_size: 64 * 1024, // Default 64KB linear memory
         }
     }
 
@@ -143,11 +146,39 @@ impl StartupCode {
         // For 0x2000: imm4=2, i=0, imm3=0, imm8=0
         code.extend_from_slice(&[0xC2, 0xF2, 0x00, 0x0B]); // MOVT R11, #0x2000
 
+        // Initialize R10 with linear memory size in bytes (for memory.size instruction)
+        // memory.size does LSR R10, #16 to convert bytes to WASM pages (65536 bytes/page)
+        {
+            let lo16 = self.memory_size & 0xFFFF;
+            let hi16 = self.memory_size >> 16;
+
+            // Thumb-2 MOVW R10, #lo16
+            // Encoding: 1111 0 i 10 0 1 0 0 imm4 | 0 imm3 Rd imm8
+            // Rd = R10 = 0xA
+            let i_bit = (lo16 >> 11) & 1;
+            let imm4 = (lo16 >> 12) & 0xF;
+            let imm3 = (lo16 >> 8) & 0x7;
+            let imm8 = lo16 & 0xFF;
+            let hw1 = (0xF240 | (i_bit << 10) | imm4) as u16;
+            let hw2 = ((imm3 << 12) | (0xA << 8) | imm8) as u16;
+            code.extend_from_slice(&hw1.to_le_bytes());
+            code.extend_from_slice(&hw2.to_le_bytes());
+
+            // Thumb-2 MOVT R10, #hi16
+            let i_bit = (hi16 >> 11) & 1;
+            let imm4 = (hi16 >> 12) & 0xF;
+            let imm3 = (hi16 >> 8) & 0x7;
+            let imm8 = hi16 & 0xFF;
+            let hw1 = (0xF2C0 | (i_bit << 10) | imm4) as u16;
+            let hw2 = ((imm3 << 12) | (0xA << 8) | imm8) as u16;
+            code.extend_from_slice(&hw1.to_le_bytes());
+            code.extend_from_slice(&hw2.to_le_bytes());
+        }
+
         // Load entry point into R0
-        // LDR r0, [pc, #offset] (load from PC+4+offset, aligned)
-        // After MOVW+MOVT (8 bytes), we have: LDR, BLX, B, padding, literal
-        // PC = current + 4 (Thumb pipeline)
-        // Literal is at PC + 4 (after BLX and B.W)
+        // LDR r0, [pc, #offset] (load from Align(PC,4) + imm*4)
+        // From here: LDR(2), BLX(2), B(2), NOP(2), literal(4)
+        // PC = LDR_addr + 4; Align(PC,4) + 4 = literal address
         code.extend_from_slice(&[0x01, 0x48]); // LDR r0, [pc, #4]
 
         // Thumb encoding for: BLX r0
diff --git a/crates/synth-backend/src/elf_builder.rs b/crates/synth-backend/src/elf_builder.rs
index c7abc6c..6161c41 100644
--- a/crates/synth-backend/src/elf_builder.rs
+++ b/crates/synth-backend/src/elf_builder.rs
@@ -394,8 +394,15 @@ impl ElfBuilder {
     }
 
     /// Set entry point
+    ///
+    /// For ARM (Thumb) targets, bit 0 is automatically set to indicate Thumb mode.
+    /// Cortex-M is Thumb-only, so function addresses in ELF must have bit 0 set.
     pub fn with_entry(mut self, entry: u32) -> Self {
-        self.entry = entry;
+        self.entry = if self.machine == ElfMachine::Arm {
+            entry | 1 // Set Thumb bit for ARM targets
+        } else {
+            entry
+        };
         self
     }
 
@@ -766,7 +773,14 @@ impl ElfBuilder {
             symtab.extend_from_slice(&name_offset.to_le_bytes());
 
             // st_value (4 bytes)
-            symtab.extend_from_slice(&symbol.value.to_le_bytes());
+            // For ARM targets, STT_FUNC symbols must have bit 0 set (Thumb interworking)
+            let value = if self.machine == ElfMachine::Arm && symbol.symbol_type == SymbolType::Func
+            {
+                symbol.value | 1
+            } else {
+                symbol.value
+            };
+            symtab.extend_from_slice(&value.to_le_bytes());
 
             // st_size (4 bytes)
             symtab.extend_from_slice(&symbol.size.to_le_bytes());
@@ -1177,7 +1191,7 @@ mod tests {
         assert!(elf.len() > 52); // At least header size
         assert!(elf.len() < 10000); // Reasonable upper bound
 
-        // Validate entry point is set correctly
+        // Validate entry point is set correctly (Thumb bit set for ARM)
         let entry_bytes = &elf[24..28];
         let entry = u32::from_le_bytes([
             entry_bytes[0],
@@ -1185,7 +1199,7 @@ mod tests {
             entry_bytes[2],
             entry_bytes[3],
         ]);
-        assert_eq!(entry, 0x8000);
+        assert_eq!(entry, 0x8001); // 0x8000 | 1 (Thumb bit)
 
         // Validate section header offset is non-zero
         let sh_off_bytes = &elf[32..36];
@@ -1303,6 +1317,7 @@ mod tests {
 
         // Second symbol should have correct encoding
         // Check st_value (bytes 4-7 of second entry)
+        // For ARM STT_FUNC symbols, bit 0 is set for Thumb interworking
         let value_bytes = &symtab[20..24];
         let value = u32::from_le_bytes([
             value_bytes[0],
@@ -1310,7 +1325,7 @@ mod tests {
             value_bytes[2],
             value_bytes[3],
         ]);
-        assert_eq!(value, 0x1000);
+        assert_eq!(value, 0x1001); // 0x1000 | 1 (Thumb bit)
 
         // Check st_size (bytes 8-11 of second entry)
         let size_bytes = &symtab[24..28];
diff --git a/crates/synth-backend/src/linker_script.rs b/crates/synth-backend/src/linker_script.rs
index 55c184f..6cb6d05 100644
--- a/crates/synth-backend/src/linker_script.rs
+++ b/crates/synth-backend/src/linker_script.rs
@@ -156,7 +156,7 @@ impl LinkerScriptGenerator {
         // .isr_vector section (interrupt vector table)
         script.push_str("  .isr_vector :\n");
         script.push_str("  {\n");
-        script.push_str("    . = ALIGN(128);  /* Vector table must be 128-byte aligned */\n");
+        script.push_str("    . = ALIGN(256);  /* Vector table must be aligned to next power-of-2 >= table size */\n");
         script.push_str("    KEEP(*(.isr_vector))\n");
         script.push_str("    . = ALIGN(4);\n");
         script.push_str("  } >FLASH\n\n");
@@ -387,8 +387,8 @@ mod tests {
         let generator = LinkerScriptGenerator::new_stm32();
         let script = generator.generate().expect("Failed to generate");
 
-        // Vector table must be 128-byte aligned
-        assert!(script.contains("ALIGN(128)"));
+        // Vector table must be 256-byte aligned (power-of-2 >= table size)
+        assert!(script.contains("ALIGN(256)"));
         // Other sections should be 4-byte aligned
         assert!(script.contains("ALIGN(4)"));
     }
diff --git a/crates/synth-backend/src/mpu.rs b/crates/synth-backend/src/mpu.rs
index fe17150..5c34c24 100644
--- a/crates/synth-backend/src/mpu.rs
+++ b/crates/synth-backend/src/mpu.rs
@@ -168,12 +168,15 @@ impl MPUAttributes {
         }
     }
 
-    /// Device memory (non-cacheable, non-bufferable)
+    /// Device memory (non-cacheable, bufferable)
+    ///
+    /// Per ARM architecture: Device memory has TEX=0b000, C=0, B=1.
+    /// This distinguishes it from Strongly-ordered (TEX=0b000, C=0, B=0).
     pub fn device() -> Self {
         Self {
             shareable: true,
             cacheable: false,
-            bufferable: false,
+            bufferable: true,
             execute_never: true,
         }
     }
diff --git a/crates/synth-backend/src/reset_handler.rs b/crates/synth-backend/src/reset_handler.rs
index 34f6b15..1121d79 100644
--- a/crates/synth-backend/src/reset_handler.rs
+++ b/crates/synth-backend/src/reset_handler.rs
@@ -4,7 +4,7 @@
 
 use crate::arm_encoder::ArmEncoder;
 use synth_core::Result;
-use synth_synthesis::{ArmOp, Operand2, Reg};
+use synth_synthesis::{ArmOp, MemAddr, Operand2, Reg};
 
 /// Reset handler generator
 pub struct ResetHandlerGenerator {
@@ -60,53 +60,148 @@ impl ResetHandlerGenerator {
         let mut instrs = Vec::new();
 
         // Copy .data section from Flash to RAM
-        // R0 = source (Flash)
-        // R1 = destination (RAM)
-        // R2 = end address
+        // R0 = source (Flash load address)
+        // R1 = destination (RAM data start)
+        // R2 = end address (RAM data end)
 
-        // Load data_load_addr into R0
-        instrs.push(ArmOp::Mov {
+        // Load data_load_addr into R0 using MOVW/MOVT (full 32-bit)
+        instrs.push(ArmOp::Movw {
+            rd: Reg::R0,
+            imm16: (self.data_load_addr & 0xFFFF) as u16,
+        });
+        instrs.push(ArmOp::Movt {
             rd: Reg::R0,
-            op2: Operand2::Imm((self.data_load_addr >> 16) as i32),
+            imm16: (self.data_load_addr >> 16) as u16,
         });
-        // Would use MOVT for upper 16 bits in real impl
 
         // Load data_start into R1
-        instrs.push(ArmOp::Mov {
+        instrs.push(ArmOp::Movw {
+            rd: Reg::R1,
+            imm16: (self.data_start & 0xFFFF) as u16,
+        });
+        instrs.push(ArmOp::Movt {
             rd: Reg::R1,
-            op2: Operand2::Imm((self.data_start >> 16) as i32),
+            imm16: (self.data_start >> 16) as u16,
         });
 
         // Load data_end into R2
-        instrs.push(ArmOp::Mov {
+        instrs.push(ArmOp::Movw {
+            rd: Reg::R2,
+            imm16: (self.data_end & 0xFFFF) as u16,
+        });
+        instrs.push(ArmOp::Movt {
             rd: Reg::R2,
-            op2: Operand2::Imm((self.data_end >> 16) as i32),
+            imm16: (self.data_end >> 16) as u16,
         });
 
-        // Copy loop label would go here
-        // For simplicity, using a simple sequence
+        // .data copy loop: copy words from Flash (R0) to RAM (R1) until R1 == R2
+        // .Lcopy_check:
+        instrs.push(ArmOp::Label {
+            name: ".Lcopy_check".to_string(),
+        });
+        instrs.push(ArmOp::Cmp {
+            rn: Reg::R1,
+            op2: Operand2::Reg(Reg::R2),
+        });
+        // BHS .Lcopy_done (branch if R1 >= R2, i.e., done)
+        instrs.push(ArmOp::Bhs {
+            label: ".Lcopy_done".to_string(),
+        });
+        // LDR R3, [R0], #4 — load word from source, post-increment
+        // Using explicit load + add since post-increment may not be available
+        instrs.push(ArmOp::Ldr {
+            rd: Reg::R3,
+            addr: MemAddr {
+                base: Reg::R0,
+                offset: 0,
+                offset_reg: None,
+            },
+        });
+        instrs.push(ArmOp::Add {
+            rd: Reg::R0,
+            rn: Reg::R0,
+            op2: Operand2::Imm(4),
+        });
+        // STR R3, [R1], #4 — store word to dest, post-increment
+        instrs.push(ArmOp::Str {
+            rd: Reg::R3,
+            addr: MemAddr {
+                base: Reg::R1,
+                offset: 0,
+                offset_reg: None,
+            },
+        });
+        instrs.push(ArmOp::Add {
+            rd: Reg::R1,
+            rn: Reg::R1,
+            op2: Operand2::Imm(4),
+        });
+        // B .Lcopy_check
+        instrs.push(ArmOp::B {
+            label: ".Lcopy_check".to_string(),
+        });
+        instrs.push(ArmOp::Label {
+            name: ".Lcopy_done".to_string(),
+        });
 
         // Zero .bss section
-        // R0 = start address
-        // R1 = end address
-        // R2 = zero value
+        // R0 = bss start, R1 = bss end, R2 = zero value
+        instrs.push(ArmOp::Movw {
+            rd: Reg::R0,
+            imm16: (self.bss_start & 0xFFFF) as u16,
+        });
+        instrs.push(ArmOp::Movt {
+            rd: Reg::R0,
+            imm16: (self.bss_start >> 16) as u16,
+        });
+
+        instrs.push(ArmOp::Movw {
+            rd: Reg::R1,
+            imm16: (self.bss_end & 0xFFFF) as u16,
+        });
+        instrs.push(ArmOp::Movt {
+            rd: Reg::R1,
+            imm16: (self.bss_end >> 16) as u16,
+        });
 
         instrs.push(ArmOp::Mov {
             rd: Reg::R2,
             op2: Operand2::Imm(0),
         });
 
-        instrs.push(ArmOp::Mov {
+        // .bss zero loop: zero words from R0 to R1
+        // .Lzero_check:
+        instrs.push(ArmOp::Label {
+            name: ".Lzero_check".to_string(),
+        });
+        instrs.push(ArmOp::Cmp {
+            rn: Reg::R0,
+            op2: Operand2::Reg(Reg::R1),
+        });
+        // BHS .Lzero_done (branch if R0 >= R1)
+        instrs.push(ArmOp::Bhs {
+            label: ".Lzero_done".to_string(),
+        });
+        instrs.push(ArmOp::Str {
+            rd: Reg::R2,
+            addr: MemAddr {
+                base: Reg::R0,
+                offset: 0,
+                offset_reg: None,
+            },
+        });
+        instrs.push(ArmOp::Add {
             rd: Reg::R0,
-            op2: Operand2::Imm((self.bss_start >> 16) as i32),
+            rn: Reg::R0,
+            op2: Operand2::Imm(4),
         });
-
-        instrs.push(ArmOp::Mov {
-            rd: Reg::R1,
-            op2: Operand2::Imm((self.bss_end >> 16) as i32),
+        // B .Lzero_check
+        instrs.push(ArmOp::B {
+            label: ".Lzero_check".to_string(),
+        });
+        instrs.push(ArmOp::Label {
+            name: ".Lzero_done".to_string(),
         });
-
-        // Zero loop would go here
 
         // Call main
         instrs.push(ArmOp::Bl {
diff --git a/crates/synth-backend/tests/integration_test.rs b/crates/synth-backend/tests/integration_test.rs
index 01e60f3..545f8b7 100644
--- a/crates/synth-backend/tests/integration_test.rs
+++ b/crates/synth-backend/tests/integration_test.rs
@@ -78,7 +78,7 @@ fn test_end_to_end_pipeline() {
         entry_bytes[2],
         entry_bytes[3],
     ]);
-    assert_eq!(entry, 0x8000);
+    assert_eq!(entry, 0x8001); // 0x8000 | 1 (Thumb bit for ARM)
 
     println!("✓ End-to-end pipeline test passed!");
     println!("  - Generated {} WASM ops", wasm_ops.len());
diff --git a/crates/synth-backend/tests/linker_integration_test.rs b/crates/synth-backend/tests/linker_integration_test.rs
index 1650f25..473cae5 100644
--- a/crates/synth-backend/tests/linker_integration_test.rs
+++ b/crates/synth-backend/tests/linker_integration_test.rs
@@ -146,8 +146,8 @@ fn test_alignment_requirements() {
     let generator = LinkerScriptGenerator::new_stm32();
     let script = generator.generate().expect("Failed to generate");
 
-    // Vector table must be 128-byte aligned (ARM Cortex-M requirement)
-    assert!(script.contains("ALIGN(128)"));
+    // Vector table must be 256-byte aligned (power-of-2 >= table size for ARM Cortex-M)
+    assert!(script.contains("ALIGN(256)"));
 
     // Data sections should be 4-byte aligned
     let align_4_count = script.matches("ALIGN(4)").count();
diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs
index d433149..201edeb 100644
--- a/crates/synth-cli/src/main.rs
+++ b/crates/synth-cli/src/main.rs
@@ -2317,7 +2317,10 @@ mod tests {
 
         // Verify entry point is 0x8000
         let entry = u32::from_le_bytes([elf_data[24], elf_data[25], elf_data[26], elf_data[27]]);
-        assert_eq!(entry, 0x8000, "Entry point should be 0x8000");
+        assert_eq!(
+            entry, 0x8001,
+            "Entry point should be 0x8001 (0x8000 | Thumb bit)"
+        );
     }
 
     #[test]
diff --git a/docs/design/cross-compilation-pipeline.md b/docs/design/cross-compilation-pipeline.md
new file mode 100644
index 0000000..4b552b0
--- /dev/null
+++ b/docs/design/cross-compilation-pipeline.md
@@ -0,0 +1,537 @@
+# Cross-Compilation Pipeline Design
+
+Issue #27 -- ARM cross-compilation toolchain for producing runnable firmware.
+
+## Status
+
+Draft -- 2026-03-21
+
+## Overview
+
+This document defines the complete cross-compilation pipeline from WASM Component
+to runnable firmware on ARM Cortex-M targets. The pipeline spans three phases:
+bare-metal (no OS), Zephyr RTOS integration, and real hardware deployment. It
+covers the roles of all PulseEngine components (synth, kiln, gale, meld) and the
+testing strategy from emulation through hardware.
+
+## Architecture Diagram
+
+```
+                          PulseEngine Cross-Compilation Pipeline
+                          ==========================================
+
+  +-----------------+       +-----------+       +-----------------+
+  | WASM Component  | ----> |   Meld    | ----> | Core WASM (.wasm)|
+  | (.wasm + .wit)  |       | (fuser)   |       | (host imports)   |
+  +-----------------+       +-----------+       +-----------------+
+                                                        |
+                                                        v
+                                                +-----------------+
+                                                |     Synth       |
+                                                | (AOT compiler)  |
+                                                +-----------------+
+                                                        |
+                                          +-------------+-------------+
+                                          |                           |
+                                          v                           v
+                                  +---------------+           +---------------+
+                                  | module.o      |           | module.s      |
+                                  | (relocatable  |           | (assembly,    |
+                                  |  ELF, ET_REL) |           |  Zephyr path) |
+                                  +---------------+           +---------------+
+                                          |                           |
+        +-----------------+               |                           |
+        | kiln-builtins.a |               |                           |
+        | (C ABI bridge,  |               |                           |
+        |  no_std, ARM)   |               |                           |
+        +-----------------+               |                           |
+                |                         |                           |
+                +-------+-----------------+                           |
+                        |                                             |
+                        v                                             v
+                +------------------+                    +----------------------------+
+                | arm-none-eabi-ld |                    |  Zephyr Build (west build) |
+                | + linker script  |                    |  CMakeLists.txt includes   |
+                +------------------+                    |  module.s as target_source |
+                        |                               +----------------------------+
+                        v                                             |
+                +------------------+                                  v
+                | firmware.elf     |                    +----------------------------+
+                | (bare-metal,     |                    | zephyr.elf                 |
+                |  standalone)     |                    | (Zephyr firmware with      |
+                +------------------+                    |  synth + gale + kiln)      |
+                        |                               +----------------------------+
+                        |                                             |
+          +-------------+-------------+                 +-------------+-------------+
+          |             |             |                 |             |             |
+          v             v             v                 v             v             v
+     +---------+   +---------+   +--------+       +---------+   +---------+   +--------+
+     | Renode  |   | QEMU    |   | J-Link |       | Renode  |   | QEMU    |   | J-Link |
+     | (CM4)   |   | (CM3)   |   | (HW)   |       | (CM4)   |   | (CM3)   |   | (HW)   |
+     +---------+   +---------+   +--------+       +---------+   +---------+   +--------+
+```
+
+## Phase 1 -- Bare-Metal (No OS)
+
+### Goal
+
+Produce a standalone firmware.elf from a WASM module that boots and executes on a
+Cortex-M4 emulator without any RTOS. This validates the core compilation chain
+end-to-end.
+
+### Build Steps
+
+```
+# Step 1: Compile WASM to relocatable ELF
+synth compile module.wasm --target cortex-m4 -o module.o
+
+# Step 2: Link with kiln-builtins stub and generated linker script
+arm-none-eabi-ld -T synth_cortex_m4.ld module.o kiln-builtins.a -o firmware.elf
+
+# Step 3: Execute on Renode emulator
+renode --execute "sysbus LoadELF @firmware.elf; start"
+```
+
+### module.o Format (Relocatable ELF)
+
+Synth emits a relocatable ELF object (ET_REL) containing:
+
+| Section             | Type        | Placement | Content |
+|---------------------|-------------|-----------|---------|
+| `.text`             | SHT_PROGBITS | FLASH    | Compiled ARM Thumb-2 code |
+| `.meld_import_table`| SHT_PROGBITS | FLASH    | Import descriptor array (KB-005 format) |
+| `.meld_import_strings` | SHT_PROGBITS | FLASH | Module/field name strings |
+| `.symtab`           | SHT_SYMTAB  | --        | Symbol table (UND for imports, GLOBAL for exports) |
+| `.strtab`           | SHT_STRTAB  | --        | String table |
+| `.rel.text`         | SHT_REL     | --        | R_ARM_THM_CALL relocations for import BLs |
+
+Undefined symbols emitted by synth:
+- `__meld_dispatch_import` -- generic import dispatch (or `__meld_import_N` per-import)
+- `__meld_get_memory_base` -- linear memory base address accessor
+- `cabi_realloc` -- canonical ABI memory allocator
+
+### kiln-builtins.a (Minimal Stub for Phase 1)
+
+For Phase 1, a minimal stub library provides the three required symbols:
+
+```c
+// kiln-builtins-stub.c -- minimal Phase 1 stub
+#include <stdint.h>
+
+// Linear memory region (statically allocated in RAM)
+static uint8_t __wasm_memory[65536] __attribute__((section(".wasm_linear_memory")));
+
+int32_t __meld_dispatch_import(uint32_t import_index,
+                                const void *args,
+                                uint32_t args_len,
+                                void *ret) {
+    // Phase 1: no host functions, return trap
+    return -1;
+}
+
+uint8_t* __meld_get_memory_base(uint32_t memory_index) {
+    return __wasm_memory;
+}
+
+uint8_t* cabi_realloc(uint8_t *old_ptr, uint32_t old_size,
+                       uint32_t align, uint32_t new_size) {
+    // Phase 1: bump allocator within linear memory
+    static uint32_t bump_offset = 0;
+    uint32_t aligned = (bump_offset + align - 1) & ~(align - 1);
+    bump_offset = aligned + new_size;
+    return &__wasm_memory[aligned];
+}
+```
+
+Cross-compile with: `arm-none-eabi-gcc -mcpu=cortex-m4 -mthumb -c -o kiln-builtins.o`
+
+### Linker Script
+
+Generated by `LinkerScriptGenerator::new_stm32().with_meld_integration().with_wasm_memory(65536)`:
+
+```
+ENTRY(Reset_Handler)
+EXTERN(__meld_dispatch_import)
+EXTERN(__meld_get_memory_base)
+
+MEMORY {
+  FLASH (rx):  ORIGIN = 0x08000000, LENGTH = 0x80000    /* 512 KB */
+  RAM   (rwx): ORIGIN = 0x20000000, LENGTH = 0x20000    /* 128 KB */
+}
+
+SECTIONS {
+  .isr_vector : { ALIGN(128); KEEP(*(.isr_vector)) } >FLASH
+  .text       : { *(.text) *(.text.*) } >FLASH
+  .meld_import_table : { KEEP(*(.meld.imports)) } >FLASH
+  .rodata     : { *(.rodata) *(.rodata*) } >FLASH
+  .data       : { *(.data) } >RAM AT> FLASH
+  .bss        : { *(.bss) } >RAM
+  .wasm_linear_memory (NOLOAD) : { . = . + 0x10000; } >RAM
+  .stack      : { . = . + 0x1000; _estack = .; } >RAM
+}
+```
+
+### CI Integration via Bazel
+
+```python
+# tests/compilation-chain/BUILD.bazel
+
+sh_test(
+    name = "bare_metal_e2e",
+    srcs = ["bare_metal_e2e_test.sh"],
+    data = [
+        "//crates:synth",
+        "//tests/compilation-chain:test_import.wat",
+        "//tests/compilation-chain:kiln-builtins-stub.a",
+        "//tests/compilation-chain:synth_cortex_m4.ld",
+    ],
+    tags = ["integration", "arm"],
+    deps = [
+        "@bazel_tools//tools/bash/runfiles",
+    ],
+)
+
+# Renode emulation test (requires rules_renode)
+renode_test(
+    name = "bare_metal_renode",
+    firmware = ":bare_metal_e2e",
+    platform = "//tests:synth_cortex_m.repl",
+    robot = "bare_metal_test.robot",
+    tags = ["renode", "emulation"],
+)
+```
+
+### Toolchain Detection
+
+Synth detects the ARM cross-linker in priority order:
+1. `--linker <path>` CLI flag
+2. `SYNTH_LINKER` environment variable
+3. PATH search for: `arm-none-eabi-ld`, `arm-zephyr-eabi-ld`, `ld.lld`
+
+---
+
+## Phase 2 -- Zephyr RTOS Integration
+
+### Goal
+
+Integrate synth-compiled WASM modules with Zephyr applications, with gale kernel
+primitives available for task isolation and kiln-builtins providing WASI dispatch
+through Zephyr APIs.
+
+### Architecture
+
+```
++------------------------------------------------------------------+
+|                     Zephyr Application                            |
+|                                                                    |
+|  +--------------------+  +------------------+  +----------------+ |
+|  | main.c             |  | synth module.s   |  | gale (Zephyr   | |
+|  | (Zephyr app logic) |  | (WASM->ARM, .s)  |  |  module via    | |
+|  |                    |  |                  |  |  libgale_ffi.a) | |
+|  | extern int32_t     |  | .global func_0  |  |                | |
+|  |   func_0(...);     |  | func_0:         |  | gale_sem_*     | |
+|  |                    |  |   push {r4,lr}   |  | gale_mutex_*   | |
+|  | result =           |  |   ...ARM code... |  | gale_msgq_*    | |
+|  |   func_0(a, b);    |  |   pop {r4,pc}   |  | gale_pipe_*    | |
+|  +--------------------+  +------------------+  +----------------+ |
+|                                                                    |
+|  +--------------------+  +------------------+                     |
+|  | kiln-builtins.a    |  | Zephyr kernel    |                     |
+|  | (dispatch, memory, |  | (scheduler,      |                     |
+|  |  cabi_realloc)     |  |  drivers, HAL)   |                     |
+|  +--------------------+  +------------------+                     |
++------------------------------------------------------------------+
+|                        Hardware (Cortex-M4)                        |
++------------------------------------------------------------------+
+```
+
+### Build Steps (Assembly Path)
+
+This path integrates synth output as assembly into the Zephyr build system,
+matching the existing `examples/zephyr-poc/` and `examples/pid-controller/` patterns:
+
+```bash
+# Step 1: Compile WASM to ARM assembly
+synth compile module.wasm --target cortex-m4 --output-format asm -o module.s
+
+# Step 2: Build with Zephyr (west build system)
+cd my-zephyr-app/
+west build -b stm32f4_disco
+```
+
+CMakeLists.txt:
+```cmake
+cmake_minimum_required(VERSION 3.20.0)
+find_package(Zephyr REQUIRED HINTS $ENV{ZEPHYR_BASE})
+project(my_wasm_app)
+
+target_sources(app PRIVATE src/main.c)
+target_sources(app PRIVATE src/module.s)       # Synth-compiled WASM
+
+# Optional: gale kernel primitives (if Zephyr module path includes gale)
+# set(EXTRA_ZEPHYR_MODULES /path/to/gale ${EXTRA_ZEPHYR_MODULES})
+```
+
+prj.conf:
+```ini
+CONFIG_PRINTK=y
+CONFIG_CONSOLE=y
+# For gale integration:
+# CONFIG_GALE_KERNEL_SEM=y
+# CONFIG_GALE_KERNEL_MUTEX=y
+# For MPU protection of WASM linear memory:
+# CONFIG_ARM_MPU=y
+# CONFIG_MPU_ALLOW_FLASH_WRITE=n
+```
+
+### Build Steps (Object Path -- Full Pipeline)
+
+For modules with host imports requiring kiln-builtins:
+
+```bash
+# Step 1: Compile WASM to relocatable ELF
+synth compile module.wasm --target cortex-m4 -o module.o
+
+# Step 2: Build kiln-builtins for ARM
+cd ../kiln && cargo build -p kiln-builtins --target thumbv7em-none-eabihf --release
+
+# Step 3: Integrate with Zephyr via external library
+# CMakeLists.txt uses target_link_libraries for module.o and kiln-builtins.a
+```
+
+### Gale Integration
+
+Gale provides formally verified Zephyr kernel primitives accessible to
+synth-compiled WASM modules via the Kiln runtime:
+
+**Path A -- Direct Zephyr Module (Phase 1, current):**
+- Gale is a Zephyr module (zephyr/module.yml)
+- C shim bridges Zephyr k_sem/k_mutex/etc. API to Rust FFI
+- CONFIG_GALE_KERNEL_SEM=y replaces kernel/sem.c count arithmetic
+- No direct WASM access -- Zephyr C code calls gale, synth code calls Zephyr
+
+**Path B -- Kiln Host Functions (Phase 2, planned per gale STKH-002):**
+- Gale primitives linked directly into Kiln as Rust crate (no C FFI)
+- WIT interfaces define kernel object operations
+- WASM components import kernel objects via WIT
+- Synth compiles imports as BL to kiln dispatch
+- Call path: WASM import -> kiln dispatch -> gale Rust method
+
+Gale primitives available:
+
+| Primitive | Zephyr Module | FFI Functions | Verified Properties |
+|-----------|---------------|---------------|---------------------|
+| Semaphore | CONFIG_GALE_KERNEL_SEM | gale_sem_count_init/give/take | P1-P3, P5-P6, P9 |
+| Mutex | CONFIG_GALE_KERNEL_MUTEX | gale_mutex_lock/unlock_validate | M3-M7, M10 |
+| Condvar | CONFIG_GALE_KERNEL_CONDVAR | (pure wait queue, no FFI) | C1-C8 |
+| Message Queue | CONFIG_GALE_KERNEL_MSGQ | gale_msgq_init/put/get/peek | MQ1-MQ13 |
+| Stack (LIFO) | CONFIG_GALE_KERNEL_STACK | gale_stack_init/push/pop_validate | SK1-SK9 |
+| Pipe | CONFIG_GALE_KERNEL_PIPE | gale_pipe_write/read_check | PP1-PP10 |
+| Timer | (planned) | -- | TM1-TM8 |
+| Event | (planned) | -- | EV1-EV8 |
+| Mem Slab | (planned) | -- | MS1-MS8 |
+
+### WASM Task Isolation via Gale
+
+For multi-component embedded applications, gale primitives provide the
+isolation boundary between WASM modules:
+
+1. Each WASM component runs in its own Zephyr thread
+2. Gale semaphores/mutexes coordinate access to shared resources
+3. Gale message queues provide inter-component communication
+4. MPU regions isolate each component's linear memory
+5. kiln-builtins mediates all cross-component calls via Meld dispatch
+
+---
+
+## Phase 3 -- Real Hardware
+
+### Goal
+
+Execute synth-compiled firmware on physical ARM Cortex-M boards, validating the
+full pipeline from WASM to silicon.
+
+### Target Boards
+
+| Board | SoC | CPU | Flash | RAM | MPU | FPU | Target Triple |
+|-------|-----|-----|-------|-----|-----|-----|---------------|
+| STM32F4-Discovery | STM32F407VG | Cortex-M4F | 1 MB @ 0x08000000 | 192 KB @ 0x20000000 | 8 regions | SP VFP | thumbv7em-none-eabihf |
+| nRF52840-DK | nRF52840 | Cortex-M4F | 1 MB @ 0x00000000 | 256 KB @ 0x20000000 | 8 regions | SP VFP | thumbv7em-none-eabihf |
+
+### Deployment
+
+```bash
+# Via Zephyr west (preferred)
+west flash -b stm32f4_disco
+
+# Via OpenOCD (bare-metal)
+openocd -f board/stm32f4discovery.cfg \
+  -c "program firmware.elf verify reset exit"
+
+# Via J-Link (nRF52840-DK)
+JLinkExe -device nRF52840_xxAA -if SWD -speed 4000 \
+  -CommanderScript flash.jlink
+```
+
+### UART Verification
+
+```bash
+# Monitor UART output for test pass/fail
+minicom -D /dev/ttyACM0 -b 115200
+
+# Expected output for calculator test:
+# synth_add(5, 42) = 47
+# synth_multiply(6, 7) = 42
+```
+
+---
+
+## Testing Strategy
+
+### Progression: Emulation to Hardware
+
+```
+Level 1: Unit Tests (cargo test --workspace)
+  - Instruction encoding correctness
+  - ELF structure validation (synth_elf_integration_test.sh)
+  - Relocation emission (synth_static_link_test.sh)
+  - Meld ABI pipeline (meld_abi_test.rs)
+  - 526+ tests, no hardware required
+
+Level 2: Renode Emulation (bazel test //tests/...)
+  - Full Cortex-M4 emulation with NVIC, SysTick, UART
+  - WAST test suite via synth-test -> Robot Framework
+  - End-to-end: WASM -> compile -> link -> boot -> execute -> verify output
+  - Platform: synth_cortex_m.repl (generic CM4 @ 0x0/0x20000000)
+
+Level 3: Zephyr QEMU (west build -b qemu_cortex_m3)
+  - Zephyr scheduler, drivers, printk via QEMU
+  - Tests: zephyr-poc, pid-controller, calculator
+  - Validates Zephyr CMake integration path
+
+Level 4: Zephyr + Gale (west build with EXTRA_ZEPHYR_MODULES=gale)
+  - Gale kernel primitives active (CONFIG_GALE_KERNEL_SEM=y, etc.)
+  - Tests: multi-threaded WASM with semaphore coordination
+  - Validates gale FFI -> Rust -> ARM -> Zephyr integration
+
+Level 5: Real Hardware (west flash -b nrf52840dk/nrf52840)
+  - Physical nRF52840-DK or STM32F4-Discovery
+  - UART output verification via serial console
+  - Validates: clock configuration, flash XIP, real MPU, real interrupts
+```
+
+### CI Pipeline
+
+```
+GitHub Actions / Bazel CI:
+  - Level 1: Always (cargo test, clippy, fmt)
+  - Level 2: Always (Renode via rules_renode, hermetic)
+  - Level 3: Gated on Zephyr SDK availability (optional)
+  - Level 4: Gated on both Zephyr SDK and gale checkout
+  - Level 5: Manual trigger, requires physical hardware runner
+```
+
+---
+
+## Cross-Repository Dependencies
+
+```
+                      +-----------+
+                      |   meld    |
+                      | (fuser)  |
+                      +-----+-----+
+                            |
+                            | Core WASM with
+                            | canonical ABI wrappers
+                            v
+    +-----------+     +-----------+     +-----------+
+    |   gale    |     |   synth   |     |   kiln    |
+    | (kernel   |     | (AOT      |     | (runtime, |
+    |  prims)   |     |  compiler)|     |  builtins)|
+    +-----------+     +-----------+     +-----------+
+         |                  |                  |
+         | Zephyr module    | module.o         | kiln-builtins.a
+         | (libgale_ffi.a)  | (ET_REL)         | (no_std ARM)
+         |                  |                  |
+         +--------+---------+--------+---------+
+                  |                  |
+                  v                  v
+           +-----------+     +-----------+
+           | Zephyr    |     | arm-none- |
+           | (west     |     | eabi-ld   |
+           |  build)   |     | (linker)  |
+           +-----------+     +-----------+
+                  |                  |
+                  v                  v
+           +-----------+     +-----------+
+           | zephyr.elf|     |firmware.elf|
+           +-----------+     +-----------+
+```
+
+### Dependency Matrix
+
+| Produces | Consumes | Interface | Status |
+|----------|----------|-----------|--------|
+| meld | synth | Core WASM (.wasm) | Draft (CC-002) |
+| synth | arm-none-eabi-ld | module.o (ET_REL) | Implemented (CC-003) |
+| synth | Zephyr CMake | module.s (assembly) | Implemented (ZI-001) |
+| kiln | arm-none-eabi-ld | kiln-builtins.a | Draft (CC-004) |
+| gale | Zephyr CMake | libgale_ffi.a + C shims | Implemented |
+| arm-none-eabi-ld | Renode/hardware | firmware.elf (ET_EXEC) | Draft (CC-005) |
+| Zephyr (west) | Renode/hardware | zephyr.elf | Implemented (ZI-001) |
+
+### Version Compatibility
+
+All PulseEngine repos target:
+- Rust edition 2024, MSRV 1.88
+- Bazel 8.x with bzlmod
+- ARM target: thumbv7em-none-eabihf (Cortex-M4F with hardware float)
+- Gale and synth both use the same Rust target triple detection logic
+
+---
+
+## Implementation Plan
+
+### Phase 1 Milestones (Issue #27)
+
+| # | Task | Artifacts | Estimate |
+|---|------|-----------|----------|
+| 1 | Create kiln-builtins-stub.a (minimal) | XC-001, XC-002 | 1 day |
+| 2 | Add `synth compile --link` CLI flag | SL-TR-002 | 2 days |
+| 3 | Linker detection and invocation | SL-001, XC-003 | 1 day |
+| 4 | Bare-metal Renode e2e test | E2E-VER-001 | 2 days |
+| 5 | Bazel CI integration | E2E-VER-007, XC-006 | 1 day |
+| 6 | Startup code: `__meld_get_memory_base` | KB-TR-005 | 1 day |
+
+### Phase 2 Milestones
+
+| # | Task | Artifacts | Estimate |
+|---|------|-----------|----------|
+| 7 | Zephyr + synth + gale CMake integration | GI-001, GI-002 | 2 days |
+| 8 | kiln-builtins with WASI stdout | E2E-VER-003 | 3 days |
+| 9 | Multi-component isolation demo | GI-003 | 3 days |
+| 10 | Zephyr QEMU CI test | XC-007 | 1 day |
+
+### Phase 3 Milestones
+
+| # | Task | Artifacts | Estimate |
+|---|------|-----------|----------|
+| 11 | STM32F4-Discovery flash test | XC-008 | 1 day |
+| 12 | nRF52840-DK flash test | XC-009 | 1 day |
+| 13 | UART output verification | E2E-VER-001 | 1 day |
+
+---
+
+## Artifact Traceability
+
+New artifacts created for this design are tracked in:
+- `artifacts/cross-compilation.yaml` -- XC-* (cross-compilation toolchain requirements)
+- `artifacts/gale-integration.yaml` -- GI-* (gale integration requirements)
+
+These trace to existing artifacts:
+- CC-001..CC-008 (compilation chain)
+- SL-001..SL-007 (static linking)
+- KB-001..KB-005 (kiln-builtins API)
+- ZI-001..ZI-010 (Zephyr integration)
+- TP-001..TP-008 (target platforms)
+- E2E-VER-001..E2E-VER-010 (end-to-end verification)
diff --git a/rivet.yaml b/rivet.yaml
index 0d912e3..9b7c015 100644
--- a/rivet.yaml
+++ b/rivet.yaml
@@ -57,3 +57,9 @@ externals:
     path: /Volumes/Home/git/pulseengine/sigil
     ref: main
     prefix: sigil
+
+  gale:
+    git: https://github.com/pulseengine/gale.git
+    path: /Volumes/Home/git/pulseengine/gale
+    ref: main
+    prefix: gale