diff --git a/loom-cli/src/main.rs b/loom-cli/src/main.rs
index 8944f62..808abbe 100644
--- a/loom-cli/src/main.rs
+++ b/loom-cli/src/main.rs
@@ -348,6 +348,56 @@ fn count_instructions_from_bytes(bytes: &[u8]) -> usize {
 /// (safe, unoptimized) bytes to `output_path` and return `Err` so the process
 /// exits non-zero. A no-op when the gate is disabled (`original` is `None`).
 #[allow(unused_variables)]
+/// Write the optimized artifact ONLY if it passes authoritative WebAssembly
+/// validation (#346).
+///
+/// `loom optimize` used to write whatever the encoder produced and print
+/// "✅ Optimization complete!" over it. When the encoder dropped the data
+/// count section while keeping the `memory.init` instructions that require it,
+/// the result was a module no validator accepts — emitted with exit code 0.
+/// Silent invalid output is the worst shape this can take: the next tool in
+/// the chain reports the failure against ITS OWN input, so the blame lands
+/// downstream of the tool that actually broke the module.
+///
+/// `loom_core::optimize::optimize_module` has carried exactly this gate since
+/// #257, described there as the systemic guarantee that loom can NEVER emit
+/// structurally invalid wasm. The CLI does not go through that function — it
+/// drives the passes directly (#345) — so it inherited none of it. This closes
+/// that hole at the only point that matters: the write.
+///
+/// On failure the ORIGINAL input is written instead, when the original itself
+/// validates, so the worst case is unoptimized-but-valid output rather than a
+/// missing or corrupt file. The exit code is still non-zero: a caller that
+/// checks it learns something went wrong, and a caller that ignores it still
+/// gets a module that loads.
+fn write_validated_output(
+    output_path: &str,
+    output_bytes: &[u8],
+    wasm_to_validate: &[u8],
+    original_input: &[u8],
+) -> Result<()> {
+    if let Err(e) = loom_core::encode::validate_output_bytes(wasm_to_validate) {
+        eprintln!("error: the optimized module failed authoritative WebAssembly validation:");
+        eprintln!("       {e}");
+        // Fall back to the input, but only after proving the input itself is
+        // valid wasm — a `.wat` input, or one that was already invalid, must
+        // not be copied over the output path and presented as a module.
+        let recovered = loom_core::encode::validate_output_bytes(original_input).is_ok()
+            && fs::write(output_path, original_input).is_ok();
+        if recovered {
+            eprintln!("note: wrote the ORIGINAL module to {output_path} instead;");
+            eprintln!("      nothing invalid was written, and nothing was optimized.");
+        } else {
+            eprintln!("note: no output was written.");
+        }
+        eprintln!("note: this is a loom bug — please report it with the input module.");
+        return Err(anyhow!("refusing to emit a module that does not validate"));
+    }
+    fs::write(output_path, output_bytes).context("Failed to write output file")?;
+    println!("✓ Written to: {}", output_path);
+    Ok(())
+}
+
 fn maybe_differential_gate(
     original: Option<&[u8]>,
     optimized_wasm: &[u8],
@@ -519,9 +569,14 @@ fn optimize_command(
 
                     // Write optimized component
                     let output_path = output.unwrap_or_else(|| "output.wasm".to_string());
-                    fs::write(&output_path, &optimized_bytes)
-                        .context("Failed to write output file")?;
-                    println!("✓ Written to: {}", output_path);
+                    // #346: components go through the same gate. `validate`
+                    // handles the component grammar as well as core modules.
+                    write_validated_output(
+                        &output_path,
+                        &optimized_bytes,
+                        &optimized_bytes,
+                        &input_bytes,
+                    )?;
                     println!("\n✅ Optimization complete!");
                     return Ok(());
                 }
@@ -653,8 +708,15 @@ fn optimize_command(
             };
             maybe_differential_gate(original_wasm.as_deref(), &opt_wasm, &output_path)?;
         }
-        fs::write(&output_path, &output_bytes).context("Failed to write output file")?;
-        println!("✓ Written to: {}", output_path);
+        // #346: validate before writing. For WAT output the bytes on disk are
+        // text, so the WASM encoding is what gets validated.
+        let validate_bytes = if output_wat {
+            loom_core::encode::encode_wasm(&module)
+                .context("Failed to encode optimized module for output validation")?
+        } else {
+            output_bytes.clone()
+        };
+        write_validated_output(&output_path, &output_bytes, &validate_bytes, &input_bytes)?;
 
         if show_stats {
             stats.print();
@@ -999,8 +1061,15 @@ fn optimize_command(
         };
         maybe_differential_gate(original_wasm.as_deref(), &opt_wasm, &output_path)?;
     }
-    fs::write(&output_path, &output_bytes).context("Failed to write output file")?;
-    println!("✓ Written to: {}", output_path);
+    // #346: validate before writing. For WAT output the bytes on disk are
+    // text, so the WASM encoding is what gets validated.
+    let validate_bytes = if output_wat {
+        loom_core::encode::encode_wasm(&module)
+            .context("Failed to encode optimized module for output validation")?
+    } else {
+        output_bytes.clone()
+    };
+    write_validated_output(&output_path, &output_bytes, &validate_bytes, &input_bytes)?;
 
     // Show statistics if requested
     if show_stats {
@@ -1532,4 +1601,72 @@ mod tests {
         assert_eq!(stats.reduction_percentage(100, 25), 75.0);
         assert_eq!(stats.reduction_percentage(0, 0), 0.0);
     }
+
+    /// The #346 backstop, tested directly on its refusal path.
+    ///
+    /// The integration sweep asserts "success implies the artifact validates",
+    /// which holds trivially while the encoder is correct — so it cannot fail
+    /// if the gate is deleted. This can: it hands the gate bytes that are
+    /// definitely invalid and asserts the three things that must follow.
+    ///
+    /// Before #346 the CLI had no such gate at all: `fs::write` was called on
+    /// whatever the encoder returned, and "✅ Optimization complete!" was
+    /// printed over it.
+    #[test]
+    fn the_output_gate_refuses_invalid_bytes_and_restores_the_original() {
+        // Valid: (module) — the 8-byte preamble is a complete empty module.
+        const VALID: &[u8] = &[0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00];
+        // Invalid: right magic, but a truncated type section header.
+        const INVALID: &[u8] = &[0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00, 0x01, 0x7f];
+        assert!(loom_core::encode::validate_output_bytes(VALID).is_ok());
+        assert!(
+            loom_core::encode::validate_output_bytes(INVALID).is_err(),
+            "the negative fixture must actually be invalid, or this test \
+             asserts nothing"
+        );
+
+        let dir = std::env::temp_dir().join(format!("loom-346-unit-{}", std::process::id()));
+        std::fs::create_dir_all(&dir).expect("create scratch dir");
+        let out_path = dir.join("out.wasm");
+        let out_str = out_path.to_str().unwrap();
+
+        let result = write_validated_output(out_str, INVALID, INVALID, VALID);
+
+        assert!(
+            result.is_err(),
+            "the gate accepted bytes that do not validate; exit 0 over an \
+             invalid module is exactly the #346 defect"
+        );
+        let written = std::fs::read(&out_path).expect("the gate must leave a valid file behind");
+        assert_ne!(
+            written, INVALID,
+            "the invalid bytes were written to the output path"
+        );
+        assert_eq!(
+            written, VALID,
+            "the gate must fall back to the original module so the worst case \
+             is unoptimized-but-valid output, never a corrupt artifact"
+        );
+
+        let _ = std::fs::remove_file(&out_path);
+    }
+
+    /// The positive control: valid bytes must be written unchanged. Without
+    /// this, a gate that refused everything would pass the test above.
+    #[test]
+    fn the_output_gate_writes_valid_bytes_unchanged() {
+        const VALID: &[u8] = &[0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00];
+        let dir = std::env::temp_dir().join(format!("loom-346-unit-ok-{}", std::process::id()));
+        std::fs::create_dir_all(&dir).expect("create scratch dir");
+        let out_path = dir.join("ok.wasm");
+        let out_str = out_path.to_str().unwrap();
+
+        write_validated_output(out_str, VALID, VALID, VALID).expect("valid output must be written");
+        assert_eq!(
+            std::fs::read(&out_path).expect("read back"),
+            VALID,
+            "valid output must reach disk byte-for-byte"
+        );
+        let _ = std::fs::remove_file(&out_path);
+    }
 }
diff --git a/loom-cli/tests/output_validation.rs b/loom-cli/tests/output_validation.rs
new file mode 100644
index 0000000..23a6225
--- /dev/null
+++ b/loom-cli/tests/output_validation.rs
@@ -0,0 +1,210 @@
+//! `loom optimize` must never write a module that does not validate (#346).
+//!
+//! Two defects met here. The encoder dropped the **data count section** while
+//! keeping the `memory.init` / `data.drop` instructions that require it — the
+//! spec makes that section mandatory precisely so those instructions can be
+//! validated without scanning the data section, so the output was structurally
+//! invalid rather than merely suboptimal. And nothing checked: the CLI wrote
+//! whatever the encoder produced and printed `✅ Optimization complete!` over
+//! it, exit 0.
+//!
+//! Silent invalid output is the worst shape this can take. The next tool in
+//! the chain reports the failure against *its own* input, so the blame lands
+//! downstream of the tool that actually broke the module.
+//!
+//! `loom_core::optimize::optimize_module` has carried an output-validation
+//! backstop since #257 — described there as the systemic guarantee that loom
+//! can NEVER emit structurally invalid wasm. The CLI does not go through that
+//! function (#345), so it inherited none of it.
+//!
+//! These tests drive the real binary, because the property is about what lands
+//! on disk.
+
+use std::process::Command;
+
+/// The #346 reproduction, assembled from:
+///
+/// ```wat
+/// (module
+///   (memory 1)
+///   (data $d "hello")
+///   (func (export "init") (param i32)
+///     local.get 0  i32.const 0  i32.const 5
+///     memory.init $d
+///     data.drop $d))
+/// ```
+///
+/// 79 bytes, valid on input, and the smallest thing that exercises both
+/// instructions that make the data count section mandatory.
+const MEMORY_INIT_WASM: &[u8] = &[
+    0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00, 0x01, 0x05, 0x01, 0x60, 0x01, 0x7f, 0x00, 0x03,
+    0x02, 0x01, 0x00, 0x05, 0x03, 0x01, 0x00, 0x01, 0x07, 0x08, 0x01, 0x04, 0x69, 0x6e, 0x69, 0x74,
+    0x00, 0x00, 0x0c, 0x01, 0x01, 0x0a, 0x11, 0x01, 0x0f, 0x00, 0x20, 0x00, 0x41, 0x00, 0x41, 0x05,
+    0xfc, 0x08, 0x00, 0x00, 0xfc, 0x09, 0x00, 0x0b, 0x0b, 0x08, 0x01, 0x01, 0x05, 0x68, 0x65, 0x6c,
+    0x6c, 0x6f, 0x00, 0x0b, 0x04, 0x6e, 0x61, 0x6d, 0x65, 0x09, 0x04, 0x01, 0x00, 0x01, 0x64,
+];
+
+fn scratch_dir(tag: &str) -> std::path::PathBuf {
+    let dir = std::env::temp_dir().join(format!("loom-346-{tag}-{}", std::process::id()));
+    std::fs::create_dir_all(&dir).expect("create scratch dir");
+    dir
+}
+
+/// Section id 12 is the data count section. Walking the section headers is
+/// enough — every section after the 8-byte preamble is `[id][uleb size]`.
+fn has_data_count_section(bytes: &[u8]) -> bool {
+    let mut i = 8; // magic + version
+    while i < bytes.len() {
+        let id = bytes[i];
+        i += 1;
+        // uleb128 section size
+        let mut size: usize = 0;
+        let mut shift = 0;
+        loop {
+            if i >= bytes.len() {
+                return false;
+            }
+            let b = bytes[i];
+            i += 1;
+            size |= ((b & 0x7f) as usize) << shift;
+            if b & 0x80 == 0 {
+                break;
+            }
+            shift += 7;
+        }
+        if id == 12 {
+            return true;
+        }
+        i += size;
+    }
+    false
+}
+
+/// The end-to-end property: a module using `memory.init` must come out valid.
+///
+/// Before the fix this wrote a module rejected with "data count section
+/// required" while exiting 0.
+#[test]
+fn a_module_using_memory_init_is_emitted_valid() {
+    let dir = scratch_dir("init");
+    let input = dir.join("in.wasm");
+    let output = dir.join("out.wasm");
+    std::fs::write(&input, MEMORY_INIT_WASM).expect("write input");
+
+    // The input itself must be valid, or the test proves nothing about output.
+    assert!(
+        loom_core::encode::validate_output_bytes(MEMORY_INIT_WASM).is_ok(),
+        "the fixture is not valid wasm; the test cannot attribute an invalid \
+         OUTPUT to the optimizer"
+    );
+
+    let out = Command::new(env!("CARGO_BIN_EXE_loom"))
+        .args([
+            "optimize",
+            input.to_str().unwrap(),
+            "-o",
+            output.to_str().unwrap(),
+        ])
+        .output()
+        .expect("failed to run the loom binary");
+
+    assert!(
+        out.status.success(),
+        "optimizing a valid memory.init module failed:\nstdout: {}\nstderr: {}",
+        String::from_utf8_lossy(&out.stdout),
+        String::from_utf8_lossy(&out.stderr)
+    );
+
+    let emitted = std::fs::read(&output).expect("read the emitted module");
+    if let Err(e) = loom_core::encode::validate_output_bytes(&emitted) {
+        panic!(
+            "loom emitted a module that does not validate: {e}\n\
+             (this is #346: the data count section is mandatory whenever \
+             memory.init or data.drop appear)"
+        );
+    }
+
+    // And specifically the section that was missing. Validation alone would
+    // also pass if some future change removed the instructions entirely, so
+    // assert the section is there rather than only that nothing complained.
+    assert!(
+        has_data_count_section(&emitted),
+        "the emitted module validates but carries no data count section — \
+         check whether the memory.init instructions survived at all"
+    );
+}
+
+/// The systemic half, and the one that matters beyond this instance: the CLI
+/// must not write output it has not validated.
+///
+/// Rather than asserting on the encoder (already covered above), this asserts
+/// the property that makes the NEXT encoder bug loud instead of silent — that
+/// success on stdout implies the artifact on disk validates. Driven over every
+/// wasm fixture in the repo that the binary accepts.
+#[test]
+fn every_successful_optimize_leaves_a_valid_module_on_disk() {
+    let fixtures =
+        std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../loom-core/tests/fixtures");
+    let dir = scratch_dir("sweep");
+
+    let mut checked = 0usize;
+    let entries = match std::fs::read_dir(&fixtures) {
+        Ok(e) => e,
+        Err(_) => return, // fixtures directory absent in some checkouts
+    };
+    for entry in entries.flatten() {
+        let path = entry.path();
+        if path.extension().and_then(|e| e.to_str()) != Some("wasm") {
+            continue;
+        }
+        // Only modules that were valid to begin with can hold loom responsible
+        // for an invalid result.
+        let input_bytes = match std::fs::read(&path) {
+            Ok(b) => b,
+            Err(_) => continue,
+        };
+        if loom_core::encode::validate_output_bytes(&input_bytes).is_err() {
+            continue;
+        }
+
+        let output = dir.join(format!(
+            "{}.opt.wasm",
+            path.file_stem().unwrap().to_string_lossy()
+        ));
+        let out = Command::new(env!("CARGO_BIN_EXE_loom"))
+            .args([
+                "optimize",
+                path.to_str().unwrap(),
+                "-o",
+                output.to_str().unwrap(),
+                // Keep the sweep quick: the full pipeline is exercised by the
+                // test above, and #347 makes `inline` unusably slow on some
+                // real modules.
+                "--passes",
+                "dce,vacuum,constant-folding",
+            ])
+            .output()
+            .expect("failed to run the loom binary");
+
+        if !out.status.success() {
+            // A refusal is the CORRECT behaviour now — it means the gate
+            // fired. What must never happen is success over invalid output.
+            continue;
+        }
+        checked += 1;
+        let emitted = std::fs::read(&output).expect("read the emitted module");
+        if let Err(e) = loom_core::encode::validate_output_bytes(&emitted) {
+            panic!(
+                "loom reported SUCCESS but wrote an invalid module for {}: {e}\n\
+                 Exit 0 must imply the artifact validates (#346).",
+                path.display()
+            );
+        }
+    }
+
+    assert!(
+        checked > 0,
+        "the sweep validated no modules at all, so it asserts nothing — check \
+         that the fixtures directory is present and that the binary accepts them"
+    );
+}
diff --git a/loom-core/src/lib.rs b/loom-core/src/lib.rs
index 864abc8..8ea30c3 100644
--- a/loom-core/src/lib.rs
+++ b/loom-core/src/lib.rs
@@ -1901,6 +1901,25 @@ pub mod encode {
         encode_wasm_with_facts(module, false)
     }
 
+    /// Run the authoritative WebAssembly spec validator over emitted bytes.
+    ///
+    /// This is the SAME check the #257 output-validation backstop applies,
+    /// exposed so a caller that does its own encoding — notably the CLI, which
+    /// drives the passes directly rather than through
+    /// [`crate::optimize::optimize_module`] — can apply the identical gate
+    /// instead of an approximation of it.
+    ///
+    /// It exists because that divergence had teeth (#346): the backstop lived
+    /// inside `optimize_module`, the binary never called it, and so
+    /// `loom optimize` emitted a module that no validator would accept while
+    /// printing a success message. A guarantee reachable only from a function
+    /// nobody calls is prose, not a guarantee.
+    pub fn validate_output_bytes(bytes: &[u8]) -> Result<()> {
+        wasmparser::validate(bytes)
+            .map(|_| ())
+            .map_err(|e| anyhow::anyhow!("{e}"))
+    }
+
     /// Encode to WebAssembly binary, optionally emitting the #231 `wsc.facts`
     /// custom section (schema v1) from `module.facts`.
     ///
@@ -2109,6 +2128,34 @@ pub mod encode {
             });
         }
 
