diff --git a/.cargo/config.toml b/.cargo/config.toml
new file mode 100644
index 0000000..7b0a7f4
--- /dev/null
+++ b/.cargo/config.toml
@@ -0,0 +1,5 @@
+# Prefer system linker so cargo isn't broken by hermetic_cc/zig from Bazel env.
+[target.aarch64-apple-darwin]
+linker = "cc"
+[target.x86_64-apple-darwin]
+linker = "cc"
diff --git a/.gitignore b/.gitignore
index 33c925f..3873e9b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,3 +6,4 @@ bazel-*
 /sample-eval
 /ote
 gen/
+/target
diff --git a/AGENTS.md b/AGENTS.md
index dc93b97..e601d91 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -54,8 +54,9 @@ CI: `tla-specs` job runs `scripts/check-specs.sh`.
 
 ```bash
 scripts/decision-check.sh              # lean: wires + decision-tagged tests
-bazel run  //tools/decision:update     # Decision.tla → committed *spec
-bazel test //tools/decision:up_to_date # codegen freshness
+bazel run  //tools/decision:update     # Decision.tla → Go *spec + Rust modules
+bazel test //tools/decision:up_to_date # Go + Rust codegen freshness
+cargo test -p decision_cores           # Rust gates + duals
 ```
 
 Rules (short):
