feat: begin formal verification pipeline (#49)

Initial experiments in 'formal verification' of authorization tooling. Current state is not to be trusted, but we are not in a security critical situation, so that is fine.
Co-authored-by: Zachery Aaron Shores-Chmielewski <zacheryasc@gmail.com>
Co-committed-by: Zachery Aaron Shores-Chmielewski <zacheryasc@gmail.com>

crates/datastore/Cargo.toml

@@ -3,6 +3,9 @@ name = "swactor-datastore"
 version = "0.1.0"
 edition = "2024"
 
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
+
 [dependencies]
 swactor = { path = "../..", features = ["serde", "transport"] }
 distribution = { path = "../distribution" }
@@ -10,30 +13,36 @@ shared-types = { path = "../shared-types" }
 serde = { version = "1", features = ["derive"] }
 serde_json = "1"
 blake3 = "1"
-tiny_http = "0.12"
+tiny_http = { version = "0.12", optional = true }
 clap = { version = "4", features = ["derive"], optional = true }
 ureq = { version = "2", features = ["json"], optional = true }
 getrandom = { version = "0.2", optional = true }
-dashboard = { path = "../dashboard" }
+ctrlc = { version = "3", optional = true }
-swactor-std = { path = "../std" }
+runtime-dashboard = { path = "../runtime-dashboard", optional = true }
-swactor-streams = { path = "../streams" }
+toml = { version = "0.8", optional = true }
-tokio = { version = "1", features = ["sync", "rt", "time"] }
 
 [dev-dependencies]
 serde_json = "1"
 proptest = "1"
+proptest-state-machine = "0.3"
 tempfile = "3"
+distribution = { path = "../distribution" }
 swactor = { path = "../.." }
-swactor-streams = { path = "../streams" }
 swactor-std = { path = "../std" }
-distribution = { path = "../distribution", features = ["iroh"] }
-tokio = { version = "1", features = ["rt-multi-thread", "macros", "io-util", "time"] }
-iroh = "0.96"
 ureq = { version = "2", features = ["json"] }
+tiny_http = "0.12"
+runtime-dashboard = { path = "../runtime-dashboard" }
+stateright = "0.31"
 
 [features]
+node = ["dep:tiny_http", "dep:clap", "dep:ctrlc", "dep:runtime-dashboard", "dep:toml"]
 cli = ["dep:clap", "dep:ureq", "dep:getrandom"]
 
+[[bin]]
+name = "swactor-store-node"
+path = "src/bin/store_node.rs"
+required-features = ["node"]
+
 [[bin]]
 name = "swactor-store"
 path = "src/bin/store_cli.rs"

crates/datastore/src/auth.rs

@@ -278,6 +278,9 @@ impl AuthzEngine {
         if *requester != self.acl.owner {
             return Err(DeniedReason::NotAuthorized);
         }
+        if key == self.acl.owner {
+            return Ok(()); // Owner has implicit access — no-op
+        }
         self.acl.authorized_keys.insert(key);
         if let Some(name) = label {
             let hex: String = key.0.iter().map(|b| format!("{b:02x}")).collect();

crates/datastore/src/kani_auth.rs

@@ -0,0 +1,381 @@
+//! Kani proof harnesses for AuthzEngine properties.
+//!
+//! Provides a bounded mirror of [`crate::auth::AuthzEngine`] that replaces
+//! hash-based collections with fixed-size arrays and stubs out ed25519
+//! crypto. This makes the logic tractable for Kani's symbolic execution
+//! while preserving identical control-flow branches.
+//!
+//! Properties proven:
+//! - **S1**: `check_node(n) = Allowed` ⟹ `n == owner ∨ n ∈ authorized_keys`
+//! - **S2/S3/S4**: 4-step signed-request check rejects in the correct order
+//! - **S5**: non-owner cannot mutate the ACL
+//! - **S6**: owner access survives any sequence of grant/revoke operations
+//! - **GC**: owner survives GC; expired nonces are freed
+
+use crate::auth::{AuthzResult, DeniedReason};
+
+// ─── Bounded types ──────────────────────────────────────────────────────────
+
+const MAX_KEYS: usize = 3;
+const MAX_NONCES: usize = 2;
+
+/// Narrowed NodeId — 2 bytes (65 536 values) is plenty for proving
+/// control-flow properties. Equality semantics identical to `[u8; 32]`.
+#[derive(Clone, Copy, PartialEq, Eq)]
+struct KaniNodeId([u8; 2]);
+
+/// Bounded mirror of `AuthzEngine`. Array-backed collections replace
+/// `HashSet`/`HashMap` so Kani avoids the SipHash symbolic explosion.
+struct KaniAuthzEngine {
+    owner: KaniNodeId,
+    authorized_keys: [Option<KaniNodeId>; MAX_KEYS],
+    key_count: usize,
+    seen_nonces: [Option<([u8; 2], u64)>; MAX_NONCES],
+    nonce_count: usize,
+    timestamp_window: u64,
+}
+
+impl KaniAuthzEngine {
+    fn new(owner: KaniNodeId) -> Self {
+        Self {
+            owner,
+            authorized_keys: [None; MAX_KEYS],
+            key_count: 0,
+            seen_nonces: [None; MAX_NONCES],
+            nonce_count: 0,
+            timestamp_window: 300,
+        }
+    }
+
+    // ── Bounded-set helpers: authorized_keys ─────────────────────────────
+
+    fn keys_contains(&self, id: &KaniNodeId) -> bool {
+        let mut i = 0;
+        while i < self.key_count {
+            if let Some(k) = self.authorized_keys[i] {
+                if k == *id {
+                    return true;
+                }
+            }
+            i += 1;
+        }
+        false
+    }
+
+    fn keys_insert(&mut self, id: KaniNodeId) {
+        if self.keys_contains(&id) {
+            return;
+        }
+        if self.key_count < MAX_KEYS {
+            self.authorized_keys[self.key_count] = Some(id);
+            self.key_count += 1;
+        }
+    }
+
+    fn keys_remove(&mut self, id: &KaniNodeId) {
+        let mut i = 0;
+        while i < self.key_count {
+            if let Some(k) = self.authorized_keys[i] {
+                if k == *id {
+                    self.authorized_keys[i] = self.authorized_keys[self.key_count - 1];
+                    self.authorized_keys[self.key_count - 1] = None;
+                    self.key_count -= 1;
+                    return;
+                }
+            }
+            i += 1;
+        }
+    }
+
+    // ── Bounded-set helpers: seen_nonces ─────────────────────────────────
+
+    fn nonces_contains(&self, nonce: &[u8; 2]) -> bool {
+        let mut i = 0;
+        while i < self.nonce_count {
+            if let Some((n, _)) = self.seen_nonces[i] {
+                if n == *nonce {
+                    return true;
+                }
+            }
+            i += 1;
+        }
+        false
+    }
+
+    fn nonces_insert(&mut self, nonce: [u8; 2], ts: u64) {
+        if self.nonce_count < MAX_NONCES {
+            self.seen_nonces[self.nonce_count] = Some((nonce, ts));
+            self.nonce_count += 1;
+        }
+    }
+
+    // ── Mirror methods (identical control flow to auth.rs) ───────────────
+
+    /// Mirrors `auth.rs` lines 211-217.
+    fn check_node(&self, node_id: &KaniNodeId) -> AuthzResult {
+        if *node_id == self.owner || self.keys_contains(node_id) {
+            AuthzResult::Allowed
+        } else {
+            AuthzResult::Denied(DeniedReason::NotAuthorized)
+        }
+    }
+
+    /// Mirrors `auth.rs` lines 277-290 (label omitted — irrelevant to auth logic).
+    fn grant(
+        &mut self,
+        requester: &KaniNodeId,
+        key: KaniNodeId,
+    ) -> Result<(), DeniedReason> {
+        if *requester != self.owner {
+            return Err(DeniedReason::NotAuthorized);
+        }
+        if key == self.owner {
+            return Ok(());
+        }
+        self.keys_insert(key);
+        Ok(())
+    }
+
+    /// Mirrors `auth.rs` lines 294-305.
+    fn revoke(
+        &mut self,
+        requester: &KaniNodeId,
+        key: KaniNodeId,
+    ) -> Result<(), DeniedReason> {
+        if *requester != self.owner {
+            return Err(DeniedReason::NotAuthorized);
+        }
+        if key != self.owner {
+            self.keys_remove(&key);
+        }
+        Ok(())
+    }
+
+    /// Mirrors `auth.rs` lines 252-273.
+    /// `sig_valid` replaces the `verify_signed_request` call (crypto stub).
+    fn check_signed_request(
+        &mut self,
+        sig_valid: bool,
+        public_key: &KaniNodeId,
+        timestamp: u64,
+        nonce: [u8; 2],
+        now: u64,
+    ) -> AuthzResult {
+        // 1. Signature
+        if !sig_valid {
+            return AuthzResult::Denied(DeniedReason::InvalidSignature);
+        }
+
+        // 2. Timestamp freshness
+        let diff = if now >= timestamp {
+            now - timestamp
+        } else {
+            timestamp - now
+        };
+        if diff > self.timestamp_window {
+            return AuthzResult::Denied(DeniedReason::RequestExpired);
+        }
+
+        // 3. Nonce uniqueness
+        if self.nonces_contains(&nonce) {
+            return AuthzResult::Denied(DeniedReason::ReplayDetected);
+        }
+        self.nonces_insert(nonce, timestamp);
+
+        // 4. ACL check
+        self.check_node(public_key)
+    }
+
+    /// Mirrors `auth.rs` lines 321-326.
+    fn gc_nonces(&mut self, now: u64) {
+        let mut write = 0;
+        let mut read = 0;
+        while read < self.nonce_count {
+            if let Some((nonce, ts)) = self.seen_nonces[read] {
+                let diff = if now >= ts { now - ts } else { ts - now };
+                if diff <= self.timestamp_window {
+                    self.seen_nonces[write] = Some((nonce, ts));
+                    write += 1;
+                }
+            }
+            read += 1;
+        }
+        let mut clear = write;
+        while clear < self.nonce_count {
+            self.seen_nonces[clear] = None;
+            clear += 1;
+        }
+        self.nonce_count = write;
+    }
+}
+
+// ─── Proof harnesses ────────────────────────────────────────────────────────
+
+/// **S5**: If `requester != owner`, both `grant()` and `revoke()` return
+/// `Err(NotAuthorized)`. No iteration — simplest harness.
+#[kani::proof]
+fn proof_s5_non_owner_cannot_mutate_acl() {
+    let owner = KaniNodeId(kani::any());
+    let requester = KaniNodeId(kani::any());
+    let target = KaniNodeId(kani::any());
+
+    kani::assume(requester != owner);
+
+    let mut engine = KaniAuthzEngine::new(owner);
+
+    assert!(engine.grant(&requester, target) == Err(DeniedReason::NotAuthorized));
+    assert!(engine.revoke(&requester, target) == Err(DeniedReason::NotAuthorized));
+}
+
+/// **S1**: `check_node(n) = Allowed` implies `n == owner` or `n` was granted.
+#[kani::proof]
+#[kani::unwind(5)]
+fn proof_s1_check_node() {
+    let owner = KaniNodeId(kani::any());
+    let mut engine = KaniAuthzEngine::new(owner);
+
+    // Grant 0..MAX_KEYS symbolic keys
+    let num_keys: usize = kani::any();
+    kani::assume(num_keys <= MAX_KEYS);
+
+    let mut granted = [KaniNodeId([0; 2]); MAX_KEYS];
+    let mut i = 0;
+    while i < num_keys {
+        granted[i] = KaniNodeId(kani::any());
+        engine.keys_insert(granted[i]);
+        i += 1;
+    }
+
+    // Query with a symbolic node
+    let query = KaniNodeId(kani::any());
+    let result = engine.check_node(&query);
+
+    if result == AuthzResult::Allowed {
+        let mut is_authorized = query == owner;
+        let mut j = 0;
+        while j < num_keys {
+            if query == granted[j] {
+                is_authorized = true;
+            }
+            j += 1;
+        }
+        assert!(is_authorized);
+    }
+}
+
+/// **S6**: After any sequence of grant/revoke operations (by any requester),
+/// `check_node(owner)` always returns `Allowed`.
+#[kani::proof]
+#[kani::unwind(7)]
+fn proof_s6_owner_irremovable() {
+    let owner = KaniNodeId(kani::any());
+    let mut engine = KaniAuthzEngine::new(owner);
+
+    const MAX_OPS: usize = 5;
+    let mut i = 0;
+    while i < MAX_OPS {
+        let requester = KaniNodeId(kani::any());
+        let target = KaniNodeId(kani::any());
+        let is_grant: bool = kani::any();
+
+        if is_grant {
+            let _ = engine.grant(&requester, target);
+        } else {
+            let _ = engine.revoke(&requester, target);
+        }
+        i += 1;
+    }
+
+    assert!(engine.check_node(&owner) == AuthzResult::Allowed);
+}
+
+/// **S2/S3/S4**: The 4-step signed-request check rejects in strict order.
+/// Each denial reason implies the correct preconditions.
+#[kani::proof]
+#[kani::unwind(4)]
+fn proof_signed_request_4step_ordering() {
+    let owner = KaniNodeId(kani::any());
+    let mut engine = KaniAuthzEngine::new(owner);
+
+    // Optionally grant one key
+    let has_granted: bool = kani::any();
+    let granted_key = KaniNodeId(kani::any());
+    if has_granted {
+        engine.keys_insert(granted_key);
+    }
+
+    // Optionally pre-insert a nonce (to test replay detection)
+    let pre_nonce: bool = kani::any();
+    let nonce: [u8; 2] = kani::any();
+    if pre_nonce {
+        let old_ts: u64 = kani::any();
+        engine.nonces_insert(nonce, old_ts);
+    }
+
+    let sig_valid: bool = kani::any();
+    let public_key = KaniNodeId(kani::any());
+    let timestamp: u64 = kani::any();
+    let now: u64 = kani::any();
+
+    let diff = if now >= timestamp {
+        now - timestamp
+    } else {
+        timestamp - now
+    };
+
+    let result = engine.check_signed_request(sig_valid, &public_key, timestamp, nonce, now);
+
+    match result {
+        AuthzResult::Denied(DeniedReason::InvalidSignature) => {
+            // Step 1 rejected: signature was invalid
+            assert!(!sig_valid);
+        }
+        AuthzResult::Denied(DeniedReason::RequestExpired) => {
+            // Step 2 rejected: sig valid, but timestamp outside window
+            assert!(sig_valid);
+            assert!(diff > 300);
+        }
+        AuthzResult::Denied(DeniedReason::ReplayDetected) => {
+            // Step 3 rejected: sig valid, timestamp fresh, but nonce replayed
+            assert!(sig_valid);
+            assert!(diff <= 300);
+            assert!(pre_nonce);
+        }
+        AuthzResult::Denied(DeniedReason::NotAuthorized) => {
+            // Step 4 rejected: sig valid, timestamp fresh, nonce fresh, not in ACL
+            assert!(sig_valid);
+            assert!(diff <= 300);
+            assert!(public_key != owner);
+        }
+        AuthzResult::Allowed => {
+            // All 4 steps passed
+            assert!(sig_valid);
+            assert!(diff <= 300);
+            assert!(public_key == owner || engine.keys_contains(&public_key));
+        }
+    }
+}
+
+/// **GC correctness**: Owner access survives GC; expired nonces are freed.
+#[kani::proof]
+#[kani::unwind(4)]
+fn proof_gc_preserves_owner_and_frees_expired() {
+    let owner = KaniNodeId(kani::any());
+    let mut engine = KaniAuthzEngine::new(owner);
+
+    let nonce: [u8; 2] = kani::any();
+    let t1: u64 = kani::any();
+    let t2: u64 = kani::any();
+    kani::assume(t2 >= t1);
+
+    engine.nonces_insert(nonce, t1);
+    engine.gc_nonces(t2);
+
+    // Owner always survives GC
+    assert!(engine.check_node(&owner) == AuthzResult::Allowed);
+
+    // Expired nonces must be freed
+    if t2 - t1 > 300 {
+        assert!(!engine.nonces_contains(&nonce));
+    }
+}

crates/datastore/src/lib.rs

@@ -6,14 +6,15 @@ pub mod actors;
 pub mod auth;
 pub mod cli;
 pub mod metrics;
+#[cfg(feature = "node")]
 pub mod api;
+#[cfg(feature = "node")]
 pub mod ui_html;
-pub mod blob_transfer;
+#[cfg(kani)]
-pub mod bridge;
+mod kani_auth;
 
 pub use types::{ChunkRef, ContentHash, DatastoreConfig, ObjectEntry, ObjectManifest};
 pub use messages::{BlobStoreMsg, DatastoreNodeMsg, DatastoreResponse, MetadataMsg, TransferMsg};
 pub use chunking::{chunk_blob, reassemble_blob, verify_integrity, ChunkingError};
 pub use storage::{StorageBackend, FilesystemBackend, InMemoryBackend};
 pub use actors::{BlobStoreActor, DatastoreNode, MetadataActor, TransferActor};
-pub use bridge::{DatastoreGroup, DatastoreGroupConfig, DatastoreAuthConfig};

crates/datastore/tests/auth_state_machine.proptest-regressions

@@ -0,0 +1,7 @@
+# Seeds for failure cases proptest has generated in the past. It is
+# automatically read and these particular cases re-run before any
+# novel cases are generated.
+#
+# It is recommended to check this file in to source control so that
+# everyone who runs the test benefits from these saved cases.
+cc 4dee9ecb00774d64ef2818551c7fe65951fce524197e3f11f193f6939e2272b3 # shrinks to (initial_state, transitions, seen_counter) = (RefAuthModel { owner_idx: 0, authorized: {}, used_nonces: {}, nonce_timestamps: {}, clock: 1000000, last_nonce: None }, [SignedRequest { signer_idx: 0, fresh_timestamp: true, reuse_nonce: false, nonce_bytes: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] }], None)

crates/datastore/tests/auth_state_machine.rs

@@ -0,0 +1,484 @@
+//! Proptest state-machine verification of AuthzEngine.
+//!
+//! Drives the auth engine through random sequences of grant/revoke/check/sign
+//! operations and verifies safety + liveness properties against a reference model.
+//!
+//! Properties verified:
+//!   S1  check_node(n) = Allowed ⟹ n = owner ∨ n ∈ authorized_keys
+//!   S2  Invalid signature → Denied(InvalidSignature)
+//!   S3  Expired timestamp → Denied(RequestExpired)
+//!   S4  Replayed nonce → Denied(ReplayDetected)
+//!   S5  Non-owner cannot mutate ACL
+//!   S6  Owner access irremovable over arbitrary op sequences
+//!   L1  Grant leads to access until revoke
+//!   L2  GC enables nonce reuse after window
+
+use std::collections::{HashMap, HashSet};
+
+use proptest::prelude::*;
+use proptest_state_machine::{prop_state_machine, ReferenceStateMachine, StateMachineTest};
+
+use distribution::crypto::Keypair;
+use swactor_datastore::auth::{
+    sign_request, AccessControlList, AuthzEngine, AuthzResult, DatastoreAction, DeniedReason,
+    SignedRequestPayload,
+};
+
+const NUM_KEYS: usize = 4; // index 0 = owner, 1..3 = clients
+
+// ─── Reference Model ────────────────────────────────────────────────────────
+
+#[derive(Clone, Debug)]
+struct RefAuthModel {
+    owner_idx: usize,
+    authorized: HashSet<usize>,
+    used_nonces: HashSet<[u8; 16]>,
+    /// Maps nonce → timestamp it was recorded at
+    nonce_timestamps: HashMap<[u8; 16], u64>,
+    clock: u64,
+    /// Track the last nonce used per signer for the reuse_nonce transition
+    last_nonce: Option<[u8; 16]>,
+}
+
+// ─── Transitions ────────────────────────────────────────────────────────────
+
+#[derive(Clone, Debug)]
+enum AuthOp {
+    Grant {
+        requester_idx: usize,
+        target_idx: usize,
+    },
+    Revoke {
+        requester_idx: usize,
+        target_idx: usize,
+    },
+    CheckNode {
+        key_idx: usize,
+    },
+    SignedRequest {
+        signer_idx: usize,
+        fresh_timestamp: bool,
+        reuse_nonce: bool,
+        nonce_bytes: [u8; 16],
+    },
+    AdvanceClock {
+        delta: u64,
+    },
+    GcNonces,
+}
+
+// ─── Reference State Machine ────────────────────────────────────────────────
+
+struct AuthModel;
+
+impl ReferenceStateMachine for AuthModel {
+    type State = RefAuthModel;
+    type Transition = AuthOp;
+
+    fn init_state() -> BoxedStrategy<Self::State> {
+        Just(RefAuthModel {
+            owner_idx: 0,
+            authorized: HashSet::new(),
+            used_nonces: HashSet::new(),
+            nonce_timestamps: HashMap::new(),
+            clock: 1_000_000,
+            last_nonce: None,
+        })
+        .boxed()
+    }
+
+    fn transitions(state: &Self::State) -> BoxedStrategy<Self::Transition> {
+        let has_last_nonce = state.last_nonce.is_some();
+
+        prop_oneof![
+            // Grant: any requester, any target
+            3 => (0..NUM_KEYS, 0..NUM_KEYS).prop_map(|(r, t)| AuthOp::Grant {
+                requester_idx: r,
+                target_idx: t,
+            }),
+            // Revoke: any requester, any target
+            3 => (0..NUM_KEYS, 0..NUM_KEYS).prop_map(|(r, t)| AuthOp::Revoke {
+                requester_idx: r,
+                target_idx: t,
+            }),
+            // CheckNode: any key
+            3 => (0..NUM_KEYS).prop_map(|k| AuthOp::CheckNode { key_idx: k }),
+            // SignedRequest: fresh nonce, fresh or stale timestamp
+            5 => (0..NUM_KEYS, any::<bool>(), prop::array::uniform16(any::<u8>()))
+                .prop_map(|(s, fresh, nonce)| AuthOp::SignedRequest {
+                    signer_idx: s,
+                    fresh_timestamp: fresh,
+                    reuse_nonce: false,
+                    nonce_bytes: nonce,
+                }),
+            // SignedRequest: reuse nonce (only when we have one)
+            2 => (0..NUM_KEYS, any::<bool>(), prop::array::uniform16(any::<u8>()))
+                .prop_map(move |(s, fresh, fallback_nonce)| AuthOp::SignedRequest {
+                    signer_idx: s,
+                    fresh_timestamp: fresh,
+                    reuse_nonce: has_last_nonce,
+                    nonce_bytes: fallback_nonce,
+                }),
+            // AdvanceClock: 0..600
+            2 => (0u64..600).prop_map(|d| AuthOp::AdvanceClock { delta: d }),
+            // GcNonces
+            1 => Just(AuthOp::GcNonces),
+        ]
+        .boxed()
+    }
+
+    fn apply(mut state: Self::State, transition: &Self::Transition) -> Self::State {
+        match transition {
+            AuthOp::Grant {
+                requester_idx,
+                target_idx,
+            } => {
+                if *requester_idx == state.owner_idx && *target_idx != state.owner_idx {
+                    state.authorized.insert(*target_idx);
+                }
+                // Non-owner grant or owner self-grant: no change
+            }
+            AuthOp::Revoke {
+                requester_idx,
+                target_idx,
+            } => {
+                if *requester_idx == state.owner_idx && *target_idx != state.owner_idx {
+                    state.authorized.remove(target_idx);
+                }
+            }
+            AuthOp::CheckNode { .. } => {
+                // Read-only — no state change
+            }
+            AuthOp::SignedRequest {
+                fresh_timestamp,
+                reuse_nonce,
+                nonce_bytes,
+                ..
+            } => {
+                let nonce = if *reuse_nonce {
+                    state.last_nonce.unwrap_or(*nonce_bytes)
+                } else {
+                    *nonce_bytes
+                };
+
+                // Model the 4-step verification to determine if nonce gets consumed:
+                // Step 1 (sig): always passes in our model (we use real signing)
+                // Step 2 (timestamp): check freshness
+                let ts = if *fresh_timestamp {
+                    state.clock
+                } else {
+                    state.clock.saturating_sub(400)
+                };
+                let diff = if state.clock >= ts {
+                    state.clock - ts
+                } else {
+                    ts - state.clock
+                };
+                if diff > 300 {
+                    // Expired — nonce NOT consumed (step 2 rejects before step 3)
+                } else if state.used_nonces.contains(&nonce) {
+                    // Replay detected — nonce already in set (step 3 rejects)
+                } else {
+                    // Nonce consumed at step 3 (before ACL check at step 4)
+                    state.used_nonces.insert(nonce);
+                    state.nonce_timestamps.insert(nonce, ts);
+                }
+
+                state.last_nonce = Some(nonce);
+            }
+            AuthOp::AdvanceClock { delta } => {
+                state.clock += delta;
+            }
+            AuthOp::GcNonces => {
+                let window = 300u64;
+                let now = state.clock;
+                state.used_nonces.retain(|nonce| {
+                    if let Some(&ts) = state.nonce_timestamps.get(nonce) {
+                        let diff = if now >= ts { now - ts } else { ts - now };
+                        diff <= window
+                    } else {
+                        false
+                    }
+                });
+                state.nonce_timestamps.retain(|_, ts| {
+                    let diff = if now >= *ts { now - *ts } else { *ts - now };
+                    diff <= window
+                });
+            }
+        }
+        state
+    }
+
+    fn preconditions(_state: &Self::State, _transition: &Self::Transition) -> bool {
+        true
+    }
+}
+
+// ─── System Under Test ──────────────────────────────────────────────────────
+
+struct SutAuth {
+    engine: AuthzEngine,
+    keys: Vec<Keypair>,
+    clock: u64,
+    last_nonce: Option<[u8; 16]>,
+    /// Mirror of the engine's nonce set — used to compute expected results
+    /// before the engine call mutates state. We can't use ref_state because
+    /// proptest-state-machine passes the *post-transition* reference state.
+    known_nonces: HashSet<[u8; 16]>,
+    /// Nonce → timestamp, mirrors engine's seen_nonces for GC
+    nonce_timestamps: HashMap<[u8; 16], u64>,
+    /// Track which key indices are authorized (pre-transition mirror).
+    /// Needed because ref_state.authorized is post-transition for Grant/Revoke.
+    authorized_indices: HashSet<usize>,
+}
+
+struct AuthTest;
+
+impl StateMachineTest for AuthTest {
+    type SystemUnderTest = SutAuth;
+    type Reference = AuthModel;
+
+    fn init_test(_ref_state: &RefAuthModel) -> Self::SystemUnderTest {
+        let keys: Vec<Keypair> = (0..NUM_KEYS).map(|_| Keypair::generate()).collect();
+        let acl = AccessControlList {
+            owner: keys[0].node_id(),
+            authorized_keys: HashSet::new(),
+            key_labels: HashMap::new(),
+        };
+        SutAuth {
+            engine: AuthzEngine::new(acl),
+            keys,
+            clock: 1_000_000,
+            last_nonce: None,
+            known_nonces: HashSet::new(),
+            nonce_timestamps: HashMap::new(),
+            authorized_indices: HashSet::new(),
+        }
+    }
+
+    fn apply(
+        mut sut: Self::SystemUnderTest,
+        _ref_state: &RefAuthModel,
+        transition: AuthOp,
+    ) -> Self::SystemUnderTest {
+        match transition {
+            AuthOp::Grant {
+                requester_idx,
+                target_idx,
+            } => {
+                let owner_idx = 0; // owner is always key index 0
+                let requester = sut.keys[requester_idx].node_id();
+                let target = sut.keys[target_idx].node_id();
+                let result = sut.engine.grant(&requester, target, None);
+
+                // S5: Non-owner cannot mutate ACL
+                if requester_idx != owner_idx {
+                    assert_eq!(
+                        result,
+                        Err(DeniedReason::NotAuthorized),
+                        "S5 violated: non-owner grant succeeded"
+                    );
+                } else {
+                    assert!(result.is_ok(), "Owner grant should succeed");
+                    if target_idx != owner_idx {
+                        sut.authorized_indices.insert(target_idx);
+                    }
+                }
+            }
+            AuthOp::Revoke {
+                requester_idx,
+                target_idx,
+            } => {
+                let owner_idx = 0;
+                let requester = sut.keys[requester_idx].node_id();
+                let target = sut.keys[target_idx].node_id();
+                let result = sut.engine.revoke(&requester, target);
+
+                // S5: Non-owner cannot mutate ACL
+                if requester_idx != owner_idx {
+                    assert_eq!(
+                        result,
+                        Err(DeniedReason::NotAuthorized),
+                        "S5 violated: non-owner revoke succeeded"
+                    );
+                } else {
+                    assert!(result.is_ok(), "Owner revoke should succeed");
+                    if target_idx != owner_idx {
+                        sut.authorized_indices.remove(&target_idx);
+                    }
+                }
+            }
+            AuthOp::CheckNode { key_idx } => {
+                let node = sut.keys[key_idx].node_id();
+                let result = sut.engine.check_node(&node);
+                let expected_allowed =
+                    key_idx == 0 || sut.authorized_indices.contains(&key_idx);
+
+                // S1: check_node matches reference model
+                if expected_allowed {
+                    assert_eq!(
+                        result,
+                        AuthzResult::Allowed,
+                        "S1 violated: key_idx={key_idx} should be allowed"
+                    );
+                } else {
+                    assert_eq!(
+                        result,
+                        AuthzResult::Denied(DeniedReason::NotAuthorized),
+                        "S1 violated: key_idx={key_idx} should be denied"
+                    );
+                }
+            }
+            AuthOp::SignedRequest {
+                signer_idx,
+                fresh_timestamp,
+                reuse_nonce,
+                nonce_bytes,
+            } => {
+                let nonce = if reuse_nonce {
+                    sut.last_nonce.unwrap_or(nonce_bytes)
+                } else {
+                    nonce_bytes
+                };
+
+                let ts = if fresh_timestamp {
+                    sut.clock
+                } else {
+                    sut.clock.saturating_sub(400)
+                };
+
+                // Compute expected result BEFORE the engine call mutates state.
+                // We use sut.known_nonces (pre-transition) instead of ref_state
+                // (post-transition) to avoid the off-by-one on nonce insertion.
+                let diff = if sut.clock >= ts {
+                    sut.clock - ts
+                } else {
+                    ts - sut.clock
+                };
+
+                let is_replay = sut.known_nonces.contains(&nonce);
+                let is_authorized =
+                    signer_idx == 0 || sut.authorized_indices.contains(&signer_idx);
+
+                let expected = if diff > 300 {
+                    // S3: Expired timestamp
+                    AuthzResult::Denied(DeniedReason::RequestExpired)
+                } else if is_replay {
+                    // S4: Replayed nonce
+                    AuthzResult::Denied(DeniedReason::ReplayDetected)
+                } else if is_authorized {
+                    AuthzResult::Allowed
+                } else {
+                    // S1: Not authorized (nonce still consumed at step 3)
+                    AuthzResult::Denied(DeniedReason::NotAuthorized)
+                };
+
+                let payload = SignedRequestPayload {
+                    action: DatastoreAction::List { name_filter: None },
+                    timestamp: ts,
+                    nonce,
+                };
+                let request = sign_request(&sut.keys[signer_idx], payload);
+                let result = sut.engine.check_signed_request(&request, sut.clock);
+
+                assert_eq!(
+                    result, expected,
+                    "SignedRequest mismatch: signer_idx={signer_idx}, fresh_ts={fresh_timestamp}, \
+                     reuse_nonce={reuse_nonce}, diff={diff}"
+                );
+
+                // Update our nonce tracker to mirror what the engine did
+                if diff <= 300 && !is_replay {
+                    sut.known_nonces.insert(nonce);
+                    sut.nonce_timestamps.insert(nonce, ts);
+                }
+
+                sut.last_nonce = Some(nonce);
+            }
+            AuthOp::AdvanceClock { delta } => {
+                sut.clock += delta;
+            }
+            AuthOp::GcNonces => {
+                sut.engine.gc_nonces(sut.clock);
+                // Mirror GC in our nonce tracker
+                let now = sut.clock;
+                sut.known_nonces.retain(|nonce| {
+                    if let Some(&ts) = sut.nonce_timestamps.get(nonce) {
+                        let diff = if now >= ts { now - ts } else { ts - now };
+                        diff <= 300
+                    } else {
+                        false
+                    }
+                });
+                sut.nonce_timestamps.retain(|_, ts| {
+                    let diff = if now >= *ts { now - *ts } else { *ts - now };
+                    diff <= 300
+                });
+            }
+        }
+        sut
+    }
+
+    fn check_invariants(sut: &Self::SystemUnderTest, ref_state: &RefAuthModel) {
+        // S6: Owner access is irremovable — must hold after every transition
+        let owner_id = sut.keys[ref_state.owner_idx].node_id();
+        assert_eq!(
+            sut.engine.check_node(&owner_id),
+            AuthzResult::Allowed,
+            "S6 violated: owner lost access"
+        );
+
+        // S1: Reference model agrees with SUT on every key
+        for idx in 0..NUM_KEYS {
+            let node = sut.keys[idx].node_id();
+            let sut_result = sut.engine.check_node(&node);
+            let ref_allowed =
+                idx == ref_state.owner_idx || ref_state.authorized.contains(&idx);
+            if ref_allowed {
+                assert_eq!(
+                    sut_result,
+                    AuthzResult::Allowed,
+                    "S1 invariant: key_idx={idx} should be allowed"
+                );
+            } else {
+                assert_eq!(
+                    sut_result,
+                    AuthzResult::Denied(DeniedReason::NotAuthorized),
+                    "S1 invariant: key_idx={idx} should be denied"
+                );
+            }
+        }
+
+        // L1: Every granted (non-revoked) key has access
+        for &idx in &ref_state.authorized {
+            let node = sut.keys[idx].node_id();
+            assert_eq!(
+                sut.engine.check_node(&node),
+                AuthzResult::Allowed,
+                "L1 violated: granted key_idx={idx} denied"
+            );
+        }
+
+        // L2 (partial): After GC, nonce count in SUT should match reference model
+        // The reference model tracks which nonces should survive GC.
+        // Full L2 is exercised by the SignedRequest transition postconditions —
+        // a nonce reuse after GC + clock advance should succeed when the
+        // reference model says it's been freed.
+    }
+}
+
+// ─── Launch ─────────────────────────────────────────────────────────────────
+
+prop_state_machine! {
+    #![proptest_config(proptest::test_runner::Config {
+        cases: 512,
+        max_shrink_iters: 1000,
+        .. proptest::test_runner::Config::default()
+    })]
+
+    /// Given random sequences of grant/revoke/check/sign/clock/gc operations,
+    /// the AuthzEngine always agrees with the reference model on authorization
+    /// decisions and maintains all safety and liveness properties.
+    #[test]
+    fn auth_engine_state_machine(sequential 1..100 => AuthTest);
+}

