gHashTag · Oct 18, 2026 · Oct 18, 2026 · Oct 18, 2026
@@ -120,6 +120,7 @@ specs/scratch/
 # rather than into tools/seal_baseline.txt, which would turn a green invariant into
 # permanent debt.
 .trinity/seals/scratch_*.json
+.trinity/seals/.*.part-*
 
 # Coq build artifacts. 208 of these were committed, carrying the absolute build
 # path of the machine that produced them -- which is what secret-scan kept

@@ -1,33 +1,33 @@
 {
-  "built_by": "t27c-bootstrap@0.5.2+89254d2",
+  "built_by": "t27c-bootstrap@0.5.2+1c8355564",
   "closure": [
     {
       "spec": "specs/verified/reuse.t27",
       "spec_hash": "sha256:79af2725711852461d2d71c0ad089fb55130199e320abed77f11e915cf9d970b"
     }
   ],
   "config": "gen=c,rust,verilog,zig;tests=zig",
-  "gen_hash_c": "sha256:5f3682132cd429701a3c174527eafa73952f9ac6fd470a6e5ba8769a95a56db7",
-  "gen_hash_rust": "sha256:be2b7658bad3f36d544ee77a831c740aaa40bd390286bd6642a7c2d581ac24fc",
-  "gen_hash_verilog": "sha256:42c766404f36a48fb80d7fd861174133ab81463adea0493e8b6f019c3bdf4e52",
-  "gen_hash_zig": "sha256:a77c3bf9bd31868508b0f9545045233253a21342a56d16356cac9ef25791267a",
+  "gen_hash_c": "sha256:83fc54f9e69b0bee6207596b3c42f717f39c5511bdf3c9f9f7a8c68de37d3af2",
+  "gen_hash_rust": "sha256:3d720a3281aafdb385553d605568744bc6d22737c36e191cb21bc0b312ddce71",
+  "gen_hash_verilog": "sha256:0ff338e626b39ad8e37e4d23f6138c77bb647ec61ba5031a007f614148924cb2",
+  "gen_hash_zig": "sha256:d40c2f9cf839b7b9ce15e741a6f7e9d8414b0543a031135bf20abdaee5180a57",
   "module": "VerifiedSealWrite",
   "ring": 12,
   "seal_schema": 2,
-  "sealed_at": "2026-10-18T12:55:35Z",
+  "sealed_at": "2026-10-18T13:37:42Z",
   "sealed_by": "t27c-bootstrap@0.5.2",
-  "spec_hash": "sha256:59262b1a210bd4775ef0dec0db9a52f1333069afb946cf4cd88c6cb894a6b6e0",
+  "spec_hash": "sha256:063e7ceb6f5c8106097b1185079c306108630bdff7877ebb947485deb27ac390",
   "spec_path": "specs/verified/seal_write.t27",
   "tests": {
     "failed": 0,
     "failing": [],
     "forced": false,
-    "passed": 14,
-    "total": 14,
+    "passed": 19,
+    "total": 19,
     "vacuous": 0
   },
   "toolchain": {
-    "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d",
+    "test_runner": "sha256:8512b80da533b79289110fca4a65f3336abd7a059ca4b72ea595d5e33ff8ad10",
     "zig": "0.16.0"
   }
 }