diff --git a/Cargo.lock b/Cargo.lock
new file mode 100644
index 0000000..57dfbd4
--- /dev/null
+++ b/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "decision_cores"
+version = "0.1.0"
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..4690a47
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,3 @@
+[workspace]
+members = ["crates/decision_cores"]
+resolver = "2"
diff --git a/crates/decision_cores/BUILD.bazel b/crates/decision_cores/BUILD.bazel
new file mode 100644
index 0000000..ad17eea
--- /dev/null
+++ b/crates/decision_cores/BUILD.bazel
@@ -0,0 +1,15 @@
+# gazelle:ignore
+# Committed Rust decision modules (generated). Up-to-date via //tools/decision:*_rs_up_to_date.
+exports_files([
+    "src/tui_reload.rs",
+    "src/rate_limit.rs",
+    "src/timing_clamp.rs",
+    "src/sync_bounds.rs",
+    "src/gha_lifecycle.rs",
+    "src/log_groups.rs",
+    "src/span_tree.rs",
+    "src/lib.rs",
+    "src/gates.rs",
+    "tests/log_groups_dual.rs",
+    "Cargo.toml",
+])
diff --git a/crates/decision_cores/Cargo.toml b/crates/decision_cores/Cargo.toml
new file mode 100644
index 0000000..42521d5
--- /dev/null
+++ b/crates/decision_cores/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "decision_cores"
+version = "0.1.0"
+edition = "2021"
+description = "TLA+ decision cores (Rust) — generated from specs/*/decision/Decision.tla"
+license = "MIT"
+publish = false
+
+[lib]
+path = "src/lib.rs"
diff --git a/crates/decision_cores/src/gates.rs b/crates/decision_cores/src/gates.rs
new file mode 100644
index 0000000..5f4d641
--- /dev/null
+++ b/crates/decision_cores/src/gates.rs
@@ -0,0 +1,96 @@
+//! Thin production-style gates over generated decision modules.
+//! Call generated pure/actions — do not re-inline formulas.
+
+use crate::log_groups;
+use crate::rate_limit;
+use crate::span_tree;
+use crate::sync_bounds;
+use crate::timing_clamp;
+use crate::tui_reload;
+
+/// log-groups: may close stack (→ `log_groups::State::can_close`).
+pub fn can_close_group(depth: i64) -> bool {
+    log_groups::State { depth }.can_close()
+}
+
+/// log-groups: may open when depth is within decision MaxDepth=3.
+pub fn can_open_group(depth: i64, max_depth: i64) -> bool {
+    if depth < 0 {
+        return false;
+    }
+    if max_depth <= 0 {
+        return true; // unbounded (matches Go splitGroups)
+    }
+    if max_depth == 3 {
+        return log_groups::State { depth }.can_open();
+    }
+    depth < max_depth
+}
+
+/// rate-limit: wait needed (scalar encoding of duration, like Go).
+pub fn rate_limit_wait_needed(remaining: i64, reset_known: bool, until_reset_positive: bool) -> bool {
+    let reset_at = if reset_known { 1 } else { 0 };
+    let clock = if until_reset_positive { 0 } else { reset_at };
+    rate_limit::State {
+        remaining,
+        sleeping: false,
+        clock,
+        reset_at,
+        sent_while_exhausted: false,
+    }
+    .wait_needed()
+}
+
+/// sync-bounds: accept jobs attempt.
+pub fn accept_jobs_attempt(stored: i64, incoming: i64) -> bool {
+    sync_bounds::State {
+        phase: String::from("stored"),
+        stored_attempt: stored,
+        incoming_attempt: incoming,
+        accepted: false,
+    }
+    .accept_allowed()
+}
+
+/// tui-reload: fresh log-fetch (job match + CanFetchAccept).
+pub fn log_fetch_result_fresh(msg_job: i64, fetching_job: i64, msg_gen: i64, reload_gen: i64) -> bool {
+    if msg_job == 0 || msg_job != fetching_job {
+        return false;
+    }
+    tui_reload::State {
+        is_loading: false,
+        reload_gen,
+        fetch_job: fetching_job,
+        fetch_gen: msg_gen,
+        stale_accepted: false,
+    }
+    .can_fetch_accept()
+}
+
+/// span-tree: drop API side of 1+1 twin.
+pub fn drop_api_for_runner_twin(api_count: i64, runner_count: i64, this_is_runner: bool) -> bool {
+    if api_count != 1 || runner_count != 1 {
+        return false;
+    }
+    let kept = span_tree::State::init()
+        .see_api()
+        .see_runner()
+        .dedup_choose()
+        .kept;
+    kept == "runner" && !this_is_runner
+}
+
+/// timing-clamp: DoClamp on hostile child.
+pub fn clamp_span_to_parent(start: i64, end: i64, parent_start: i64, parent_end: i64) -> (i64, i64) {
+    let s = timing_clamp::State {
+        phase: String::from("init"),
+        start,
+        end,
+        parent_start,
+        parent_end,
+        out_start: 0,
+        out_end: 0,
+    }
+    .do_clamp();
+    (s.out_start, s.out_end)
+}
diff --git a/crates/decision_cores/src/gha_lifecycle.rs b/crates/decision_cores/src/gha_lifecycle.rs
new file mode 100644
index 0000000..2362cca
--- /dev/null
+++ b/crates/decision_cores/src/gha_lifecycle.rs
@@ -0,0 +1,195 @@
+// Code generated by specgen from specs/gha-lifecycle/decision/Decision.tla — DO NOT EDIT.
+//
+// Source:     specs/gha-lifecycle/decision/Decision.tla
+// Regenerate: bazel run //tools/decision:update
+//
+// Edit the .tla, not this file. Language: Rust (PATH A decision core).
+// Package/module hint: ghalifecyclespec
+
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub struct State {
+	pub has_completed_at: bool,
+	pub conclusion: String,
+	pub counted_pending: bool,
+	pub counted_failed: bool,
+	pub queue_counted: bool,
+}
+
+impl State {
+	/// Initial state from the TLA+ Init predicate.
+	pub fn init() -> Self {
+		Self {
+			has_completed_at: false,
+			conclusion: String::from("failure"),
+			counted_pending: false,
+			counted_failed: false,
+			queue_counted: false,
+		}
+	}
+
+	/// Guard for action ClassifyPending.
+	pub fn can_classify_pending(&self) -> bool {
+		!(self.has_completed_at) && !(self.counted_pending)
+	}
+
+	/// Apply action ClassifyPending (consuming self — pure transition).
+	pub fn classify_pending(self) -> Self {
+		let pre = self;
+		Self {
+			counted_pending: true,
+			has_completed_at: pre.has_completed_at,
+			conclusion: pre.conclusion,
+			counted_failed: pre.counted_failed,
+			queue_counted: pre.queue_counted,
+		}
+	}
+
+	/// Guard for action ClassifyFailed.
+	pub fn can_classify_failed(&self) -> bool {
+		((false || self.has_completed_at) && ((self.conclusion == "failure") || (self.conclusion == "timed_out"))) && !(self.counted_failed)
+	}
+
+	/// Apply action ClassifyFailed (consuming self — pure transition).
+	pub fn classify_failed(self) -> Self {
+		let pre = self;
+		Self {
+			counted_failed: true,
+			has_completed_at: pre.has_completed_at,
+			conclusion: pre.conclusion,
+			counted_pending: pre.counted_pending,
+			queue_counted: pre.queue_counted,
+		}
+	}
+
+	/// Guard for action ClassifyQueue.
+	pub fn can_classify_queue(&self) -> bool {
+		(false || self.has_completed_at) && !(self.queue_counted)
+	}
+
+	/// Apply action ClassifyQueue (consuming self — pure transition).
+	pub fn classify_queue(self) -> Self {
+		let pre = self;
+		Self {
+			queue_counted: true,
+			has_completed_at: pre.has_completed_at,
+			conclusion: pre.conclusion,
+			counted_pending: pre.counted_pending,
+			counted_failed: pre.counted_failed,
+		}
+	}
+
+	/// Guard for action Reset.
+	pub fn can_reset(&self) -> bool {
+		true
+	}
+
+	/// Apply action Reset (consuming self — pure transition).
+	pub fn reset(self) -> Self {
+		let pre = self;
+		Self {
+			counted_pending: false,
+			counted_failed: false,
+			queue_counted: false,
+			has_completed_at: true,
+			conclusion: (if pre.conclusion == "failure" { String::from("timed_out") } else { if pre.conclusion == "timed_out" { String::from("success") } else { String::from("failure") } }),
+		}
+	}
+
+	/// Names of actions whose guards hold.
+	pub fn enabled_actions(&self) -> Vec<&'static str> {
+		let mut out = Vec::new();
+		if self.can_classify_pending() {
+			out.push("ClassifyPending");
+		}
+		if self.can_classify_failed() {
+			out.push("ClassifyFailed");
+		}
+		if self.can_classify_queue() {
+			out.push("ClassifyQueue");
+		}
+		if self.can_reset() {
+			out.push("Reset");
+		}
+		out
+	}
+
+	/// Apply a named action if its guard holds.
+	pub fn apply_action(self, name: &str) -> Option<Self> {
+		match name {
+			"ClassifyPending" => {
+				if self.can_classify_pending() {
+					Some(self.classify_pending())
+				} else {
+					None
+				}
+			}
+			"ClassifyFailed" => {
+				if self.can_classify_failed() {
+					Some(self.classify_failed())
+				} else {
+					None
+				}
+			}
+			"ClassifyQueue" => {
+				if self.can_classify_queue() {
+					Some(self.classify_queue())
+				} else {
+					None
+				}
+			}
+			"Reset" => {
+				if self.can_reset() {
+					Some(self.reset())
+				} else {
+					None
+				}
+			}
+			_ => None,
+		}
+	}
+}
+
+impl State {
+	/// Pure TLA+ operator PendingNeverFailed.
+	pub fn pending_never_failed(&self) -> bool {
+		!((self.counted_pending && self.counted_failed))
+	}
+
+	/// Pure TLA+ operator QueueOnlyNotPending.
+	pub fn queue_only_not_pending(&self) -> bool {
+		!(self.queue_counted) || (self.has_completed_at)
+	}
+
+}
+
+/// Named pure predicates for dual/CI enumeration.
+pub struct PurePredicate {
+	pub name: &'static str,
+	pub check: fn(&State) -> bool,
+}
+
+/// Every pure operator emitted for this module.
+pub const PURE_PREDICATES: &[PurePredicate] = &[
+	PurePredicate { name: "PendingNeverFailed", check: State::pending_never_failed },
+	PurePredicate { name: "QueueOnlyNotPending", check: State::queue_only_not_pending },
+];
+
+#[cfg(test)]
+mod tests {
+	use super::*;
+
+	#[test]
+	fn init_ok() {
+		let s = State::init();
+		let _ = s.enabled_actions();
+	}
+
+	#[test]
+	fn pure_predicates_no_panic() {
+		let s = State::init();
+		assert_eq!(PURE_PREDICATES.len(), 2);
+		for p in PURE_PREDICATES {
+			let _ = (p.check)(&s);
+		}
+	}
+}
diff --git a/crates/decision_cores/src/lib.rs b/crates/decision_cores/src/lib.rs
new file mode 100644
index 0000000..100c3d8
--- /dev/null
+++ b/crates/decision_cores/src/lib.rs
@@ -0,0 +1,20 @@
+//! Decision cores for otel-explorer (Rust peer of Go `*spec` packages).
+//!
+//! **SSOT:** `specs/<core>/decision/Decision.tla`  
+//! **Regen:** `bazel run //tools/decision:update`  
+//! **Check:** `cargo test -p decision_cores` and `bazel test //tools/decision:up_to_date`
+//!
+//! Generated modules are pure state machines. Production-style gates live in
+//! [`gates`] — thin wrappers (same idea as Go `canCloseGroup` → `CanClose`).
+
+#![allow(dead_code)]
+
+pub mod gha_lifecycle;
+pub mod log_groups;
+pub mod rate_limit;
+pub mod span_tree;
+pub mod sync_bounds;
+pub mod timing_clamp;
+pub mod tui_reload;
+
+pub mod gates;
diff --git a/crates/decision_cores/src/log_groups.rs b/crates/decision_cores/src/log_groups.rs
new file mode 100644
index 0000000..0751120
--- /dev/null
+++ b/crates/decision_cores/src/log_groups.rs
@@ -0,0 +1,165 @@
+// Code generated by specgen from specs/log-groups/decision/Decision.tla — DO NOT EDIT.
+//
+// Source:     specs/log-groups/decision/Decision.tla
+// Regenerate: bazel run //tools/decision:update
+//
+// Edit the .tla, not this file. Language: Rust (PATH A decision core).
+// Package/module hint: loggroupsspec
+
+#[derive(Copy, Clone, Debug, Default, PartialEq, Eq)]
+pub struct State {
+	pub depth: i64,
+}
+
+impl State {
+	/// Initial state from the TLA+ Init predicate.
+	pub fn init() -> Self {
+		Self {
+			depth: 0,
+		}
+	}
+
+	/// Guard for action Open.
+	pub fn can_open(&self) -> bool {
+		(self.depth >= 0) && (self.depth < 3)
+	}
+
+	/// Apply action Open (consuming self — pure transition).
+	pub fn open(self) -> Self {
+		let pre = self;
+		Self {
+			depth: (pre.depth + 1),
+		}
+	}
+
+	/// Guard for action Close.
+	pub fn can_close(&self) -> bool {
+		self.depth > 0
+	}
+
+	/// Apply action Close (consuming self — pure transition).
+	pub fn close(self) -> Self {
+		let pre = self;
+		Self {
+			depth: (pre.depth - 1),
+		}
+	}
+
+	/// Guard for action CloseBug.
+	pub fn can_close_bug(&self) -> bool {
+		false && (self.depth == 0)
+	}
+
+	/// Apply action CloseBug (consuming self — pure transition).
+	pub fn close_bug(self) -> Self {
+		let pre = self;
+		Self {
+			depth: (pre.depth - 1),
+		}
+	}
+
+	/// Guard for action Terminating.
+	pub fn can_terminating(&self) -> bool {
+		true
+	}
+
+	/// Apply action Terminating (consuming self — pure transition).
+	pub fn terminating(self) -> Self {
+		let pre = self;
+		Self {
+			depth: pre.depth,
+		}
+	}
+
+	/// Names of actions whose guards hold.
+	pub fn enabled_actions(&self) -> Vec<&'static str> {
+		let mut out = Vec::new();
+		if self.can_open() {
+			out.push("Open");
+		}
+		if self.can_close() {
+			out.push("Close");
+		}
+		if self.can_close_bug() {
+			out.push("CloseBug");
+		}
+		if self.can_terminating() {
+			out.push("Terminating");
+		}
+		out
+	}
+
+	/// Apply a named action if its guard holds.
+	pub fn apply_action(self, name: &str) -> Option<Self> {
+		match name {
+			"Open" => {
+				if self.can_open() {
+					Some(self.open())
+				} else {
+					None
+				}
+			}
+			"Close" => {
+				if self.can_close() {
+					Some(self.close())
+				} else {
+					None
+				}
+			}
+			"CloseBug" => {
+				if self.can_close_bug() {
+					Some(self.close_bug())
+				} else {
+					None
+				}
+			}
+			"Terminating" => {
+				if self.can_terminating() {
+					Some(self.terminating())
+				} else {
+					None
+				}
+			}
+			_ => None,
+		}
+	}
+}
+
+impl State {
+	/// Pure TLA+ operator Inv_DepthNonNeg.
+	pub fn inv_depth_non_neg(&self) -> bool {
+		self.depth >= 0
+	}
+
+}
+
+/// Named pure predicates for dual/CI enumeration.
+pub struct PurePredicate {
+	pub name: &'static str,
+	pub check: fn(&State) -> bool,
+}
+
+/// Every pure operator emitted for this module.
+pub const PURE_PREDICATES: &[PurePredicate] = &[
+	PurePredicate { name: "Inv_DepthNonNeg", check: State::inv_depth_non_neg },
+];
+
+#[cfg(test)]
+mod tests {
+	use super::*;
+
+	#[test]
+	fn init_ok() {
+		let s = State::init();
+		let _ = s.enabled_actions();
+	}
+
+	#[test]
+	fn pure_predicates_no_panic() {
+		let s = State::init();
+		assert_eq!(PURE_PREDICATES.len(), 1);
+		for p in PURE_PREDICATES {
+			let _ = (p.check)(&s);
+		}
+	}
+}
diff --git a/crates/decision_cores/src/rate_limit.rs b/crates/decision_cores/src/rate_limit.rs
new file mode 100644
index 0000000..482e692
--- /dev/null
+++ b/crates/decision_cores/src/rate_limit.rs
@@ -0,0 +1,276 @@
+// Code generated by specgen from specs/rate-limit/decision/Decision.tla — DO NOT EDIT.
+//
+// Source:     specs/rate-limit/decision/Decision.tla
+// Regenerate: bazel run //tools/decision:update
+//
+// Edit the .tla, not this file. Language: Rust (PATH A decision core).
+// Package/module hint: ratelimitspec
+
+#[derive(Copy, Clone, Debug, Default, PartialEq, Eq)]
+pub struct State {
+	pub remaining: i64,
+	pub sleeping: bool,
+	pub clock: i64,
+	pub reset_at: i64,
+	pub sent_while_exhausted: bool,
+}
+
+impl State {
+	/// Initial state from the TLA+ Init predicate.
+	pub fn init() -> Self {
+		Self {
+			remaining: 2,
+			sleeping: false,
+			clock: 0,
+			reset_at: 0,
+			sent_while_exhausted: false,
+		}
+	}
+
+	/// Guard for action LearnExhausted.
+	pub fn can_learn_exhausted(&self) -> bool {
+		(self.remaining > 0) && (self.clock < 3)
+	}
+
+	/// Apply action LearnExhausted (consuming self — pure transition).
+	pub fn learn_exhausted(self) -> Self {
+		let pre = self;
+		Self {
+			remaining: 0,
+			reset_at: (pre.clock + 1),
+			sleeping: pre.sleeping,
+			clock: pre.clock,
+			sent_while_exhausted: pre.sent_while_exhausted,
+		}
+	}
+
+	/// Guard for action StartSleep.
+	pub fn can_start_sleep(&self) -> bool {
+		(((self.remaining == 0) && !(self.sleeping)) && (self.clock < self.reset_at)) && (self.reset_at > 0)
+	}
+
+	/// Apply action StartSleep (consuming self — pure transition).
+	pub fn start_sleep(self) -> Self {
+		let pre = self;
+		Self {
+			sleeping: true,
+			remaining: pre.remaining,
+			clock: pre.clock,
+			reset_at: pre.reset_at,
+			sent_while_exhausted: pre.sent_while_exhausted,
+		}
+	}
+
+	/// Guard for action WakeRecheckSend.
+	pub fn can_wake_recheck_send(&self) -> bool {
+		self.sleeping && !((((self.remaining == 0) && (self.reset_at > 0)) && (self.clock < self.reset_at)))
+	}
+
+	/// Apply action WakeRecheckSend (consuming self — pure transition).
+	pub fn wake_recheck_send(self) -> Self {
+		let pre = self;
+		Self {
+			sleeping: false,
+			remaining: 2,
+			clock: pre.clock,
+			reset_at: pre.reset_at,
+			sent_while_exhausted: pre.sent_while_exhausted,
+		}
+	}
+
+	/// Guard for action WakeRecheckResleep.
+	pub fn can_wake_recheck_resleep(&self) -> bool {
+		(((!(false) && self.sleeping) && (self.remaining == 0)) && (self.reset_at > 0)) && (self.clock < self.reset_at)
+	}
+
+	/// Apply action WakeRecheckResleep (consuming self — pure transition).
+	pub fn wake_recheck_resleep(self) -> Self {
+		let pre = self;
+		Self {
+			remaining: pre.remaining,
+			sleeping: pre.sleeping,
+			clock: pre.clock,
+			reset_at: pre.reset_at,
+			sent_while_exhausted: pre.sent_while_exhausted,
+		}
+	}
+
+	/// Guard for action WakeBugSend.
+	pub fn can_wake_bug_send(&self) -> bool {
+		false && self.sleeping
+	}
+
+	/// Apply action WakeBugSend (consuming self — pure transition).
+	pub fn wake_bug_send(self) -> Self {
+		let pre = self;
+		Self {
+			sleeping: false,
+			sent_while_exhausted: (((pre.remaining == 0) && (pre.reset_at > 0)) && (pre.clock < pre.reset_at)),
+			remaining: (if ((pre.remaining == 0) && (pre.reset_at > 0)) && (pre.clock < pre.reset_at) { pre.remaining } else { 2 }),
+			clock: pre.clock,
+			reset_at: pre.reset_at,
+		}
+	}
+
+	/// Guard for action Tick.
+	pub fn can_tick(&self) -> bool {
+		self.clock < 3
+	}
+
+	/// Apply action Tick (consuming self — pure transition).
+	pub fn tick(self) -> Self {
+		let pre = self;
+		Self {
+			clock: (pre.clock + 1),
+			remaining: (if ((pre.remaining == 0) && (pre.reset_at > 0)) && ((pre.clock + 1) >= pre.reset_at) { 2 } else { pre.remaining }),
+			sleeping: pre.sleeping,
+			reset_at: pre.reset_at,
+			sent_while_exhausted: pre.sent_while_exhausted,
+		}
+	}
+
+	/// Guard for action SendOk.
+	pub fn can_send_ok(&self) -> bool {
+		(self.remaining > 0) && !(self.sleeping)
+	}
+
+	/// Apply action SendOk (consuming self — pure transition).
+	pub fn send_ok(self) -> Self {
+		let pre = self;
+		Self {
+			remaining: (pre.remaining - 1),
+			sleeping: pre.sleeping,
+			clock: pre.clock,
+			reset_at: pre.reset_at,
+			sent_while_exhausted: pre.sent_while_exhausted,
+		}
+	}
+
+	/// Names of actions whose guards hold.
+	pub fn enabled_actions(&self) -> Vec<&'static str> {
+		let mut out = Vec::new();
+		if self.can_learn_exhausted() {
+			out.push("LearnExhausted");
+		}
+		if self.can_start_sleep() {
+			out.push("StartSleep");
+		}
+		if self.can_wake_recheck_send() {
+			out.push("WakeRecheckSend");
+		}
+		if self.can_wake_recheck_resleep() {
+			out.push("WakeRecheckResleep");
+		}
+		if self.can_wake_bug_send() {
+			out.push("WakeBugSend");
+		}
+		if self.can_tick() {
+			out.push("Tick");
+		}
+		if self.can_send_ok() {
+			out.push("SendOk");
+		}
+		out
+	}
+
+	/// Apply a named action if its guard holds.
+	pub fn apply_action(self, name: &str) -> Option<Self> {
+		match name {
+			"LearnExhausted" => {
+				if self.can_learn_exhausted() {
+					Some(self.learn_exhausted())
+				} else {
+					None
+				}
+			}
+			"StartSleep" => {
+				if self.can_start_sleep() {
+					Some(self.start_sleep())
+				} else {
+					None
+				}
+			}
+			"WakeRecheckSend" => {
+				if self.can_wake_recheck_send() {
+					Some(self.wake_recheck_send())
+				} else {
+					None
+				}
+			}
+			"WakeRecheckResleep" => {
+				if self.can_wake_recheck_resleep() {
+					Some(self.wake_recheck_resleep())
+				} else {
+					None
+				}
+			}
+			"WakeBugSend" => {
+				if self.can_wake_bug_send() {
+					Some(self.wake_bug_send())
+				} else {
+					None
+				}
+			}
+			"Tick" => {
+				if self.can_tick() {
+					Some(self.tick())
+				} else {
+					None
+				}
+			}
+			"SendOk" => {
+				if self.can_send_ok() {
+					Some(self.send_ok())
+				} else {
+					None
+				}
+			}
+			_ => None,
+		}
+	}
+}
+
+impl State {
+	/// Pure TLA+ operator WaitNeeded.
+	pub fn wait_needed(&self) -> bool {
+		((self.remaining == 0) && (self.reset_at > 0)) && (self.clock < self.reset_at)
+	}
+
+	/// Pure TLA+ operator NoSendWhileExhausted.
+	pub fn no_send_while_exhausted(&self) -> bool {
+		!(self.sent_while_exhausted)
+	}
+
+}
+
+/// Named pure predicates for dual/CI enumeration.
+pub struct PurePredicate {
+	pub name: &'static str,
+	pub check: fn(&State) -> bool,
+}
+
+/// Every pure operator emitted for this module.
+pub const PURE_PREDICATES: &[PurePredicate] = &[
+	PurePredicate { name: "WaitNeeded", check: State::wait_needed },
+	PurePredicate { name: "NoSendWhileExhausted", check: State::no_send_while_exhausted },
+];
+
+#[cfg(test)]
+mod tests {
+	use super::*;
+
+	#[test]
+	fn init_ok() {
+		let s = State::init();
+		let _ = s.enabled_actions();
+	}
+
+	#[test]
+	fn pure_predicates_no_panic() {
+		let s = State::init();
+		assert_eq!(PURE_PREDICATES.len(), 2);
+		for p in PURE_PREDICATES {
+			let _ = (p.check)(&s);
+		}
+	}
+}
diff --git a/crates/decision_cores/src/span_tree.rs b/crates/decision_cores/src/span_tree.rs
new file mode 100644
index 0000000..f44f1a4
--- /dev/null
+++ b/crates/decision_cores/src/span_tree.rs
@@ -0,0 +1,209 @@
+// Code generated by specgen from specs/span-tree/decision/Decision.tla — DO NOT EDIT.
+//
+// Source:     specs/span-tree/decision/Decision.tla
+// Regenerate: bazel run //tools/decision:update
+//
+// Edit the .tla, not this file. Language: Rust (PATH A decision core).
+// Package/module hint: spantreespec
+
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub struct State {
+	pub have_api: bool,
+	pub have_runner: bool,
+	pub kept: String,
+	pub done: bool,
+}
+
+impl State {
+	/// Initial state from the TLA+ Init predicate.
+	pub fn init() -> Self {
+		Self {
+			have_api: false,
+			have_runner: false,
+			kept: String::from("none"),
+			done: false,
+		}
+	}
+
+	/// Guard for action SeeAPI.
+	pub fn can_see_api(&self) -> bool {
+		!(self.done) && !(self.have_api)
+	}
+
+	/// Apply action SeeAPI (consuming self — pure transition).
+	pub fn see_api(self) -> Self {
+		let pre = self;
+		Self {
+			have_api: true,
+			have_runner: pre.have_runner,
+			kept: pre.kept,
+			done: pre.done,
+		}
+	}
+
+	/// Guard for action SeeRunner.
+	pub fn can_see_runner(&self) -> bool {
+		!(self.done) && !(self.have_runner)
+	}
+
+	/// Apply action SeeRunner (consuming self — pure transition).
+	pub fn see_runner(self) -> Self {
+		let pre = self;
+		Self {
+			have_runner: true,
+			have_api: pre.have_api,
+			kept: pre.kept,
+			done: pre.done,
+		}
+	}
+
+	/// Guard for action DedupChoose.
+	pub fn can_dedup_choose(&self) -> bool {
+		!(self.done) && (if self.have_api { true } else { self.have_runner })
+	}
+
+	/// Apply action DedupChoose (consuming self — pure transition).
+	pub fn dedup_choose(self) -> Self {
+		let pre = self;
+		Self {
+			done: true,
+			kept: (if pre.have_api && pre.have_runner { String::from("runner") } else { if pre.have_runner { String::from("runner") } else { String::from("api") } }),
+			have_api: pre.have_api,
+			have_runner: pre.have_runner,
+		}
+	}
+
+	/// Guard for action DedupBug.
+	pub fn can_dedup_bug(&self) -> bool {
+		((false && !(self.done)) && self.have_api) && self.have_runner
+	}
+
+	/// Apply action DedupBug (consuming self — pure transition).
+	pub fn dedup_bug(self) -> Self {
+		let pre = self;
+		Self {
+			done: true,
+			kept: String::from("api"),
+			have_api: pre.have_api,
+			have_runner: pre.have_runner,
+		}
+	}
+
+	/// Guard for action Terminating.
+	pub fn can_terminating(&self) -> bool {
+		self.done
+	}
+
+	/// Apply action Terminating (consuming self — pure transition).
+	pub fn terminating(self) -> Self {
+		let pre = self;
+		Self {
+			have_api: pre.have_api,
+			have_runner: pre.have_runner,
+			kept: pre.kept,
+			done: pre.done,
+		}
+	}
+
+	/// Names of actions whose guards hold.
+	pub fn enabled_actions(&self) -> Vec<&'static str> {
+		let mut out = Vec::new();
+		if self.can_see_api() {
+			out.push("SeeAPI");
+		}
+		if self.can_see_runner() {
+			out.push("SeeRunner");
+		}
+		if self.can_dedup_choose() {
+			out.push("DedupChoose");
+		}
+		if self.can_dedup_bug() {
+			out.push("DedupBug");
+		}
+		if self.can_terminating() {
+			out.push("Terminating");
+		}
+		out
+	}
+
+	/// Apply a named action if its guard holds.
+	pub fn apply_action(self, name: &str) -> Option<Self> {
+		match name {
+			"SeeAPI" => {
+				if self.can_see_api() {
+					Some(self.see_api())
+				} else {
+					None
+				}
+			}
+			"SeeRunner" => {
+				if self.can_see_runner() {
+					Some(self.see_runner())
+				} else {
+					None
+				}
+			}
+			"DedupChoose" => {
+				if self.can_dedup_choose() {
+					Some(self.dedup_choose())
+				} else {
+					None
+				}
+			}
+			"DedupBug" => {
+				if self.can_dedup_bug() {
+					Some(self.dedup_bug())
+				} else {
+					None
+				}
+			}
+			"Terminating" => {
+				if self.can_terminating() {
+					Some(self.terminating())
+				} else {
+					None
+				}
+			}
+			_ => None,
+		}
+	}
+}
+
+impl State {
+	/// Pure TLA+ operator Inv_RunnerWins.
+	pub fn inv_runner_wins(&self) -> bool {
+		!(((self.done && self.have_api) && self.have_runner)) || ((self.kept == "runner"))
+	}
+
+}
+
+/// Named pure predicates for dual/CI enumeration.
+pub struct PurePredicate {
+	pub name: &'static str,
+	pub check: fn(&State) -> bool,
+}
+
+/// Every pure operator emitted for this module.
+pub const PURE_PREDICATES: &[PurePredicate] = &[
+	PurePredicate { name: "Inv_RunnerWins", check: State::inv_runner_wins },
+];
+
+#[cfg(test)]
+mod tests {
+	use super::*;
+
+	#[test]
+	fn init_ok() {
+		let s = State::init();
+		let _ = s.enabled_actions();
+	}
+
+	#[test]
+	fn pure_predicates_no_panic() {
+		let s = State::init();
+		assert_eq!(PURE_PREDICATES.len(), 1);
+		for p in PURE_PREDICATES {
+			let _ = (p.check)(&s);
+		}
+	}
+}
diff --git a/crates/decision_cores/src/sync_bounds.rs b/crates/decision_cores/src/sync_bounds.rs
new file mode 100644
index 0000000..ec0b560
--- /dev/null
+++ b/crates/decision_cores/src/sync_bounds.rs
@@ -0,0 +1,215 @@
+// Code generated by specgen from specs/sync-bounds/decision/Decision.tla — DO NOT EDIT.
+//
+// Source:     specs/sync-bounds/decision/Decision.tla
+// Regenerate: bazel run //tools/decision:update
+//
+// Edit the .tla, not this file. Language: Rust (PATH A decision core).
+// Package/module hint: syncboundsspec
+
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub struct State {
+	pub phase: String,
+	pub stored_attempt: i64,
+	pub incoming_attempt: i64,
+	pub accepted: bool,
+}
+
+impl State {
+	/// Initial state from the TLA+ Init predicate.
+	pub fn init() -> Self {
+		Self {
+			phase: String::from("empty"),
+			stored_attempt: 0,
+			incoming_attempt: 0,
+			accepted: false,
+		}
+	}
+
+	/// Guard for action Store1.
+	pub fn can_store1(&self) -> bool {
+		(self.phase == "empty") || (self.phase == "stored")
+	}
+
+	/// Apply action Store1 (consuming self — pure transition).
+	pub fn store1(self) -> Self {
+		let pre = self;
+		Self {
+			phase: String::from("stored"),
+			stored_attempt: 1,
+			incoming_attempt: pre.incoming_attempt,
+			accepted: pre.accepted,
+		}
+	}
+
+	/// Guard for action Store2.
+	pub fn can_store2(&self) -> bool {
+		(self.phase == "empty") || (self.phase == "stored")
+	}
+
+	/// Apply action Store2 (consuming self — pure transition).
+	pub fn store2(self) -> Self {
+		let pre = self;
+		Self {
+			phase: String::from("stored"),
+			stored_attempt: 2,
+			incoming_attempt: pre.incoming_attempt,
+			accepted: pre.accepted,
+		}
+	}
+
+	/// Guard for action Store3.
+	pub fn can_store3(&self) -> bool {
+		(self.phase == "empty") || (self.phase == "stored")
+	}
+
+	/// Apply action Store3 (consuming self — pure transition).
+	pub fn store3(self) -> Self {
+		let pre = self;
+		Self {
+			phase: String::from("stored"),
+			stored_attempt: 3,
+			incoming_attempt: pre.incoming_attempt,
+			accepted: pre.accepted,
+		}
+	}
+
+	/// Guard for action OfferNewer.
+	pub fn can_offer_newer(&self) -> bool {
+		(self.phase == "stored") && (self.stored_attempt > 0)
+	}
+
+	/// Apply action OfferNewer (consuming self — pure transition).
+	pub fn offer_newer(self) -> Self {
+		let pre = self;
+		Self {
+			phase: String::from("decided"),
+			incoming_attempt: pre.stored_attempt,
+			accepted: true,
+			stored_attempt: pre.stored_attempt,
+		}
+	}
+
+	/// Guard for action OfferOlder.
+	pub fn can_offer_older(&self) -> bool {
+		(self.phase == "stored") && (self.stored_attempt > 1)
+	}
+
+	/// Apply action OfferOlder (consuming self — pure transition).
+	pub fn offer_older(self) -> Self {
+		let pre = self;
+		Self {
+			phase: String::from("decided"),
+			incoming_attempt: (pre.stored_attempt - 1),
+			accepted: false,
+			stored_attempt: pre.stored_attempt,
+		}
+	}
+
+	/// Names of actions whose guards hold.
+	pub fn enabled_actions(&self) -> Vec<&'static str> {
+		let mut out = Vec::new();
+		if self.can_store1() {
+			out.push("Store1");
+		}
+		if self.can_store2() {
+			out.push("Store2");
+		}
+		if self.can_store3() {
+			out.push("Store3");
+		}
+		if self.can_offer_newer() {
+			out.push("OfferNewer");
+		}
+		if self.can_offer_older() {
+			out.push("OfferOlder");
+		}
+		out
+	}
+
+	/// Apply a named action if its guard holds.
+	pub fn apply_action(self, name: &str) -> Option<Self> {
+		match name {
+			"Store1" => {
+				if self.can_store1() {
+					Some(self.store1())
+				} else {
+					None
+				}
+			}
+			"Store2" => {
+				if self.can_store2() {
+					Some(self.store2())
+				} else {
+					None
+				}
+			}
+			"Store3" => {
+				if self.can_store3() {
+					Some(self.store3())
+				} else {
+					None
+				}
+			}
+			"OfferNewer" => {
+				if self.can_offer_newer() {
+					Some(self.offer_newer())
+				} else {
+					None
+				}
+			}
+			"OfferOlder" => {
+				if self.can_offer_older() {
+					Some(self.offer_older())
+				} else {
+					None
+				}
+			}
+			_ => None,
+		}
+	}
+}
+
+impl State {
+	/// Pure TLA+ operator NoStaleAccepted.
+	pub fn no_stale_accepted(&self) -> bool {
+		!(self.accepted) || ((self.incoming_attempt >= self.stored_attempt))
+	}
+
+	/// Pure TLA+ operator AcceptAllowed.
+	pub fn accept_allowed(&self) -> bool {
+		(self.incoming_attempt == 0) || (self.incoming_attempt == self.stored_attempt)
+	}
+
+}
+
+/// Named pure predicates for dual/CI enumeration.
+pub struct PurePredicate {
+	pub name: &'static str,
+	pub check: fn(&State) -> bool,
+}
+
+/// Every pure operator emitted for this module.
+pub const PURE_PREDICATES: &[PurePredicate] = &[
+	PurePredicate { name: "NoStaleAccepted", check: State::no_stale_accepted },
+	PurePredicate { name: "AcceptAllowed", check: State::accept_allowed },
+];
+
+#[cfg(test)]
+mod tests {
+	use super::*;
+
+	#[test]
+	fn init_ok() {
+		let s = State::init();
+		let _ = s.enabled_actions();
+	}
+
+	#[test]
+	fn pure_predicates_no_panic() {
+		let s = State::init();
+		assert_eq!(PURE_PREDICATES.len(), 2);
+		for p in PURE_PREDICATES {
+			let _ = (p.check)(&s);
+		}
+	}
+}
diff --git a/crates/decision_cores/src/timing_clamp.rs b/crates/decision_cores/src/timing_clamp.rs
new file mode 100644
index 0000000..58d733e
--- /dev/null
+++ b/crates/decision_cores/src/timing_clamp.rs
@@ -0,0 +1,207 @@
+// Code generated by specgen from specs/timing-clamp/decision/Decision.tla — DO NOT EDIT.
+//
+// Source:     specs/timing-clamp/decision/Decision.tla
+// Regenerate: bazel run //tools/decision:update
+//
+// Edit the .tla, not this file. Language: Rust (PATH A decision core).
+// Package/module hint: timingclampspec
+
+#[derive(Clone, Debug, Default, PartialEq, Eq)]
+pub struct State {
+	pub phase: String,
+	pub start: i64,
+	pub end: i64,
+	pub parent_start: i64,
+	pub parent_end: i64,
+	pub out_start: i64,
+	pub out_end: i64,
+}
+
+impl State {
+	/// Initial state from the TLA+ Init predicate.
+	pub fn init() -> Self {
+		Self {
+			phase: String::from("init"),
+			start: 2,
+			end: 4,
+			parent_start: 1,
+			parent_end: 3,
+			out_start: 0,
+			out_end: 0,
+		}
+	}
+
+	/// Guard for action SetHostile.
+	pub fn can_set_hostile(&self) -> bool {
+		self.phase == "init"
+	}
+
+	/// Apply action SetHostile (consuming self — pure transition).
+	pub fn set_hostile(self) -> Self {
+		let pre = self;
+		Self {
+			start: 0,
+			end: 4,
+			parent_start: 2,
+			parent_end: 3,
+			phase: pre.phase,
+			out_start: pre.out_start,
+			out_end: pre.out_end,
+		}
+	}
+
+	/// Guard for action DoClamp.
+	pub fn can_do_clamp(&self) -> bool {
+		(self.phase == "init") && !(false)
+	}
+
+	/// Apply action DoClamp (consuming self — pure transition).
+	pub fn do_clamp(self) -> Self {
+		let pre = self;
+		Self {
+			phase: String::from("clamped"),
+			out_start: (if pre.start < pre.parent_start { pre.parent_start } else { if pre.start > ((if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end }) - 1) { (if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end }) - 1 } else { pre.start } }),
+			out_end: (if (if pre.end > (if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end }) { if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end } } else { pre.end }) < ((if pre.start < pre.parent_start { pre.parent_start } else { if pre.start > ((if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end }) - 1) { (if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end }) - 1 } else { pre.start } }) + 1) { (if pre.start < pre.parent_start { pre.parent_start } else { if pre.start > ((if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end }) - 1) { (if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end }) - 1 } else { pre.start } }) + 1 } else { if pre.end > (if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end }) { if pre.parent_end <= pre.parent_start { pre.parent_start + 1 } else { pre.parent_end } } else { pre.end } }),
+			start: pre.start,
+			end: pre.end,
+			parent_start: pre.parent_start,
+			parent_end: pre.parent_end,
+		}
+	}
+
+	/// Guard for action BugPassthrough.
+	pub fn can_bug_passthrough(&self) -> bool {
+		(self.phase == "init") && false
+	}
+
+	/// Apply action BugPassthrough (consuming self — pure transition).
+	pub fn bug_passthrough(self) -> Self {
+		let pre = self;
+		Self {
+			phase: String::from("clamped"),
+			out_start: pre.start,
+			out_end: pre.end,
+			start: pre.start,
+			end: pre.end,
+			parent_start: pre.parent_start,
+			parent_end: pre.parent_end,
+		}
+	}
+
+	/// Guard for action Finish.
+	pub fn can_finish(&self) -> bool {
+		self.phase == "clamped"
+	}
+
+	/// Apply action Finish (consuming self — pure transition).
+	pub fn finish(self) -> Self {
+		let pre = self;
+		Self {
+			phase: String::from("done"),
+			start: pre.start,
+			end: pre.end,
+			parent_start: pre.parent_start,
+			parent_end: pre.parent_end,
+			out_start: pre.out_start,
+			out_end: pre.out_end,
+		}
+	}
+
+	/// Names of actions whose guards hold.
+	pub fn enabled_actions(&self) -> Vec<&'static str> {
+		let mut out = Vec::new();
+		if self.can_set_hostile() {
+			out.push("SetHostile");
+		}
+		if self.can_do_clamp() {
+			out.push("DoClamp");
+		}
+		if self.can_bug_passthrough() {
+			out.push("BugPassthrough");
+		}
+		if self.can_finish() {
+			out.push("Finish");
+		}
+		out
+	}
+
+	/// Apply a named action if its guard holds.
+	pub fn apply_action(self, name: &str) -> Option<Self> {
+		match name {
+			"SetHostile" => {
+				if self.can_set_hostile() {
+					Some(self.set_hostile())
+				} else {
+					None
+				}
+			}
+			"DoClamp" => {
+				if self.can_do_clamp() {
+					Some(self.do_clamp())
+				} else {
+					None
+				}
+			}
+			"BugPassthrough" => {
+				if self.can_bug_passthrough() {
+					Some(self.bug_passthrough())
+				} else {
+					None
+				}
+			}
+			"Finish" => {
+				if self.can_finish() {
+					Some(self.finish())
+				} else {
+					None
+				}
+			}
+			_ => None,
+		}
+	}
+}
+
+impl State {
+	/// Pure TLA+ operator ClampedOrdered.
+	pub fn clamped_ordered(&self) -> bool {
+		!(((self.phase == "clamped") || (self.phase == "done"))) || ((self.out_start < self.out_end))
+	}
+
+	/// Pure TLA+ operator ClampedContained.
+	pub fn clamped_contained(&self) -> bool {
+		!(((self.phase == "clamped") || (self.phase == "done"))) || (((self.out_start >= self.parent_start) && (!((self.parent_end > self.parent_start)) || (((self.out_start <= (self.parent_end - 1)) && (self.out_end <= self.parent_end))))))
+	}
+
+}
+
+/// Named pure predicates for dual/CI enumeration.
+pub struct PurePredicate {
+	pub name: &'static str,
+	pub check: fn(&State) -> bool,
+}
+
+/// Every pure operator emitted for this module.
+pub const PURE_PREDICATES: &[PurePredicate] = &[
+	PurePredicate { name: "ClampedOrdered", check: State::clamped_ordered },
+	PurePredicate { name: "ClampedContained", check: State::clamped_contained },
+];
+
+#[cfg(test)]
+mod tests {
+	use super::*;
+
+	#[test]
+	fn init_ok() {
+		let s = State::init();
+		let _ = s.enabled_actions();
+	}
+
+	#[test]
+	fn pure_predicates_no_panic() {
+		let s = State::init();
+		assert_eq!(PURE_PREDICATES.len(), 2);
+		for p in PURE_PREDICATES {
+			let _ = (p.check)(&s);
+		}
+	}
+}
diff --git a/crates/decision_cores/src/tui_reload.rs b/crates/decision_cores/src/tui_reload.rs
new file mode 100644
index 0000000..592b1a0
--- /dev/null
+++ b/crates/decision_cores/src/tui_reload.rs
@@ -0,0 +1,270 @@
+// Code generated by specgen from specs/tui-reload/decision/Decision.tla — DO NOT EDIT.
+//
+// Source:     specs/tui-reload/decision/Decision.tla
+// Regenerate: bazel run //tools/decision:update
+//
+// Edit the .tla, not this file. Language: Rust (PATH A decision core).
+// Package/module hint: tuireloadspec
+
+#[derive(Copy, Clone, Debug, Default, PartialEq, Eq)]
+pub struct State {
+	pub is_loading: bool,
+	pub reload_gen: i64,
+	pub fetch_job: i64,
+	pub fetch_gen: i64,
+	pub stale_accepted: bool,
+}
+
+impl State {
+	/// Initial state from the TLA+ Init predicate.
+	pub fn init() -> Self {
+		Self {
+			is_loading: false,
+			reload_gen: 0,
+			fetch_job: 0,
+			fetch_gen: 0,
+			stale_accepted: false,
+		}
+	}
+
+	/// Guard for action PressReload.
+	pub fn can_press_reload(&self) -> bool {
+		(false || !(self.is_loading)) && (self.reload_gen < 2)
+	}
+
+	/// Apply action PressReload (consuming self — pure transition).
+	pub fn press_reload(self) -> Self {
+		let pre = self;
+		Self {
+			is_loading: true,
+			reload_gen: pre.reload_gen,
+			fetch_job: pre.fetch_job,
+			fetch_gen: pre.fetch_gen,
+			stale_accepted: pre.stale_accepted,
+		}
+	}
+
+	/// Guard for action ReloadDone.
+	pub fn can_reload_done(&self) -> bool {
+		self.is_loading && (self.reload_gen < 2)
+	}
+
+	/// Apply action ReloadDone (consuming self — pure transition).
+	pub fn reload_done(self) -> Self {
+		let pre = self;
+		Self {
+			is_loading: false,
+			reload_gen: (pre.reload_gen + 1),
+			fetch_job: pre.fetch_job,
+			fetch_gen: pre.fetch_gen,
+			stale_accepted: pre.stale_accepted,
+		}
+	}
+
+	/// Guard for action PressFetch1.
+	pub fn can_press_fetch1(&self) -> bool {
+		!(self.is_loading) && (self.fetch_job == 0)
+	}
+
+	/// Apply action PressFetch1 (consuming self — pure transition).
+	pub fn press_fetch1(self) -> Self {
+		let pre = self;
+		Self {
+			fetch_job: 1,
+			fetch_gen: pre.reload_gen,
+			is_loading: pre.is_loading,
+			reload_gen: pre.reload_gen,
+			stale_accepted: pre.stale_accepted,
+		}
+	}
+
+	/// Guard for action PressFetch2.
+	pub fn can_press_fetch2(&self) -> bool {
+		!(self.is_loading) && (self.fetch_job == 0)
+	}
+
+	/// Apply action PressFetch2 (consuming self — pure transition).
+	pub fn press_fetch2(self) -> Self {
+		let pre = self;
+		Self {
+			fetch_job: 2,
+			fetch_gen: pre.reload_gen,
+			is_loading: pre.is_loading,
+			reload_gen: pre.reload_gen,
+			stale_accepted: pre.stale_accepted,
+		}
+	}
+
+	/// Guard for action FetchAccept.
+	pub fn can_fetch_accept(&self) -> bool {
+		(self.fetch_job != 0) && (self.fetch_gen == self.reload_gen)
+	}
+
+	/// Apply action FetchAccept (consuming self — pure transition).
+	pub fn fetch_accept(self) -> Self {
+		let pre = self;
+		Self {
+			fetch_job: 0,
+			is_loading: pre.is_loading,
+			reload_gen: pre.reload_gen,
+			fetch_gen: pre.fetch_gen,
+			stale_accepted: pre.stale_accepted,
+		}
+	}
+
+	/// Guard for action FetchDiscard.
+	pub fn can_fetch_discard(&self) -> bool {
+		(self.fetch_job != 0) && (self.fetch_gen != self.reload_gen)
+	}
+
+	/// Apply action FetchDiscard (consuming self — pure transition).
+	pub fn fetch_discard(self) -> Self {
+		let pre = self;
+		Self {
+			fetch_job: 0,
+			is_loading: pre.is_loading,
+			reload_gen: pre.reload_gen,
+			fetch_gen: pre.fetch_gen,
+			stale_accepted: pre.stale_accepted,
+		}
+	}
+
+	/// Guard for action FetchStaleBug.
+	pub fn can_fetch_stale_bug(&self) -> bool {
+		(false && (self.fetch_job != 0)) && (self.fetch_gen != self.reload_gen)
+	}
+
+	/// Apply action FetchStaleBug (consuming self — pure transition).
+	pub fn fetch_stale_bug(self) -> Self {
+		let pre = self;
+		Self {
+			stale_accepted: true,
+			fetch_job: 0,
+			is_loading: pre.is_loading,
+			reload_gen: pre.reload_gen,
+			fetch_gen: pre.fetch_gen,
+		}
+	}
+
+	/// Names of actions whose guards hold.
+	pub fn enabled_actions(&self) -> Vec<&'static str> {
+		let mut out = Vec::new();
+		if self.can_press_reload() {
+			out.push("PressReload");
+		}
+		if self.can_reload_done() {
+			out.push("ReloadDone");
+		}
+		if self.can_press_fetch1() {
+			out.push("PressFetch1");
+		}
+		if self.can_press_fetch2() {
+			out.push("PressFetch2");
+		}
+		if self.can_fetch_accept() {
+			out.push("FetchAccept");
+		}
+		if self.can_fetch_discard() {
+			out.push("FetchDiscard");
+		}
+		if self.can_fetch_stale_bug() {
+			out.push("FetchStaleBug");
+		}
+		out
+	}
+
+	/// Apply a named action if its guard holds.
+	pub fn apply_action(self, name: &str) -> Option<Self> {
+		match name {
+			"PressReload" => {
+				if self.can_press_reload() {
+					Some(self.press_reload())
+				} else {
+					None
+				}
+			}
+			"ReloadDone" => {
+				if self.can_reload_done() {
+					Some(self.reload_done())
+				} else {
+					None
+				}
+			}
+			"PressFetch1" => {
+				if self.can_press_fetch1() {
+					Some(self.press_fetch1())
+				} else {
+					None
+				}
+			}
+			"PressFetch2" => {
+				if self.can_press_fetch2() {
+					Some(self.press_fetch2())
+				} else {
+					None
+				}
+			}
+			"FetchAccept" => {
+				if self.can_fetch_accept() {
+					Some(self.fetch_accept())
+				} else {
+					None
+				}
+			}
+			"FetchDiscard" => {
+				if self.can_fetch_discard() {
+					Some(self.fetch_discard())
+				} else {
+					None
+				}
+			}
+			"FetchStaleBug" => {
+				if self.can_fetch_stale_bug() {
+					Some(self.fetch_stale_bug())
+				} else {
+					None
+				}
+			}
+			_ => None,
+		}
+	}
+}
+
+impl State {
+	/// Pure TLA+ operator NoStaleAccepted.
+	pub fn no_stale_accepted(&self) -> bool {
+		!(self.stale_accepted)
+	}
+
+}
+
+/// Named pure predicates for dual/CI enumeration.
+pub struct PurePredicate {
+	pub name: &'static str,
+	pub check: fn(&State) -> bool,
+}
+
+/// Every pure operator emitted for this module.
+pub const PURE_PREDICATES: &[PurePredicate] = &[
+	PurePredicate { name: "NoStaleAccepted", check: State::no_stale_accepted },
+];
+
+#[cfg(test)]
+mod tests {
+	use super::*;
+
+	#[test]
+	fn init_ok() {
+		let s = State::init();
+		let _ = s.enabled_actions();
+	}
+
+	#[test]
+	fn pure_predicates_no_panic() {
+		let s = State::init();
+		assert_eq!(PURE_PREDICATES.len(), 1);
+		for p in PURE_PREDICATES {
+			let _ = (p.check)(&s);
+		}
+	}
+}
diff --git a/crates/decision_cores/tests/log_groups_dual.rs b/crates/decision_cores/tests/log_groups_dual.rs
new file mode 100644
index 0000000..6056a11
--- /dev/null
+++ b/crates/decision_cores/tests/log_groups_dual.rs
@@ -0,0 +1,38 @@
+//! Dual: Rust gates ↔ generated log_groups decision core (same tables as Go duals).
+
+use decision_cores::gates;
+use decision_cores::log_groups;
+
+#[test]
+fn close_forbidden_at_zero() {
+    let s = log_groups::State::init();
+    assert_eq!(s.depth, 0);
+    assert!(!s.can_close());
+    assert!(!gates::can_close_group(0));
+}
+
+#[test]
+fn open_close_roundtrip() {
+    let s = log_groups::State::init();
+    assert!(s.can_open());
+    let s = s.open();
+    assert_eq!(s.depth, 1);
+    assert!(gates::can_close_group(s.depth));
+    assert!(s.can_close());
+    let s = s.close();
+    assert_eq!(s.depth, 0);
+}
+
+#[test]
+fn max_depth_three_matches_can_open() {
+    assert!(gates::can_open_group(0, 3));
+    assert!(gates::can_open_group(2, 3));
+    assert!(!gates::can_open_group(3, 3));
+    assert!(gates::can_open_group(3, 0)); // unbounded
+}
+
+#[test]
+fn pure_inv_depth_non_neg() {
+    let s = log_groups::State::init();
+    assert!(s.inv_depth_non_neg());
+}
diff --git a/specs/DECISION_CORES.md b/specs/DECISION_CORES.md
index 6ed866a..b88bd00 100644
--- a/specs/DECISION_CORES.md
+++ b/specs/DECISION_CORES.md
@@ -86,23 +86,28 @@ func PurePredicates() []PurePredicate     // enumerate all pure gates
 // (do not re-list PurePredicates in production dual tests)
 ```
 
-**Rust (peer language):** PATH A scalar cores via canonical JIT `specgen -lang rust`
-(`~/.ai` tool — not yet wired into this repo’s Bazel `//tools/decision` pipeline).
+**Rust (peer language):** same Decision.tla → hermetic `//tools/specgen -lang rust`
+and committed under `crates/decision_cores/src/*.rs`.
 
 ```bash
-# one core
-specgen -lang rust -const MaxDepth=3 -const Bug=FALSE \
-  -o ./out specs/log-groups/decision/Decision.tla   # → out/spec.rs
+# regen Go *spec + Rust modules (canonical)
+bazel run //tools/decision:update
+bazel test //tools/decision:up_to_date   # includes *_rs_up_to_date
 
-# all cores (optional rustc + Go↔Rust name SSOT)
-scripts/gen-decision-rust.sh
+# thin gates + duals (Rust)
+cargo test -p decision_cores
+
+# optional JIT parity / rustc (needs PATH specgen)
 scripts/gen-decision-rust.sh --check --parity
 ```
 
 Idiomatic Rust: `snake_case`, `can_open` / `open(self)`, `apply_action`,
