diff --git a/benches/gust/drivers/hm-thin/Cargo.lock b/benches/gust/drivers/hm-thin/Cargo.lock
new file mode 100644
index 0000000..088e438
--- /dev/null
+++ b/benches/gust/drivers/hm-thin/Cargo.lock
@@ -0,0 +1,335 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "anyhow"
+version = "1.0.104"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470"
+
+[[package]]
+name = "bitflags"
+version = "2.13.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b588b76d00fde79687d7646a9b5bdf3cc0f655e0bbd080335a95d7e96f3587da"
+
+[[package]]
+name = "equivalent"
+version = "1.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
+
+[[package]]
+name = "foldhash"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2"
+
+[[package]]
+name = "gust-hm-thin"
+version = "0.1.0"
+dependencies = [
+ "wit-bindgen",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.15.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1"
+dependencies = [
+ "foldhash",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.17.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a"
+
+[[package]]
+name = "heck"
+version = "0.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea"
+
+[[package]]
+name = "id-arena"
+version = "2.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954"
+
+[[package]]
+name = "indexmap"
+version = "2.14.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
+dependencies = [
+ "equivalent",
+ "hashbrown 0.17.1",
+ "serde",
+ "serde_core",
+]
+
+[[package]]
+name = "itoa"
+version = "1.0.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682"
+
+[[package]]
+name = "leb128fmt"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2"
+
+[[package]]
+name = "log"
+version = "0.4.33"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0ceec5bc11778974d1bcb055b18002eba7f4b3518b6a0081b3af5f21666da9ad"
+
+[[package]]
+name = "memchr"
+version = "2.8.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98"
+
+[[package]]
+name = "prettyplease"
+version = "0.2.37"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b"
+dependencies = [
+ "proc-macro2",
+ "syn 2.0.119",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.107"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.47"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "semver"
+version = "1.0.28"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"
+
+[[package]]
+name = "serde"
+version = "1.0.229"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba"
+dependencies = [
+ "serde_core",
+]
+
+[[package]]
+name = "serde_core"
+version = "1.0.229"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48"
+dependencies = [
+ "serde_derive",
+]
+
+[[package]]
+name = "serde_derive"
+version = "1.0.229"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 3.0.3",
+]
+
+[[package]]
+name = "serde_json"
+version = "1.0.151"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14"
+dependencies = [
+ "itoa",
+ "memchr",
+ "serde",
+ "serde_core",
+ "zmij",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.119"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "syn"
+version = "3.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "unicode-xid"
+version = "0.2.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
+
+[[package]]
+name = "wasm-encoder"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "990065f2fe63003fe337b932cfb5e3b80e0b4d0f5ff650e6985b1048f62c8319"
+dependencies = [
+ "leb128fmt",
+ "wasmparser",
+]
+
+[[package]]
+name = "wasm-metadata"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909"
+dependencies = [
+ "anyhow",
+ "indexmap",
+ "wasm-encoder",
+ "wasmparser",
+]
+
+[[package]]
+name = "wasmparser"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe"
+dependencies = [
+ "bitflags",
+ "hashbrown 0.15.5",
+ "indexmap",
+ "semver",
+]
+
+[[package]]
+name = "wit-bindgen"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4e048f41ef90f0b5dd61f1059c35f5636252e56813bf616d0803aa3739867230"
+dependencies = [
+ "wit-bindgen-rust-macro",
+]
+
+[[package]]
+name = "wit-bindgen-core"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c15e7a56641cc9040480a26526a3229cbc4e8065adf98c9755d21c4c9b446c4c"
+dependencies = [
+ "anyhow",
+ "heck",
+ "wit-parser",
+]
+
+[[package]]
+name = "wit-bindgen-rust"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bd81b0ae1ec492bfe91683f1da6db6492ebc682e72d4f2715619dba783b066ca"
+dependencies = [
+ "anyhow",
+ "heck",
+ "indexmap",
+ "prettyplease",
+ "syn 2.0.119",
+ "wasm-metadata",
+ "wit-bindgen-core",
+ "wit-component",
+]
+
+[[package]]
+name = "wit-bindgen-rust-macro"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "54e6ce04c549e7149b66a70d34fc5a2a01b374bf49ca61db65d16e3ae922866e"
+dependencies = [
+ "anyhow",
+ "prettyplease",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.119",
+ "wit-bindgen-core",
+ "wit-bindgen-rust",
+]
+
+[[package]]
+name = "wit-component"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2"
+dependencies = [
+ "anyhow",
+ "bitflags",
+ "indexmap",
+ "log",
+ "serde",
+ "serde_derive",
+ "serde_json",
+ "wasm-encoder",
+ "wasm-metadata",
+ "wasmparser",
+ "wit-parser",
+]
+
+[[package]]
+name = "wit-parser"
+version = "0.244.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736"
+dependencies = [
+ "anyhow",
+ "id-arena",
+ "indexmap",
+ "log",
+ "semver",
+ "serde",
+ "serde_derive",
+ "serde_json",
+ "unicode-xid",
+ "wasmparser",
+]
+
+[[package]]
+name = "zmij"
+version = "1.0.23"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "29666d0abbfad1e3dc4dcf6144730dd3a3ab225bbbdac83319345b1b44ccfc1b"
diff --git a/benches/gust/drivers/hm-thin/Cargo.toml b/benches/gust/drivers/hm-thin/Cargo.toml
new file mode 100644
index 0000000..c001d4f
--- /dev/null
+++ b/benches/gust/drivers/hm-thin/Cargo.toml
@@ -0,0 +1,15 @@
+[workspace]
+[package]
+name = "gust-hm-thin"
+version = "0.1.0"
+edition = "2021"
+description = "T2 stage 2: the Verus/Kani-verified Health-Monitor value-domain predicates as a dissolvable wasm component. Bodies lifted VERBATIM from plain/src/health_monitor.rs. Zero seams, zero SRAM \u2014 the cheapest proof that the isolation core can move onto the dissolve path (REQ-OS-OBJVERIFY-001)."
+[lib]
+crate-type = ["cdylib", "rlib"]
+[dependencies]
+wit-bindgen = { version = "0.52", default-features = false, features = ["macros"] }
+[profile.release]
+panic = "abort"
+opt-level = "s"
+lto = true
+codegen-units = 1
diff --git a/benches/gust/drivers/hm-thin/RESULTS.md b/benches/gust/drivers/hm-thin/RESULTS.md
new file mode 100644
index 0000000..f554d83
--- /dev/null
+++ b/benches/gust/drivers/hm-thin/RESULTS.md
@@ -0,0 +1,87 @@
+# hm-thin — the isolation core, dissolved. And an honest coverage report
+
+**Date:** 2026-08-07 · **T2 / REQ-OS-OBJVERIFY-001 stage 2** · meld 0.41.3, loom 1.2.0,
+synth 0.52.0 built with `--features verify`
+
+`REQ-OS-OBJVERIFY-001` needs the isolation core lowered by a compiler that carries
+per-rule obligations. `health_monitor.rs` is the cheapest possible first step: **zero
+hardware seams**, pure scalar predicates. If it could not dissolve, nothing in the
+isolation core could.
+
+## It dissolves
+
+    plain/src/health_monitor.rs   (Verus + Kani verified — bodies lifted VERBATIM)
+      -> cargo wasm32              2 401 B
+      -> wasm-tools component new  3 956 B
+      -> meld fuse --memory shared
+      -> loom optimize --passes inline
+      -> synth compile --target cortex-m3 --all-exports --relocatable
+
+    text 1054   data 0   bss 0        undefined symbols: none
+
+Zero SRAM, and correctly **no** undefined symbols — unlike the fused OS composite,
+where an empty undefined set is the failure mode, `hm-thin` genuinely has no seam to
+preserve. It computes over scalars and returns.
+
+## BIN-VERIFY runs on it
+
+    6 functions · 8 rules verified · 0 failed · 0 unknown · 0 declined
+    rules: i32.and · i32.eqz · i32.gt_s · i32.le_s · i32.le_u · i32.sub
+
+## THIS IS NOT A ZERO-GAP RESULT, AND THE SUMMARY LOOKS LIKE ONE
+
+The line above reads as complete coverage. It is not, and the discrepancy is the
+whole reason `REQ-OS-OBJVERIFY-001` defines its denominator as the **union** of
+RULE-VERIFY and BIN-VERIFY rather than as whatever the tool prints.
+
+**The object contains 29 `i32.const`.** BIN-VERIFY classes Const as a register
+operation and skips it *silently* — it is not in the verified list and not in a
+declined list, because there is no declined list. So:
+
+| rule | BIN-VERIFY | RULE-VERIFY (Rocq) | covered? |
+|---|---|---|---|
+| `i32.and`, `i32.eqz`, `i32.sub` | verified | `Qed` | yes, both halves |
+| `i32.gt_s`, `i32.le_s`, `i32.le_u` | verified | **no theorem exists** | yes, by BIN-VERIFY only |
+| **`i32.const`** (×29) | **skipped, unreported** | **`Admitted`** | **NO — neither half** |
+
+`i32_const_correct` is Admitted because it is false as stated for un-normalized
+operands; the supporting arithmetic (`i32_const_large_reconstruct`,
+`movw_movt_reconstruct_Z`) is `Qed`. Filed as **synth#933**.
+
+That the gap is invisible in the tool's own output is filed separately as
+**synth#935** — a consumer cannot compute a coverage denominator from `synth verify`,
+because it never reports the rules it declined.
+
+**So: zero-gap CANNOT be claimed for this object.** One rule, named, filed, and
+appearing 29 times.
+
+## What this does establish
+
+- The construction works. Verified Rust lifted verbatim into a wasm component
+  dissolves to a native object, and translation validation runs on the result.
+- The isolation core is **not** blocked on a rewrite. All three modules are already
+  thin-seam shaped; this one simply had no seam at all.
+- Instruction selection, register allocation and scheduling for this object are now
+  performed by a compiler that carries obligations, instead of by LLVM.
+
+## What it does NOT establish
+
+- **Not the full evidence-on-wasm set.** `REQ-OS-OBJVERIFY-001` also requires witness
+  MC/DC with zero unresolved gap rows, scry's verdicts and gap report, and the
+  `REQ-OS-HM-001` oracles **re-run against the wasm build**. None of those has been
+  done for this artifact. Without them, BIN-VERIFY shows the lowering is faithful but
+  not that the wasm refines the Verus-proven Rust.
+- **Not executed.** Nothing has run this object.
+- **Not the switch.** `partition_switch` (3 seams) and `mpu_switch` (1 seam) are the
+  remaining stage-2 work; HM was chosen first precisely because it is the easy case.
+- **7 exported predicates became 6 functions** in the object. Presumed inlining;
+  not yet confirmed, and stated here rather than left unnoticed.
+
+## Reproduce
+
+    cd benches/gust/drivers/hm-thin && cargo build --release --target wasm32-unknown-unknown
+    wasm-tools component new target/wasm32-unknown-unknown/release/gust_hm_thin.wasm -o hm.component.wasm
+    meld fuse hm.component.wasm --memory shared -o hm.fused.wasm
+    loom optimize hm.fused.wasm --passes inline --attestation false -o hm.loom.wasm
+    synth compile hm.loom.wasm --target cortex-m3 --all-exports --relocatable -o hm-thin-cm3.o
+    synth verify hm.loom.wasm hm-thin-cm3.o     # needs a --features verify build
diff --git a/benches/gust/drivers/hm-thin/hm-thin-cm3.o b/benches/gust/drivers/hm-thin/hm-thin-cm3.o
new file mode 100644
index 0000000..7fdf9f1
Binary files /dev/null and b/benches/gust/drivers/hm-thin/hm-thin-cm3.o differ
diff --git a/benches/gust/drivers/hm-thin/src/lib.rs b/benches/gust/drivers/hm-thin/src/lib.rs
new file mode 100644
index 0000000..f7913ec
--- /dev/null
+++ b/benches/gust/drivers/hm-thin/src/lib.rs
@@ -0,0 +1,68 @@
+//! SPIKE — gust:hm thin-seam Health Monitor.
+//! Bodies lifted VERBATIM from plain/src/health_monitor.rs (Verus+Kani verified).
+#![no_std]
+#[panic_handler]
+fn ph(_: &core::panic::PanicInfo) -> ! { loop {} }
+
+// wit-bindgen's canonical-ABI glue must LINK against a global allocator; this world
+// is scalar-only (u32/i32/bool in, bool out), so nothing ever calls it and a
+// zero-state trapping allocator keeps the 0-SRAM property intact. Same construction
+// as the thin-seam drivers.
+use core::alloc::{GlobalAlloc, Layout};
+struct NoAlloc;
+unsafe impl GlobalAlloc for NoAlloc {
+    unsafe fn alloc(&self, _: Layout) -> *mut u8 { core::ptr::null_mut() }
+    unsafe fn dealloc(&self, _: *mut u8, _: Layout) {}
+}
+#[global_allocator]
+static ALLOC: NoAlloc = NoAlloc;
+
+wit_bindgen::generate!({ world: "hm-thin", path: "wit" });
+
+mod hm {
+pub fn fresh(age_ms: u32, limit_ms: u32) -> bool {
+    age_ms <= limit_ms
+}
+
+pub fn plausible(value: i32, lo: i32, hi: i32) -> bool {
+    lo <= value && value <= hi
+}
+
+pub fn innovation_ok(innov_abs: u32, k_sigma: u32) -> bool {
+    innov_abs <= k_sigma
+}
+
+pub fn budget_ok(used_us: u32, budget_us: u32) -> bool {
+    used_us <= budget_us
+}
+
+pub fn deadline_ok(lateness_us: u32) -> bool {
+    lateness_us == 0
+}
+
+pub fn heartbeat_ok(missed_beats: u32) -> bool {
+    missed_beats == 0
+}
+
+pub fn vote_ok(s0: i32, s1: i32, s2: i32, tol: i32) -> bool {
+    let t = tol as i64;
+    let d01 = s0 as i64 - s1 as i64;
+    let d02 = s0 as i64 - s2 as i64;
+    let d12 = s1 as i64 - s2 as i64;
+    let a01 = (if d01 >= 0 { d01 } else { -d01 }) <= t;
+    let a02 = (if d02 >= 0 { d02 } else { -d02 }) <= t;
+    let a12 = (if d12 >= 0 { d12 } else { -d12 }) <= t;
+    (a01 && a02) || (a01 && a12) || (a02 && a12)
+}}
+
+struct P;
+impl exports::gust::hm::detect::Guest for P {
+    fn fresh(a: u32, l: u32) -> bool { hm::fresh(a, l) }
+    fn plausible(v: i32, lo: i32, hi: i32) -> bool { hm::plausible(v, lo, hi) }
+    fn innovation_ok(i: u32, k: u32) -> bool { hm::innovation_ok(i, k) }
+    fn budget_ok(u: u32, b: u32) -> bool { hm::budget_ok(u, b) }
+    fn deadline_ok(l: u32) -> bool { hm::deadline_ok(l) }
+    fn heartbeat_ok(m: u32) -> bool { hm::heartbeat_ok(m) }
+    fn vote_ok(a: i32, b: i32, c: i32, t: i32) -> bool { hm::vote_ok(a, b, c, t) }
+}
+export!(P);
diff --git a/benches/gust/drivers/hm-thin/wit/gust-hm.wit b/benches/gust/drivers/hm-thin/wit/gust-hm.wit
new file mode 100644
index 0000000..4190cab
--- /dev/null
+++ b/benches/gust/drivers/hm-thin/wit/gust-hm.wit
@@ -0,0 +1,15 @@
+package gust:hm@0.1.0;
+
+/// The Health-Monitor value-domain predicates — pure scalar logic, no seam.
+/// Derived from plain/src/health_monitor.rs (Verus + Kani verified).
+interface detect {
+    fresh: func(age-ms: u32, limit-ms: u32) -> bool;
+    plausible: func(value: s32, lo: s32, hi: s32) -> bool;
+    innovation-ok: func(innov-abs: u32, k-sigma: u32) -> bool;
+    budget-ok: func(used-us: u32, budget-us: u32) -> bool;
+    deadline-ok: func(lateness-us: u32) -> bool;
+    heartbeat-ok: func(missed-beats: u32) -> bool;
+    vote-ok: func(s0: s32, s1: s32, s2: s32, tol: s32) -> bool;
+}
+
+world hm-thin { export detect; }