diff --git a/Cargo.lock b/Cargo.lock
index cb2d633c..f8159d06 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1160,7 +1160,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_builtins"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "chrono",
  "fast-float",
@@ -1185,7 +1185,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_bytecode"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "num-bigint",
  "oxide_log",
@@ -1193,7 +1193,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_cfg"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "oxide_bytecode",
  "oxide_emit",
@@ -1204,7 +1204,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_cli"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "ansi_term",
  "bumpalo",
@@ -1226,7 +1226,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_code_cache"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "lru",
  "oxide_bytecode",
@@ -1235,7 +1235,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_compiler"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "oxide_bytecode",
  "oxide_cfg",
@@ -1255,7 +1255,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_dce"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "oxide_bytecode",
  "oxide_cfg",
@@ -1269,7 +1269,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_emit"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "num-bigint",
  "oxc_allocator",
@@ -1284,7 +1284,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_engine"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "oxide_bytecode",
  "oxide_compiler",
@@ -1296,7 +1296,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_ir"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "oxide_bytecode",
  "oxide_log",
@@ -1305,7 +1305,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_kernel"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "bumpalo",
  "dashmap",
@@ -1319,7 +1319,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_liveness"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "oxide_bytecode",
  "oxide_cfg",
@@ -1331,7 +1331,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_log"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "tracing",
  "tracing-appender",
@@ -1340,7 +1340,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_parser"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "oxc_allocator",
  "oxc_ast",
@@ -1355,7 +1355,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_regalloc"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "oxide_bytecode",
  "oxide_cfg",
@@ -1371,7 +1371,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_runtime_api"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "num-bigint",
  "num-traits",
@@ -1384,7 +1384,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_test262"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "oxide_bytecode",
  "oxide_compiler",
@@ -1402,7 +1402,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_types"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "bumpalo",
  "dashmap",