@@ -0,0 +1,154 @@
+// Generated from .t27 spec
+// DO NOT EDIT — generated by t27c
+// NOT LOWERED BY THIS BACKEND: 19 test(s), 0 invariant(s), 0 function(s) with no body.
+// This backend emits declarations only. The spec's checks live in
+// the Zig and Verilog outputs; do not read this file as verified.
+
+pub const WRITE_OK: u8 = 0;
+
+pub const WRITE_COLLISION: u8 = 1;
+
+pub const WRITE_OWNER_UNKNOWN: u8 = 2;
+
+pub const WRITE_SPEC_MOVED: u8 = 3;
+
+pub const WRITE_TESTED_OTHER: u8 = 4;
+
+pub const WRITE_READBACK_DIFF: u8 = 5;
+
+pub const WRITE_GEN_MOVED: u8 = 6;
+
+pub const SEAL_STAGE_SUFFIX: &'static str = ".part";
+
+pub const PROTO_IN_PLACE: u8 = 1;
+
+pub const PROTO_WRITE_THEN_RESTORE: u8 = 2;
+
+pub const PROTO_STAGE_THEN_RENAME: u8 = 3;
+
+pub const CUT_BEFORE_WRITE: u8 = 1;
+
+pub const CUT_DURING_WRITE: u8 = 2;
+
+pub const CUT_AFTER_WRITE: u8 = 3;
+
+pub const CUT_AFTER_COMMIT: u8 = 4;
+
+pub const DISK_OLD: u8 = 1;
+
+pub const DISK_NEW_CHECKED: u8 = 2;
+
+pub const DISK_NEW_UNCHECKED: u8 = 3;
+
+pub const DISK_TORN: u8 = 4;
+
+pub const DISK_FOREIGN: u8 = 5;
+
+pub fn names_collide(exact_equal: bool, casefold_equal: bool) -> bool {
+    if exact_equal {
+        return true;
+    }
+    return casefold_equal;
+}
+
+pub fn dest_check(dest_exists: bool, owner_known: bool, owner_is_this_spec: bool) -> u8 {
+    if (dest_exists == false) {
+        return WRITE_OK;
+    }
+    if (owner_known == false) {
+        return WRITE_OWNER_UNKNOWN;
+    }
+    if owner_is_this_spec {
+        return WRITE_OK;
+    }
+    return WRITE_COLLISION;
+}
+
+pub fn dest_check_today(dest_exists: bool, owner_known: bool, owner_is_this_spec: bool) -> u8 {
+    return WRITE_OK;
+}
+
+pub fn post_write_check(recorded: u64, after: u64, tested: u64, readback_equal: bool) -> u8 {
+    if (tested != recorded) {
+        return WRITE_TESTED_OTHER;
+    }
+    if (after != recorded) {
+        return WRITE_SPEC_MOVED;
+    }
+    if (readback_equal == false) {
+        return WRITE_READBACK_DIFF;
+    }
+    return WRITE_OK;
+}
+
+pub fn dest_allowed(code: u8, force: bool) -> bool {
+    if (code == WRITE_OK) {
+        return true;
+    }
+    if (code == WRITE_OWNER_UNKNOWN) {
+        return force;
+    }
+    return false;
+}
+
+pub fn gens_check(code: u8, gens_same: bool) -> u8 {
+    if (code != WRITE_OK) {
+        return code;
+    }
+    if gens_same {
+        return WRITE_OK;
+    }
+    return WRITE_GEN_MOVED;
+}
+
+pub fn post_write_check_today(recorded: u64, after: u64, tested: u64, readback_equal: bool) -> u8 {
+    return WRITE_OK;
+}
+
+pub fn after_cut(proto: u8, cut: u8, foreign: bool) -> u8 {
+    if (cut == CUT_BEFORE_WRITE) {
+        return DISK_OLD;
+    }
+    if (proto == PROTO_STAGE_THEN_RENAME) {
+        if (cut == CUT_AFTER_COMMIT) {
+            return DISK_NEW_CHECKED;
+        }
+        return DISK_OLD;
+    }
+    if (cut == CUT_DURING_WRITE) {
+        return DISK_TORN;
+    }
+    if foreign {
+        if (proto == PROTO_WRITE_THEN_RESTORE) {
+            if (cut == CUT_AFTER_COMMIT) {
+                return DISK_OLD;
+            }
+        }
+        return DISK_FOREIGN;
+    }
+    return DISK_NEW_UNCHECKED;
+}
+
+pub fn cut_safe(disk: u8) -> bool {
+    if (disk == DISK_OLD) {
+        return true;
+    }
+    return (disk == DISK_NEW_CHECKED);
+}
+
+pub fn proto_cut_safe(proto: u8) -> bool {
+    if (cut_safe(after_cut(proto, CUT_DURING_WRITE, false)) == false) {
+        return false;
+    }
+    if (cut_safe(after_cut(proto, CUT_AFTER_WRITE, false)) == false) {
+        return false;
+    }
+    if (cut_safe(after_cut(proto, CUT_AFTER_WRITE, true)) == false) {
+        return false;
+    }
+    if (cut_safe(after_cut(proto, CUT_AFTER_COMMIT, false)) == false) {
+        return false;
+    }
+    return cut_safe(after_cut(proto, CUT_AFTER_COMMIT, true));
+}
+
@@ -118,6 +118,9 @@ mod test_report_exit;
 #[path = "../gen/rust/verified/seal_identity.rs"]
 #[allow(dead_code, unused_parens, unused_mut, unused_assignments, unused_variables, non_snake_case, non_upper_case_globals, clippy::all)]
 mod seal_identity;
