diff --git a/safety/stpa/control-structure.yaml b/safety/stpa/control-structure.yaml
new file mode 100644
index 0000000..c880fe8
--- /dev/null
+++ b/safety/stpa/control-structure.yaml
@@ -0,0 +1,190 @@
+# STPA Step 2: Control Structure
+#
+# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler
+#
+# Synth is a build-time tool (like Meld). Its control structure models the
+# compilation pipeline where each stage controls the transformation of
+# WebAssembly input into ARM Cortex-M ELF output. The "controlled processes"
+# are the intermediate and final representations being constructed.
+#
+# Unlike a runtime (Kiln), Synth has no real-time feedback loops. The
+# controllers operate sequentially during a single compilation pass.
+# Feedback is immediate: each stage observes the result of the previous
+# stage's transformation.
+#
+# Reference: STPA Handbook (Leveson & Thomas, 2018), Chapter 2
+
+controllers:
+  - id: CTRL-1
+    name: Instruction Selector
+    type: automated
+    description: >
+      The pattern-matching instruction selector in synth-synthesis. Maps each
+      WebAssembly operation (WasmOp) to an ARM Cortex-M instruction sequence.
+      Handles arithmetic, comparisons, conversions, memory access, control flow
+      (block/loop/if/br/br_if), and function calls. Consults the target profile
+      to determine available instructions (Thumb-1 vs Thumb-2, VFP, etc.).
+    source-file: crates/synth-synthesis/src/lib.rs
+    control-actions:
+      - ca: CA-1
+        target: CP-1
+        action: Emit ARM instruction sequence for a WASM operation
+      - ca: CA-7
+        target: CP-1
+        action: Emit bounds check sequence for memory access
+      - ca: CA-8
+        target: CP-1
+        action: Emit multi-instruction division sequence with trap
+    feedback:
+      - from: CP-1
+        info: Current instruction stream state, label offsets
+    process-model:
+      - WASM operation semantics are correctly understood
+      - Target ISA capabilities are accurately known
+      - Virtual register state tracks physical register availability
+      - Stack depth matches WASM operand stack model
+
+  - id: CTRL-2
+    name: Peephole Optimizer
+    type: automated
+    description: >
+      The peephole optimizer in synth-synthesis. Scans the emitted ARM
+      instruction stream for patterns that can be simplified or fused.
+      Performs constant propagation, strength reduction, redundant load
+      elimination, and instruction fusion. Must preserve the semantics
+      of the original instruction sequence.
+    source-file: crates/synth-synthesis/src/peephole.rs
+    control-actions:
+      - ca: CA-2
+        target: CP-1
+        action: Rewrite instruction sequence to optimized equivalent
+    feedback:
+      - from: CP-1
+        info: Instruction patterns available for optimization
+    process-model:
+      - Rewritten sequences produce identical results for all inputs
+      - Flag-setting side effects are preserved
+      - Memory ordering constraints are respected
+      - Instruction dependencies are correctly tracked
+
+  - id: CTRL-3
+    name: ARM Encoder
+    type: automated
+    description: >
+      The ARM instruction encoder in synth-backend. Converts abstract ARM
+      instruction representations into concrete Thumb/Thumb-2 machine code
+      bytes. Handles encoding selection (narrow vs wide Thumb), immediate
+      value fitting, condition code encoding, and branch offset calculation.
+    source-file: crates/synth-backend/src/arm.rs
+    control-actions:
+      - ca: CA-3
+        target: CP-1
+        action: Encode abstract ARM instruction to machine code bytes
+    feedback:
+      - from: CP-1
+        info: Encoding result (success, immediate-out-of-range, invalid-for-target)
+      - from: CP-2
+        info: Current code section offset for branch calculations
+    process-model:
+      - Instruction encoding matches ARM Architecture Reference Manual
+      - Immediate values fit within the encoding format
+      - Branch offsets are within the encodable range
+      - Target ISA variant supports the instruction
+
+  - id: CTRL-4
+    name: ELF Builder
+    type: automated
+    description: >
+      The ELF binary constructor in synth-backend. Assembles encoded machine
+      code into ELF sections (.text, .data, .bss, .rodata), generates the
+      vector table, computes section addresses from linker script, writes
+      ELF headers, program headers, and symbol table.
+    source-file: crates/synth-backend/src/elf.rs
+    control-actions:
+      - ca: CA-4
+        target: CP-2
+        action: Build ELF section with correct load address and alignment
+      - ca: CA-9
+        target: CP-2
+        action: Generate vector table with reset and fault handlers
+      - ca: CA-10
+        target: CP-3
+        action: Assign memory regions from linker script
+    feedback:
+      - from: CP-2
+        info: Section sizes, symbol addresses, relocation results
+      - from: CP-3
+        info: Available memory regions, address ranges
+    process-model:
+      - Linker script memory regions are non-overlapping
+      - Vector table entries point to valid code addresses
+      - Section load addresses match the target's memory map
+      - ELF headers conform to the ELF specification
+
+  - id: CTRL-5
+    name: ISA Validator
+    type: automated
+    description: >
+      The target capability validator in synth-synthesis. Gates each
+      instruction against the target profile's ISA feature set. Rejects
+      Thumb-2 instructions on Cortex-M0 (Thumb-1 only), VFP instructions
+      on cores without FPU, DSP instructions on non-DSP cores. Uses the
+      target profile system from synth-backend.
+    source-file: crates/synth-synthesis/src/target.rs
+    control-actions:
+      - ca: CA-5
+        target: CP-1
+        action: Validate instruction against target ISA capabilities
+    feedback:
+      - from: CP-1
+        info: Validation pass/fail with reason
+    process-model:
+      - Target profile accurately describes the hardware capabilities
+      - ISA feature database is complete for all supported cores
+      - Instruction-to-feature mapping is correct
+
+  - id: CTRL-6
+    name: Z3 Verifier
+    type: automated
+    description: >
+      The Z3 SMT translation validator in synth-verify. Encodes each
+      synthesis rule as a pair of SMT formulas (WASM semantics, ARM
+      semantics) and checks equivalence. Reports counterexamples when
+      a rule is unsound. Operates offline or as part of CI.
+    source-file: crates/synth-verify/src/lib.rs
+    control-actions:
+      - ca: CA-6
+        target: CP-1
+        action: Verify synthesis rule via SMT equivalence check
+    feedback:
+      - from: CP-1
+        info: Verification result (valid, counterexample, timeout, unknown)
+    process-model:
+      - SMT encoding accurately models WASM and ARM semantics
+      - Verification covers all synthesis rules in use
+      - Timeout does not mean the rule is correct
+
+controlled-processes:
+  - id: CP-1
+    name: ARM Instruction Stream
+    description: >
+      The sequence of abstract and concrete ARM instructions being built
+      during compilation. Starts as abstract WasmOp-to-ARM mappings from
+      the instruction selector, is refined by the peephole optimizer,
+      validated by the ISA validator, verified by Z3, and finally encoded
+      to machine code bytes by the ARM encoder.
+
+  - id: CP-2
+    name: ELF Binary
+    description: >
+      The output ELF binary being assembled. Contains .text (machine code),
+      .data (initialized data), .bss (zero-initialized data), .rodata
+      (constants), vector table, section headers, program headers, and
+      symbol table. The final artifact delivered to the target hardware.
+
+  - id: CP-3
+    name: Memory Layout
+    description: >
+      The target memory map: flash and RAM regions, their addresses and
+      sizes, stack placement, heap placement, and WebAssembly linear memory
+      allocation. Derived from the linker script and target profile.
diff --git a/safety/stpa/controller-constraints.yaml b/safety/stpa/controller-constraints.yaml
new file mode 100644
index 0000000..fb27322
--- /dev/null
+++ b/safety/stpa/controller-constraints.yaml
@@ -0,0 +1,209 @@
+# STPA Step 3b: Controller Constraints
+#
+# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler
+#
+# Each controller constraint is derived from one or more UCAs. It specifies
+# the required behavior of a controller to prevent the unsafe control action.
+
+controller-constraints:
+  # =========================================================================
+  # Instruction Selector constraints
+  # =========================================================================
+  - id: CC-IS-1
+    controller: CTRL-1
+    constraint: >
+      Instruction selector shall consult the target profile before emitting
+      any VFP/FPU instruction. If the target profile does not include FPU
+      capability, the selector shall emit a software floating-point sequence
+      or report an error. No hardware FPU instruction shall appear in output
+      for a non-FPU target.
+    ucas: [UCA-1]
+    hazards: [H-4]
+
+  - id: CC-IS-2
+    controller: CTRL-1
+    constraint: >
+      Instruction selector shall emit a bounds check sequence (CMP + BHS to
+      trap) before every memory load and store instruction when bounds
+      checking is enabled. The check shall compare the effective address
+      plus access size against the linear memory size.
+    ucas: [UCA-2]
+    hazards: [H-3]
+
+  - id: CC-IS-3
+    controller: CTRL-1
+    constraint: >
+      Instruction selector shall use the correct signed/unsigned variant
+      for all division (SDIV vs UDIV) and shift (ASR vs LSR) instructions.
+      The variant shall be determined by the WASM operation's signedness
+      (div_s vs div_u, shr_s vs shr_u).
+    ucas: [UCA-8]
+    hazards: [H-1]
+
+  - id: CC-IS-4
+    controller: CTRL-1
+    constraint: >
+      Instruction selector shall emit complete multi-instruction sequences.
+      For division, this includes the divide-by-zero check, the division
+      instruction, and (for signed division) the INT_MIN/-1 overflow check.
+      No partial sequence shall be emitted.
+    ucas: [UCA-11]
+    hazards: [H-1]
+
+  - id: CC-IS-5
+    controller: CTRL-1
+    constraint: >
+      Instruction selector shall preserve all callee-saved registers
+      (r4-r11, lr) by emitting PUSH at function entry and POP at function
+      exit for any registers used within the function body.
+    ucas: [UCA-14]
+    hazards: [H-6]
+
+  - id: CC-IS-6
+    controller: CTRL-1
+    constraint: >
+      Instruction selector shall complete all label fixups for block, loop,
+      and if constructs. Every forward branch shall have its offset resolved
+      before the function is finalized. Every loop back-edge shall target the
+      correct loop header label.
+    ucas: [UCA-11b]
+    hazards: [H-5]
+
+  - id: CC-IS-7
+    controller: CTRL-1
+    constraint: >
+      Instruction selector shall emit __meld_dispatch_import call stubs
+      with the correct calling convention: import index in the register
+      specified by the ABI, arguments in the correct order per AAPCS,
+      and return value read from R0. The ABI shall match Kiln's
+      dispatch handler implementation.
+    ucas: [UCA-13]
+    hazards: [H-8]
+
+  # =========================================================================
+  # Peephole Optimizer constraints
+  # =========================================================================
+  - id: CC-PO-1
+    controller: CTRL-2
+    constraint: >
+      Peephole optimizer shall only apply rewrites that are proven to
+      preserve semantics for all possible input values. Each rewrite
+      pattern shall be covered by a Rocq proof or Z3 equivalence check.
+      Rewrites that change flag-setting behavior shall be rejected.
+    ucas: [UCA-3]
+    hazards: [H-2]
+
+  - id: CC-PO-2
+    controller: CTRL-2
+    constraint: >
+      Peephole optimizer shall not reorder instructions that have memory
+      side effects or that set/read condition flags. Instruction
+      dependencies (data, control, and memory) shall be tracked and
+      respected during rewriting.
+    ucas: [UCA-10]
+    hazards: [H-1]
+
+  # =========================================================================
+  # ARM Encoder constraints
+  # =========================================================================
+  - id: CC-AE-1
+    controller: CTRL-3
+    constraint: >
+      ARM encoder shall produce correct condition code encoding for all
+      conditional instructions. The condition code field shall match the
+      ARM Architecture Reference Manual's encoding table. Condition codes
+      shall be tested with both taken and not-taken branches.
+    ucas: [UCA-4]
+    hazards: [H-5]
+
+  - id: CC-AE-2
+    controller: CTRL-3
+    constraint: >
+      ARM encoder shall reject immediate values that do not fit the
+      instruction's encoding format. When an immediate is out of range,
+      the encoder shall return an error (not silently truncate). The
+      instruction selector shall then emit a multi-instruction sequence
+      to materialize the constant.
+    ucas: [UCA-12]
+    hazards: [H-4]
+
+  - id: CC-AE-3
+    controller: CTRL-3
+    constraint: >
+      ARM encoder shall compute branch offsets after all instructions in
+      the function are finalized. Offset calculation shall account for
+      Thumb instruction alignment (PC + 4 bias) and variable-width
+      instruction sizes.
+    ucas: [UCA-12b]
+    hazards: [H-5]
+
+  # =========================================================================
+  # ELF Builder constraints
+  # =========================================================================
+  - id: CC-EB-1
+    controller: CTRL-4
+    constraint: >
+      ELF builder shall generate a correct vector table for the target
+      Cortex-M variant. The reset handler address shall have the Thumb
+      bit set (LSB = 1). The HardFault handler shall always be present.
+      Vector table entries shall point to valid .text addresses.
+    ucas: [UCA-5]
+    hazards: [H-7]
+
+  - id: CC-EB-2
+    controller: CTRL-4
+    constraint: >
+      ELF builder shall place code in flash and data in RAM according to
+      the linker script memory map. Section load addresses shall be
+      validated against the target's physical memory regions. No section
+      shall be placed outside the declared memory regions.
+    ucas: [UCA-9]
+    hazards: [H-7]
+
+  - id: CC-EB-3
+    controller: CTRL-4
+    constraint: >
+      ELF builder shall verify that all memory regions in the linker
+      script are non-overlapping. If any two sections (including stack,
+      heap, .text, .data, .bss) overlap in address space, the build
+      shall fail with a diagnostic error.
+    ucas: [UCA-15]
+    hazards: [H-7]
+
+  # =========================================================================
+  # ISA Validator constraints
+  # =========================================================================
+  - id: CC-IV-1
+    controller: CTRL-5
+    constraint: >
+      ISA validator shall reject any instruction that is not in the
+      target profile's supported instruction set. The feature database
+      shall cover all supported Cortex-M variants (M0, M0+, M3, M4,
+      M4F, M7, M23, M33). Each instruction shall be mapped to the
+      minimum ISA feature level that supports it.
+    ucas: [UCA-6]
+    hazards: [H-4]
+
+  # =========================================================================
+  # Z3 Verifier constraints
+  # =========================================================================
+  - id: CC-Z3-1
+    controller: CTRL-6
+    constraint: >
+      Z3 verifier shall run for every synthesis rule before the rule is
+      included in a release build. CI shall enforce that no unverified
+      rules are merged. A Z3 timeout shall be treated as "unverified"
+      (not as "valid").
+    ucas: [UCA-7]
+    hazards: [H-9]
+
+  - id: CC-Z3-2
+    controller: CTRL-6
+    constraint: >
+      Z3 verifier's SMT encoding shall accurately model the full
+      semantics of both the WASM operation and the ARM instruction
+      sequence, including flag side effects, bit-width, and overflow
+      behavior. The encoding shall be reviewed against the ARM
+      Architecture Reference Manual and WebAssembly spec.
+    ucas: [UCA-7b]
+    hazards: [H-9]
diff --git a/safety/stpa/loss-scenarios.yaml b/safety/stpa/loss-scenarios.yaml
new file mode 100644
index 0000000..18ec875
--- /dev/null
+++ b/safety/stpa/loss-scenarios.yaml
@@ -0,0 +1,221 @@
+# STPA Step 4: Loss Scenarios
+#
+# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler
+#
+# Each scenario explains WHY a specific UCA might occur. Scenarios identify
+# causal factors that can be addressed through design, testing, or verification.
+
+loss-scenarios:
+  # =========================================================================
+  # Instruction Selector scenarios
+  # =========================================================================
+  - id: LS-1
+    title: Target capability check has incomplete ISA feature database
+    uca: UCA-1
+    hazards: [H-4]
+    type: inadequate-process-model
+    scenario: >
+      The instruction selector's target profile database does not include
+      all Cortex-M variants. A new target (e.g., Cortex-M23) is added as
+      "Cortex-M class" without specifying that it lacks VFP. The selector
+      emits VADD.F32 for an f32.add operation. The instruction causes a
+      UsageFault on the target hardware because the M23 has no FPU.
+    causal-factors:
+      - Target profile database uses coarse-grained "Cortex-M" classification
+      - New target variants added without reviewing FPU capability
+      - No compile-time assertion that float ops require FPU feature flag
+    process-model-flaw: >
+      Selector assumes all Cortex-M4 and above have FPU; some M4 SKUs lack it
+
+  - id: LS-2
+    title: Bounds check omitted for memory access with constant zero offset
+    uca: UCA-2
+    hazards: [H-3]
+    type: inadequate-control-algorithm
+    scenario: >
+      The instruction selector has an optimization that skips bounds checks
+      for memory accesses with a static offset of zero, assuming the base
+      address was already validated. However, the base address comes from
+      an i32.add that can overflow, producing a small address from two
+      large operands. The bounds check is needed but not emitted.
+    causal-factors:
+      - Optimization assumes zero-offset accesses are always safe
+      - Integer overflow in address computation not considered
+      - Bounds check elision logic does not account for all address sources
+
+  - id: LS-3
+    title: Peephole optimizer pattern matches without checking flag side effects
+    uca: UCA-3
+    hazards: [H-2]
+    type: inadequate-control-algorithm
+    scenario: >
+      The peephole optimizer matches a pattern "MOVS Rd, #0; ADDS Rd, Rn, Rm"
+      and rewrites it to "ADD Rd, Rn, Rm" (removing the redundant MOV).
+      However, the original ADDS sets the condition flags (N, Z, C, V) which
+      are read by a subsequent BEQ instruction. The replacement ADD does not
+      set flags. The conditional branch now reads stale flags from a prior
+      instruction, branching on the wrong condition.
+    causal-factors:
+      - Pattern matcher checks opcode and operands but not flag-setting behavior
+      - No liveness analysis for condition flags across rewrite boundaries
+      - Test suite does not cover flag-dependent control flow after optimization
+
+  - id: LS-4
+    title: ARM encoder uses wrong condition code encoding table
+    uca: UCA-4
+    hazards: [H-5]
+    type: inadequate-control-algorithm
+    scenario: >
+      The ARM encoder's condition code table maps the abstract condition
+      "less than (signed)" to the ARM condition code LO (unsigned lower)
+      instead of LT (signed less than). For positive operands, LO and LT
+      produce the same result. For negative operands, LO (which tests C=0)
+      gives the wrong answer. The bug is not caught by tests that only use
+      positive test values.
+    causal-factors:
+      - Condition code table has a transposition error between LT and LO
+      - Test values do not include negative numbers for comparison operations
+      - LO and LT produce identical results for the most common test cases
+
+  - id: LS-5
+    title: Rocq proof model does not distinguish Cortex-M variants
+    uca: UCA-6
+    hazards: [H-4]
+    type: inadequate-process-model
+    scenario: >
+      The Rocq proof suite models ARM semantics with a single instruction
+      set that includes all Thumb-2 instructions. The proofs establish
+      correctness for the full instruction set but do not model the
+      per-variant instruction availability. A proof for i32.clz using CLZ
+      (Thumb-2) is valid, but CLZ is not available on Cortex-M0. The ISA
+      validator should reject it, but the proof gives false confidence.
+    causal-factors:
+      - Rocq ARM semantics model is variant-agnostic
+      - Proofs establish semantic correctness but not target compatibility
+      - No formal model of ISA feature levels in the proof suite
+    process-model-flaw: >
+      Proof suite assumes a single ARM ISA; does not model per-variant subsets
+
+  - id: LS-6
+    title: Z3 verification timeout treated as success
+    uca: UCA-7
+    hazards: [H-9]
+    type: sensor-failure
+    scenario: >
+      The Z3 verifier is configured with a 30-second timeout. A complex
+      synthesis rule involving 64-bit multiplication times out. The CI
+      script interprets the exit code as "no counterexample found" (success)
+      rather than "inconclusive." The rule is merged and deployed. Later,
+      a user discovers that the rule produces wrong results for specific
+      inputs that Z3 would have found with more time.
+    causal-factors:
+      - CI script does not distinguish timeout from valid/unsat
+      - Z3 timeout exit code is 0 with "unknown" result, not checked
+      - No secondary verification (e.g., property-based testing) as fallback
+
+  - id: LS-7
+    title: Signed division sequence omits INT_MIN/-1 overflow check
+    uca: UCA-8
+    hazards: [H-1]
+    type: inadequate-control-algorithm
+    scenario: >
+      The instruction selector emits a signed division sequence: check
+      divisor != 0, then SDIV. It omits the check for INT_MIN / -1 which
+      overflows in two's complement (the result would be INT_MAX + 1, which
+      is not representable). The WASM spec requires a trap for this case.
+      ARM's SDIV instruction silently returns INT_MIN. The compiled code
+      returns -2147483648 instead of trapping.
+    causal-factors:
+      - Division sequence template only checks for zero divisor
+      - WASM i32.div_s overflow trap requirement not in the code comments
+      - ARM SDIV does not trap on overflow (implementation-defined behavior)
+
+  - id: LS-8
+    title: Vector table reset handler missing Thumb bit
+    uca: UCA-5
+    hazards: [H-7]
+    type: inadequate-control-algorithm
+    scenario: >
+      The ELF builder writes the reset handler address into the vector
+      table without setting bit 0 (the Thumb interworking bit). On
+      Cortex-M, all code executes in Thumb mode and the vector table
+      entries must have bit 0 set. The MCU reads the reset vector,
+      sees bit 0 = 0, attempts to enter ARM mode (which Cortex-M does
+      not support), and immediately takes a HardFault. The device
+      fails to boot.
+    causal-factors:
+      - Vector table address calculation does not OR with 1
+      - Cortex-M always executes in Thumb mode (no ARM mode)
+      - Bug only manifests on real hardware, not in some emulators
+
+  - id: LS-9
+    title: Peephole optimizer reorders load across store to same address
+    uca: UCA-10
+    hazards: [H-1]
+    type: inadequate-control-algorithm
+    scenario: >
+      The peephole optimizer moves a load instruction before a store to
+      the same memory address to improve pipeline utilization. The
+      original program stores a value then loads it back (a common
+      pattern for WASM local variables via linear memory). After
+      reordering, the load reads the old value before the store writes
+      the new value, producing incorrect results.
+    causal-factors:
+      - Reordering pass does not check for memory address aliasing
+      - WASM linear memory accesses all alias through a single base pointer
+      - Alias analysis is absent or overly optimistic
+
+  - id: LS-10
+    title: Meld dispatch stub passes import index in wrong register
+    uca: UCA-13
+    hazards: [H-8]
+    type: inadequate-process-model
+    scenario: >
+      The instruction selector's __meld_dispatch_import stub places the
+      WASM import function index in R1 (the second argument register per
+      AAPCS). Kiln's dispatch handler expects the import index in R0
+      (the first argument). The handler reads R0 which contains the
+      first WASM argument, interprets it as an import index, and
+      dispatches to the wrong function.
+    causal-factors:
+      - Synth and Kiln ABI documentation disagrees on register assignment
+      - No shared ABI definition file or header between the projects
+      - Integration tests mock the dispatch handler instead of using real Kiln
+    process-model-flaw: >
+      Synth's model of the Kiln dispatch ABI is out of sync with Kiln's implementation
+
+  - id: LS-11
+    title: Immediate value truncation produces wrong constant
+    uca: UCA-12
+    hazards: [H-4]
+    type: inadequate-control-algorithm
+    scenario: >
+      The ARM encoder receives a MOV instruction with immediate value
+      0x1FF (511). The Thumb-1 MOV immediate format supports only 8-bit
+      immediates (0-255). Instead of returning an error, the encoder
+      takes the low 8 bits (0xFF = 255) and encodes MOV Rd, #255. The
+      instruction appears valid but loads the wrong constant. Downstream
+      computation uses 255 instead of 511.
+    causal-factors:
+      - Encoder masks immediate to field width without range check
+      - No assertion that immediate fits before encoding
+      - Thumb-1 immediate range is 0-255 but this is not validated
+
+  - id: LS-12
+    title: Overlapping linker script regions not detected
+    uca: UCA-15
+    hazards: [H-7]
+    type: inadequate-control-algorithm
+    scenario: >
+      The linker script for a custom board defines flash at 0x08000000
+      (256K) and RAM at 0x20000000 (64K). A user modifies the flash
+      size to 512K without updating the RAM start address. On a device
+      where flash and RAM are not contiguous, this is fine. But on a
+      device where flash extends to 0x20000000, the .data section
+      (placed in RAM) overlaps with the end of .text (in flash). The
+      ELF builder does not detect the overlap. At runtime, writing to
+      .data corrupts code in flash.
+    causal-factors:
+      - ELF builder does not validate that sections are non-overlapping
+      - Linker script memory regions are trusted without cross-checking
+      - Overlap detection requires knowledge of the physical memory map
diff --git a/safety/stpa/system-constraints.yaml b/safety/stpa/system-constraints.yaml
new file mode 100644
index 0000000..5d76aff
--- /dev/null
+++ b/safety/stpa/system-constraints.yaml
@@ -0,0 +1,120 @@
+# STPA Step 1c: System-Level Constraints
+#
+# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler
+#
+# Each constraint is the inversion of a hazard: it specifies the condition
+# that must be enforced to prevent the hazard.
+#
+# Spec baselines:
+#   Core: WebAssembly Specification 3.0 (2025-12-03)
+#   ARM: ARM Architecture Reference Manual (ARMv6-M, ARMv7-M, ARMv8-M)
+#   ELF: ELF for ARM Architecture (ARM IHI 0044)
+
+system-constraints:
+  - id: SC-1
+    title: Instruction selection must preserve WASM operation semantics
+    description: >
+      For every WebAssembly operation, the compiled ARM instruction sequence
+      shall produce identical results to the WebAssembly specification for
+      all possible input values. This includes arithmetic edge cases
+      (overflow, division by zero, INT_MIN/-1), correct signedness
+      (signed vs unsigned), correct conversion semantics (truncation vs
+      saturation), and correct trap behavior.
+    hazards: [H-1]
+    spec-baseline: "WebAssembly Core Specification 3.0"
+
+  - id: SC-2
+    title: Peephole optimization must not change observable behavior
+    description: >
+      Every peephole optimization rewrite shall produce an instruction
+      sequence that is semantically equivalent to the original for all
+      possible inputs. Flag-setting side effects, memory ordering, and
+      exception behavior shall be preserved. Each rewrite shall be
+      verified by Rocq proof or Z3 equivalence check.
+    hazards: [H-2]
+    spec-baseline: "WebAssembly Core Specification 3.0"
+
+  - id: SC-3
+    title: Memory bounds checks must be correct when enabled
+    description: >
+      When bounds checking is enabled, every memory load and store shall
+      be preceded by a bounds check that compares the effective address
+      plus access size against the linear memory size. The check shall
+      trap (branch to trap handler) if the access is out of bounds. No
+      bounds check shall be elided unless formally proven unnecessary.
+    hazards: [H-3]
+
+  - id: SC-4
+    title: Generated ARM code must be valid for the target ISA variant
+    description: >
+      Every ARM instruction in the compiled output shall be valid for the
+      target Cortex-M variant specified in the target profile. No Thumb-2
+      instruction shall appear in output for Thumb-1-only targets. No VFP
+      instruction shall appear for targets without FPU. No unaligned
+      access shall be emitted for strict-alignment targets. Immediate
+      values shall fit within the encoding format.
+    hazards: [H-4]
+    spec-baseline: "ARM Architecture Reference Manual (ARMv6-M, ARMv7-M)"
+
+  - id: SC-5
+    title: Control flow translation must produce correct branch targets
+    description: >
+      All branch instructions in the compiled output shall target the
+      correct code address. Block/loop/if/br/br_if translation shall
+      produce correct label offsets. Condition codes shall match the
+      WASM comparison semantics. Branch offset calculation shall account
+      for Thumb instruction alignment and variable instruction widths.
+    hazards: [H-5]
+    spec-baseline: "WebAssembly Core Specification 3.0, Section 4.4.8"
+
+  - id: SC-6
+    title: Register allocation must preserve all live values
+    description: >
+      The register allocator shall not overwrite a register that is still
+      needed by a subsequent instruction. Callee-saved registers (r4-r11,
+      lr) shall be preserved across function calls. The virtual stack
+      model shall accurately track which physical registers hold which
+      WASM values at every point in the compiled code.
+    hazards: [H-6]
+
+  - id: SC-7
+    title: ELF output must be well-formed for the target
+    description: >
+      The generated ELF binary shall have correct section headers, program
+      headers, symbol table, and vector table. Section load addresses shall
+      match the target's physical memory map. Memory regions shall not
+      overlap. The vector table reset handler shall have the Thumb bit set.
+      The binary shall load and execute correctly on the target hardware.
+    hazards: [H-7]
+    spec-baseline: "ELF for ARM Architecture (ARM IHI 0044)"
+
+  - id: SC-8
+    title: Meld dispatch ABI must match Kiln's implementation
+    description: >
+      The __meld_dispatch_import calling convention generated by Synth
+      shall match Kiln's dispatch handler exactly. Import index register,
+      argument order, and return value convention shall be consistent
+      between the two projects. The ABI shall be defined in a shared
+      specification and tested with cross-project integration tests.
+    hazards: [H-8]
+
+  - id: SC-9
+    title: Verification must cover all deployed synthesis rules
+    description: >
+      Every synthesis rule used in production shall be verified by at
+      least one of: Rocq proof (T1/T2), Z3 SMT check, or exhaustive
+      property-based testing. Admitted proofs shall be tracked and their
+      assumptions documented. Z3 timeouts shall be treated as unverified.
+      No unverified rule shall be deployed without explicit sign-off.
+    hazards: [H-9]
+
+  - id: SC-10
+    title: Canonical ABI implementation must agree with Meld and Kiln
+    description: >
+      Synth's synth-abi crate shall compute identical canonical ABI layouts
+      (element sizes, field alignment, string encoding) as Meld's parser.rs
+      and Kiln's kiln-component. Disagreement between any two tools is a
+      blocking defect. Cross-tool consistency shall be verified by shared
+      test fixtures.
+    hazards: [H-10]
+    spec-baseline: "Component Model commit deb0b0a, Canonical ABI"
diff --git a/safety/stpa/ucas.yaml b/safety/stpa/ucas.yaml
new file mode 100644
index 0000000..70e997f
--- /dev/null
+++ b/safety/stpa/ucas.yaml
@@ -0,0 +1,215 @@
+# STPA Step 3: Unsafe Control Actions
+#
+# System: Synth — WebAssembly-to-ARM Cortex-M AOT compiler
+#
+# Format: UCAs grouped by controller, categorized by type:
+#   not-providing: Action needed but not taken
+#   providing: Action taken when it shouldn't be, or taken incorrectly
+#   too-early-too-late: Action timing or ordering incorrect
+#   stopped-too-soon: Action duration too short / incomplete
+
+instruction-selector-ucas:
+  control-action: "Emit ARM instruction sequence for WASM operation"
+  controller: CTRL-1
+
+  providing:
+    - id: UCA-1
+      description: >
+        Instruction selector emits a VFP floating-point instruction (VADD,
+        VMUL, VCVT, etc.) for a target profile that lacks an FPU. The
+        instruction is invalid on the target core and causes an
+        UsageFault/HardFault at runtime.
+      context: "Compiling float operation for Cortex-M0/M0+ or M4 without FPU"
+      hazards: [H-4]
+
+    - id: UCA-8
+      description: >
+        Instruction selector emits UDIV where SDIV is needed (or vice versa)
+        for a division operation, producing wrong results for negative
+        operands. Similarly, emits LSR where ASR is needed for signed
+        right shift.
+      context: "i32.div_s, i32.shr_s with negative operands"
+      hazards: [H-1]
+
+    - id: UCA-11
+      description: >
+        Instruction selector stops emitting a multi-instruction sequence
+        before all instructions are produced. For example, a division
+        sequence that requires a divide-by-zero check, the division itself,
+        and an overflow check emits only the division instruction without
+        the trap checks.
+      context: "i32.div_s which requires check for zero and INT_MIN/-1"
+      hazards: [H-1]
+
+  not-providing:
+    - id: UCA-2
+      description: >
+        Instruction selector does not emit a bounds check (CMP + conditional
+        branch) before a memory load or store instruction when bounds
+        checking is enabled. The compiled code accesses memory beyond the
+        WebAssembly linear memory bounds.
+      context: "i32.load, i32.store with --bounds-check enabled"
+      hazards: [H-3]
+
+    - id: UCA-14
+      description: >
+        Instruction selector does not emit callee-save register
+        preservation (PUSH/POP of r4-r11, lr) at function entry/exit.
+        When the compiled function calls another function or returns,
+        the caller's register state is corrupted.
+      context: "Function that uses more than r0-r3 scratch registers"
+      hazards: [H-6]
+
+  stopped-too-soon:
+    - id: UCA-11b
+      description: >
+        Instruction selector emits a partial multi-instruction sequence
+        for a block/loop/if construct. For example, a loop back-edge
+        branch is emitted but the label fixup is not completed, leaving
+        the branch offset as zero (branch to self = infinite loop) or
+        pointing to wrong code.
+      context: "Nested block/loop with forward and backward branches"
+      hazards: [H-5]
+
+peephole-optimizer-ucas:
+  control-action: "Rewrite instruction sequence to optimized equivalent"
+  controller: CTRL-2
+
+  providing:
+    - id: UCA-3
+      description: >
+        Peephole optimizer rewrites an instruction sequence in a way that
+        changes the program's observable behavior. For example, replacing
+        a MUL with a shift-and-add that produces a different result for
+        edge-case inputs (INT_MIN), or eliminating a CMP that sets flags
+        needed by a subsequent conditional branch.
+      context: "Strength reduction, dead code elimination, instruction fusion"
+      hazards: [H-2]
+
+    - id: UCA-10
+      description: >
+        Peephole optimizer reorders instructions across a memory barrier
+        or across instructions with side effects (flag-setting, memory
+        access). The reordered sequence executes memory operations in a
+        different order than the WASM semantics require.
+      context: "Load-store reordering near conditional branches"
+      hazards: [H-1]
+
+arm-encoder-ucas:
+  control-action: "Encode abstract ARM instruction to machine code bytes"
+  controller: CTRL-3
+
+  providing:
+    - id: UCA-4
+      description: >
+        ARM encoder produces wrong encoding for a conditional instruction.
+        Condition code bits (EQ/NE/LT/GE/GT/LE) are mapped incorrectly,
+        causing the branch or conditional execution to trigger on the
+        wrong condition.
+      context: "Encoding BEQ, BNE, BLT, BGE with condition code field"
+      hazards: [H-5]
+
+    - id: UCA-12
+      description: >
+        ARM encoder silently truncates an immediate value that does not
+        fit the instruction's encoding format. For example, a Thumb-2
+        modified immediate constant that requires rotation is instead
+        truncated to 8 bits, producing a different constant value in
+        the encoded instruction.
+      context: "MOV with large immediate, ADD with immediate > 255"
+      hazards: [H-4]
+
+  too-early-too-late:
+    - id: UCA-12b
+      description: >
+        ARM encoder calculates branch offsets before all instructions are
+        emitted, then instruction insertion or deletion by the peephole
+        optimizer changes the offsets. The branch target is now wrong
+        because the offset was computed too early.
+      context: "Forward branch to end-of-block after peephole optimization pass"
+      hazards: [H-5]
+
+elf-builder-ucas:
+  control-action: "Build ELF section with correct load address"
+  controller: CTRL-4
+
+  providing:
+    - id: UCA-5
+      description: >
+        ELF builder generates an incorrect vector table entry. The reset
+        handler address is wrong (off by one for Thumb bit, or points to
+        data instead of code), or the HardFault handler is missing. The
+        target MCU jumps to wrong code on reset or fault.
+      context: "Vector table generation for Cortex-M4 with FPU"
+      hazards: [H-7]
+
+    - id: UCA-9
+      description: >
+        ELF builder places code in the wrong memory region for the target.
+        Code is placed in RAM instead of flash, or data is placed at an
+        address that overlaps the vector table. The binary fails to boot
+        or corrupts its own code at runtime.
+      context: "Linker script with flash at 0x08000000, RAM at 0x20000000"
+      hazards: [H-7]
+
+    - id: UCA-15
+      description: >
+        ELF builder assigns overlapping memory regions in the linker
+        script output. The .text and .data sections overlap, or the
+        stack region overlaps with the heap region. Code or data is
+        silently overwritten at runtime.
+      context: "Target with small flash/RAM where sections are tightly packed"
+      hazards: [H-7]
+
+isa-validator-ucas:
+  control-action: "Validate instruction against target ISA capabilities"
+  controller: CTRL-5
+
+  not-providing:
+    - id: UCA-6
+      description: >
+        ISA validator does not reject an instruction that is unsupported
+        on the target core. For example, a Thumb-2 wide instruction
+        (32-bit encoding) passes validation for a Cortex-M0 target
+        that only supports Thumb-1 (16-bit) instructions.
+      context: "Compiling for Cortex-M0 with Thumb-2 instruction in output"
+      hazards: [H-4]
+
+z3-verifier-ucas:
+  control-action: "Verify synthesis rule via SMT equivalence check"
+  controller: CTRL-6
+
+  not-providing:
+    - id: UCA-7
+      description: >
+        Z3 verifier does not run for a newly added or modified synthesis
+        rule. The rule is deployed without verification, and it may
+        contain a semantic error that produces wrong ARM code for
+        certain inputs.
+      context: "New instruction selection rule added without CI verification"
+      hazards: [H-9]
+
+  providing:
+    - id: UCA-7b
+      description: >
+        Z3 verifier reports "valid" for a rule that is actually unsound
+        because the SMT encoding of the ARM or WASM semantics is
+        incomplete or wrong. The encoding omits flag side effects,
+        uses wrong bit-width, or models the wrong instruction variant.
+      context: "Z3 check for rule involving flag-setting arithmetic"
+      hazards: [H-9]
+
+meld-dispatch-ucas:
+  control-action: "Emit Meld dispatch import stub"
+  controller: CTRL-1
+
+  providing:
+    - id: UCA-13
+      description: >
+        Instruction selector generates a __meld_dispatch_import call stub
+        that uses the wrong calling convention. Import index is placed
+        in the wrong register, arguments are passed in the wrong order,
+        or the return value is read from the wrong register. The Kiln
+        runtime bridge receives garbled arguments.
+      context: "Compiled WASM module calling an imported function via Kiln"
+      hazards: [H-8]