diff --git a/artifacts/gust_os_roadmap.yaml b/artifacts/gust_os_roadmap.yaml
index 95b39d19..2cda7ea1 100644
--- a/artifacts/gust_os_roadmap.yaml
+++ b/artifacts/gust_os_roadmap.yaml
@@ -460,6 +460,33 @@ artifacts:
     links:
       - type: verifies
         target: REQ-OS-SYSCALL-001
+  - id: VER-OS-TIME-MATH-001
+    type: sw-verification
+    title: "gust:os time seam — wrap-safe deadline/elapsed math Kani-proven (5/5)"
+    status: verified
+    release: v0.5.1
+    description: >
+      Additional formal evidence hardening the gust:os `time` capability (over the
+      test-level VER-OS-SYSCALL-001). The `time` interface documents its
+      deadline/elapsed helpers as wrap-safe over the counter domain widened to u64;
+      that arithmetic is now a single verified core, `drivers/os-time-math`, that the
+      time-provider binds to instead of carrying the math inline. Kani-proven (5/5
+      harnesses, 0 failures, `cargo kani`): deadline is total and `deadline(now,0)==now`
+      (deadline_total_and_zero_is_now); a fresh deadline is not yet elapsed for any
+      real half-domain-bounded non-zero delay (fresh_deadline_not_elapsed); a deadline
+      is elapsed exactly at itself (at_deadline_is_elapsed) and once now has advanced by
+      the full delay, wrap-safe across the domain (advanced_to_deadline_is_elapsed); and
+      the wrap-safe form agrees with a plain `>=` compare in the non-wrapping regime, so
+      it is a strict superset not a behavior change (matches_plain_compare_without_wrap).
+      This also corrects a latent gap: the prior inline `elapsed = now >= deadline` was
+      only correct in the non-wrapping window despite the WIT's wrap-safe wording; the
+      verified core uses the wrapping-difference half-range test that is genuinely
+      wrap-safe. Proof is source-level over the pure math; the wasm->native dissolve of
+      the provider remains differentially trusted (docs/safety/verification-honesty.md).
+    tags: [gust, os, time, syscall, kani, wrap-safe, verified]
+    links:
+      - type: verifies
+        target: REQ-OS-SYSCALL-001
   - id: REQ-DRV-ADC-001
     type: sw-req
     title: "ADC is a verified thin-seam driver — read-after-EOC exactly-once analog input"