+// specs/verified/seal_write.t27 (#10457, #10454): what one seal write must check before and after it lands.
+#[path = "../gen/rust/verified/seal_write.rs"]
+#[allow(dead_code, unused_parens, unused_mut, unused_assignments, unused_variables, non_snake_case, non_upper_case_globals, clippy::all)] mod seal_write;
 // specs/verified/verdict_audit.t27 (#8542): which reused verdicts `frontier --audit` reruns.
 #[path = "../gen/rust/verified/verdict_audit.rs"]
 #[allow(dead_code, unused_parens, unused_mut, unused_assignments, unused_variables, non_snake_case, non_upper_case_globals, clippy::all)]
@@ -5859,6 +5862,16 @@ fn seal_file_path(module: &str, input_path: &str) -> std::path::PathBuf {
     Path::new(".trinity").join("seals").join(name)
 }
 
+/// seal_write.t27 STAGE_THEN_RENAME (#10454): stage `.<name>.part-<pid>` beside the seal, sync, let `check` judge the staged file, then one rename; any other answer removes the stage and leaves the old seal.
+fn write_seal_atomic(path: &Path, bytes: &[u8], check: impl FnOnce(&Path) -> u8) -> anyhow::Result<u8> {
+    let (dir, part) = (path.parent().filter(|d| !d.as_os_str().is_empty()).unwrap_or(Path::new(".")), path.with_file_name(format!(".{}{}-{}", path.file_name().unwrap_or_default().to_string_lossy(), seal_write::SEAL_STAGE_SUFFIX, std::process::id())));
+    let w = fs::File::create(&part).and_then(|mut f| { std::io::Write::write_all(&mut f, bytes)?; f.sync_all() }).map(|_| check(&part)).and_then(|c| if c == seal_write::WRITE_OK { fs::rename(&part, path).map(|_| c) } else { Ok(c) });
+    if w.as_ref().map_or(true, |c| *c != seal_write::WRITE_OK) { let _ = fs::remove_file(&part); } let c = w.with_context(|| format!("writing {}", path.display()))?; if let Ok(d) = fs::File::open(dir) { let _ = d.sync_all(); } Ok(c)
+}
+/// The staged file read back equals what was written (seal_write.t27 post_write_check's readback_equal).
+fn staged_is(bytes: &[u8]) -> impl FnOnce(&Path) -> u8 + '_ { move |p| seal_write::post_write_check(0, 0, 0, fs::read(p).map_or(false, |b| b == bytes)) }
+/// The five hashes a seal records, in the order seal prints them.
+fn hash_pairs(h: &SealHashes) -> [(&'static str, &String); 5] { [("spec_hash", &h.spec_hash), ("gen_hash_zig", &h.gen_hash_zig), ("gen_hash_verilog", &h.gen_hash_verilog), ("gen_hash_c", &h.gen_hash_c), ("gen_hash_rust", &h.gen_hash_rust)] }
 /// The producer identity a seal and a receipt both carry: `name@version+git`,
 /// defined ONCE. specs/verified/receipt.t27's `producer_matches` compares two
 /// producer identities verbatim -- no normalization anywhere, matching is not
@@ -5939,13 +5952,7 @@ fn run_seal(input_path: &str, save: bool, verify: bool, force: bool) -> anyhow::
             serde_json::from_str(&fs::read_to_string(&seal_path)?)?;
 
         let mut all_match = true;
-        let checks = [
-            ("spec_hash", &hashes.spec_hash),
-            ("gen_hash_zig", &hashes.gen_hash_zig),
-            ("gen_hash_verilog", &hashes.gen_hash_verilog),
-            ("gen_hash_c", &hashes.gen_hash_c),
-            ("gen_hash_rust", &hashes.gen_hash_rust),
-        ];
+        let checks = hash_pairs(&hashes);
 
         for (field, current) in &checks {
             let saved = saved_json
@@ -6115,28 +6122,19 @@ fn run_seal(input_path: &str, save: bool, verify: bool, force: bool) -> anyhow::
             "tests": tests_record
         });
 
-        // The derived name and the file on disk can differ ONLY IN CASE: the
-        // tool would write `ar_restraint.json` where `ar_Restraint.json` is
-        // tracked. macOS resolves those to one file and hides it; on the
-        // case-sensitive filesystem CI runs on, `--save` would create a SECOND
-        // seal for the same spec and neither would be wrong-looking. Measured
-        // over the store: 751 filenames match the derived name exactly, 4
-        // differ only by case, 558 use the older bare-`<module>` scheme.
-        //
-        // An existing file wins, so the store cannot grow a case-variant twin.
+        // An existing file wins, even one that differs only in case: seal_write.t27 names_collide() says why.
         let derived = seal_file_path(&hashes.module, &hashes.spec_path);
-        let seal_path = fs::read_dir(&seals_dir)
-            .ok()
-            .and_then(|entries| {
-                let want = derived.file_name()?.to_string_lossy().to_lowercase();
-                entries.flatten().find_map(|e| {
-                    let p = e.path();
-                    (p.file_name()?.to_string_lossy().to_lowercase() == want).then_some(p)
-                })
-            })
-            .unwrap_or(derived);
+        let want = derived.file_name().map(|n| n.to_string_lossy().into_owned()).unwrap_or_default();
+        let seal_path = fs::read_dir(&seals_dir).ok().and_then(|es| es.flatten().map(|e| e.path()).find(|p| p.file_name().map_or(false, |n| seal_write::names_collide(n.to_string_lossy() == want, n.to_string_lossy().to_lowercase() == want.to_lowercase())))).unwrap_or(derived);
         let pretty = serde_json::to_string_pretty(&seal_obj)?;
-        fs::write(&seal_path, &pretty)?;
+        // seal_write.t27 dest_check + dest_allowed (#10454): another spec's seal is refused, --force included; an unreadable owner (torn or legacy) only with --force.
+        let owner = fs::read(&seal_path).ok().and_then(|b| serde_json::from_slice::<serde_json::Value>(&b).ok()).and_then(|v| v["spec_path"].as_str().map(|s| s.trim_start_matches("./").to_string()));
+        let dest = seal_write::dest_check(seal_path.exists(), owner.is_some(), owner.as_deref() == Some(hashes.spec_path.as_str()));
+        if !seal_write::dest_allowed(dest, force) { eprintln!("refusing to seal {}: {}", hashes.spec_path, if dest == seal_write::WRITE_COLLISION { format!("{} is the seal of {}, and both specs derive that name (parent directory + module). Rename one spec's module or directory; --force does not override this.", seal_path.display(), owner.unwrap_or_default()) } else { format!("{} names no readable spec_path (a torn write or a legacy seal); --force replaces it.", seal_path.display()) }); std::process::exit(1); } else if dest == seal_write::WRITE_OWNER_UNKNOWN { println!("{} names no readable spec_path: replacing it (--force)", seal_path.display()); }
+        // seal_write.t27 post_write_check + gens_check judge the staged file before the rename: the spec hashed and generated again, the bytes the tests read, the stage read back.
+        let tested = report.read.as_ref().map_or(0, |r| (format!("sha256:{r}") != hashes.spec_hash) as u64); // 0 = the recorded bytes, or no test read any
+        let code = write_seal_atomic(&seal_path, pretty.as_bytes(), |p| { let again = compute_seal_hashes(input_path).ok(); seal_write::gens_check(seal_write::post_write_check(0, again.as_ref().map_or(1, |a| (a.spec_hash != hashes.spec_hash) as u64), tested, staged_is(pretty.as_bytes())(p) == seal_write::WRITE_OK), again.map_or(false, |a| hash_pairs(&a)[1..] == hash_pairs(&hashes)[1..])) })?;
+        if code != seal_write::WRITE_OK { eprintln!("seal of {} not kept: {}; the old seal is untouched", hashes.spec_path, match code { seal_write::WRITE_TESTED_OTHER => "the tests read other bytes than the ones hashed", seal_write::WRITE_SPEC_MOVED => "the spec changed while it was being sealed", seal_write::WRITE_READBACK_DIFF => "the staged file read back is not the seal written", _ => "a second generation of the same spec gave other code (a gen hash nobody can reproduce)" }); std::process::exit(1); }
 
         // A spec can own MORE THAN ONE seal file, and writing only the
         // canonical name leaves the others describing output that no longer
@@ -6154,62 +6152,23 @@ fn run_seal(input_path: &str, save: bool, verify: bool, force: bool) -> anyhow::
         // each file has it, because the file is NAMED after that field and
         // overwriting it would leave a seal whose name and contents disagree --
         // which is the defect this is repairing, not a second copy of it.
-        let mut also_updated = 0usize;
-        if let Ok(entries) = fs::read_dir(&seals_dir) {
-            for entry in entries.flatten() {
-                let path = entry.path();
-                if path == seal_path || path.extension().and_then(|e| e.to_str()) != Some("json") {
-                    continue;
-                }
-                let Ok(text) = fs::read_to_string(&path) else { continue };
-                let Ok(mut existing) = serde_json::from_str::<serde_json::Value>(&text) else {
-                    continue;
-                };
-                if existing.get("spec_path").and_then(|v| v.as_str()) != Some(hashes.spec_path.as_str())
-                {
-                    continue;
-                }
-                for (k, v) in [
-                    ("spec_hash", &hashes.spec_hash),
-                    ("gen_hash_zig", &hashes.gen_hash_zig),
-                    ("gen_hash_verilog", &hashes.gen_hash_verilog),
-                    ("gen_hash_c", &hashes.gen_hash_c),
-                    ("gen_hash_rust", &hashes.gen_hash_rust),
-                ] {
-                    existing[k] = serde_json::Value::String(v.clone());
-                }
-                existing["sealed_at"] = serde_json::Value::String(now.clone());
-                existing["tests"] = tests_record.clone();
-                if let Ok(out) = serde_json::to_string_pretty(&existing) {
-                    if fs::write(&path, &out).is_ok() {
-                        also_updated += 1;
-                    }
-                }
-            }
-        }
-
-        // Also print hashes to stdout
-        println!("spec_hash={}", hashes.spec_hash);
-        println!("gen_hash_zig={}", hashes.gen_hash_zig);
-        println!("gen_hash_verilog={}", hashes.gen_hash_verilog);
-        println!("gen_hash_c={}", hashes.gen_hash_c);
-        println!("gen_hash_rust={}", hashes.gen_hash_rust);
+        let (mut also_updated, mut twins_failed) = (0usize, Vec::new());
+        for path in fs::read_dir(&seals_dir).into_iter().flatten().flatten().map(|e| e.path()).filter(|p| p != &seal_path && p.extension().and_then(|e| e.to_str()) == Some("json")) {
+            let Some(mut existing) = fs::read_to_string(&path).ok().and_then(|t| serde_json::from_str::<serde_json::Value>(&t).ok()) else { continue };
+            if existing.get("spec_path").and_then(|v| v.as_str()) != Some(hashes.spec_path.as_str()) { continue; }
+            for (k, v) in hash_pairs(&hashes) { existing[k] = serde_json::Value::String(v.clone()); }
+            existing["sealed_at"] = serde_json::Value::String(now.clone()); existing["tests"] = tests_record.clone();
+            let out = serde_json::to_string_pretty(&existing)?; // #10454: staged, read back, renamed; a twin that failed is named and fails the command, not skipped
+            if write_seal_atomic(&path, out.as_bytes(), staged_is(out.as_bytes())).map_or(false, |c| c == seal_write::WRITE_OK) { also_updated += 1 } else { twins_failed.push(path.display().to_string()) }
+        }
+        for (k, v) in hash_pairs(&hashes) { println!("{k}={v}"); }
         println!("\nSeal saved to {}", seal_path.display());
-        if also_updated > 0 {
-            // Said out loud: a command that silently touched other files would
-            // be worse than one that touches too few.
-            println!(
-                "  and {} other seal file(s) naming the same spec",
-                also_updated
-            );
-        }
+        // Said out loud: a command that silently touched other files would be worse than one that touches too few.
+        if also_updated > 0 { println!("  and {} other seal file(s) naming the same spec", also_updated); }
+        anyhow::ensure!(twins_failed.is_empty(), "{} other seal file(s) naming {} were not rewritten: {}", twins_failed.len(), hashes.spec_path, twins_failed.join(", "));
     } else {
         // Default: just print hashes (existing behavior, enhanced with all backends)
-        println!("spec_hash={}", hashes.spec_hash);
-        println!("gen_hash_zig={}", hashes.gen_hash_zig);
-        println!("gen_hash_verilog={}", hashes.gen_hash_verilog);
-        println!("gen_hash_c={}", hashes.gen_hash_c);
-        println!("gen_hash_rust={}", hashes.gen_hash_rust);
+        for (k, v) in hash_pairs(&hashes) { println!("{k}={v}"); }
     }
 
     Ok(())

