diff --git a/VERIFICATION.md b/VERIFICATION.md
index 77b079879..b928079e5 100644
--- a/VERIFICATION.md
+++ b/VERIFICATION.md
@@ -254,6 +254,55 @@ retains the original accepted identifier language and all source-audit
 prohibitions. Raw logs are retained under ignored
 `target/semantic-reserved-identifiers-{lean-red,complete-variants,mutant}.log`.
 
+### explicit byte-literal lowering can fail
+
+A modeled byte literal used to be written `ByteArray.mk #[n, ...]`. It is now
+written `_root_.ByteArray.mk #[...]` with every octet an explicit
+`_root_.UInt8.ofNat (nat_lit n)`; an octet occurring four or more times in one
+literal is bound once by a `let __byteN` local to that literal, so no generated
+local outside the literal takes part in its meaning. The canonical document
+keeps the original decimal numbers and order. SM-19, for languages 1.1 and 1.2,
+reads every generated literal back with an independent closed-grammar reader
+(it neither evaluates Lean nor calls the renderer), checks the document
+display, verifies, and evaluates the generated definitions against the
+original bytes. MD-02 applies the same reader to every embedded artifact byte.
+The reader's own controls refuse foreign, noncanonical and unused syntax, and
+a binding name that disagrees with its value.
+
+Observed before the change: with the lowerer of `main` `243f0c734` unchanged,
+`conformance_sm_19` fails at its first fixture, the empty array, with
+`closed explicit-octet lowering: "expected closed byte syntax \"_root_.ByteArray.mk #[\""`.
+That is the reader rejecting the old spelling. It is not a Lean failure: the
+largest SM-19 corpus (1024 bytes, all 256 values) elaborates under `main`'s
+rendering at the default `maxRecDepth` (1.1 s; 0.8 s explicit).
+
+Measured, not claimed as an improvement beyond these numbers: Lean 4.32.1
+(x86-64 Linux, 4 cores, one run each) on a file holding one `public def` of a
+seeded-random byte literal in which all 256 values occur.
+
+| bytes | `maxRecDepth` | `main` rendering | explicit rendering |
+| --- | --- | --- | --- |
+| 4096 | 100000 | 3.0 s, ok | 2.1 s, ok |
+| 4096 | default | 2.6 s, ok | 2.3 s, ok |
+| 16384 | 100000 | 12.7 s, ok | 11.3 s, ok |
+| 16384 | default | 10.8 s, recursion depth | 8.9 s, recursion depth |
+| 65536 | 100000 | 37.1 s, heartbeats (`isDefEq`) | 49.2 s, heartbeats (`LCNF compiler`) |
+| 65536 | default | 33.3 s, heartbeats (`isDefEq`) | 42.7 s, recursion depth |
+
+Bisection at the default `maxRecDepth` (no `set_option`), by 16-byte steps
+between 1024 and 16384 bytes, one run per size, seeded-random bytes with all 256
+values present: the largest literal that elaborates is 6394 bytes under both
+renderings, and 6409 bytes fails under both (`maximum recursion depth has been
+reached`). Elaboration time at 4096 bytes is 2.0 s under both; at 6394 bytes it
+is 4.4 s for the `main` rendering and 3.3 s for the explicit one. The lowering
+does not move the largest elaborable literal.
+
+No size succeeds under one rendering and fails under the other. Both fail at
+16384 bytes at the default depth and at 65536 bytes at either depth; the
+explicit form is faster at 4096 and 16384 bytes and slower at 65536. The
+timing script is not committed; it writes the two spellings above for the
+same seeded bytes and runs `lean` on the file.
+
 ### native diagnostic detail can fail
 
 `CL-21` was registered before its named test failed on the unwired case.
diff --git a/crates/conformance/src/cases/models.rs b/crates/conformance/src/cases/models.rs
index c88b1f041..fcbfaac82 100644
--- a/crates/conformance/src/cases/models.rs
+++ b/crates/conformance/src/cases/models.rs
@@ -535,6 +535,97 @@ fn check_wide_artifact(root: &camino::Utf8Path) {
     );
 }
 