@@ -1415,7 +1415,7 @@ dependencies = [
 
 [[package]]
 name = "oxide_vm"
-version = "0.13.12"
+version = "0.13.13"
 dependencies = [
  "bumpalo",
  "chrono",
diff --git a/Cargo.toml b/Cargo.toml
index d299059a..33448c26 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -23,7 +23,7 @@ members = [
 ]
 
 [workspace.package]
-version = "0.13.12"
+version = "0.13.13"
 edition = "2021"
 license = "MIT"
 rust-version = "1.80"
diff --git a/crates/oxide_emit/src/expr/identifier.rs b/crates/oxide_emit/src/expr/identifier.rs
index a44da956..0c245da2 100644
--- a/crates/oxide_emit/src/expr/identifier.rs
+++ b/crates/oxide_emit/src/expr/identifier.rs
@@ -272,7 +272,8 @@ impl Emitter {
     /// # 边界与前提
     /// - 仅在 `with_stack` 非空且名字非 with 内部绑定时调用。
     /// - 对象属性存在性判定与动态读取一致（`in` 含原型链）。
-    /// - 回退目标未在静态作用域声明时不登记全局（with 外不应可见）。
+    /// - 回退目标未在静态作用域声明时落隐式全局（sloppy 物化全局属性，
+    ///   strict 抛 ReferenceError），与静态写路径同形。
     pub(crate) fn emit_with_dynamic_write(
         &self, name: &str, val_reg: u32, const_flag: u16, ctx: &mut CompileCtx,
     ) -> Result<(), String> {
@@ -297,10 +298,9 @@ impl Emitter {
         ctx.inst(Inst::jmp(end_label));
 
         ctx.labels.set_label_pos(fallback_label, ctx.insts.len());
-        // 回退只写静态作用域已声明的绑定；未声明时丢弃值（隐式全局在 with 外不可解析）。
-        if ctx.scopes.symbols.lookup_any(name).is_some() {
-            self.emit_identifier_store(name, val_reg, const_flag, ctx)?;
-        }
+        // 回退写静态作用域：已声明绑定走常规写路径；未声明名是隐式全局
+        // （sloppy 物化全局属性、strict 抛 ReferenceError），与静态写路径同形。
+        self.emit_identifier_store(name, val_reg, const_flag, ctx)?;
         ctx.labels.set_label_pos(end_label, ctx.insts.len());
         Ok(())
     }
diff --git a/crates/oxide_emit/src/shared/binding.rs b/crates/oxide_emit/src/shared/binding.rs
index ab49453b..70fd47f8 100644
--- a/crates/oxide_emit/src/shared/binding.rs
+++ b/crates/oxide_emit/src/shared/binding.rs
@@ -115,8 +115,8 @@ impl Emitter {
                 ));
             }
         } else if !ctx.with_stack.is_empty() && !ctx.is_with_internal_binding(name) {
-            // with 内 var 初始化：对象有该属性则写对象，否则写提升槽（动态解析）。
-            // ponytail: with 内顶层 var 不写全局对象属性，with 语句本身已是稀见用例。
+            // with 内 var 初始化：对象有该属性则写对象，否则写提升槽（动态解析）；
+            // 未声明名经回退臂落隐式全局，与静态写路径同形。
             self.emit_with_dynamic_write(name, src_reg, 0, ctx)?;
         } else {
             // const 声明路径 STORE_VAR 恒 b=0，不查运行时 guard。
diff --git a/crates/oxide_vm/tests/with_fallback_implicit_global_tests.rs b/crates/oxide_vm/tests/with_fallback_implicit_global_tests.rs
new file mode 100644
index 00000000..f11642e9
--- /dev/null
+++ b/crates/oxide_vm/tests/with_fallback_implicit_global_tests.rs
@@ -0,0 +1,70 @@
+use std::sync::Arc;
+
+use oxide_compiler::compiler::Compiler;
+use oxide_compiler::DefaultCompilerService;
+use oxide_parser::Allocator;
+use oxide_vm::vm::Vm;
+
+fn eval(source: &str) -> String {
+    let allocator = Allocator::default();
+    let program = match oxide_parser::parse(&allocator, source) {
+        Ok(p) => p,
+        Err(e) => return format!("parse error: {}", e[0].message),
+    };
+    let module = match Compiler::new().compile(&program) {
+        Ok(m) => m,
+        Err(e) => return format!("compile error: {e}"),
+    };
+    let mut vm = Vm::new();
+    vm.set_compiler_service(Arc::new(DefaultCompilerService));
+    match vm.run(&Arc::new(module)) {
+        Ok(result) => format!("{result}"),
+        Err(e) => format!("vm error: {e}"),
+    }
+}
+
+// 规范（ECMA-262 `with` 写解析）：with 对象无该属性且名字未在静态作用域
+// 声明时，写落隐式全局——sloppy 物化全局属性；对象命中臂与已声明绑定的
+// 回退分支行为不变。严格模式禁止 `with` 语句（解析期 SyntaxError），
+// 故回退臂的 strict 抛错分支仅经静态写路径可达。
+
+#[test]
+fn with_fallback_undeclared_write_goes_to_implicit_global() {
+    assert_eq!(
+        eval("var o={}; with(o){x=42;} globalThis.x===42"),
+        "true",
+        "sloppy with 回退未声明名写物化隐式全局属性"
+    );
+}
+
+#[test]
+fn with_hit_write_stays_on_object() {
+    assert_eq!(
+        eval("var o={x:1}; with(o){x=42;} o.x===42 && globalThis.x===undefined"),
+        "true",
+        "with 对象命中臂写对象属性，不落全局"
+    );
+}
+
+#[test]
+fn with_fallback_declared_var_writes_outer_binding() {
+    assert_eq!(
+        eval(
+            "(function(){var o={}, y=0; with(o){y=1;} \
+             return y===1 && globalThis.y===undefined;})()"
+        ),
+        "true",
+        "with 回退已声明 var 写外层绑定，不落全局"
+    );
+}
+
+#[test]
+fn with_fallback_compound_undeclared_write_keeps_existing_behavior() {
+    // 复合赋值回退臂走静态复合路径：未声明名旧值按 undefined 读
+    // （GetBaseValue 语义不抛），复合运算结果落隐式全局。
+    assert_eq!(
+        eval("var o={}; with(o){x+=1;} isNaN(globalThis.x)"),
+        "true",
+        "with 回退未声明名复合赋值保持既有读 undefined 行为"
+    );
+}