@@ -5672,7 +5672,7 @@ pub fn run_frontier(list: bool, reseal: bool, audit: Option<u32>, watch: bool, o
         let keep = sealed && si::remint_keeps(new["seal_schema"].as_u64().unwrap_or(0) as u32, new.pointer("/tests/failed").and_then(|v| v.as_u64()) == Some(0), new.pointer("/tests/forced").and_then(|v| v.as_bool()) == Some(true), new.pointer("/tests/total").and_then(|v| v.as_u64()).unwrap_or(0) as u32, src.lines().filter(|l| l.trim_start().starts_with("invariant ")).count() as u32, new.pointer("/tests/vacuous").and_then(|v| v.as_u64()).unwrap_or(0) as u32, !old.iter().any(|(f, _, mine)| f == &primary && !mine));
         let same = |o: &str| serde_json::from_str::<serde_json::Value>(o).map_or(false, |mut v| { v["sealed_at"] = new["sealed_at"].clone(); v["built_by"] = new["built_by"].clone(); v == new }); // only when and by which build: no change
         if !keep && !old.iter().any(|(f, ..)| f == &primary) { let _ = std::fs::remove_file(&primary); }
-        for (f, o, mine) in &old { std::fs::write(f, if keep && *mine && !same(o) { serde_json::to_string_pretty(&new)? } else { o.clone() })? }
+        for (f, o, mine) in &old { let b = if keep && *mine && !same(o) { serde_json::to_string_pretty(&new)? } else { o.clone() }; anyhow::ensure!(crate::write_seal_atomic(f, b.as_bytes(), crate::staged_is(b.as_bytes()))? == crate::seal_write::WRITE_OK, "{} read back other bytes", f.display()) } // #10454 seal_write.t27 STAGE_THEN_RENAME: a killed reseal leaves no torn seal
         println!("{} {p}", if keep { "resealed" } else { "kept the old seal" });
     }
     let _ = std::fs::remove_dir_all(&zc);