+        // Build the DATA COUNT section (id 12) — #346.
+        //
+        // The spec makes this section MANDATORY whenever `memory.init` or
+        // `data.drop` appear in the code: it exists so those instructions can
+        // be validated without scanning the data section, and a validator
+        // rejects the module outright when it is missing. loom preserved the
+        // data section and the instructions but never emitted this section at
+        // all — there was no reference to it anywhere in the crate — so any
+        // module using `memory.init` came out structurally INVALID while the
+        // CLI reported success.
+        //
+        // It must be written between the element section (9) and the code
+        // section (10), which is why it is emitted here rather than beside the
+        // data section it describes.
+        //
+        // The count is the number of data segments, not the number of
+        // instructions referencing them: it is the length of the data index
+        // space that `memory.init`/`data.drop` index into.
+        if module.functions.iter().any(|f| {
+            f.instructions
+                .iter()
+                .any(|i| matches!(i, Instruction::MemoryInit { .. } | Instruction::DataDrop(_)))
+        }) {
+            wasm_module.section(&wasm_encoder::DataCountSection {
+                count: module.data_segments.len() as u32,
+            });
+        }
+
         // Build code section (function bodies)
         let mut code = CodeSection::new();
         for func in &module.functions {
diff --git a/loom-core/src/verify.rs b/loom-core/src/verify.rs
index 02dfc5e..5f28a24 100644
--- a/loom-core/src/verify.rs
+++ b/loom-core/src/verify.rs
@@ -88,6 +88,191 @@ pub struct VerificationSignatureContext {
     pub function_bodies: Vec<Option<std::sync::Arc<Function>>>,
 }
 
+#[cfg(all(test, feature = "verification"))]
+mod memory_bound_tests_347 {
+    use super::*;
+
+    fn f(instrs: Vec<Instruction>) -> Function {
+        Function {
+            name: None,
+            signature: FunctionSignature {
+                params: vec![],
+                results: vec![],
+            },
+            locals: vec![],
+            instructions: instrs,
+        }
+    }
+
+    fn store() -> Instruction {
+        Instruction::I32Store {
+            offset: 0,
+            align: 2,
+            mem: 0,
+        }
+    }
+
+    fn load() -> Instruction {
+        Instruction::I64Load {
+            offset: 0,
+            align: 3,
+            mem: 0,
+        }
+    }
+
+    #[test]
+    fn counts_array_modelled_loads_and_stores() {
+        assert_eq!(count_array_memory_ops(&f(vec![])), 0);
+        assert_eq!(
+            count_array_memory_ops(&f(vec![store(), load(), Instruction::I32Const(1)])),
+            2,
+            "only the memory accesses count, not the arithmetic beside them"
+        );
+    }
+
+    /// The count must see through structured control flow. A body that hides
+    /// its stores inside a block would otherwise slip under the bound and
+    /// reintroduce the hang the bound exists to prevent.
+    #[test]
+    fn counts_nested_bodies() {
+        let inner = Instruction::Block {
+            block_type: BlockType::Empty,
+            body: vec![store(), store()],
+        };
+        let outer = Instruction::If {
+            block_type: BlockType::Empty,
+            then_body: vec![store(), inner],
+            else_body: vec![load()],
+        };
+        assert_eq!(
+            count_array_memory_ops(&f(vec![outer, store()])),
+            5,
+            "stores nested in block/if bodies must be counted"
+        );
+    }
+
+    /// Float and partial-width loads are deliberately NOT counted: they are
+    /// rejected earlier by `contains_unverifiable_instructions` and never
+    /// reach the array theory, so counting them would defer functions this
+    /// bound has no reason to defer.
+    #[test]
+    fn does_not_count_accesses_that_never_reach_the_array_theory() {
+        let float_store = Instruction::F64Store {
+            offset: 0,
+            align: 3,
+            mem: 0,
+        };
+        let partial_load = Instruction::I32Load8U {
+            offset: 0,
+            align: 0,
+            mem: 0,
+        };
+        assert_eq!(
+            count_array_memory_ops(&f(vec![float_store, partial_load])),
+            0
+        );
+    }
+
+    /// The #219 exemption, asserted as a property rather than left implicit in
+    /// the seam tests.
+    ///
+    /// The bound defers only bodies that are BOTH memory-dense and non-trivial.
+    /// Dropping the instruction floor makes the memory-seam and division-seam
+    /// dissolution tests fail — measured, not assumed: at a floor of 0 the
+    /// bound needs to be >= 4 for those to pass, while #347 needs <= 2, and
+    /// the two are irreconcilable without this exemption.
+    #[test]
+    fn a_tiny_memory_dense_body_is_exempt_from_the_bound() {
+        let tiny = f(vec![store(), store(), store(), store()]);
+        assert!(
+            count_array_memory_ops(&tiny) > DEFAULT_MAX_ARRAY_MEMORY_OPS,
+            "the fixture must exceed the memory bound, or it proves nothing"
+        );
+        assert!(
+            count_function_instructions(&tiny) <= DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR,
+            "a body this small must fall under the instruction floor, which is \
+             what keeps #219's seam-dissolution inlines verifiable"
+        );
+    }
+
+    /// The control for the exemption: a body that is memory-dense AND large
+    /// must NOT be exempt, or the bound would never fire and #347 returns.
+    #[test]
+    fn a_large_memory_dense_body_is_not_exempt() {
+        let mut instrs = vec![store(); 4];
+        instrs.extend(std::iter::repeat_n(
+            Instruction::I32Const(0),
+            DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR + 1,
+        ));
+        let big = f(instrs);
+        assert!(count_array_memory_ops(&big) > DEFAULT_MAX_ARRAY_MEMORY_OPS);
+        assert!(
+            count_function_instructions(&big) > DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR,
+            "this body must clear the floor so the bound actually applies to it"
+        );
+    }
+}
+
+/// Count the memory accesses in a function that the SMT encoder models with
+/// the solver's ARRAY theory (#347).
+///
+/// This exists because `count_function_instructions` bounds the wrong
+/// quantity. Profiling the meld-fused module that would not finish in 300 s
+/// showed 97% of wall time inside `Z3_solver_check`, and **40% of the whole
+/// process** inside `theory_array_base::propagate` →
+/// `assert_store_axiom2_core`. Those are the array store axioms, and they are
+/// instantiated PAIRWISE, so the cost grows quadratically in the number of
+/// memory accesses reachable in one function body.
+///
+/// Instruction count does not track that at all: a body well under
+/// `LOOM_Z3_MAX_INSTRUCTIONS` can carry enough stores to be intractable,
+/// which is exactly how a 463 KB module ran past 455 s while a structurally
+/// denser 1.13 MB module finished in 39 s.
+///
+/// Only the inliner triggers it in practice, and for a structural reason: it
+/// is the one pass that concatenates callee bodies into a caller, so it is the
+/// one pass that multiplies memory accesses PER FUNCTION. Every other pass
+/// leaves that count roughly where it found it.
+///
+/// Counted here are the accesses the encoder actually lowers to array
+/// select/store. The float and partial-width loads that
+/// `contains_memory_instructions` rejects are deliberately NOT counted: those
+/// bail out earlier and never reach the array theory, so counting them would
+/// defer functions this bound has no reason to defer.
+#[cfg(feature = "verification")]
+fn count_array_memory_ops(func: &Function) -> usize {
+    fn count_body(instrs: &[Instruction]) -> usize {
+        let mut n = 0;
+        for instr in instrs {
+            match instr {
+                Instruction::I32Load { .. }
+                | Instruction::I64Load { .. }
+                | Instruction::I32Store { .. }
+                | Instruction::I64Store { .. }
+                | Instruction::I32Store8 { .. }
+                | Instruction::I32Store16 { .. }
+                | Instruction::I64Store8 { .. }
+                | Instruction::I64Store16 { .. }
+                | Instruction::I64Store32 { .. } => n += 1,
+                Instruction::Block { body, .. } | Instruction::Loop { body, .. } => {
+                    n += count_body(body);
+                }
+                Instruction::If {
+                    then_body,
+                    else_body,
+                    ..
+                } => {
+                    n += count_body(then_body);
+                    n += count_body(else_body);
+                }
+                _ => {}
+            }
+        }
+        n
+    }
+    count_body(&func.instructions)
+}
+
 #[cfg(feature = "verification")]
 impl VerificationSignatureContext {
     /// Create a new empty context (for backwards compatibility)
@@ -1527,6 +1712,39 @@ const MAX_LOOP_NESTING_DEPTH: usize = 1;
 /// When false, falls back to bounded unrolling only
 const ENABLE_K_INDUCTION: bool = true;
 
+/// Default ceiling on array-modelled memory accesses per function before the
+/// translation validator defers the obligation (#347).
+///
+/// Chosen by measurement, not taste. Full-pipeline sweep on the meld-fused
+/// module from #347 (463 KB, 1444 functions), which does not finish at all
+/// today — killed at 455 s:
+///
+/// | bound | wall clock | proven |
+/// |-------|-----------|--------|
+/// | 0     | 2 s       | 21.6%  |
+/// | **2** | **45 s**  | 45.0%  |
+/// | 4     | > 240 s   | —      |
+///
+/// The knee between 2 and 4 is far sharper than a "quadratic in stores"
+/// reading suggests, because memory is modelled BYTE-level: one `i64.store`
+/// is eight array stores, so four of them already generate on the order of
+/// 500 axiom pairs.
+///
+/// That sharpness makes this number fragile — it is tuned on ONE module and
+/// should be revisited against a corpus. It is recorded here rather than
+/// hidden so the next person knows it is empirical and narrow, not derived.
+///
+/// A wall-clock budget would generalise better and is deliberately NOT used:
+/// which functions got verified would then depend on machine speed, so the
+/// same input could produce different output, violating REQ-14 (deterministic
+/// optimization output). A count is the only mechanism here that stays
+/// deterministic.
+const DEFAULT_MAX_ARRAY_MEMORY_OPS: usize = 2;
+
+/// Bodies at or below this instruction count are exempt from the memory-op
+/// bound (#347). See the sweep in `TEST-347-MEMORY-OP-BOUND`.
+const DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR: usize = 16;
+
 /// K value for K-induction (number of base case iterations)
 /// Higher K = stronger base case but slower verification
 #[allow(dead_code)]
@@ -2832,6 +3050,27 @@ thread_local! {
         const { std::cell::Cell::new(None) };
 }
 
+thread_local! {
+    /// Why the validator REFUSED an obligation, when the reason is more
+    /// specific than "the proof failed" — read back by `verify_or_revert` so
+    /// the revert is attributed in `--stats` instead of landing in the
+    /// undifferentiated per-pass bucket.
+    static DEFERRAL_REASON: std::cell::Cell<Option<&'static str>> =
+        const { std::cell::Cell::new(None) };
+}
+
+/// Record why this obligation is being refused.
+#[cfg(feature = "verification")]
+fn note_deferral_reason(reason: &'static str) {
+    DEFERRAL_REASON.with(|c| c.set(Some(reason)));
+}
+
+/// Read and clear the pending refusal reason.
+#[cfg(feature = "verification")]
+fn take_deferral_reason() -> Option<&'static str> {
+    DEFERRAL_REASON.with(|c| c.take())
+}
+
 /// Record that this attempt is about to be ACCEPTED without a proof.
 #[cfg(feature = "verification")]
 fn note_unproven_acceptance(reason: &'static str) {
@@ -3396,6 +3635,71 @@ impl TranslationValidator {
             return Ok(());
         }
 
+        // #347 — MEMORY-OPERATION bound, beside the instruction bound above.
+        //
+        // The instruction bound cannot see the cost that actually blows up
+        // here. Profiling a meld-fused module that ran past 455 s put 97% of
+        // wall time in `Z3_solver_check` and 40% of the whole process in the
+        // solver's array theory instantiating store axioms PAIRWISE — a cost
+        // quadratic in memory accesses per body, which inlining multiplies by
+        // concatenating callees into their caller.
+        //
+        // Two things this deliberately is NOT:
+        //
+        //  * It is not a fix. It buys termination by declining to verify the
+        //    hardest inlines, so it trades proof coverage for completing at
+        //    all. Those obligations are only really discharged when the
+        //    memory model stops being the incumbent's array theory (#313
+        //    slice 5). The honest framing is a bound, not a solution.
+        //  * It is not a timeout. The solver's own timeout IS wired
+        //    (`LOOM_Z3_TIMEOUT_MS`, default 5000) and measurably does not
+        //    bound this: at 100 ms the pass still exceeded 120 s, because the
+        //    time goes into axiom instantiation and internalisation rather
+        //    than the search the timeout guards.
+        //
+        // The transform is KEPT, exactly as with the instruction bound, and
+        // recorded as kept-without-proof so `--stats` reports it against a
+        // denominator instead of it vanishing (#331). A deferral nobody can
+        // see is the failure mode this project keeps finding.
+        let max_memory_ops: usize = std::env::var("LOOM_Z3_MAX_MEMORY_OPS")
+            .ok()
+            .and_then(|s| s.parse().ok())
+            .unwrap_or(DEFAULT_MAX_ARRAY_MEMORY_OPS);
+        let n_memory_ops =
+            count_array_memory_ops(&self.original).max(count_array_memory_ops(optimized));
+        // Tiny bodies are exempt regardless of memory-op count: they are
+        // cheap for the solver whatever they touch, and they are where the
+        // #219 seam-dissolution inlines live. Bounding them would trade a
+        // shipped, silicon-validated capability for nothing measurable.
+        let memory_bound_floor: usize = std::env::var("LOOM_Z3_MEMORY_BOUND_FLOOR")
+            .ok()
+            .and_then(|s| s.parse().ok())
+            .unwrap_or(DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR);
+        if n_memory_ops > max_memory_ops && n_instr > memory_bound_floor {
+            // REVERT, not keep — deliberately unlike the instruction bound
+            // directly above.
+            //
+            // Returning `Ok(())` would accept a transform nothing verified,
+            // and at a default this low that would ship thousands of unproven
+            // transforms per module: the wrong direction for a charter whose
+            // rule is "skip the function rather than risk incorrect
+            // optimization". Refusing costs optimization on memory-dense
+            // inlines and costs nothing in safety, which is what makes a bound
+            // this aggressive defensible at all.
+            //
+            // The instruction bound above still keeps. That inconsistency is
+            // real and is left visible rather than quietly harmonised here —
+            // changing long-shipped behaviour belongs in its own change.
+            note_deferral_reason("memory-ops-over-threshold");
+            return Err(anyhow!(
+                "{}: {} array-modelled memory operations exceeds the limit of {} \
+                 (#347) - optimization rejected (unproven)",
+                self.pass_name,
+                n_memory_ops,
+                max_memory_ops
+            ));
+        }
+
         // PR-C (#219) M3.2: precise acyclic-CF fast-path for the inliner. The
         // main encoder models br_table approximately and a br_table callee is
         // not straight-line-by-body-modelable, so it cannot prove `call F`
@@ -3483,6 +3787,8 @@ impl TranslationValidator {
     /// Reverts are recorded in `crate::stats::record_revert(pass_name)` so
     /// callers can observe how often verification rejects a transform.
     pub fn verify_or_revert(&self, func: &mut Function) -> bool {
+        // Clear any stale note before the attempt we are about to classify.
+        let _ = take_deferral_reason();
         match self.verify(func) {
             Ok(()) => true,
             Err(e) => {
@@ -3490,7 +3796,17 @@ impl TranslationValidator {
                     "{}: reverting function: {}",
                     self.pass_name, e
                 ));
-                crate::stats::record_revert(&self.pass_name);
+                // Attribute the revert when the validator said something more
+                // specific than "the proof failed". Recorded HERE and only
+                // here: recording at the refusal site too would count one
+                // revert twice, and an inflated revert total is the same class
+                // of defect as the mislabelled one this replaced.
+                match take_deferral_reason() {
+                    Some(reason) => {
+                        crate::stats::record_revert(&format!("{}/{}", self.pass_name, reason))
+                    }
+                    None => crate::stats::record_revert(&self.pass_name),
+                }
                 func.instructions = self.original.instructions.clone();
                 func.locals = self.original.locals.clone();
                 false
diff --git a/safety/requirements/verification.yaml b/safety/requirements/verification.yaml
index a7005bd..77ebfbe 100644
--- a/safety/requirements/verification.yaml
+++ b/safety/requirements/verification.yaml
@@ -1119,3 +1119,148 @@ artifacts:
         target: REQ-3
       - type: verifies
         target: REQ-1
+
+  # ============================================================================
+  # #346 / #345 — v1.4.1: the binary must not emit what it has not validated.
+  #
+  # The encoder never emitted a data count section — there was no reference to
+  # it anywhere in the crate — so any module using `memory.init` or `data.drop`
+  # came out structurally INVALID. Nothing caught it, because the #257
+  # output-validation backstop lives inside `optimize_module` and the CLI
+  # drives the passes directly (#345). A guarantee reachable only from a
+  # function nobody calls is prose, not a guarantee.
+  # ============================================================================
+
+  - id: TEST-346-OUTPUT-IS-VALIDATED-BEFORE-IT-IS-WRITTEN
+    type: feature
+    title: the data count section is emitted, and no unvalidated module is ever written (#346, #345)
+    description: >
+      Verifies both halves of the #346 defect. The narrow half: the encoder
+      now emits the data count section (id 12, between element and code)
+      whenever `memory.init` or `data.drop` survive into the output. The spec
+      makes that section mandatory for those instructions — it exists so they
+      can be validated without scanning the data section — and loom preserved
+      the data section and the instructions while dropping the section that
+      makes them legal.
+      The systemic half, which is the one that generalises: every CLI write
+      path now runs the authoritative WebAssembly spec validator BEFORE
+      writing, using the same check `optimize_module` has applied since #257.
+      On failure the ORIGINAL input is written instead — but only after the
+      original is itself proven valid, so a `.wat` input or an
+      already-invalid one is never copied over the output path and presented
+      as a module — and the exit code is non-zero. Worst case becomes
+      unoptimized-but-valid output; success can no longer be printed over an
+      invalid artifact.
+      Asserted: (1) a module using `memory.init` and `data.drop` is emitted
+      valid AND carries a data count section — the second assertion matters
+      because validation alone would also pass if the instructions were
+      simply deleted; (2) across every valid in-tree wasm fixture, a
+      successful exit implies the artifact on disk validates; (3) fed bytes
+      that definitely do not validate, the gate REFUSES, does not write them,
+      and restores the original; (4) fed valid bytes it writes them
+      byte-for-byte — the positive control, without which a gate that refused
+      everything would pass (3).
+      Confirmed discriminating: with the encoder fix reverted, (1) fails on
+      "data count section required".
+    fields:
+      method: automated-test
+      acceptance-criteria:
+        - "Given a module using memory.init/data.drop, the output validates AND contains a data count section"
+        - "Given any valid fixture, exit 0 implies the written artifact validates"
+        - "Given bytes that do not validate, the gate refuses, writes the original instead, and exits non-zero"
+        - "Given valid bytes, the gate writes them unchanged"
+        - "Given an original that is not itself valid wasm, it is NOT written over the output path"
+      steps:
+        - run: |
+            cargo test --release -p loom-cli --test output_validation
+        - run: |
+            cargo test --release -p loom-cli --bin loom -- the_output_gate
+    status: verified
+    release: v1.4.1
+    tags: [v141, encoder, honesty, no-silent-failures, safety]
+    links:
+      - type: verifies
+        target: REQ-3
+      - type: verifies
+        target: REQ-12
+      - type: verifies
+        target: REQ-1
+
+  # ============================================================================
+  # #347 — v1.4.1: bound the quantity that actually drives solver cost.
+  #
+  # 97 of 100 real-world components exceeded a 60 s budget; one 463 KB fused
+  # module ran past 455 s and was killed, while a structurally denser 1.13 MB
+  # ordinary module finished in 39 s. Profiling put 97% of wall clock inside
+  # the solver and 40% of the whole process inside its ARRAY theory
+  # instantiating store axioms pairwise. Instruction count — the only quantity
+  # loom bounded — does not track that at all.
+  # ============================================================================
+
+  - id: TEST-347-MEMORY-OP-BOUND
+    type: feature
+    title: the translation validator bounds array-modelled memory operations, and refuses rather than ships what it declines to verify (#347)
+    description: >
+      Verifies the memory-operation bound that makes store-dense inlines
+      terminate. The cost driver is the solver's array theory, whose store
+      axioms are instantiated pairwise, so cost grows quadratically in memory
+      accesses per body — a quantity inlining multiplies by concatenating
+      callee bodies into their caller, which is why only the inliner triggers
+      it.
+      Two design decisions are recorded because both were reached by
+      measurement and both could reasonably have gone the other way.
+      FIRST, exceeding the bound REVERTS rather than keeps. The existing
+      instruction bound keeps, and copying that here would have shipped
+      thousands of unproven transforms per module at this bound — the wrong
+      direction for a charter whose rule is to skip rather than risk. Refusing
+      costs optimization and costs nothing in safety. The instruction bound's
+      keep-behaviour is left untouched and the inconsistency stated rather
+      than quietly harmonised.
+      SECOND, tiny bodies are EXEMPT. Without the exemption the bound must be
+      2 or lower for the 463 KB module to finish, while #219's memory-seam and
+      division-seam dissolution require 4 or higher — irreconcilable, and the
+      naive bound silently broke a shipped, silicon-validated capability. The
+      exemption resolves it: measured 45 s (from >455 s killed) with the seam
+      intact, and slightly BETTER proof coverage than without it (49.8% vs
+      45.2%).
+      A wall-clock budget would generalise better and is deliberately not
+      used: which functions got verified would depend on machine speed, so the
+      same input could produce different output, violating REQ-14. A count is
+      the only mechanism here that stays deterministic. The solver's own
+      timeout is wired and measurably does NOT bound this — at 100 ms the pass
+      still exceeded 120 s, because the cost is axiom instantiation rather
+      than the search a timeout guards.
+      Asserted: (1) the counter counts array-modelled loads and stores; (2) it
+      sees through block/if bodies, so a body cannot hide its stores under the
+      bound; (3) it does NOT count float or partial-width accesses, which bail
+      earlier and never reach the array theory; (4) a tiny memory-dense body
+      is exempt — the #219 property, asserted directly rather than left
+      implicit in the seam tests; (5) a LARGE memory-dense body is not exempt,
+      the control without which the bound could never fire.
+      This is a BOUND, not a solution: it buys termination by declining the
+      hardest obligations. They are discharged only when the memory model
+      stops being the incumbent's array theory (#313 slice 5).
+    fields:
+      method: automated-test
+      acceptance-criteria:
+        - "Given a body with nested stores, all of them are counted"
+        - "Given float/partial-width accesses, none are counted"
+        - "Given a tiny memory-dense body, the bound does NOT apply (#219 seams keep dissolving)"
+        - "Given a large memory-dense body, the bound DOES apply"
+        - "Given the bound fires, the transform is REVERTED and the revert is attributed by reason"
+        - "Given the #347 module at default settings, the full pipeline completes and the output validates"
+      steps:
+        - run: |
+            cargo test --release -p loom-core --features verification --lib memory_bound_tests_347
+        - run: |
+            cargo test --release -p loom-core --features verification --lib -- seam_fully_dissolves
+    status: verified
+    release: v1.4.1
+    tags: [v141, verification, performance, solver-migration]
+    links:
+      - type: verifies
+        target: REQ-5
+      - type: verifies
+        target: REQ-14
+      - type: verifies
+        target: REQ-3