crates/datastore/tests/gateway_model_check.rs

@@ -0,0 +1,455 @@
+//! Stateright model-checking of GatewayActor dispatch logic.
+//!
+//! Verifies property **S7**: `DatastoreNodeMsg` is only ever dispatched when
+//! `AuthzResult::Allowed` is returned for an authorized signer. Uses bounded
+//! model checking to exhaustively explore all message orderings across grants,
+//! revokes, signed requests, signature checks, GC ticks, and clock advances.
+
+use stateright::*;
+
+// ── Bounded constants ────────────────────────────────────────────────────────
+
+const OWNER: u8 = 0;
+const KEY_A: u8 = 1;
+const KEY_B: u8 = 2;
+
+/// Nonce values in the model. Two nonces are enough to expose replay bugs.
+const NONCES: [u8; 2] = [0, 1];
+
+/// Timestamp values actions can carry. Combined with a window of 1,
+/// any `|now - ts| > 1` is "expired".
+const TIMESTAMPS: [u8; 4] = [0, 1, 2, 3];
+
+/// Scaled replay-window (production = 300 s; model window = 1 tick).
+const WINDOW: u8 = 1;
+
+/// All node identities explored by the model.
+const KEYS: [u8; 3] = [OWNER, KEY_A, KEY_B];
+
+// ── Model state ──────────────────────────────────────────────────────────────
+
+/// Minimal abstract state of the GatewayActor's authorization layer.
+///
+/// Sorted `Vec`s (not `HashMap`/`HashSet`) because `State` must be `Hash`.
+#[derive(Clone, Debug, Hash, PartialEq, Eq)]
+struct GatewayState {
+    /// Sorted list of explicitly authorized keys (owner has implicit access).
+    acl: Vec<u8>,
+    /// Sorted `(nonce, timestamp)` pairs currently tracked for replay detection.
+    seen_nonces: Vec<(u8, u8)>,
+    /// Current wall clock (advanced by `AdvanceClock`).
+    now: u8,
+    /// Monotonic violation flag — set true if an unauthorized dispatch occurs.
+    s7_violated: bool,
+    /// True after any dispatch to `datastore_node`.
+    has_dispatched: bool,
+}
+
+// ── Actions ──────────────────────────────────────────────────────────────────
+
+/// Every action the model can take in a single step.
+#[derive(Clone, Debug, Hash, PartialEq, Eq)]
+enum GatewayAction {
+    /// Mirrors `GatewayMsg::HandleSignedRequest` — the only handler that
+    /// dispatches to `datastore_node`.
+    SignedRequest {
+        signer: u8,
+        nonce: u8,
+        timestamp: u8,
+        sig_valid: bool,
+    },
+    /// Mirrors `GatewayMsg::Authorize` — consumes a nonce, sends to `reply_to`.
+    Authorize {
+        signer: u8,
+        nonce: u8,
+        timestamp: u8,
+        sig_valid: bool,
+    },
+    /// Mirrors `GatewayMsg::VerifySignature` — consumes a nonce, no ACL check.
+    VerifySignature {
+        signer: u8,
+        nonce: u8,
+        timestamp: u8,
+        sig_valid: bool,
+    },
+    /// Mirrors `GatewayMsg::Grant`.
+    Grant { requester: u8, target: u8 },
+    /// Mirrors `GatewayMsg::Revoke`.
+    Revoke { requester: u8, target: u8 },
+    /// Mirrors `GatewayMsg::NonceGcTick`.
+    GcTick,
+    /// Advances the model clock by 1 tick.
+    AdvanceClock,
+}
+
+// ── Mirror functions ─────────────────────────────────────────────────────────
+//
+// Each mirrors the production AuthzEngine method with bounded types.
+// The `bool` return means "Allowed" (true) or "Denied" (false).
+
+/// Whether `key` is authorized: owner always is; others need explicit ACL entry.
+/// Mirrors `AuthzEngine::check_node` (auth.rs:211-217).
+fn is_authorized(key: u8, acl: &[u8]) -> bool {
+    key == OWNER || acl.contains(&key)
+}
+
+/// Insert into a sorted Vec if not already present.
+fn sorted_insert<T: Ord>(v: &mut Vec<T>, val: T) {
+    if let Err(pos) = v.binary_search(&val) {
+        v.insert(pos, val);
+    }
+}
+
+/// Remove from a sorted Vec.
+fn sorted_remove<T: Ord>(v: &mut Vec<T>, val: &T) {
+    if let Ok(pos) = v.binary_search(val) {
+        v.remove(pos);
+    }
+}
+
+/// Result of a signed-request check.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+enum CheckResult {
+    Allowed,
+    DeniedBadSig,
+    DeniedExpired,
+    DeniedReplay,
+    DeniedNotAuthorized,
+}
+
+/// Mirrors `AuthzEngine::check_signed_request` (auth.rs:252-273).
+///
+/// Four-step chain: sig → timestamp → nonce → ACL.
+/// Nonce is consumed at step 3 (before ACL), matching production behavior.
+fn check_signed_request_model(
+    state: &mut GatewayState,
+    signer: u8,
+    nonce: u8,
+    timestamp: u8,
+    sig_valid: bool,
+) -> CheckResult {
+    // 1. Signature
+    if !sig_valid {
+        return CheckResult::DeniedBadSig;
+    }
+
+    // 2. Timestamp freshness: |now - ts| <= WINDOW
+    let diff = if state.now >= timestamp {
+        state.now - timestamp
+    } else {
+        timestamp - state.now
+    };
+    if diff > WINDOW {
+        return CheckResult::DeniedExpired;
+    }
+
+    // 3. Nonce uniqueness (consumed before ACL — matches production)
+    let nonce_entry = (nonce, timestamp);
+    if state.seen_nonces.contains(&nonce_entry) {
+        return CheckResult::DeniedReplay;
+    }
+    sorted_insert(&mut state.seen_nonces, nonce_entry);
+
+    // 4. ACL check
+    if is_authorized(signer, &state.acl) {
+        CheckResult::Allowed
+    } else {
+        CheckResult::DeniedNotAuthorized
+    }
+}
+
+/// Mirrors `AuthzEngine::check_signature_only` (auth.rs:223-243).
+///
+/// Steps 1-3 only, no ACL check. Used by `VerifySignature`.
+fn check_signature_only_model(
+    state: &mut GatewayState,
+    nonce: u8,
+    timestamp: u8,
+    sig_valid: bool,
+) -> CheckResult {
+    // 1. Signature
+    if !sig_valid {
+        return CheckResult::DeniedBadSig;
+    }
+
+    // 2. Timestamp freshness
+    let diff = if state.now >= timestamp {
+        state.now - timestamp
+    } else {
+        timestamp - state.now
+    };
+    if diff > WINDOW {
+        return CheckResult::DeniedExpired;
+    }
+
+    // 3. Nonce uniqueness
+    let nonce_entry = (nonce, timestamp);
+    if state.seen_nonces.contains(&nonce_entry) {
+        return CheckResult::DeniedReplay;
+    }
+    sorted_insert(&mut state.seen_nonces, nonce_entry);
+
+    CheckResult::Allowed
+}
+
+/// Mirrors `AuthzEngine::grant` (auth.rs:277-289).
+fn grant_model(state: &mut GatewayState, requester: u8, target: u8) {
+    // Owner guard
+    if requester != OWNER {
+        return;
+    }
+    // Self-grant is a no-op
+    if target == OWNER {
+        return;
+    }
+    sorted_insert(&mut state.acl, target);
+}
+
+/// Mirrors `AuthzEngine::revoke` (auth.rs:294-305).
+fn revoke_model(state: &mut GatewayState, requester: u8, target: u8) {
+    // Owner guard
+    if requester != OWNER {
+        return;
+    }
+    // Owner-revoke is a no-op
+    if target == OWNER {
+        return;
+    }
+    sorted_remove(&mut state.acl, &target);
+}
+
+/// Mirrors `AuthzEngine::gc_nonces` (auth.rs:321-326).
+fn gc_nonces_model(state: &mut GatewayState) {
+    state.seen_nonces.retain(|&(_, ts)| {
+        let diff = if state.now >= ts {
+            state.now - ts
+        } else {
+            ts - state.now
+        };
+        diff <= WINDOW
+    });
+}
+
+// ── Stateright Model ─────────────────────────────────────────────────────────
+
+/// The gateway dispatch model — explores all interleavings of grants, revokes,
+/// signed requests, authorizations, signature checks, GC ticks, and clock
+/// advances over bounded parameters.
+#[derive(Clone)]
+struct GatewayModel;
+
+impl Model for GatewayModel {
+    type State = GatewayState;
+    type Action = GatewayAction;
+
+    fn init_states(&self) -> Vec<Self::State> {
+        vec![GatewayState {
+            acl: Vec::new(),
+            seen_nonces: Vec::new(),
+            now: 0,
+            s7_violated: false,
+            has_dispatched: false,
+        }]
+    }
+
+    fn actions(&self, _state: &Self::State, actions: &mut Vec<Self::Action>) {
+        // SignedRequest: for each (signer, nonce, timestamp, sig_valid)
+        for &signer in &KEYS {
+            for &nonce in &NONCES {
+                for &ts in &TIMESTAMPS {
+                    for &sig_valid in &[true, false] {
+                        actions.push(GatewayAction::SignedRequest {
+                            signer,
+                            nonce,
+                            timestamp: ts,
+                            sig_valid,
+                        });
+                    }
+                }
+            }
+        }
+
+        // Authorize: same parameter space (consumes nonces, shared state)
+        for &signer in &KEYS {
+            for &nonce in &NONCES {
+                for &ts in &TIMESTAMPS {
+                    for &sig_valid in &[true, false] {
+                        actions.push(GatewayAction::Authorize {
+                            signer,
+                            nonce,
+                            timestamp: ts,
+                            sig_valid,
+                        });
+                    }
+                }
+            }
+        }
+
+        // VerifySignature: same parameter space (consumes nonces, no ACL check)
+        for &signer in &KEYS {
+            for &nonce in &NONCES {
+                for &ts in &TIMESTAMPS {
+                    for &sig_valid in &[true, false] {
+                        actions.push(GatewayAction::VerifySignature {
+                            signer,
+                            nonce,
+                            timestamp: ts,
+                            sig_valid,
+                        });
+                    }
+                }
+            }
+        }
+
+        // Grant: for each (requester, target) pair
+        for &requester in &KEYS {
+            for &target in &KEYS {
+                actions.push(GatewayAction::Grant { requester, target });
+            }
+        }
+
+        // Revoke: for each (requester, target) pair
+        for &requester in &KEYS {
+            for &target in &KEYS {
+                actions.push(GatewayAction::Revoke { requester, target });
+            }
+        }
+
+        // GC tick and clock advance
+        actions.push(GatewayAction::GcTick);
+        actions.push(GatewayAction::AdvanceClock);
+    }
+
+    fn next_state(&self, state: &Self::State, action: Self::Action) -> Option<Self::State> {
+        let mut next = state.clone();
+
+        match action {
+            GatewayAction::SignedRequest {
+                signer,
+                nonce,
+                timestamp,
+                sig_valid,
+            } => {
+                let result =
+                    check_signed_request_model(&mut next, signer, nonce, timestamp, sig_valid);
+                if result == CheckResult::Allowed {
+                    // Dual-rail S7 check: independently verify the signer IS authorized
+                    if !is_authorized(signer, &state.acl) {
+                        next.s7_violated = true;
+                    }
+                    next.has_dispatched = true;
+                }
+            }
+
+            GatewayAction::Authorize {
+                signer: _,
+                nonce,
+                timestamp,
+                sig_valid,
+            } => {
+                // Authorize uses check_signed_request (same as HandleSignedRequest),
+                // but sends result to reply_to — never dispatches to datastore_node.
+                let _result =
+                    check_signed_request_model(&mut next, OWNER, nonce, timestamp, sig_valid);
+                // Note: Authorize handler calls check_signed_request with the request's
+                // signer, but for nonce-consumption modeling, the key identity doesn't
+                // matter — only the nonce/timestamp pair is consumed. We use the actual
+                // signer parameter isn't needed for state effects beyond nonce tracking.
+                // The handler sends to reply_to only, never to datastore_node.
+            }
+
+            GatewayAction::VerifySignature {
+                signer: _,
+                nonce,
+                timestamp,
+                sig_valid,
+            } => {
+                // VerifySignature uses check_signature_only — no ACL check.
+                // Sends to reply_to only, never to datastore_node.
+                let _result =
+                    check_signature_only_model(&mut next, nonce, timestamp, sig_valid);
+            }
+
+            GatewayAction::Grant { requester, target } => {
+                grant_model(&mut next, requester, target);
+            }
+
+            GatewayAction::Revoke { requester, target } => {
+                revoke_model(&mut next, requester, target);
+            }
+
+            GatewayAction::GcTick => {
+                gc_nonces_model(&mut next);
+            }
+
+            GatewayAction::AdvanceClock => {
+                // Cap at max timestamp to keep state space bounded
+                if next.now < *TIMESTAMPS.last().unwrap() {
+                    next.now += 1;
+                } else {
+                    return None; // no-op, prune
+                }
+            }
+        }
+
+        // Prune: if state didn't change, no need to explore further
+        if next == *state {
+            return None;
+        }
+
+        Some(next)
+    }
+
+    fn properties(&self) -> Vec<Property<Self>> {
+        vec![
+            // S7: No unauthorized dispatch — the critical safety property.
+            Property::<Self>::always("S7: no unauthorized dispatch", |_, state| {
+                !state.s7_violated
+            }),
+            // S6-gw: Owner is always authorized (never removed from implicit access).
+            Property::<Self>::always("S6-gw: owner always authorized", |_, state| {
+                is_authorized(OWNER, &state.acl)
+            }),
+            // L3: Authorized dispatch is reachable (canary — model isn't vacuously safe).
+            Property::<Self>::sometimes(
+                "L3: authorized dispatch reachable",
+                |_, state| state.has_dispatched && !state.s7_violated,
+            ),
+            // L4: A granted (non-owner) key can dispatch.
+            Property::<Self>::sometimes("L4: granted key can dispatch", |_, state| {
+                !state.acl.is_empty() && state.has_dispatched
+            }),
+            // L5: Nonce reuse after GC is reachable (GC actually enables re-dispatch).
+            Property::<Self>::sometimes(
+                "L5: dispatch with empty nonce table reachable",
+                |_, state| state.has_dispatched && state.seen_nonces.is_empty(),
+            ),
+        ]
+    }
+}
+
+// ── Test ─────────────────────────────────────────────────────────────────────
+
+#[test]
+fn gateway_dispatch_model_check() {
+    let result = GatewayModel
+        .checker()
+        .spawn_dfs()
+        .join();
+
+    // Report summary before asserting, to aid debugging on failure.
+    let unique_states = result.unique_state_count();
+    println!(
+        "Stateright: explored {} unique states, max depth {}",
+        unique_states,
+        result.max_depth(),
+    );
+
+    result.assert_properties();
+
+    // Sanity: the model actually explored a meaningful state space.
+    assert!(
+        unique_states > 100,
+        "Model explored too few states ({unique_states}); check action generation",
+    );
+}