diff --git a/benches/gust/drivers/os-time-math/Cargo.lock b/benches/gust/drivers/os-time-math/Cargo.lock
new file mode 100644
index 00000000..164297f2
--- /dev/null
+++ b/benches/gust/drivers/os-time-math/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "gust-os-time-math"
+version = "0.1.0"
diff --git a/benches/gust/drivers/os-time-math/Cargo.toml b/benches/gust/drivers/os-time-math/Cargo.toml
new file mode 100644
index 00000000..c31ef2ce
--- /dev/null
+++ b/benches/gust/drivers/os-time-math/Cargo.toml
@@ -0,0 +1,14 @@
+[package]
+name = "gust-os-time-math"
+version = "0.1.0"
+edition = "2021"
+description = "Verified wrap-safe time math for the gust:os time seam (deadline/elapsed). Kani-proven; shared by time-provider."
+
+[workspace]
+
+[lib]
+crate-type = ["rlib"]
+
+[profile.release]
+panic = "abort"
+opt-level = "s"
diff --git a/benches/gust/drivers/os-time-math/src/lib.rs b/benches/gust/drivers/os-time-math/src/lib.rs
new file mode 100644
index 00000000..58a29d16
--- /dev/null
+++ b/benches/gust/drivers/os-time-math/src/lib.rs
@@ -0,0 +1,93 @@
+//! Verified wrap-safe time math for the **gust:os `time`** capability seam
+//! (REQ-OS-SYSCALL-001 / REQ-OS-TIMER-001). The `time` interface in
+//! `drivers/wit-os/gust-os.wit` documents its deadline/elapsed helpers as
+//! *wrap-safe over the counter domain, widened to u64* — this crate is the
+//! single implementation of that math, Kani-proven, so the time-provider is a
+//! thin binding over a verified core rather than carrying the arithmetic inline.
+//!
+//! The seam widens a free-running hardware counter to u64 and never rewinds, so
+//! `now` advances monotonically from whatever base a deadline was computed at.
+//! `elapsed` is written wrap-safe (a wrapping-difference half-range test) so it
+//! stays correct even across a single wrap of the domain — not merely in the
+//! non-wrapping window a plain `now >= deadline` would cover.
+#![cfg_attr(not(kani), no_std)]
+
+/// Half of the u64 domain — the wrap-safe "reached" boundary. A deadline is
+/// considered reached once `now` is within the trailing half-domain of it
+/// (`now - deadline` small), and still pending while it is within the leading
+/// half (`deadline - now` small). This is the standard tick-comparison idiom.
+const HALF: u64 = 1 << 63;
+
+/// Deadline = `now + ticks`, wrapping over the u64 domain (never panics/overflows).
+/// `ticks` is the caller's requested delay; the seam contract is that meaningful
+/// delays are `< HALF` (astronomically large at any real tick rate).
+#[inline]
+pub const fn deadline(now: u64, ticks: u64) -> u64 {
+    now.wrapping_add(ticks)
+}
+
+/// Has `deadline` been reached, given the current `now`? Wrap-safe: true once
+/// `now` has advanced to or past `deadline` (within the trailing half-domain),
+/// false while `deadline` is still ahead (within the leading half-domain).
+/// Equivalent to `now >= deadline` in the non-wrapping window, but correct across
+/// one wrap — which a plain comparison is not.
+#[inline]
+pub const fn elapsed(now: u64, deadline: u64) -> bool {
+    now.wrapping_sub(deadline) < HALF
+}
+
+// ───────────────────────────── proofs ─────────────────────────────
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    /// `deadline` is total (never panics/overflows) and `deadline(now, 0) == now`.
+    #[kani::proof]
+    fn deadline_total_and_zero_is_now() {
+        let now: u64 = kani::any();
+        let ticks: u64 = kani::any();
+        let _ = deadline(now, ticks); // no panic for any inputs
+        assert_eq!(deadline(now, 0), now);
+    }
+
+    /// A deadline is NOT yet elapsed the instant it is set, for any real
+    /// (half-domain-bounded, non-zero) delay — the wrap-safe "in the future" property.
+    #[kani::proof]
+    fn fresh_deadline_not_elapsed() {
+        let now: u64 = kani::any();
+        let ticks: u64 = kani::any();
+        kani::assume(ticks > 0 && ticks < HALF);
+        assert!(!elapsed(now, deadline(now, ticks)));
+    }
+
+    /// Exactly at the deadline, it IS elapsed (`elapsed(d, d)` is true).
+    #[kani::proof]
+    fn at_deadline_is_elapsed() {
+        let d: u64 = kani::any();
+        assert!(elapsed(d, d));
+    }
+
+    /// Once `now` has advanced by the full delay, the deadline IS elapsed —
+    /// wrap-safe across the domain. Monotone completion of a set deadline.
+    #[kani::proof]
+    fn advanced_to_deadline_is_elapsed() {
+        let base: u64 = kani::any();
+        let ticks: u64 = kani::any();
+        kani::assume(ticks < HALF);
+        let d = deadline(base, ticks);
+        assert!(elapsed(base.wrapping_add(ticks), d));
+    }
+
+    /// `elapsed` agrees with a plain `>=` comparison whenever no wrap occurs
+    /// (the practical regime) — so the wrap-safe form is a strict superset, not a
+    /// behavior change for real values.
+    #[kani::proof]
+    fn matches_plain_compare_without_wrap() {
+        let now: u64 = kani::any();
+        let d: u64 = kani::any();
+        // No wrap in either direction of the difference within the half-domain.
+        kani::assume(now >= d);
+        kani::assume(now - d < HALF);
+        assert!(elapsed(now, d));
+    }
+}
diff --git a/benches/gust/drivers/time-provider/Cargo.lock b/benches/gust/drivers/time-provider/Cargo.lock
new file mode 100644
index 00000000..ee61832a
--- /dev/null
+++ b/benches/gust/drivers/time-provider/Cargo.lock
@@ -0,0 +1,340 @@
+# 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-os-time-math"
+version = "0.1.0"
+
+[[package]]
+name = "gust-time-provider"
+version = "0.1.0"
+dependencies = [
+ "gust-os-time-math",
+ "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/time-provider/Cargo.toml b/benches/gust/drivers/time-provider/Cargo.toml
index 90dee770..63fc8595 100644
--- a/benches/gust/drivers/time-provider/Cargo.toml
+++ b/benches/gust/drivers/time-provider/Cargo.toml
@@ -6,6 +6,7 @@ edition = "2021"
 [lib]
 crate-type = ["cdylib"]
 [dependencies]
+gust-os-time-math = { path = "../os-time-math" }
 wit-bindgen = { version = "0.52", default-features = false, features = ["macros"] }
 [profile.release]
 panic = "abort"
diff --git a/benches/gust/drivers/time-provider/src/lib.rs b/benches/gust/drivers/time-provider/src/lib.rs
index 081702b9..5f77971e 100644
--- a/benches/gust/drivers/time-provider/src/lib.rs
+++ b/benches/gust/drivers/time-provider/src/lib.rs
@@ -24,8 +24,10 @@ const RESOLUTION_HZ: u64 = 1_000_000;
 struct P;
 impl Guest for P {
     fn now() -> u64 { read32(TIM2_CNT) as u64 }
-    fn deadline(now: u64, ticks: u64) -> u64 { now.wrapping_add(ticks) }
-    fn elapsed(now: u64, deadline: u64) -> bool { now >= deadline }
+    // deadline/elapsed delegate to the Kani-proven wrap-safe core (os-time-math),
+    // so the seam's documented wrap-safety is backed by a proof, not asserted inline.
+    fn deadline(now: u64, ticks: u64) -> u64 { gust_os_time_math::deadline(now, ticks) }
+    fn elapsed(now: u64, deadline: u64) -> bool { gust_os_time_math::elapsed(now, deadline) }
     fn resolution() -> u64 { RESOLUTION_HZ }
 }
 export!(P);