+// Decode the closed generated expression independently of the renderer. An
+// exact octet comparison must survive literal-local sharing, not accept an
+// opaque expression or merely find the bytes somewhere in the module.
+fn embedded_artifact_octets(lean: &str, name: &str) -> Vec<u8> {
+    let prefix = format!("@[expose] public def {name}.bytes : ByteArray := ");
+    let expressions = lean
+        .lines()
+        .filter_map(|line| line.strip_prefix(&prefix))
+        .collect::<Vec<_>>();
+    assert_eq!(expressions.len(), 1, "one exact artifact definition");
+    let mut expression = expressions[0];
+    if expression.starts_with('(') {
+        expression = expression
+            .strip_prefix('(')
+            .and_then(|value| value.strip_suffix(')'))
+            .expect("closed literal-local expression");
+    }
+    let octet = |text: &str| {
+        let value = text.parse::<u8>().expect("bounded octet");
+        assert_eq!(text, value.to_string(), "canonical octet");
+        value
+    };
+    let mut bindings = std::collections::BTreeMap::new();
+    while expression.starts_with("let ") {
+        let (binding, rest) = expression.split_once("; ").expect("local separator");
+        let (name, value) = binding
+            .strip_prefix("let __byte")
+            .and_then(|value| value.split_once(" : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit "))
+            .expect("closed octet binding");
+        let name = octet(name);
+        let value = octet(value.strip_suffix(')').expect("closed octet value"));
+        assert_eq!(name, value, "local name binds its own octet");
+        assert!(bindings.insert(name, value).is_none(), "unique local");
+        expression = rest;
+    }
+    let contents = expression
+        .strip_prefix("_root_.ByteArray.mk #[")
+        .and_then(|value| value.strip_suffix(']'))
+        .expect("closed byte array constructor");
+    if contents.is_empty() {
+        return Vec::new();
+    }
+    contents
+        .split(", ")
+        .map(|item| {
+            if let Some(name) = item.strip_prefix("__byte") {
+                *bindings.get(&octet(name)).expect("literal-local binding")
+            } else {
+                let value = item
+                    .strip_prefix("(_root_.UInt8.ofNat (nat_lit ")
+                    .and_then(|value| value.strip_suffix("))"))
+                    .expect("closed explicit octet");
+                octet(value)
+            }
+        })
+        .collect()
+}
+
+#[test]
+fn artifact_octet_oracle_rejects_opaque_unbound_and_forged_literals() {
+    let definition = |expression: &str| {
+        format!("@[expose] public def artifact.bytes : ByteArray := {expression}\n")
+    };
+    let direct = "_root_.ByteArray.mk #[(_root_.UInt8.ofNat (nat_lit 0)), (_root_.UInt8.ofNat (nat_lit 255))]";
+    assert_eq!(
+        embedded_artifact_octets(&definition(direct), "artifact"),
+        [0, 255]
+    );
+    let shared = "(let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 0); _root_.ByteArray.mk #[__byte0, __byte0])";
+    assert_eq!(
+        embedded_artifact_octets(&definition(shared), "artifact"),
+        [0, 0]
+    );
+    assert_eq!(
+        embedded_artifact_octets(&definition("_root_.ByteArray.mk #[]"), "artifact"),
+        Vec::<u8>::new()
+    );
+    for expression in [
+        "opaqueArtifact",
+        "_root_.ByteArray.mk #[__byte0]",
+        "_root_.ByteArray.mk #[(_root_.UInt8.ofNat (nat_lit 256))]",
+        "_root_.ByteArray.mk #[(_root_.UInt8.ofNat (nat_lit 00))]",
+        "(let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 1); _root_.ByteArray.mk #[__byte0])",
+        "(let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 0); let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 0); _root_.ByteArray.mk #[__byte0])",
+    ] {
+        assert!(std::panic::catch_unwind(|| embedded_artifact_octets(&definition(expression), "artifact")).is_err());
+    }
+    let duplicate = definition(direct) + &definition(direct);
+    assert!(std::panic::catch_unwind(|| embedded_artifact_octets(&duplicate, "artifact")).is_err());
+}
+
 fn md_02() {
     if let Ok(root) = std::env::var(WIDE_ARTIFACT_PROJECT) {
         check_wide_artifact(camino::Utf8Path::new(&root));
@@ -570,14 +661,7 @@ fn md_02() {
     let lean = support::lean_text(&build, "Recognizer");
     let banner = std::fs::read(project.root.join("artifacts/banner.bin").as_std_path())
         .expect("banner bytes");
-    let embedded = banner
-        .iter()
-        .map(u8::to_string)
-        .collect::<Vec<_>>()
-        .join(", ");
-    assert!(lean.contains(&format!(
-        "public def banner.bytes : ByteArray := ByteArray.mk #[{embedded}]"
-    )));
+    assert_eq!(embedded_artifact_octets(&lean, "banner"), banner);
     assert!(lean.contains("public theorem banner.decoded : banner = banner.bytes := rfl"));
     let weights = std::fs::read(
         project
@@ -591,9 +675,7 @@ fn md_02() {
         .map(u8::to_string)
         .collect::<Vec<_>>()
         .join(", ");
-    assert!(lean.contains(&format!(
-        "public def hiddenWeights.bytes : ByteArray := ByteArray.mk #[{embedded}]"
-    )));
+    assert_eq!(embedded_artifact_octets(&lean, "hiddenWeights"), weights);
     assert!(lean.contains(
         "public theorem hiddenWeights.decoded : (LexLeanModels.tensorMatches 1 true hiddenWeights.flatten hiddenWeights.bytes && (hiddenWeights.length == 12) && (hiddenWeights.map List.length == List.replicate 12 7)) = true := by decide"
     ));
diff --git a/crates/conformance/src/cases/semantic_ir.rs b/crates/conformance/src/cases/semantic_ir.rs
index d34a5318b..467eef779 100644
--- a/crates/conformance/src/cases/semantic_ir.rs
+++ b/crates/conformance/src/cases/semantic_ir.rs
@@ -7,6 +7,7 @@ use sha2::Digest;
 
 use crate::support::{self, P};
 
+mod bytes;
 mod names;
 mod strings;
 
@@ -140,25 +141,8 @@ fn verify_large_byte_declaration(varied: bool) {
     );
     let rendered = support::rendered(&project);
     let generated = support::lean_text(&rendered, "Main");
-    let emitted: Vec<_> = generated
-        .split("ByteArray.mk #[")
-        .skip(1)
-        .map(|tail| {
-            let literal = tail.split_once(']').expect("closed generated array").0;
-            if literal.is_empty() {
-                return String::new();
-            }
-            literal
-                .split(", ")
-                .map(|value| {
-                    format!(
-                        "{:02x}",
-                        value.parse::<u8>().expect("exact generated UInt8 literal")
-                    )
-                })
-                .collect::<String>()
-        })
-        .collect();
+    let emitted = bytes::emitted_literals(&generated)
+        .expect("every generated byte literal has the closed explicit-octet grammar");
     assert_eq!(
         emitted, expected,
         "the actual generated declaration retains every byte in order"
@@ -1097,6 +1081,7 @@ pub(crate) fn run(id: &str) {
             );
         }
         "SM-19" => {
+            bytes::verify();
             strings::verify();
             names::verify();
             verify_large_byte_declaration(false);
diff --git a/crates/conformance/src/cases/semantic_ir/bytes.rs b/crates/conformance/src/cases/semantic_ir/bytes.rs
new file mode 100644
index 000000000..32296445a
--- /dev/null
+++ b/crates/conformance/src/cases/semantic_ir/bytes.rs
@@ -0,0 +1,439 @@
+//! Independent readback and real evaluation of closed generated byte literals.
+
+use std::collections::BTreeMap;
+
+use crate::support::{self, P};
+use serde_json::json;
+
+const ARRAY: &str = "_root_.ByteArray.mk #[";
+const OCTET: &str = "_root_.UInt8.ofNat (nat_lit ";
+
+struct Reader<'a> {
+    remaining: &'a str,
+}
+
+impl Reader<'_> {
+    fn take(&mut self, expected: &str) -> Result<(), String> {
+        self.remaining = self
+            .remaining
+            .strip_prefix(expected)
+            .ok_or_else(|| format!("expected closed byte syntax {expected:?}"))?;
+        Ok(())
+    }
+
+    fn octet(&mut self) -> Result<u8, String> {
+        let count = self
+            .remaining
+            .bytes()
+            .take_while(u8::is_ascii_digit)
+            .count();
+        let number = &self.remaining[..count];
+        let value: u8 = number.parse().map_err(|_| "an octet is exactly 0..255")?;
+        if number != value.to_string() {
+            return Err("an octet has canonical decimal spelling".to_owned());
+        }
+        self.remaining = &self.remaining[count..];
+        Ok(value)
+    }
+
+    fn binding(&mut self) -> Result<(u8, u8), String> {
+        self.take("let __byte")?;
+        let name = self.octet()?;
+        self.take(" : _root_.UInt8 := ")?;
+        self.take(OCTET)?;
+        let value = self.octet()?;
+        self.take("); ")?;
+        Ok((name, value))
+    }
+}
+
+// This reader recognizes a closed grammar; it does not evaluate Lean, call the
+// renderer, or infer a value from the name of an unchecked shared binding.
+fn read_prefix(text: &str) -> Result<(Vec<u8>, usize), String> {
+    let mut reader = Reader { remaining: text };
+    let shared = text.starts_with("(let ");
+    let mut bindings = BTreeMap::new();
+    if shared {
+        reader.take("(")?;
+        while reader.remaining.starts_with("let ") {
+            let (name, value) = reader.binding()?;
+            if name != value
+                || bindings
+                    .last_key_value()
+                    .is_some_and(|(prior, _)| *prior >= name)
+            {
+                return Err("shared octets must be exact, distinct and ascending".to_owned());
+            }
+            bindings.insert(name, value);
+        }
+        if bindings.is_empty() {
+            return Err("a shared expression must bind an octet".to_owned());
+        }
+    }
+    reader.take(ARRAY)?;
+    let mut values = Vec::new();
+    let mut references = BTreeMap::<u8, usize>::new();
+    if !reader.remaining.starts_with(']') {
+        loop {
+            let value = if reader.remaining.starts_with("__byte") {
+                reader.take("__byte")?;
+                let name = reader.octet()?;
+                let value = *bindings
+                    .get(&name)
+                    .ok_or("a shared reference must be bound")?;
+                *references.entry(name).or_default() += 1;
+                value
+            } else {
+                reader.take("(")?;
+                reader.take(OCTET)?;
+                let value = reader.octet()?;
+                reader.take("))")?;
+                if bindings.contains_key(&value) {
+                    return Err("a shared octet cannot also be inlined".to_owned());
+                }
+                value
+            };
+            values.push(value);
+            if reader.remaining.starts_with(']') {
+                break;
+            }
+            reader.take(", ")?;
+        }
+    }
+    reader.take("]")?;
+    if shared {
+        reader.take(")")?;
+    }
+    let mut counts = BTreeMap::<u8, usize>::new();
+    for value in &values {
+        *counts.entry(*value).or_default() += 1;
+    }
+    for (value, count) in &counts {
+        if (*count >= 4) != bindings.contains_key(value) {
+            return Err(
+                "exactly the octets occurring at least four times must be shared".to_owned(),
+            );
+        }
+    }
+    if bindings
+        .keys()
+        .any(|value| references.get(value).copied().unwrap_or(0) < 4)
+    {
+        return Err("every binding must be used at least four times".to_owned());
+    }
+    Ok((values, text.len() - reader.remaining.len()))
+}
+
+fn read_expression(text: &str) -> Result<Vec<u8>, String> {
+    let (values, consumed) = read_prefix(text)?;
+    if consumed != text.len() {
+        return Err("trailing text outside the closed byte expression".to_owned());
+    }
+    Ok(values)
+}
+
+fn hex(values: &[u8]) -> String {
+    values.iter().map(|value| format!("{value:02x}")).collect()
+}
+
+pub(super) fn emitted_literals(mut text: &str) -> Result<Vec<String>, String> {
+    let mut values = Vec::new();
+    while let Some(array) = text.find("ByteArray.mk #[") {
+        let root = array
+            .checked_sub("_root_.".len())
+            .ok_or("an array must be rooted")?;
+        // Locate only an immediately adjacent closed binding sequence, not
+        // an unrelated earlier generated let enclosing this literal. This
+        // locates byte subexpressions in the two fixed nested-record fixtures;
+        // it is not a parser or authority for arbitrary surrounding Lean.
+        let start = text[..root]
+            .rfind("(let __byte")
+            .filter(|start| {
+                let mut reader = Reader {
+                    remaining: &text[start + 1..root],
+                };
+                while !reader.remaining.is_empty() {
+                    if reader.binding().is_err() {
+                        return false;
+                    }
+                }
+                true
+            })
+            .unwrap_or(root);
+        let (bytes, consumed) = read_prefix(&text[start..])?;
+        values.push(hex(&bytes));
+        text = &text[start + consumed..];
+    }
+    if text.contains("(let __byte") {
+        return Err("a binding without its byte array".to_owned());
+    }
+    Ok(values)
+}
+
+fn vectors() -> Vec<Vec<u8>> {
+    vec![
+        vec![],
+        vec![0, 255, 128, 192, 175, 237, 160, 128],
+        vec![0],
+        vec![0; 2],
+        vec![0; 3],
+        vec![0; 4],
+        vec![255; 4],
+        vec![0, 255, 0, 255, 0, 255, 0, 255, 128],
+        (0..=255).collect(),
+        (0..4).flat_map(|_| 0..=255).collect(),
+    ]
+}
+
+pub(super) fn verify() {
+    for language in ["1.1", "1.2"] {
+        verify_language(language);
+    }
+}
+
+fn verify_language(language: &str) {
+    let values = vectors();
+    let project = P::example();
+    project.edit(
+        "lexlean.toml",
+        "language = \"1.0\"",
+        &format!("language = \"{language}\""),
+    );
+    let bytes_type = json!({"kind":"bytes"});
+    let literal = |bytes: &[u8]| json!({"kind":"bytes", "hex":hex(bytes)});
+    let append = |left, right| {
+        json!({"kind":"primitive", "operation":"append", "result":bytes_type,
+        "arguments":[left, right]})
+    };
+    let mut declarations: Vec<_> = values
+        .iter()
+        .enumerate()
+        .map(|(index, bytes)| {
+            json!({"kind":"definition", "name":format!("literal{index}"), "parameters":[],
+            "result":bytes_type, "axioms":[], "body":literal(bytes)})
+        })
+        .collect();
+    declarations.push(json!({"kind":"definition", "name":"withBinders",
+        "parameters":[{"name":"llb0", "type":bytes_type}, {"name":"llb255", "type":bytes_type},
+                      {"name":"nat_lit", "type":bytes_type}], "result":bytes_type, "axioms":[],
+        "body":append(json!({"kind":"var", "name":"llb0"}),
+            append(literal(&[0,255,0,255,0,255,0,255]),
+                append(json!({"kind":"var", "name":"nat_lit"}), json!({"kind":"var", "name":"llb255"}))))}));
+    let spec = if language == "1.1" {
+        "lexlean/semantic-module/1"
+    } else {
+        "lexlean/semantic-module/2"
+    };
+    let module = json!({"spec":spec, "declarations":declarations});
+    project.write("src/Main.lex.tex", &format!(
+        "\\begin{{lexlean}}{{Main}}\n\\useglossary{{lexlean.std.nat@{language}.0}}\n\\title{{Natural number addition}}\n\\begin{{semanticmodule}}\n\\semanticdata{{{module}}}\n\\end{{semanticmodule}}\n\\end{{lexlean}}\n"
+    ));
+    project.relock();
+    let before = project
+        .engine()
+        .snapshot(lexlean::CheckRequest {
+            selection: lexlean::Selection::Entrypoints,
+        })
+        .expect("byte fixture snapshot")
+        .canonical_bytes();
+    let rendered = support::rendered(&project);
+    let lean = support::lean_text(&rendered, "Main");
+    for (index, expected) in values.iter().enumerate() {
+        let marker = format!("public def literal{index} : ByteArray := ");
+        let body = lean
+            .lines()
+            .find_map(|line| line.split_once(&marker).map(|(_, body)| body))
+            .expect("the actual generated literal definition");
+        assert_eq!(
+            read_expression(body).expect("closed explicit-octet lowering"),
+            *expected,
+            "language {language}, literal{index}: every original byte in order"
+        );
+    }
+    let tex = &rendered
+        .modules
+        .iter()
+        .find(|module| module.module == "Main")
+        .expect("Main")
+        .tex_text;
+    assert!(
+        !tex.contains("ofNat") && !tex.contains("\\_\\_byte"),
+        "canonical document must not expose lowering-only syntax"
+    );
+    let definitions: Vec<_> = tex
+        .lines()
+        .filter_map(|line| line.strip_prefix("\\noindent Definition: \\texttt{"))
+        .collect();
+    assert_eq!(
+        definitions.len(),
+        values.len() + 1,
+        "all document definitions remain"
+    );
+    for (shown, expected) in definitions.iter().zip(&values) {
+        let numbers = expected
+            .iter()
+            .map(u8::to_string)
+            .collect::<Vec<_>>()
+            .join(", ");
+        assert_eq!(
+            *shown,
+            format!("ByteArray.mk \\#[{numbers}]}}.\\par"),
+            "canonical byte display retains the original decimal numbers"
+        );
+    }
+    let _ = support::verify_ok_backed("SM-19", &project);
+    assert_eq!(
+        before,
+        project
+            .engine()
+            .snapshot(lexlean::CheckRequest {
+                selection: lexlean::Selection::Entrypoints,
+            })
+            .expect("verified byte fixture snapshot")
+            .canonical_bytes()
+    );
+    if support::lean_backed("SM-19") {
+        evaluate(&project, &lean, &values);
+    }
+}
+
+fn evaluate(project: &P, lean: &str, values: &[Vec<u8>]) {
+    use lexlean::verify::child::{ChildHome, ChildSpec, Normalizer};
+
+    let mut probes = String::new();
+    for (index, bytes) in values.iter().enumerate() {
+        let expected = bytes
+            .iter()
+            .map(u8::to_string)
+            .collect::<Vec<_>>()
+            .join(", ");
+        probes.push_str(&format!("#eval (LexLeanExample.Main.literal{index}.toList.map UInt8.toNat) == ([{expected}] : List Nat)\n"));
+    }
+    probes.push_str("#eval ((LexLeanExample.Main.withBinders (ByteArray.mk #[19]) (ByteArray.mk #[29]) (ByteArray.mk #[23])).toList.map UInt8.toNat) == ([19, 0, 255, 0, 255, 0, 255, 0, 255, 23, 29] : List Nat)\n");
+    let directory = tempfile::tempdir().expect("byte evaluation directory");
+    let scratch = camino::Utf8Path::from_path(directory.path()).expect("UTF-8 scratch path");
+    let path = scratch.join("ByteRuntime.lean");
+    std::fs::write(&path, format!("{lean}\n{probes}"))
+        .expect("generated bytes and independent probes");
+    let _guard = support::env_shared();
+    let limits = support::limits(project);
+    let toolchain = lexlean::verify::toolchain::preflight(&limits).expect("pinned Lean admission");
+    let bin = toolchain.root.join("bin");
+    // The generated module imports the shipped runtime (SPEC.md §17.12); its
+    // objects are compiled here by the same pinned Lean so the probes run the
+    // actual generated text, not a copy with the import removed.
+    let compiled = scratch.join("objects");
+    let sources = scratch.join("runtime");
+    let search = std::env::join_paths([
+        compiled.as_std_path(),
+        toolchain.root.join("lib/lean").as_std_path(),
+    ])
+    .expect("LEAN_PATH");
+    for runtime in lexlean::backend::runtime::imported_by([lean]).expect("the shipped runtime") {
+        let relative = runtime.name.replace('.', "/");
+        let source = sources.join(format!("{relative}.lean"));
+        let object = compiled.join(format!("{relative}.olean"));
+        for directory in [source.parent(), object.parent()] {
+            std::fs::create_dir_all(directory.expect("parent")).expect("runtime directory");
+        }
+        std::fs::write(&source, &runtime.text).expect("runtime source");
+        let built = std::process::Command::new(&toolchain.lean.path)
+            .arg("-o")
+            .arg(&object)
+            .arg(format!("{relative}.lean"))
+            .current_dir(&sources)
+            .env("LEAN_PATH", &search)
+            .output()
+            .expect("pinned Lean compiles the runtime");
+        assert!(
+            built.status.success(),
+            "{} does not compile:\n{}\n{}",
+            runtime.name,
+            String::from_utf8_lossy(&built.stdout),
+            String::from_utf8_lossy(&built.stderr)
+        );
+    }
+    let normalizer = Normalizer::new(scratch, &project.root, scratch, &toolchain.root);
+    let output = lexlean::verify::child::run(
+        &ChildSpec {
+            tool: "lean",
+            module: Some("ByteRuntime".to_owned()),
+            program: &toolchain.lean.path,
+            executable_sha256: toolchain.lean.sha256,
+            argv: vec![path.to_string()],
+            cwd: scratch,
+            extra_env: vec![(
+                "LEAN_PATH".to_owned(),
+                search.to_string_lossy().into_owned(),
+            )],
+            home: ChildHome::Toolchain {
+                toolchain_bin: &bin,
+            },
+        },
+        &limits,
+        &normalizer,
+    )
+    .expect("pinned Lean evaluates actual generated definitions under unchanged child limits");
+    assert_eq!(output.exit_code, 0, "{}\n{}", output.stdout, output.stderr);
+    assert_eq!(output.stdout, "true\n".repeat(values.len() + 1));
+}
+
+#[cfg(test)]
+mod tests {
+    use super::{emitted_literals, read_expression, ARRAY, OCTET};
+
+    #[test]
+    fn closed_byte_oracle_refuses_foreign_noncanonical_and_unused_syntax() {
+        let empty = format!("{ARRAY}]");
+        assert_eq!(read_expression(&empty).expect("empty"), Vec::<u8>::new());
+        let shared = "(let __byte255 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 255); _root_.ByteArray.mk #[__byte255, __byte255, __byte255, __byte255])";
+        assert_eq!(read_expression(shared).expect("shared"), vec![255; 4]);
+        assert_eq!(
+            emitted_literals(&format!("(let __byte0 : Nat := 9; {empty})")).expect("outer local"),
+            vec![String::new()]
+        );
+        assert_eq!(
+            emitted_literals(&format!("(let __byte0 : Nat := 9; {shared})"))
+                .expect("nested local scope"),
+            vec!["ffffffff"]
+        );
+        assert!(emitted_literals(&shared.replace("nat_lit 255", "nat_lit 254")).is_err());
+        for bad in [
+            "ByteArray.mk #[255]".to_owned(),
+            format!("{ARRAY}({OCTET}256))]"),
+            format!("{ARRAY}({OCTET}00))]"),
+            format!("{ARRAY}__byte255]"),
+            format!("{empty}; IO.println 0"),
+            shared.replace("nat_lit 255", "nat_lit 254"),
+            shared.replace("let __byte255", "let foreign"),
+            shared.replace(" := _root_.UInt8.ofNat (nat_lit 255)", " := __byte255"),
+            shared.replace(", __byte255", ""),
+            shared.replace("; _root_.ByteArray", "; let __byte255 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 255); _root_.ByteArray"),
+            shared.replace("; _root_.ByteArray", "; let __byte254 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 254); _root_.ByteArray"),
+            shared.replace("#[__byte255", "#[(_root_.UInt8.ofNat (nat_lit 255))"),
+            format!("{ARRAY}({OCTET}0)), ({OCTET}0)), ({OCTET}0)), ({OCTET}0))]"),
+        ] {
+            assert!(read_expression(&bad).is_err(), "unexpectedly admitted {bad}");
+        }
+    }
+
+    #[test]
+    fn closed_byte_oracle_reads_values_not_the_expected_literal_or_binding_name() {
+        let original = format!("{ARRAY}({OCTET}0)), ({OCTET}255)), ({OCTET}128))]");
+        let expected = vec![0, 255, 128];
+        assert_eq!(read_expression(&original).expect("original"), expected);
+        for mutant in [
+            original.replace("nat_lit 255", "nat_lit 254"),
+            original
+                .replace("nat_lit 0", "nat_lit 255")
+                .replace("nat_lit 128", "nat_lit 0"),
+            original.replace(", (_root_.UInt8.ofNat (nat_lit 128))", ""),
+            original.replace("nat_lit 128", "nat_lit 255"),
+        ] {
+            assert_ne!(
+                read_expression(&mutant).expect("well-formed mutation"),
+                expected
+            );
+        }
+    }
+}
diff --git a/crates/lexlean/src/backend/semantic.rs b/crates/lexlean/src/backend/semantic.rs
index eda958ef1..2f3fd6575 100644
--- a/crates/lexlean/src/backend/semantic.rs
+++ b/crates/lexlean/src/backend/semantic.rs
@@ -803,10 +803,46 @@ impl Render<'_> {
                         let pair = core::str::from_utf8(pair).expect("validated byte literal");
                         u8::from_str_radix(pair, 16).expect("validated byte literal")
                     })
-                    .map(|value| value.to_string())
+                    .collect::<Vec<_>>();
+                if self.document {
+                    let numbers = values
+                        .iter()
+                        .map(u8::to_string)
+                        .collect::<Vec<_>>()
+                        .join(", ");
+                    return format!("ByteArray.mk #[{numbers}]");
+                }
+                let mut counts = [0_usize; 256];
+                for value in &values {
+                    counts[usize::from(*value)] += 1;
+                }
+                // Keep sharing inside this literal: generated locals outside it
+                // must not participate in the meaning of its octets.
+                let mut bindings = String::new();
+                for (value, count) in counts.iter().enumerate() {
+                    if *count >= 4 {
+                        bindings.push_str(&format!(
+                            "let __byte{value} : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit {value}); "
+                        ));
+                    }
+                }
+                let octets = values
+                    .iter()
+                    .map(|value| {
+                        if counts[usize::from(*value)] >= 4 {
+                            format!("__byte{value}")
+                        } else {
+                            format!("(_root_.UInt8.ofNat (nat_lit {value}))")
+                        }
+                    })
                     .collect::<Vec<_>>()
                     .join(", ");
-                format!("ByteArray.mk #[{values}]")
+                let array = format!("_root_.ByteArray.mk #[{octets}]");
+                if bindings.is_empty() {
+                    array
+                } else {
+                    format!("({bindings}{array})")
+                }
             }
             SemanticTerm::Primitive {
                 operation,
@@ -3083,6 +3119,103 @@ pub fn render_latex(
     }
 }
 
+#[cfg(test)]
+mod byte_literal_tests {
+    use super::{Render, SemanticParameter, SemanticTerm, SemanticType};
+
+    fn render(document: bool, term: &SemanticTerm) -> String {
+        let imports = std::collections::BTreeMap::new();
+        Render {
+            prefix: "ByteFixture",
+            lean_imports: &imports,
+            hypotheses: std::collections::BTreeMap::new(),
+            document,
+            qualify: None,
+        }
+        .term(term)
+    }
+
+    fn literal(values: &[u8]) -> SemanticTerm {
+        SemanticTerm::Bytes {
+            hex: values.iter().map(|value| format!("{value:02x}")).collect(),
+        }
+    }
+
+    #[test]
+    fn byte_literals_are_explicit_octets_without_changing_document_numbers() {
+        for values in [vec![], vec![0, 255, 128], (0..=255).collect()] {
+            let term = literal(&values);
+            let explicit = values
+                .iter()
+                .map(|value| format!("(_root_.UInt8.ofNat (nat_lit {value}))"))
+                .collect::<Vec<_>>()
+                .join(", ");
+            assert_eq!(
+                render(false, &term),
+                format!("_root_.ByteArray.mk #[{explicit}]")
+            );
+            let numbers = values
+                .iter()
+                .map(u8::to_string)
+                .collect::<Vec<_>>()
+                .join(", ");
+            assert_eq!(render(true, &term), format!("ByteArray.mk #[{numbers}]"));
+        }
+    }
+
+    #[test]
+    fn repeated_octets_have_one_closed_binding_at_the_four_occurrence_boundary() {
+        assert_eq!(
+            render(false, &literal(&[0, 255, 0, 255, 0, 255, 0, 255, 128])),
+            "(let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 0); let __byte255 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 255); _root_.ByteArray.mk #[__byte0, __byte255, __byte0, __byte255, __byte0, __byte255, __byte0, __byte255, (_root_.UInt8.ofNat (nat_lit 128))])"
+        );
+        for count in 1..=3 {
+            let text = render(false, &literal(&vec![255; count]));
+            assert!(!text.contains("let "), "{count} occurrences: {text}");
+            assert_eq!(text.matches("UInt8.ofNat").count(), count);
+        }
+        let all: Vec<u8> = (0..4).flat_map(|_| 0..=255).collect();
+        let text = render(false, &literal(&all));
+        assert_eq!(text.matches("let __byte").count(), 256);
+        assert_eq!(text.matches("UInt8.ofNat").count(), 256);
+        assert_eq!(text.matches("_root_.ByteArray.mk #[").count(), 1);
+        let numbers = all.iter().map(u8::to_string).collect::<Vec<_>>().join(", ");
+        assert_eq!(
+            render(true, &literal(&all)),
+            format!("ByteArray.mk #[{numbers}]")
+        );
+        assert_eq!(
+            text,
+            render(false, &literal(&all)),
+            "deterministic literal-local scope"
+        );
+    }
+
+    #[test]
+    fn shared_octet_scope_cannot_capture_an_outer_generated_local() {
+        let bytes = literal(&[0; 4]);
+        let term = SemanticTerm::Let {
+            binder: SemanticParameter {
+                name: "__byte0".to_owned(),
+                r#type: SemanticType::Nat,
+            },
+            value: Box::new(SemanticTerm::Nat {
+                value: "9".to_owned(),
+            }),
+            body: Box::new(SemanticTerm::Pair {
+                left: Box::new(SemanticTerm::Var {
+                    name: "__byte0".to_owned(),
+                }),
+                right: Box::new(bytes),
+            }),
+        };
+        assert_eq!(
+            render(false, &term),
+            "(let __byte0 : Nat := 9; (__byte0, (let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 0); _root_.ByteArray.mk #[__byte0, __byte0, __byte0, __byte0])))"
+        );
+    }
+}
+
 #[cfg(test)]
 mod declaration_span_tests {
     use super::declaration_spans_in;
diff --git a/features/suites/semantic-ir.feature b/features/suites/semantic-ir.feature
index 3bc22d8c8..16ae42d58 100644
--- a/features/suites/semantic-ir.feature
+++ b/features/suites/semantic-ir.feature
@@ -133,6 +133,7 @@ Feature: semantic-ir
     Then the generated runtime and module elaborate and replay
     And each computational definition reports exactly its source-declared axiom policy
     And nested records retain every large arbitrary-byte literal during elaboration and replay
+    And byte literals use closed explicit octets with deterministic literal-local sharing while canonical document numbers and every byte remain unchanged
 
   @SM-20 @build
   Scenario: Noncanonical, out-of-range, invalid-byte, ill-typed, and unbounded fixed-width values fail before either backend runs.