xtask/src/main.rs

@@ -1,6 +1,3 @@
-mod deploy;
-mod sim_cluster;
-
 use std::path::{Path, PathBuf};
 use std::process::Command;
 use std::time::Instant;
@@ -34,7 +31,7 @@ struct Cli {
 enum Cmd {
     /// Run test groups
     Test {
-        /// Test group to run (core, distribution, cluster-sims, integrated, essential, all)
+        /// Test group to run (core, distribution, cluster-sims, integrated, kani, stateright, essential, all)
         group: Option<String>,
 
         /// Show all groups and the cargo commands they run
@@ -42,40 +39,33 @@ enum Cmd {
         list: bool,
     },
 
-    /// Start a local swactor node (full features, no cluster)
+    /// Start a datastore node
     #[command(trailing_var_arg = true)]
     Node {
-        /// Dashboard HTTP port
+        /// Port for the node
         #[arg(long)]
         port: Option<u16>,
 
-        /// Storage path for persistent datastore (omit for in-memory)
+        /// Storage path
         #[arg(long)]
         storage_path: Option<String>,
 
-        /// Build in release mode
+        /// Enable auth (bare --auth → true, --auth=false → false)
-        #[arg(long)]
+        #[arg(long, num_args = 0..=1, default_missing_value = "true")]
-        release: bool,
+        auth: Option<bool>,
 
-        /// Extra arguments forwarded to the swactor binary
+        /// Auth directory
+        #[arg(long)]
+        auth_dir: Option<String>,
+
+        /// Extra arguments forwarded to the underlying binary
         #[arg(allow_hyphen_values = true)]
         extra: Vec<String>,
     },
 
-    /// Build the swactor binary (release, ready to ship)
-    Build,
-
     /// Build the crypto WASM module
     Wasm,
 
-    /// Launch a dev node (distribution + dashboard + datastore)
-    #[command(trailing_var_arg = true)]
-    DevNode {
-        /// Extra arguments forwarded to the dev node
-        #[arg(allow_hyphen_values = true)]
-        extra: Vec<String>,
-    },
-
     /// Run a datastore CLI command
     #[command(trailing_var_arg = true)]
     Cli {
@@ -91,62 +81,26 @@ enum Cmd {
         #[arg(allow_hyphen_values = true)]
         extra: Vec<String>,
     },
-
-    /// Scaffold identity + config for a node role
-    InitNode {
-        /// Role: vps-seed, laptop, home
-        role: String,
-
-        /// Output directory (default: ./<role>)
-        #[arg(long)]
-        dir: Option<String>,
-    },
-
-    /// Generate a peers.json containing public keys from multiple identity dirs
-    GenPeers {
-        /// Identity directories to include
-        dirs: Vec<String>,
-    },
-
-    /// Launch a local sim-cluster (relay + N nodes) for development
-    SimCluster {
-        /// Number of nodes (default: 5)
-        #[arg(long, default_value = "5")]
-        nodes: usize,
-    },
-
-    /// Deploy swactor to remote machines
-    Deploy {
-        /// Deploy via Docker over SSH (build image, push, run containers)
-        #[arg(long)]
-        docker: bool,
-
-        /// Path to deploy config file [default: .deploy/deploy.toml or .deploy/docker.toml]
-        #[arg(long)]
-        config: Option<String>,
-
-        /// Skip Docker image build (use existing archive)
-        #[arg(long)]
-        skip_build: bool,
-
-        /// Skip health check and convergence verification
-        #[arg(long)]
-        skip_verify: bool,
-
-        /// Skip peer introduction (deploy only)
-        #[arg(long)]
-        skip_peers: bool,
-    },
 }
 
 // ── Config file ─────────────────────────────────────────────────────
 
 #[derive(Deserialize, Default)]
 struct Config {
+    #[serde(default)]
+    node: NodeConfig,
     #[serde(default)]
     cli: CliConfig,
 }
 
+#[derive(Deserialize, Default)]
+struct NodeConfig {
+    port: Option<u16>,
+    storage_path: Option<String>,
+    auth: Option<bool>,
+    auth_dir: Option<String>,
+}
+
 #[derive(Deserialize, Default)]
 struct CliConfig {
     url: Option<String>,
@@ -224,16 +178,36 @@ const CLUSTER_SIMS: Group = Group {
     }],
 };
 
+const KANI: Group = Group {
+    name: "kani",
+    description: "Kani formal verification proofs (requires cargo-kani)",
+    steps: &[TestStep {
+        label: "authz engine proofs",
+        args: &["kani", "-p", "swactor-datastore"],
+    }],
+};
+
+const STATERIGHT: Group = Group {
+    name: "stateright",
+    description: "Stateright model checking (gateway dispatch)",
+    steps: &[TestStep {
+        label: "gateway dispatch model check",
+        args: &["test", "-p", "swactor-datastore", "--test", "gateway_model_check"],
+    }],
+};
+
 const INTEGRATED: Group = Group {
     name: "integrated",
     description: "HTTP API + dashboard end-to-end tests",
     steps: &[
         TestStep {
-            label: "datastore integration",
+            label: "datastore integration (node features)",
             args: &[
                 "test",
                 "-p",
                 "swactor-datastore",
+                "--features",
+                "node",
                 "--test",
                 "api_integration_test",
                 "--test",
@@ -241,8 +215,8 @@ const INTEGRATED: Group = Group {
             ],
         },
         TestStep {
-            label: "dashboard",
+            label: "runtime dashboard",
-            args: &["test", "-p", "dashboard"],
+            args: &["test", "-p", "runtime-dashboard"],
         },
     ],
 };
@@ -253,6 +227,8 @@ fn groups_for(name: &str) -> Option<Vec<&'static Group>> {
         "distribution" => Some(vec![&DISTRIBUTION]),
         "cluster-sims" => Some(vec![&CLUSTER_SIMS]),
         "integrated" => Some(vec![&INTEGRATED]),
+        "kani" => Some(vec![&KANI]),
+        "stateright" => Some(vec![&STATERIGHT]),
         "essential" => Some(vec![&CORE, &DISTRIBUTION, &INTEGRATED]),
         "all" => Some(vec![&CORE, &DISTRIBUTION, &CLUSTER_SIMS, &INTEGRATED]),
         _ => None,
@@ -280,31 +256,20 @@ fn run_step(group_name: &str, step: &TestStep) -> bool {
 fn print_usage() {
     println!(
         "\
-USAGE: cargo xtask <COMMAND>
+USAGE: cargo xtask test <GROUP>
 
-COMMANDS:
+GROUPS:
-  test <GROUP>  Run a test group
-  node [OPTS]   Start a local swactor node (full features, no cluster)
-  dev-node [OPTS]  Launch a dev node (legacy)
-  build         Build the swactor binary (release)
-
-TEST GROUPS:
   core          Actor runtime, message delivery, property tests
   distribution  Distribution protocol + datastore
   cluster-sims  Deterministic cluster simulations
   integrated    HTTP API + dashboard end-to-end tests
-  sim-cluster   Multi-process cluster with local iroh relay
+  kani          Kani formal verification proofs (requires cargo-kani)
+  stateright    Stateright model checking (gateway dispatch)
   essential     core + distribution + integrated (merge gate)
   all           Every test group
 
-TEST FLAGS:
+FLAGS:
-  --list        Show all groups and the cargo commands they run
+  --list        Show all groups and the cargo commands they run"
-
-NODE OPTIONS:
-  --port PORT           Dashboard port (default: 9091)
-  --storage-path PATH   Persistent storage dir (omit for in-memory)
-  --release             Build in release mode
-  -- [EXTRA...]         Extra args forwarded to swactor binary"
     );
 }
 
@@ -314,6 +279,8 @@ fn print_list() {
         (&[], &DISTRIBUTION),
         (&[], &CLUSTER_SIMS),
         (&[], &INTEGRATED),
+        (&[], &KANI),
+        (&[], &STATERIGHT),
     ];
 
     println!("Available test groups:\n");
@@ -326,7 +293,6 @@ fn print_list() {
         println!();
     }
 
-    println!("  {:<14}Multi-process cluster with local iroh relay", "sim-cluster");
     println!("  {:<14}core + distribution + integrated (merge gate)", "essential");
     println!("  {:<14}Every test group", "all");
 }
@@ -347,11 +313,6 @@ fn run_test(group: Option<String>, list: bool) {
         }
     };
 
-    if group_name == "sim-cluster" {
-        sim_cluster::run();
-        return;
-    }
-
     let groups = match groups_for(&group_name) {
         Some(g) => g,
         None => {
@@ -388,174 +349,32 @@ fn run_test(group: Option<String>, list: bool) {
     );
 }
 
-// ── Build ────────────────────────────────────────────────────────────────
-
-fn run_build() {
-    println!("Building swactor (release)...\n");
-
-    let status = Command::new("cargo")
-        .args(["build", "--release", "-p", "swactor-node"])
-        .status();
-
-    match status {
-        Ok(s) if s.success() => {
-            let root = workspace_root();
-            let bin = root.join("target/release/swactor");
-            let size = std::fs::metadata(&bin).map(|m| m.len()).unwrap_or(0);
-            println!(
-                "\nDone: {} ({:.1} MB)",
-                bin.display(),
-                size as f64 / 1_048_576.0
-            );
-        }
-        Ok(s) => std::process::exit(s.code().unwrap_or(1)),
-        Err(e) => {
-            eprintln!("Failed to execute cargo: {e}");
-            std::process::exit(1);
-        }
-    }
-}
-
-// ── Dev node launcher ───────────────────────────────────────────────────
-
-fn run_dev(extra_args: Vec<String>) {
-    ignore_sigint();
-    let mut port = "9090".to_string();
-    let mut listen: Option<String> = None;
-    let mut actors = "3".to_string();
-    let mut storage: Option<String> = None;
-    let mut no_datastore = false;
-    let mut use_tcp = false;
-    let mut release = false;
-
-    let mut i = 0;
-    while i < extra_args.len() {
-        match extra_args[i].as_str() {
-            "--port" => {
-                i += 1;
-                port = extra_args.get(i).cloned().unwrap_or_else(|| {
-                    eprintln!("--port requires a value");
-                    std::process::exit(1);
-                });
-            }
-            "--listen" => {
-                i += 1;
-                listen = Some(extra_args.get(i).cloned().unwrap_or_else(|| {
-                    eprintln!("--listen requires a value");
-                    std::process::exit(1);
-                }));
-            }
-            "--actors" => {
-                i += 1;
-                actors = extra_args.get(i).cloned().unwrap_or_else(|| {
-                    eprintln!("--actors requires a value");
-                    std::process::exit(1);
-                });
-            }
-            "--storage" => {
-                i += 1;
-                storage = Some(extra_args.get(i).cloned().unwrap_or_else(|| {
-                    eprintln!("--storage requires a value");
-                    std::process::exit(1);
-                }));
-            }
-            "--no-datastore" => {
-                no_datastore = true;
-            }
-            "--tcp" => {
-                use_tcp = true;
-            }
-            "--release" => {
-                release = true;
-            }
-            other => {
-                eprintln!("Unknown dev-node option: {other}");
-                std::process::exit(1);
-            }
-        }
-        i += 1;
-    }
-
-    if use_tcp && listen.is_none() {
-        listen = Some("127.0.0.1:7000".to_string());
-    }
-
-    let mut cargo_args: Vec<&str> = vec!["run", "-p", "swactor-node", "--bin", "swactor"];
-    if use_tcp {
-        cargo_args.push("--features");
-        cargo_args.push("tcp");
-    }
-    if release {
-        cargo_args.push("--release");
-    }
-    cargo_args.push("--");
-
-    if use_tcp {
-        cargo_args.push("--transport");
-        cargo_args.push("tcp");
-    }
-
-    let listen_ref;
-    if let Some(ref l) = listen {
-        listen_ref = l.as_str();
-        cargo_args.push("--listen");
-        cargo_args.push(listen_ref);
-    }
-
-    cargo_args.push("--dashboard-port");
-    cargo_args.push(&port);
-    cargo_args.push("--actors");
-    cargo_args.push(&actors);
-
-    let storage_ref;
-    if let Some(ref s) = storage {
-        storage_ref = s.as_str();
-        cargo_args.push("--storage-path");
-        cargo_args.push(storage_ref);
-    }
-
-    if no_datastore {
-        cargo_args.push("--no-datastore");
-    }
-
-    println!("    cargo {}", cargo_args.join(" "));
-    println!();
-
-    let status = Command::new("cargo")
-        .args(&cargo_args)
-        .status();
-
-    match status {
-        Ok(s) => {
-            if !s.success() {
-                std::process::exit(s.code().unwrap_or(1));
-            }
-        }
-        Err(e) => {
-            eprintln!("Failed to execute cargo: {e}");
-            std::process::exit(1);
-        }
-    }
-}
-
 fn run_node(
     port: Option<u16>,
     storage_path: Option<String>,
-    release: bool,
+    auth: Option<bool>,
+    auth_dir: Option<String>,
     extra: Vec<String>,
+    cfg: &NodeConfig,
 ) {
     ignore_sigint();
+    let port = port.or(cfg.port).unwrap_or(9091);
+    let storage_path = storage_path
+        .or_else(|| cfg.storage_path.clone())
+        .unwrap_or_else(|| "./datastore".into());
+    let auth_enabled = auth.or(cfg.auth).unwrap_or(true);
+    let auth_dir = auth_dir
+        .or_else(|| cfg.auth_dir.clone())
+        .unwrap_or_else(|| "./auth".into());
 
-    // Build the full swactor binary (same one produced by `cargo xtask build`).
+    // Build first, then run the binary directly (not via `cargo run`).
-    let mut build_args = vec![
+    // This avoids cargo sitting in the middle of the process chain and
-        "build", "-p", "swactor-node",
+    // dying from SIGINT before the node finishes its shutdown.
-    ];
-    if release {
-        build_args.push("--release");
-    }
-
     let build_status = Command::new("cargo")
-        .args(&build_args)
+        .args([
+            "build", "-p", "swactor-datastore", "--features", "node",
+            "--bin", "swactor-store-node",
+        ])
         .status();
     match build_status {
         Ok(s) if !s.success() => std::process::exit(s.code().unwrap_or(1)),
@@ -568,49 +387,26 @@ fn run_node(
 
     // Locate the built binary
     let root = workspace_root();
-    let profile = if release { "release" } else { "debug" };
+    let binary = root.join("target/debug/swactor-store-node");
-    let binary = root.join(format!("target/{profile}/swactor"));
     if !binary.exists() {
         eprintln!("Binary not found at {}", binary.display());
         std::process::exit(1);
     }
 
-    // Use a local working directory so the node doesn't write into ~/.swactor
-    let work_dir = root.join(".dev-node");
-    std::fs::create_dir_all(&work_dir).expect("failed to create .dev-node directory");
-
-    let identity_dir = work_dir.join("identity");
-    let auth_dir = work_dir.join("auth");
-    let default_storage = work_dir.join("datastore");
-    std::fs::create_dir_all(&identity_dir).expect("failed to create identity dir");
-    std::fs::create_dir_all(&auth_dir).expect("failed to create auth dir");
-
-    // Write a minimal config so the swactor binary doesn't auto-create ~/.swactor
-    let config_path = work_dir.join("node.toml");
-    let storage = storage_path.unwrap_or_else(|| default_storage.to_string_lossy().into_owned());
-    let port = port.unwrap_or(9091);
-    let config_content = format!(
-        r#"transport = "iroh"
-dashboard_port = {port}
-storage_path = "{storage}"
-identity_dir = "{identity}"
-auth = true
-auth_dir = "{auth}"
-"#,
-        identity = identity_dir.display(),
-        auth = auth_dir.display(),
-    );
-    std::fs::write(&config_path, &config_content).expect("failed to write dev config");
-
     let mut bin_args: Vec<String> = vec![
-        "--config".into(),
+        "--port".into(),
-        config_path.to_string_lossy().into_owned(),
+        port.to_string(),
+        "--storage-path".into(),
+        storage_path,
     ];
 
-    bin_args.extend(extra);
+    if auth_enabled {
+        bin_args.push("--auth".into());
+        bin_args.push("--auth-dir".into());
+        bin_args.push(auth_dir);
+    }
 
-    println!("    {} {}", binary.display(), bin_args.join(" "));
+    bin_args.extend(extra);
-    println!();
 
     let status = Command::new(&binary).args(&bin_args).status();
     match status {
@@ -694,7 +490,7 @@ fn run_wasm() {
             "build",
             "--target", "wasm32-unknown-unknown",
             "--release",
-            "-p", "wasm-crypto",
+            "-p", "swactor-crypto-wasm",
         ])
         .status();
 
@@ -710,7 +506,7 @@ fn run_wasm() {
         _ => {}
     }
 
-    let src = root.join("target/wasm32-unknown-unknown/release/wasm_crypto.wasm");
+    let src = root.join("target/wasm32-unknown-unknown/release/swactor_crypto_wasm.wasm");
     let dst = root.join("crates/datastore/src/crypto_wasm.wasm");
 
     std::fs::copy(&src, &dst).unwrap_or_else(|e| {
@@ -728,200 +524,6 @@ fn run_wasm() {
     }
 }
 
-// ── Init-node scaffolding ────────────────────────────────────────────────
-
-fn run_init_node(role: &str, dir: Option<&str>) {
-    let base = dir
-        .map(PathBuf::from)
-        .unwrap_or_else(|| PathBuf::from(format!("./{role}")));
-    let identity_dir = base.join("identity");
-    let auth_dir = base.join("auth");
-
-    std::fs::create_dir_all(&identity_dir).expect("failed to create identity dir");
-    std::fs::create_dir_all(&auth_dir).expect("failed to create auth dir");
-
-    // Generate keypair
-    let key_path = identity_dir.join("node.key.json");
-    if key_path.exists() {
-        println!("Identity already exists: {}", key_path.display());
-    } else {
-        // Build and run: cargo run -p swactor-node -- --identity-dir ... --no-datastore
-        // Simpler: generate inline using the same JSON format
-        let secret = generate_random_bytes_32();
-        let public = ed25519_public_from_secret(&secret);
-        let json = serde_json::json!({
-            "version": 1,
-            "secret_key": hex_encode_bytes(&secret),
-            "public_key": hex_encode_bytes(&public),
-            "created_at": "generated-by-xtask",
-        });
-        std::fs::write(
-            &key_path,
-            serde_json::to_string_pretty(&json).unwrap(),
-        )
-        .expect("failed to write key file");
-        println!("Generated keypair: {}", key_path.display());
-        println!("  Node ID: {}", hex_encode_bytes(&public));
-    }
-
-    // Generate config TOML
-    let config_path = base.join("node.toml");
-    let (storage_prefix, id_prefix, auth_prefix) = match role {
-        "vps-seed" => (
-            "/var/lib/swactor/datastore",
-            "/var/lib/swactor/identity",
-            "/var/lib/swactor/auth",
-        ),
-        _ => (
-            "./swactor-data/datastore",
-            "./swactor-data/identity",
-            "./swactor-data/auth",
-        ),
-    };
-
-    let toml_content = format!(
-        r#"transport = "iroh"
-dashboard_port = 9090
-storage_path = "{storage_prefix}"
-identity_dir = "{id_prefix}"
-auth = true
-auth_dir = "{auth_prefix}"
-"#,
-    );
-    std::fs::write(&config_path, &toml_content).expect("failed to write config");
-    println!("Config: {}", config_path.display());
-
-    // Create empty peers.json
-    let peers_path = base.join("peers.json");
-    if !peers_path.exists() {
-        let peers = serde_json::json!({
-            "version": 1,
-            "peers": [],
-        });
-        std::fs::write(
-            &peers_path,
-            serde_json::to_string_pretty(&peers).unwrap(),
-        )
-        .expect("failed to write peers.json");
-        println!("Peers: {}", peers_path.display());
-    }
-
-    println!("\nDone. To start: swactor --config {}", config_path.display());
-}
-
-fn run_gen_peers(dirs: &[String]) {
-    if dirs.is_empty() {
-        eprintln!("Usage: cargo xtask gen-peers <dir1> <dir2> ...");
-        std::process::exit(1);
-    }
-
-    let mut peers = Vec::new();
-
-    for dir in dirs {
-        let key_path = Path::new(dir).join("identity/node.key.json");
-        if !key_path.exists() {
-            // Try dir/node.key.json as well
-            let alt = Path::new(dir).join("node.key.json");
-            if alt.exists() {
-                let data = std::fs::read_to_string(&alt).expect("failed to read key file");
-                let json: serde_json::Value =
-                    serde_json::from_str(&data).expect("invalid key file");
-                let pub_hex = json
-                    .get("public_key")
-                    .and_then(|v| v.as_str())
-                    .expect("missing public_key");
-                let label = Path::new(dir)
-                    .file_name()
-                    .map(|s| s.to_string_lossy().to_string())
-                    .unwrap_or_default();
-                peers.push(serde_json::json!({
-                    "node_id": pub_hex,
-                    "label": label,
-                }));
-                continue;
-            }
-            eprintln!("No key file found in {dir}");
-            std::process::exit(1);
-        }
-
-        let data = std::fs::read_to_string(&key_path).expect("failed to read key file");
-        let json: serde_json::Value = serde_json::from_str(&data).expect("invalid key file");
-        let pub_hex = json
-            .get("public_key")
-            .and_then(|v| v.as_str())
-            .expect("missing public_key");
-        let label = Path::new(dir)
-            .file_name()
-            .map(|s| s.to_string_lossy().to_string())
-            .unwrap_or_default();
-        peers.push(serde_json::json!({
-            "node_id": pub_hex,
-            "label": label,
-        }));
-    }
-
-    let peers_json = serde_json::json!({
-        "version": 1,
-        "peers": peers,
-    });
-    let content = serde_json::to_string_pretty(&peers_json).unwrap();
-
-    // Write to each dir
-    for dir in dirs {
-        let out = Path::new(dir).join("peers.json");
-        std::fs::write(&out, &content).unwrap_or_else(|e| {
-            eprintln!("Failed to write {}: {e}", out.display());
-        });
-        println!("Wrote {}", out.display());
-    }
-
-    println!(
-        "\nGenerated peers.json with {} peer(s)",
-        peers.len()
-    );
-}
-
-// Simple helpers to avoid depending on distribution crate from xtask
-fn generate_random_bytes_32() -> [u8; 32] {
-    use std::time::{SystemTime, UNIX_EPOCH};
-    let mut bytes = [0u8; 32];
-    let nanos = SystemTime::now()
-        .duration_since(UNIX_EPOCH)
-        .unwrap()
-        .as_nanos();
-    for (i, b) in nanos.to_le_bytes().iter().enumerate() {
-        bytes[i % 32] ^= *b;
-    }
-    let pid = std::process::id();
-    for (i, b) in pid.to_le_bytes().iter().enumerate() {
-        bytes[(i + 8) % 32] ^= *b;
-    }
-    // XOR with a counter to add more entropy per invocation
-    let addr = &bytes as *const _ as usize;
-    for (i, b) in addr.to_le_bytes().iter().enumerate() {
-        bytes[(i + 16) % 32] ^= *b;
-    }
-    bytes
-}
-
-fn ed25519_public_from_secret(secret: &[u8; 32]) -> [u8; 32] {
-    // ed25519-dalek: SigningKey::from_bytes → verifying_key().to_bytes()
-    // We can't easily use the crate from xtask without adding the dep,
-    // so we generate a random 32-byte "public key" placeholder.
-    // The actual keypair should be generated by swactor-node --identity-dir on first start.
-    // For xtask init-node, we just create a placeholder that gets replaced on first real start.
-    let mut pub_bytes = [0u8; 32];
-    // Hash the secret with a simple mix to get a deterministic but non-crypto placeholder
-    for i in 0..32 {
-        pub_bytes[i] = secret[i].wrapping_mul(37).wrapping_add(secret[(i + 1) % 32]);
-    }
-    pub_bytes
-}
-
-fn hex_encode_bytes(bytes: &[u8]) -> String {
-    bytes.iter().map(|b| format!("{b:02x}")).collect()
-}
-
 fn main() {
     let cli = Cli::parse();
     let root = workspace_root();
@@ -929,32 +531,18 @@ fn main() {
 
     match cli.command {
         Cmd::Test { group, list } => run_test(group, list),
-        Cmd::Build => run_build(),
         Cmd::Wasm => run_wasm(),
         Cmd::Node {
             port,
             storage_path,
-            release,
+            auth,
+            auth_dir,
             extra,
-        } => run_node(port, storage_path, release, extra),
+        } => run_node(port, storage_path, auth, auth_dir, extra, &config.node),
-        Cmd::DevNode { extra } => run_dev(extra),
         Cmd::Cli {
             url,
             key,
             extra,
         } => run_cli(url, key, extra, &config.cli),
-        Cmd::InitNode { role, dir } => run_init_node(&role, dir.as_deref()),
-        Cmd::GenPeers { dirs } => run_gen_peers(&dirs),
-        Cmd::SimCluster { nodes } => sim_cluster::run_interactive(nodes),
-        Cmd::Deploy { docker, config, skip_build, skip_verify, skip_peers } => {
-            let config = config.unwrap_or_else(|| {
-                if docker { ".deploy/docker.toml" } else { ".deploy/deploy.toml" }.into()
-            });
-            if docker {
-                deploy::run_deploy(&root, &config, skip_build, skip_verify, skip_peers);
-            } else {
-                deploy::run_native_deploy(&root, &config, skip_build, skip_verify, skip_peers);
-            }
-        }
     }
 }