-`Copy`/`Clone`, `PURE_PREDICATES`.  
-`--parity` asserts Go `Can*` / pure names match Rust (same Decision.tla SSOT).  
-Go remains the production path for ote.
+`PURE_PREDICATES`, thin `gates::*` wrappers.  
+Go remains ote production; both share Decision.tla SSOT.
+
+**New cores:** only when a new concurrent/stale/race decision appears — add
+`Decision.tla` + `decision_core(...)` (Go dest + `src_rs`) + duals; do not
+expand into multi-object record codegen.
 
 ```bash
 # Hermetic Bazel pipeline (preferred — used by CI via bazel test //...)
diff --git a/tools/decision/BUILD.bazel b/tools/decision/BUILD.bazel
index e8e42eb..799af54 100644
--- a/tools/decision/BUILD.bazel
+++ b/tools/decision/BUILD.bazel
@@ -2,14 +2,14 @@ load(":defs.bzl", "decision_core")
 
 # gazelle:ignore
 #
-# Decision cores: Decision.tla → pkg/.../*spec via hermetic //tools/specgen.
+# Decision cores: Decision.tla → Go *spec + Rust crates/decision_cores via //tools/specgen.
 #
-#   bazel test  //tools/decision:up_to_date   # fail if committed *spec is stale
-#   bazel run   //tools/decision:update       # rewrite committed *spec from .tla
-#   bazel build //tools/specgen               # hermetic codegen binary
+#   bazel test  //tools/decision:up_to_date   # fail if committed Go/Rust gen is stale
+#   bazel run   //tools/decision:update       # rewrite committed sources from .tla
+#   bazel build //tools/specgen
 #
-# Keep this table in sync with scripts/regenerate-decision-cores.sh and
-# specs/DECISION_CORES.md.
+# Keep this table in sync with scripts/regenerate-decision-cores.sh,
+# scripts/gen-decision-rust.sh, and specs/DECISION_CORES.md.
 
 decision_core(
     name = "tui_reload",
@@ -18,6 +18,7 @@ decision_core(
     pkg = "tuireloadspec",
     src_go = "//pkg/tui/results/tuireloadspec:spec.go",
     src_test = "//pkg/tui/results/tuireloadspec:spec_test.go",
+    src_rs = "//crates/decision_cores:src/tui_reload.rs",
     tla = "//specs:tui-reload/decision/Decision.tla",
 )
 
@@ -28,6 +29,7 @@ decision_core(
     pkg = "ratelimitspec",
     src_go = "//pkg/githubapi/ratelimitspec:spec.go",
     src_test = "//pkg/githubapi/ratelimitspec:spec_test.go",
+    src_rs = "//crates/decision_cores:src/rate_limit.rs",
     tla = "//specs:rate-limit/decision/Decision.tla",
 )
 
@@ -38,6 +40,7 @@ decision_core(
     pkg = "timingclampspec",
     src_go = "//pkg/analyzer/timingclampspec:spec.go",
     src_test = "//pkg/analyzer/timingclampspec:spec_test.go",
+    src_rs = "//crates/decision_cores:src/timing_clamp.rs",
     tla = "//specs:timing-clamp/decision/Decision.tla",
 )
 
@@ -48,6 +51,7 @@ decision_core(
     pkg = "syncboundsspec",
     src_go = "//pkg/store/syncboundsspec:spec.go",
     src_test = "//pkg/store/syncboundsspec:spec_test.go",
+    src_rs = "//crates/decision_cores:src/sync_bounds.rs",
     tla = "//specs:sync-bounds/decision/Decision.tla",
 )
 
@@ -58,6 +62,7 @@ decision_core(
     pkg = "ghalifecyclespec",
     src_go = "//pkg/analyzer/ghalifecyclespec:spec.go",
     src_test = "//pkg/analyzer/ghalifecyclespec:spec_test.go",
+    src_rs = "//crates/decision_cores:src/gha_lifecycle.rs",
     tla = "//specs:gha-lifecycle/decision/Decision.tla",
 )
 
@@ -68,6 +73,7 @@ decision_core(
     pkg = "loggroupsspec",
     src_go = "//pkg/logparse/loggroupsspec:spec.go",
     src_test = "//pkg/logparse/loggroupsspec:spec_test.go",
+    src_rs = "//crates/decision_cores:src/log_groups.rs",
     tla = "//specs:log-groups/decision/Decision.tla",
 )
 
@@ -78,6 +84,7 @@ decision_core(
     pkg = "spantreespec",
     src_go = "//pkg/analyzer/spantreespec:spec.go",
     src_test = "//pkg/analyzer/spantreespec:spec_test.go",
+    src_rs = "//crates/decision_cores:src/span_tree.rs",
     tla = "//specs:span-tree/decision/Decision.tla",
 )
 
@@ -92,6 +99,13 @@ test_suite(
         ":gha_lifecycle_up_to_date",
         ":log_groups_up_to_date",
         ":span_tree_up_to_date",
+        ":tui_reload_rs_up_to_date",
+        ":rate_limit_rs_up_to_date",
+        ":timing_clamp_rs_up_to_date",
+        ":sync_bounds_rs_up_to_date",
+        ":gha_lifecycle_rs_up_to_date",
+        ":log_groups_rs_up_to_date",
+        ":span_tree_rs_up_to_date",
     ],
     visibility = ["//visibility:public"],
 )
diff --git a/tools/decision/defs.bzl b/tools/decision/defs.bzl
index 800dc32..f3fe6a7 100644
--- a/tools/decision/defs.bzl
+++ b/tools/decision/defs.bzl
@@ -1,4 +1,4 @@
-"""Decision-core codegen rules: Decision.tla → pkg/.../*spec via //tools/specgen."""
+"""Decision-core codegen rules: Decision.tla → Go *spec + optional Rust via //tools/specgen."""
 
 def decision_core(
         name,
@@ -7,43 +7,51 @@ def decision_core(
         pkg,
         consts,
         src_go,
-        src_test):
-    """Declare genrule + up_to_date test for one decision core.
+        src_test,
+        src_rs = None):
+    """Declare genrule + up_to_date tests for one decision core.
 
     Args:
       name: Bazel-safe name (underscores), e.g. "timing_clamp".
       tla: Label of Decision.tla.
-      dest: Source-tree package path (for docs only).
-      pkg: Go package name for -p.
+      dest: Source-tree Go package path (for docs / update.sh).
+      pkg: Go package / Rust module hint for -p.
       consts: List of "Name=Value" for -const flags.
-      src_go / src_test: Labels of committed generated sources.
+      src_go / src_test: Labels of committed generated Go sources.
+      src_rs: Optional label of committed Rust lib (crates/.../src/<mod>.rs).
     """
     _ = dest  # reserved for update.sh mapping docs
 
     const_flags = " ".join(["-const " + c for c in consts])
     gen_name = name + "_gen"
 
+    outs = [
+        name + "_gen/spec.go",
+        name + "_gen/spec_test.go",
+        name + "_gen/spec.rs",
+    ]
+
     native.genrule(
         name = gen_name,
         srcs = [tla],
-        outs = [
-            name + "_gen/spec.go",
-            name + "_gen/spec_test.go",
-        ],
+        outs = outs,
         cmd = """
 set -euo pipefail
-# Relative out dir so headers stay path-stable; then rewrite Regenerate line
-# to the Bazel update target (canonical for this repo).
 tmpdir=codegen_tmp_{name}
 mkdir -p "$$tmpdir"
+# Go (production ote path)
 $(location //tools/specgen) {consts} -o "$$tmpdir" -p {pkg} $(location {tla})
 for f in "$$tmpdir/spec.go" "$$tmpdir/spec_test.go"; do
-  # portable sed: rewrite regenerate instruction to the Bazel entrypoint
   sed -e 's|^// Regenerate:.*|// Regenerate: bazel run //tools/decision:update|' "$$f" > "$$f.sed"
   mv "$$f.sed" "$$f"
 done
+# Rust peer (same Decision.tla SSOT)
+$(location //tools/specgen) -lang rust {consts} -o "$$tmpdir" -p {pkg} $(location {tla})
+sed -e 's|^// Regenerate:.*|// Regenerate: bazel run //tools/decision:update|' "$$tmpdir/spec.rs" > "$$tmpdir/spec.rs.sed"
+mv "$$tmpdir/spec.rs.sed" "$$tmpdir/spec.rs"
 cp "$$tmpdir/spec.go" $(location {name}_gen/spec.go)
 cp "$$tmpdir/spec_test.go" $(location {name}_gen/spec_test.go)
+cp "$$tmpdir/spec.rs" $(location {name}_gen/spec.rs)
 rm -rf "$$tmpdir"
 """.format(
             consts = const_flags,
@@ -52,13 +60,12 @@ rm -rf "$$tmpdir"
             name = name,
         ),
         tools = ["//tools/specgen"],
-        # Public so go_library in pkg/.../*spec can use outs as srcs
-        # (complete graph: Decision.tla → genrule → go_library → ote).
         visibility = ["//visibility:public"],
     )
 
     gen_go = ":" + name + "_gen/spec.go"
     gen_test = ":" + name + "_gen/spec_test.go"
+    gen_rs = ":" + name + "_gen/spec.rs"
     native.sh_test(
         name = name + "_up_to_date",
         srcs = ["diff_gen.sh"],
@@ -77,3 +84,16 @@ rm -rf "$$tmpdir"
         size = "small",
         tags = ["decision"],
     )
+
+    if src_rs != None:
+        native.sh_test(
+            name = name + "_rs_up_to_date",
+            srcs = ["diff_rs.sh"],
+            args = [
+                "$(location {gen_rs})".format(gen_rs = gen_rs),
+                "$(location {src_rs})".format(src_rs = src_rs),
+            ],
+            data = [gen_rs, src_rs],
+            size = "small",
+            tags = ["decision", "rust"],
+        )
diff --git a/tools/decision/diff_rs.sh b/tools/decision/diff_rs.sh
new file mode 100755
index 0000000..722ff6f
--- /dev/null
+++ b/tools/decision/diff_rs.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+# Compare generated Rust decision module to the committed crate source.
+# Args: <gen_spec.rs> <committed.rs>
+set -euo pipefail
+gen="$1"
+src="$2"
+if ! diff -u "$src" "$gen"; then
+  echo "Rust decision core stale: $src" >&2
+  echo "Run: bazel run //tools/decision:update" >&2
+  exit 1
+fi
diff --git a/tools/decision/update.sh b/tools/decision/update.sh
index 3d4ca94..463ed8b 100755
--- a/tools/decision/update.sh
+++ b/tools/decision/update.sh
@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-# Copy Bazel-generated decision cores into the source tree.
+# Copy Bazel-generated decision cores into the source tree (Go + Rust).
 # Usage: bazel run //tools/decision:update
 set -euo pipefail
 
@@ -9,48 +9,62 @@ if [ -z "${BUILD_WORKSPACE_DIRECTORY:-}" ]; then
 fi
 
 ROOT="$BUILD_WORKSPACE_DIRECTORY"
-# Runfiles: each genrule produces <name>_gen/spec.go under tools/decision/
-# When executed via bazel run, data files are in RUNFILES_DIR.
 RF="${RUNFILES_DIR:-}/_main"
 if [ ! -d "$RF" ]; then
-  # Fallback for older layouts
   RF="${BASH_SOURCE[0]}.runfiles/_main"
 fi
 
-copy_one() {
-  local name="$1" dest="$2"
+find_gendir() {
+  local name="$1"
   local gendir="$RF/tools/decision/${name}_gen"
-  if [ ! -f "$gendir/spec.go" ]; then
-    # Try rlocation-style path used by rules_shell / bash runfiles
-    gendir="$RF/otel-explorer/tools/decision/${name}_gen"
+  if [ -f "$gendir/spec.go" ]; then
+    echo "$gendir"
+    return 0
+  fi
+  gendir="$RF/otel-explorer/tools/decision/${name}_gen"
+  if [ -f "$gendir/spec.go" ]; then
+    echo "$gendir"
+    return 0
   fi
-  if [ ! -f "$gendir/spec.go" ]; then
-    # Direct path from runfiles manifest discovery
-    local found
-    found=$(find "${RUNFILES_DIR:-/nonexistent}" -path "*/${name}_gen/spec.go" 2>/dev/null | head -1 || true)
-    if [ -n "$found" ]; then
-      gendir=$(dirname "$found")
-    fi
+  local found
+  found=$(find "${RUNFILES_DIR:-/nonexistent}" -path "*/${name}_gen/spec.go" 2>/dev/null | head -1 || true)
+  if [ -n "$found" ]; then
+    dirname "$found"
+    return 0
   fi
-  if [ ! -f "$gendir/spec.go" ] || [ ! -f "$gendir/spec_test.go" ]; then
-    echo "error: missing generated files for $name (looked in $gendir)" >&2
+  return 1
+}
+
+copy_one() {
+  local name="$1" dest="$2" rs_dest="$3"
+  local gendir
+  gendir=$(find_gendir "$name") || {
+    echo "error: missing generated files for $name" >&2
     echo "RUNFILES_DIR=${RUNFILES_DIR:-}" >&2
     find "${RUNFILES_DIR:-/tmp}" -name 'spec.go' 2>/dev/null | head -20 >&2 || true
     exit 1
+  }
+  if [ ! -f "$gendir/spec.go" ] || [ ! -f "$gendir/spec_test.go" ] || [ ! -f "$gendir/spec.rs" ]; then
+    echo "error: incomplete gen for $name in $gendir" >&2
+    ls -la "$gendir" >&2 || true
+    exit 1
   fi
   mkdir -p "$ROOT/$dest"
   cp "$gendir/spec.go" "$ROOT/$dest/spec.go"
   cp "$gendir/spec_test.go" "$ROOT/$dest/spec_test.go"
-  echo "updated $dest"
+  mkdir -p "$(dirname "$ROOT/$rs_dest")"
+  # Crate module: strip crate-level test module noise is fine; keep full gen.
+  cp "$gendir/spec.rs" "$ROOT/$rs_dest"
+  echo "updated $dest + $rs_dest"
 }
 
-# Keep in sync with tools/decision/BUILD.bazel CORES.
-copy_one tui_reload pkg/tui/results/tuireloadspec
-copy_one rate_limit pkg/githubapi/ratelimitspec
-copy_one timing_clamp pkg/analyzer/timingclampspec
-copy_one sync_bounds pkg/store/syncboundsspec
-copy_one gha_lifecycle pkg/analyzer/ghalifecyclespec
-copy_one log_groups pkg/logparse/loggroupsspec
-copy_one span_tree pkg/analyzer/spantreespec
+# Go dest | Rust module path under crates/decision_cores
+copy_one tui_reload pkg/tui/results/tuireloadspec crates/decision_cores/src/tui_reload.rs
+copy_one rate_limit pkg/githubapi/ratelimitspec crates/decision_cores/src/rate_limit.rs
+copy_one timing_clamp pkg/analyzer/timingclampspec crates/decision_cores/src/timing_clamp.rs
+copy_one sync_bounds pkg/store/syncboundsspec crates/decision_cores/src/sync_bounds.rs
+copy_one gha_lifecycle pkg/analyzer/ghalifecyclespec crates/decision_cores/src/gha_lifecycle.rs
+copy_one log_groups pkg/logparse/loggroupsspec crates/decision_cores/src/log_groups.rs
+copy_one span_tree pkg/analyzer/spantreespec crates/decision_cores/src/span_tree.rs
 
 echo "done. Review diffs and commit."
diff --git a/tools/specgen/BUILD.bazel b/tools/specgen/BUILD.bazel
index 458e60f..499d763 100644
--- a/tools/specgen/BUILD.bazel
+++ b/tools/specgen/BUILD.bazel
@@ -13,6 +13,7 @@ go_library(
     name = "specgen_lib",
     srcs = [
         "codegen.go",
+        "codegen_rust.go",
         "main.go",
         "tla_alias.go",
     ],
diff --git a/tools/specgen/codegen_rust.go b/tools/specgen/codegen_rust.go
new file mode 100644
index 0000000..9d8ff80
--- /dev/null
+++ b/tools/specgen/codegen_rust.go
@@ -0,0 +1,508 @@
+package main
+
+import (
+	"fmt"
+	"strings"
+	"unicode"
+
+	"github.com/stefanpenner/otel-explorer/tools/specgen/tla"
+)
+
+// GenerateRust produces an idiomatic Rust decision module for PATH A
+// (named scalar actions only). Go remains the default language.
+//
+// Rust shape (not a Go transliteration):
+//   - snake_case methods (can_open / open)
+//   - Copy+Clone when all fields are Copy; else Clone
+//   - consuming self for transitions (ownership = new state)
+//   - pure predicates as &self methods + PURE_PREDICATES registry
+//
+// Unsupported (clear error via supportsRust): PATH B/C, maps/sets, non-scalars.
+func (cg *CodeGen) supportsRust() error {
+	if cg.Dispatch != nil {
+		return fmt.Errorf("rust: Step-dispatch specs (PATH B) not supported yet; use -lang go or a named-action decision core")
+	}
+	if cg.isParamLib() {
+		return fmt.Errorf("rust: parameterised actions (PATH C) not supported yet; use -lang go")
+	}
+	if len(cg.Actions) == 0 {
+		return fmt.Errorf("rust: no named actions to generate")
+	}
+	for _, v := range cg.Spec.Variables {
+		t := cg.inferType(v)
+		switch t {
+		case "bool", "int64", "string":
+			// ok
+		default:
+			return fmt.Errorf("rust: variable %q has type %s (only bool, i64, String for now)", v, t)
+		}
+	}
+	return nil
+}
+
+// GenerateRust returns the full Rust source for spec.rs.
+func (cg *CodeGen) GenerateRust() string {
+	var b strings.Builder
+	cg.writeRustHeader(&b)
+	cg.writeRustState(&b)
+	cg.writeRustImpl(&b)
+	cg.writeRustPurePredicates(&b)
+	cg.writeRustTests(&b)
+	return b.String()
+}
+
+func (cg *CodeGen) writeRustHeader(b *strings.Builder) {
+	fmt.Fprintf(b, "// Code generated by specgen from %s — DO NOT EDIT.\n", stablePath(cg.SpecPath))
+	b.WriteString("//\n")
+	fmt.Fprintf(b, "// Source:     %s\n", stablePath(cg.SpecPath))
+	fmt.Fprintf(b, "// Regenerate: %s\n", cg.regenCommandRust())
+	b.WriteString("//\n")
+	b.WriteString("// Edit the .tla, not this file. Language: Rust (PATH A decision core).\n")
+	b.WriteString("// Package/module hint: ")
+	b.WriteString(cg.pkgName())
+	b.WriteString("\n\n")
+}
+
+func (cg *CodeGen) regenCommandRust() string {
+	parts := []string{"specgen", "-lang", "rust"}
+	for _, c := range cg.ConstFlags {
+		parts = append(parts, "-const", c)
+	}
+	if cg.OutputDir != "" {
+		parts = append(parts, "-o", stablePath(cg.OutputDir))
+	}
+	if cg.PackageName != "" {
+		parts = append(parts, "-p", cg.PackageName)
+	}
+	source := cg.SpecPath
+	if source == "" {
+		source = cg.Spec.Name + ".tla"
+	}
+	parts = append(parts, stablePath(source))
+	return strings.Join(parts, " ")
+}
+
+func (cg *CodeGen) rustAllCopy() bool {
+	for _, v := range cg.Spec.Variables {
+		if cg.inferType(v) == "string" {
+			return false
+		}
+	}
+	return true
+}
+
+func (cg *CodeGen) writeRustState(b *strings.Builder) {
+	if cg.rustAllCopy() {
+		b.WriteString("#[derive(Copy, Clone, Debug, Default, PartialEq, Eq)]\n")
+	} else {
+		b.WriteString("#[derive(Clone, Debug, Default, PartialEq, Eq)]\n")
+	}
+	b.WriteString("pub struct State {\n")
+	for _, v := range cg.Spec.Variables {
+		fmt.Fprintf(b, "\tpub %s: %s,\n", rustField(v), rustType(cg.inferType(v)))
+	}
+	b.WriteString("}\n\n")
+}
+
+func (cg *CodeGen) writeRustImpl(b *strings.Builder) {
+	b.WriteString("impl State {\n")
+	// init
+	b.WriteString("\t/// Initial state from the TLA+ Init predicate.\n")
+	b.WriteString("\tpub fn init() -> Self {\n")
+	b.WriteString("\t\tSelf {\n")
+	initBody := cg.Spec.FindDef("Init")
+	for _, v := range cg.Spec.Variables {
+		val := findInitVal(v, initBody)
+		fmt.Fprintf(b, "\t\t\t%s: %s,\n", rustField(v), cg.litToRust(val))
+	}
+	b.WriteString("\t\t}\n")
+	b.WriteString("\t}\n\n")
+
+	// actions
+	for _, act := range cg.Actions {
+		can := rustCanMethod(act.Name)
+		do := rustMethod(act.Name)
+		fmt.Fprintf(b, "\t/// Guard for action %s.\n", act.Name)
+		fmt.Fprintf(b, "\tpub fn %s(&self) -> bool {\n", can)
+		fmt.Fprintf(b, "\t\t%s\n", rustReturnExpr(cg.exprToRust(act.Guard, "self", false)))
+		b.WriteString("\t}\n\n")
+
+		fmt.Fprintf(b, "\t/// Apply action %s (consuming self — pure transition).\n", act.Name)
+		fmt.Fprintf(b, "\tpub fn %s(self) -> Self {\n", do)
+		// simultaneous assign: build from pre (only if read)
+		touched := map[string]bool{}
+		var fields strings.Builder
+		for _, u := range act.Update {
+			if isSelfAssign(u) {
+				continue
+			}
+			touched[u.Var] = true
+			fmt.Fprintf(&fields, "\t\t\t%s: %s,\n", rustField(u.Var), cg.exprToRust(u.Val, "pre", true))
+		}
+		for _, v := range cg.Spec.Variables {
+			if touched[v] {
+				continue
+			}
+			fmt.Fprintf(&fields, "\t\t\t%s: pre.%s,\n", rustField(v), rustField(v))
+		}
+		body := fields.String()
+		if strings.Contains(body, "pre.") {
+			b.WriteString("\t\tlet pre = self;\n")
+		} else {
+			// no field reads — drop unused self without warning
+			b.WriteString("\t\tlet _ = self;\n")
+		}
+		b.WriteString("\t\tSelf {\n")
+		b.WriteString(body)
+		b.WriteString("\t\t}\n")
+		b.WriteString("\t}\n\n")
+	}
+
+	// enabled_actions
+	b.WriteString("\t/// Names of actions whose guards hold.\n")
+	b.WriteString("\tpub fn enabled_actions(&self) -> Vec<&'static str> {\n")
+	b.WriteString("\t\tlet mut out = Vec::new();\n")
+	for _, act := range cg.Actions {
+		fmt.Fprintf(b, "\t\tif self.%s() {\n", rustCanMethod(act.Name))
+		fmt.Fprintf(b, "\t\t\tout.push(%q);\n", act.Name)
+		b.WriteString("\t\t}\n")
+	}
+	b.WriteString("\t\tout\n")
+	b.WriteString("\t}\n\n")
+
+	// apply_action — peer of Go ApplyAction; name is TLA action id.
+	b.WriteString("\t/// Apply a named action if its guard holds.\n")
+	b.WriteString("\tpub fn apply_action(self, name: &str) -> Option<Self> {\n")
+	b.WriteString("\t\tmatch name {\n")
+	for _, act := range cg.Actions {
+		fmt.Fprintf(b, "\t\t\t%q => {\n", act.Name)
+		fmt.Fprintf(b, "\t\t\t\tif self.%s() {\n", rustCanMethod(act.Name))
+		fmt.Fprintf(b, "\t\t\t\t\tSome(self.%s())\n", rustMethod(act.Name))
+		b.WriteString("\t\t\t\t} else {\n")
+		b.WriteString("\t\t\t\t\tNone\n")
+		b.WriteString("\t\t\t\t}\n")
+		b.WriteString("\t\t\t}\n")
+	}
+	b.WriteString("\t\t\t_ => None,\n")
+	b.WriteString("\t\t}\n")
+	b.WriteString("\t}\n")
+	b.WriteString("}\n\n")
+}
+
+func (cg *CodeGen) writeRustPurePredicates(b *strings.Builder) {
+	preds := cg.purePredicatesRust()
+	if len(preds) == 0 {
+		return
+	}
+	b.WriteString("impl State {\n")
+	for _, p := range preds {
+		fmt.Fprintf(b, "\t/// Pure TLA+ operator %s.\n", p.name)
+		fmt.Fprintf(b, "\tpub fn %s(&self) -> bool {\n", rustMethod(p.name))
+		fmt.Fprintf(b, "\t\t%s\n", rustReturnExpr(p.expr))
+		b.WriteString("\t}\n\n")
+	}
+	b.WriteString("}\n\n")
+
+	// Registry: name + method for dual enumeration (idiomatic const table).
+	b.WriteString("/// Named pure predicates for dual/CI enumeration.\n")
+	b.WriteString("pub struct PurePredicate {\n")
+	b.WriteString("\tpub name: &'static str,\n")
+	b.WriteString("\tpub check: fn(&State) -> bool,\n")
+	b.WriteString("}\n\n")
+	b.WriteString("/// Every pure operator emitted for this module.\n")
+	b.WriteString("pub const PURE_PREDICATES: &[PurePredicate] = &[\n")
+	for _, p := range preds {
+		fmt.Fprintf(b, "\tPurePredicate { name: %q, check: State::%s },\n", p.name, rustMethod(p.name))
+	}
+	b.WriteString("];\n\n")
+}
+
+type rustPure struct {
+	name string
+	expr string
+}
+
+func (cg *CodeGen) purePredicatesRust() []rustPure {
+	var out []rustPure
+	actionNames := map[string]bool{}
+	for _, a := range cg.Actions {
+		actionNames[a.Name] = true
+	}
+	reserved := map[string]bool{
+		"Init": true, "Next": true, "Spec": true, "TypeOK": true, "TypeOk": true, "vars": true,
+	}
+	for _, d := range cg.Spec.Defs {
+		if reserved[d.Name] || actionNames[d.Name] || len(d.Params) > 0 {
+			continue
+		}
+		// Match Go purePredicates: Bait* is TLC-only (must FAIL), not dual SSOT.
+		if strings.HasPrefix(d.Name, "Bait") {
+			continue
+		}
+		if cg.Spec.Recursive != nil && cg.Spec.Recursive[d.Name] {
+			continue
+		}
+		if d.Body == nil || tla.HasPrimed(d.Body) {
+			continue
+		}
+		inlined, err := tla.Inline(cg.Spec, d.Body)
+		if err != nil {
+			continue
+		}
+		expr := cg.exprToRust(inlined, "self", false)
+		if expr == "" || strings.Contains(expr, "/* unsupported") {
+			continue
+		}
+		out = append(out, rustPure{name: d.Name, expr: expr})
+	}
+	return out
+}
+
+func (cg *CodeGen) writeRustTests(b *strings.Builder) {
+	b.WriteString("#[cfg(test)]\n")
+	b.WriteString("mod tests {\n")
+	b.WriteString("\tuse super::*;\n\n")
+	b.WriteString("\t#[test]\n")
+	b.WriteString("\tfn init_ok() {\n")
+	b.WriteString("\t\tlet s = State::init();\n")
+	b.WriteString("\t\tlet _ = s.enabled_actions();\n")
+	b.WriteString("\t}\n\n")
+	b.WriteString("\t#[test]\n")
+	b.WriteString("\tfn pure_predicates_no_panic() {\n")
+	preds := cg.purePredicatesRust()
+	if len(preds) == 0 {
+		b.WriteString("\t\t// no pure predicates\n")
+	} else {
+		b.WriteString("\t\tlet s = State::init();\n")
+		b.WriteString("\t\tassert_eq!(PURE_PREDICATES.len(), ")
+		fmt.Fprintf(b, "%d);\n", len(preds))
+		b.WriteString("\t\tfor p in PURE_PREDICATES {\n")
+		b.WriteString("\t\t\tlet _ = (p.check)(&s);\n")
+		b.WriteString("\t\t}\n")
+	}
+	b.WriteString("\t}\n")
+	b.WriteString("}\n")
+}
+
+func rustType(goType string) string {
+	switch goType {
+	case "bool":
+		return "bool"
+	case "int64":
+		return "i64"
+	case "string":
+		return "String"
+	default:
+		return "()"
+	}
+}
+
+// rustField maps a TLA variable to a snake_case field name.
+func rustField(name string) string { return toSnake(name) }
+
+// rustMethod maps TurnOn / Inv_DepthNonNeg → turn_on / inv_depth_non_neg.
+func rustMethod(name string) string { return toSnake(name) }
+
+func rustCanMethod(action string) string { return "can_" + toSnake(action) }
+
+// toSnake maps TLA/Go-ish names to snake_case without shredding acronyms:
+// TurnOn → turn_on, haveAPI → have_api, Inv_DepthNonNeg → inv_depth_non_neg.
+func toSnake(s string) string {
+	if s == "" {
+		return s
+	}
+	runes := []rune(s)
+	var b strings.Builder
+	for i, r := range runes {
+		if r == '_' {
+			if b.Len() > 0 {
+				out := b.String()
+				if !strings.HasSuffix(out, "_") {
+					b.WriteByte('_')
+				}
+			}
+			continue
+		}
+		if unicode.IsUpper(r) {
+			if i > 0 {
+				prev := runes[i-1]
+				nextLower := i+1 < len(runes) && unicode.IsLower(runes[i+1])
+				// lower→Upper or acronym boundary UpperUpperLower
+				if prev != '_' && (unicode.IsLower(prev) || unicode.IsDigit(prev) ||
+					(unicode.IsUpper(prev) && nextLower)) {
+					b.WriteByte('_')
+				}
+			}
+			b.WriteRune(unicode.ToLower(r))
+			continue
+		}
+		b.WriteRune(r)
+	}
+	return b.String()
+}
+
+// rustReturnExpr drops one layer of redundant outer parens for block returns
+// (avoids rustc unused_parens warnings while keeping nested ops parenthesized).
+func rustReturnExpr(s string) string {
+	s = strings.TrimSpace(s)
+	if len(s) < 2 || s[0] != '(' || s[len(s)-1] != ')' {
+		return s
+	}
+	depth := 0
+	for i := 0; i < len(s); i++ {
+		switch s[i] {
+		case '(':
+			depth++
+		case ')':
+			depth--
+			if depth == 0 && i != len(s)-1 {
+				return s // outer pair doesn't wrap the whole expr
+			}
+		}
+	}
+	if depth == 0 {
+		return strings.TrimSpace(s[1 : len(s)-1])
+	}
+	return s
+}
+
+// litToRust renders Init-time literals (and simple bound consts).
+func (cg *CodeGen) litToRust(e tla.Expr) string {
+	switch v := e.(type) {
+	case tla.BoolLit:
+		if v.Val {
+			return "true"
+		}
+		return "false"
+	case tla.IntLit:
+		return fmt.Sprintf("%d", v.Val)
+	case tla.StrLit:
+		return fmt.Sprintf("String::from(%q)", v.Val)
+	case nil:
+		return "Default::default()"
+	default:
+		// fall through to general expr with dummy recv
+		return cg.exprToRust(e, "/*init*/", false)
+	}
+}
+
+// exprToRust lowers a scalar TLA expression. recv is "self" or "pre".
+// asValue: when true, string vars use clone (for owned field construction).
+func (cg *CodeGen) exprToRust(e tla.Expr, recv string, asValue bool) string {
+	switch v := e.(type) {
+	case tla.BoolLit:
+		if v.Val {
+			return "true"
+		}
+		return "false"
+	case tla.IntLit:
+		return fmt.Sprintf("%d", v.Val)
+	case tla.StrLit:
+		if asValue {
+			return fmt.Sprintf("String::from(%q)", v.Val)
+		}
+		return fmt.Sprintf("%q", v.Val)
+	case tla.VarRef:
+		if g, ok := cg.constRust(v.Name); ok {
+			return g
+		}
+		field := rustField(v.Name)
+		ref := recv + "." + field
+		if asValue && cg.inferType(v.Name) == "string" {
+			return ref + ".clone()"
+		}
+		return ref
+	case tla.UnaryOp:
+		if v.Op == "~" {
+			return "!(" + cg.exprToRust(v.Operand, recv, false) + ")"
+		}
+		return "/* unsupported unary " + v.Op + " */ true"
+	case tla.BinOp:
+		lhs := cg.exprToRust(v.Lhs, recv, false)
+		rhs := cg.exprToRust(v.Rhs, recv, false)
+		switch v.Op {
+		case "=":
+			return fmt.Sprintf("(%s == %s)", lhs, rhs)
+		case "/=":
+			return fmt.Sprintf("(%s != %s)", lhs, rhs)
+		case "/\\":
+			return fmt.Sprintf("(%s && %s)", lhs, rhs)
+		case "\\/":
+			return fmt.Sprintf("(%s || %s)", lhs, rhs)
+		case "+":
+			return fmt.Sprintf("(%s + %s)", lhs, rhs)
+		case "-":
+			return fmt.Sprintf("(%s - %s)", lhs, rhs)
+		case "*":
+			return fmt.Sprintf("(%s * %s)", lhs, rhs)
+		case ">":
+			return fmt.Sprintf("(%s > %s)", lhs, rhs)
+		case "<":
+			return fmt.Sprintf("(%s < %s)", lhs, rhs)
+		case ">=":
+			return fmt.Sprintf("(%s >= %s)", lhs, rhs)
+		case "<=":
+			return fmt.Sprintf("(%s <= %s)", lhs, rhs)
+		case "=>":
+			return fmt.Sprintf("(!(%s) || (%s))", lhs, rhs)
+		case "\\in":
+			// phase \in {"clamped", "done"} → (phase == "clamped" || phase == "done")
+			if sl, ok := v.Rhs.(tla.SetLit); ok {
+				var parts []string
+				for _, el := range sl.Elems {
+					parts = append(parts, fmt.Sprintf("(%s == %s)", lhs, cg.exprToRust(el, recv, false)))
+				}
+				if len(parts) == 0 {
+					return "false"
+				}
+				return "(" + strings.Join(parts, " || ") + ")"
+			}
+			return fmt.Sprintf("/* unsupported \\in */ true")
+		case "\\notin":
+			if sl, ok := v.Rhs.(tla.SetLit); ok {
+				var parts []string
+				for _, el := range sl.Elems {
+					parts = append(parts, fmt.Sprintf("(%s != %s)", lhs, cg.exprToRust(el, recv, false)))
+				}
+				if len(parts) == 0 {
+					return "true"
+				}
+				return "(" + strings.Join(parts, " && ") + ")"
+			}
+			return fmt.Sprintf("/* unsupported \\notin */ true")
+		default:
+			return fmt.Sprintf("/* unsupported op %s */ true", v.Op)
+		}
+	case tla.IfExpr:
+		// Always parenthesize if-expressions so `if c { a } else { b } + 1`
+		// parses as intended. Cond/then/else drop redundant outer layers.
+		return fmt.Sprintf(
+			"(if %s { %s } else { %s })",
+			rustReturnExpr(cg.exprToRust(v.Cond, recv, false)),
+			rustReturnExpr(cg.exprToRust(v.Then, recv, asValue)),
+			rustReturnExpr(cg.exprToRust(v.Else, recv, asValue)),
+		)
+	default:
+		return "/* unsupported expr */ true"
+	}
+}
+
+func (cg *CodeGen) constRust(name string) (string, bool) {
+	isConst := false
+	for _, c := range cg.Spec.Constants {
+		if c == name {
+			isConst = true
+			break
+		}
+	}
+	if !isConst {
+		return "", false
+	}
+	if cg.Spec.ConstBindings != nil {
+		if bound, ok := cg.Spec.ConstBindings[name]; ok {
+			return cg.exprToRust(bound, "self", false), true
+		}
+	}
+	// Unbound non-set CONSTANT: model value as string (rare in decision cores).
+	return fmt.Sprintf("%q", name), true
+}
diff --git a/tools/specgen/main.go b/tools/specgen/main.go
index edac506..88b0a3f 100644
--- a/tools/specgen/main.go
+++ b/tools/specgen/main.go
@@ -1,4 +1,4 @@
-// specgen — generate a Go decision module from a TLA+ spec.
+// specgen — generate a decision module from a TLA+ spec (Go default; Rust PATH A).
 //
 // The generated module mirrors the spec's state machine as pure functions:
 // State struct, Init(), Can<Action>() guards, <Action>() transitions,
@@ -28,14 +28,15 @@ import (
 	"github.com/stefanpenner/otel-explorer/tools/specgen/tla"
 )
 
-const usage = `specgen — generate a Go decision module from a TLA+ spec
+const usage = `specgen — generate a decision module from a TLA+ spec
 
 Usage:
   specgen [flags] <spec.tla>
 
 Flags:
   -o, --output <dir>    output directory (default: <spec>_gen)
-  -p, --package <name>  Go package name (default: <spec>spec)
+  -p, --package <name>  Go package / Rust module hint (default: <spec>spec)
+  -lang go|rust         target language (default: go; rust = PATH A scalars)
   -const Name=Value     bind a CONSTANT to a literal before codegen
                         (repeatable). TRUE/FALSE -> bool, else an integer
                         if parseable, else a string. A CONSTANT referenced
@@ -67,14 +68,16 @@ func main() {
 	var (
 		outputDir string
 		pkgName   string
+		lang      string
 		help      bool
 		consts    constFlags
 	)
 	fs := flag.NewFlagSet("specgen", flag.ExitOnError)
 	fs.StringVar(&outputDir, "o", "", "output directory")
 	fs.StringVar(&outputDir, "output", "", "output directory")
-	fs.StringVar(&pkgName, "p", "", "Go package name")
-	fs.StringVar(&pkgName, "package", "", "Go package name")
+	fs.StringVar(&pkgName, "p", "", "Go package / Rust module hint")
+	fs.StringVar(&pkgName, "package", "", "Go package / Rust module hint")
+	fs.StringVar(&lang, "lang", "go", "target language: go|rust")
 	fs.Var(&consts, "const", "bind a CONSTANT to a literal (Name=Value, repeatable)")
 	fs.BoolVar(&help, "h", false, "show help")
 	fs.BoolVar(&help, "help", false, "show help")
@@ -95,7 +98,7 @@ func main() {
 	}
 
 	specPath := fs.Arg(0)
-	if err := run(specPath, outputDir, pkgName, bindings, []string(consts)); err != nil {
+	if err := run(specPath, outputDir, pkgName, bindings, []string(consts), lang); err != nil {
 		fmt.Fprintf(os.Stderr, "specgen: %v\n", err)
 		os.Exit(1)
 	}
@@ -153,7 +156,18 @@ func findSkipped(spec *Spec, name string) string {
 	return ""
 }
 
-func run(specPath, outputDir, pkgName string, constBindings map[string]tla.Expr, constFlags []string) error {
+// run generates a decision module. Optional langOpt is "go" (default) or "rust".
+func run(specPath, outputDir, pkgName string, constBindings map[string]tla.Expr, constFlags []string, langOpt ...string) error {
+	lang := "go"
+	if len(langOpt) > 0 && strings.TrimSpace(langOpt[0]) != "" {
+		lang = strings.ToLower(strings.TrimSpace(langOpt[0]))
+	}
+	switch lang {
+	case "go", "rust":
+	default:
+		return fmt.Errorf("-lang %q: want go or rust", lang)
+	}
+
 	src, err := os.ReadFile(specPath)
 	if err != nil {
 		return fmt.Errorf("read %s: %w", specPath, err)
@@ -245,6 +259,18 @@ func run(specPath, outputDir, pkgName string, constBindings map[string]tla.Expr,
 		return fmt.Errorf("create output dir: %w", err)
 	}
 
+	if lang == "rust" {
+		if err := cg.supportsRust(); err != nil {
+			return err
+		}
+		specFile := filepath.Join(outputDir, "spec.rs")
+		if err := os.WriteFile(specFile, []byte(cg.GenerateRust()), 0644); err != nil {
+			return fmt.Errorf("write spec.rs: %w", err)
+		}
+		fmt.Printf("generated %s\n", specFile)
+		return nil
+	}
+
 	specFile := filepath.Join(outputDir, "spec.go")
 	if err := os.WriteFile(specFile, formatOrRaw(cg.Generate()), 0644); err != nil {
 		return fmt.Errorf("write spec.go: %w", err)