diff --git a/docs/miniscript-reference/README.md b/docs/miniscript-reference/README.md
new file mode 100644
index 0000000..f1a5d53
--- /dev/null
+++ b/docs/miniscript-reference/README.md
@@ -0,0 +1,43 @@
+> [!WARNING]
+> **BITME-ONLY REFERENCE MATERIAL:** The policies and flows shown in this file (e.g., exactly one immediate path, server-side hold/veto) belong to Bitme, NOT Keeper.
+> Keeper's actual wallet policy (including Miniscript inheritance paths) and server constraints differ. Any future implementation or tests for Keeper must use the actual Keeper Miniscript policy.
+
+# Miniscript Coordinator Pattern — Reference Implementation
+
+This directory contains reference material for the coordinator-side Miniscript approach, adapted from [TDH-Labs/Bitme](https://github.com/TDH-Labs/Bitme).
+
+## The Pattern
+
+Hardware wallets that don't natively understand Miniscript (Satochip, TAPSIGNER, Jade, Coldcard) can still participate in Miniscript wallets:
+
+1. **Coordinator** (wallet app) parses the Miniscript descriptor
+2. **Coordinator** determines which spending path applies
+3. **Coordinator** constructs the PSBT with the correct `witness_script` for that path
+4. **Hardware** signs the sighash digest (just a hash — no policy understanding needed)
+5. **Coordinator** collects signatures and finalizes
+
+The hardware never needs to understand the policy. It just signs what the coordinator gives it.
+
+## Files
+
+- **`invariants-reference.rs`**: Formal Miniscript invariant tests using rust-miniscript's `entails` algorithm. Proves:
+  - No single key can spend alone
+  - Intended signer combinations can spend (immediately or after timelock)
+  - Timelock boundaries hold exactly (not one block early)
+  
+  Adapted from Bitme's `bitme-cosigner/src/invariants.rs`. Hardware references generalized from Satochip-specific to generic "hardware".
+
+- **`descriptor-reference.rs`**: Miniscript descriptor construction with BIP389 multipath. Shows the pattern of building descriptors from labeled keys.
+  
+  Adapted from Bitme's `bitme-cosigner/src/descriptor.rs`. Note: Bitme's specific policy (Hardware+Server as the HOT path) is NOT Keeper's policy — Keeper uses 2-of-3 Mobile + Hardware + Server as the base. This is the *construction pattern*, not the *policy*.
+
+- **`coordinator-pattern.md`**: Excerpt explaining the coordinator flow — how the hardware and server never communicate directly, with the wallet app carrying the PSBT between them.
+
+## What's Next
+
+These are Rust references. For TypeScript implementation in SigningServer, we need to decide:
+1. Which JS/TS Miniscript library to use
+2. Where the TypeScript port should live (`src/miniscript/` vs `src/wallet/`)
+3. Whether invariant tests run in CI or serve as reference
+
+See the PR description for discussion.
diff --git a/docs/miniscript-reference/coordinator-pattern.md b/docs/miniscript-reference/coordinator-pattern.md
new file mode 100644
index 0000000..2ea3c59
--- /dev/null
+++ b/docs/miniscript-reference/coordinator-pattern.md
@@ -0,0 +1,55 @@
+> [!WARNING]
+> **BITME-ONLY REFERENCE MATERIAL:** The policies and flows shown in this file (e.g., exactly one immediate path, server-side hold/veto) belong to Bitme, NOT Keeper.
+> Keeper's actual wallet policy (including Miniscript inheritance paths) and server constraints differ. Any future implementation or tests for Keeper must use the actual Keeper Miniscript policy.
+
+
+## How a spend actually works
+
+**The Hardware never talks to the server. It has no networking - no WiFi, no Bluetooth, nothing
+that reaches the internet.** It only ever talks to whatever taps it: your phone over NFC, or a
+card reader plugged into a computer. Every "HARDWARE + SERVER" spend is really two separate,
+disconnected steps stitched together by a PSBT file that your wallet app carries between them -
+never a live connection between the card and this service.
+
+The server never signs the moment you ask, either way. It queues, it tells you, it waits, and
+only then does it sign - so a signature is never the first you hear about a transaction.
+
+```mermaid
+sequenceDiagram
+    participant SC as Your Hardware
+    participant You as Your wallet app
+    participant CS as Cosigner
+    participant Node as Your bitcoind
+    participant N as Notification
+
+    Note over SC,You: Tap to phone / card reader - purely local, no network
+    SC->>You: Partial signature (HARDWARE's share)
+    You->>CS: POST /sign_psbt (HARDWARE's signature already attached)
+    CS->>Node: Are these coins real? Whose are they?
+    Node-->>CS: UTXO details
+    Note over CS: Re-derives every address itself.<br/>Never trusts what the PSBT claims.
+    CS->>CS: Check against policy
+    alt Over your limits
+        CS-->>You: 422 denied — nothing queued, nothing signed
+    else Allowed
+        CS->>N: "Pending spend: 50,000 sat to bc1q… — signs in 15 min"
+        CS-->>You: 202 Accepted + id
+        Note over CS: Holding. You can POST /veto/{id}
+        alt You veto
+            CS->>CS: Cancelled permanently
+        else Hold elapses
+            CS->>CS: Re-check policy against live state
+            CS->>CS: Add the SERVER signature
+            CS-->>You: PSBT with both signatures — 2 of 3, spendable
+        end
+    end
+    Note over You: You broadcast. The server never does.<br/>Notice the Hardware only ever appears in the top line.
+```
+
+The cosigner never talks to the Hardware either — as far as this service is concerned, "HARDWARE
+signed" just means *a PSBT arrived with a valid signature under HARDWARE's key already in it*. It
+has no way to reach the card, ask it to sign, or know it exists except through that signature.
+Your wallet app (Bitcoin Keeper, or Sparrow with a card reader) is the only thing that talks to
+both sides — locally to the Hardware, over the network to the cosigner — and a PSBT file is the
+only thing that ever crosses between them.
+
diff --git a/docs/miniscript-reference/descriptor-reference.rs b/docs/miniscript-reference/descriptor-reference.rs
new file mode 100644
index 0000000..48132f9
--- /dev/null
+++ b/docs/miniscript-reference/descriptor-reference.rs
@@ -0,0 +1,433 @@
+/*
+ * BITME-ONLY REFERENCE MATERIAL
+ * The policies and flows shown in this file (e.g., exactly one immediate path, server-side hold/veto) belong to Bitme, NOT Keeper.
+ * Keeper's actual wallet policy (including Miniscript inheritance paths) and server constraints differ.
+ * Any future implementation or tests for Keeper must use the actual Keeper Miniscript policy.
+ */
+
+//! Constructs and parses the wallet's miniscript descriptor.
+//!
+//! Policy: **any two of the three keys can spend, but any spend involving the MOBILE key waits
+//! `N` blocks.**
+//!
+//!   wsh(thresh(2,pk(HARDWARE),s:pk(SERVER),snj:and_v(v:pk(MOBILE),older(N))))
+//!
+//! Which gives exactly three spending combinations:
+//!
+//!   - HARDWARE + SERVER, immediately - the "HOT" path, and the only one this service
+//!     co-signs on demand, subject to the policy engine.
+//!   - HARDWARE + MOBILE, after `N` blocks - recovery when *this service* is gone.
+//!   - MOBILE + SERVER, after `N` blocks - recovery when the *HARDWARE* is gone.
+//!
+//! That third combination is the reason for this shape. An earlier revision made HARDWARE
+//! mandatory in both branches
+//! (`and_v(v:pk(HARDWARE),or_d(pk(SERVER),and_v(v:pk(MOBILE),older(N))))`), which meant losing
+//! the HARDWARE seed lost the funds outright - a single point of catastrophic failure with no
+//! recourse. Every single-device loss is now survivable, which is the property Bitkey's 2-of-3
+//! has and that one lacked.
+//!
+//! The timelock on the MOBILE branch is what keeps this service meaningful: the *only* way to
+//! spend without waiting `N` blocks is HARDWARE + SERVER, so the policy engine cannot be
+//! side-stepped for day-to-day spending. And unlike Bitkey - whose "Delay & Notify" waiting
+//! period is enforced by their server and therefore evaporates if that server is compromised or
+//! shut down - this delay is a consensus rule. It holds even if this service is rooted, seized,
+//! or deleted.
+
+use std::str::FromStr;
+
+use anyhow::{bail, Context, Result};
+use bitcoin::Address;
+use miniscript::descriptor::{DefiniteDescriptorKey, DescriptorType};
+use miniscript::{Descriptor, DescriptorPublicKey, ForEachKey, ToPublicKey};
+
+use crate::config::{ChainNetwork, KeySpec, WalletConfig};
+
+/// A fully constructed wallet descriptor, split into its receive (external) and change
+/// (internal) halves per BIP389 multipath convention `<0;1>`.
+#[derive(Debug, Clone)]
+pub struct BuiltDescriptor {
+    /// The single descriptor string containing both paths via `<0;1>`, as configured.
+    pub multipath: Descriptor<DescriptorPublicKey>,
+    /// Receive addresses (multipath index 0).
+    pub external: Descriptor<DescriptorPublicKey>,
+    /// Change addresses (multipath index 1).
+    pub internal: Descriptor<DescriptorPublicKey>,
+    pub timelock_blocks: u16,
+}
+
+fn key_expr(key: &KeySpec) -> Result<String> {
+    let fp = key.master_fingerprint.trim().to_lowercase();
+    let path = bitcoin::bip32::DerivationPath::from_str(key.derivation_path.trim())
+        .context("invalid derivation path")?;
+    let xpub = key.xpub.trim();
+    if path.is_empty() {
+        Ok(format!("[{fp}]{xpub}/<0;1>/*"))
+    } else {
+        Ok(format!("[{fp}/{path}]{xpub}/<0;1>/*"))
+    }
+}
+
+/// Builds the raw descriptor string
+/// `wsh(thresh(2,pk(A),s:pk(B),snj:and_v(v:pk(C),older(N))))` from three already-formatted key
+/// expressions. Shared by the production builder and by tests, so the policy shape used in
+/// tests can never drift from the one actually deployed.
+///
+/// The `s:`/`snj:` wrappers are miniscript type-system coercions (`thresh` needs every branch
+/// to leave a 0-or-1 on the stack); this exact form is what rust-miniscript's own policy
+/// compiler emits for `thresh(2,pk(A),pk(B),and(pk(C),older(N)))`, kept literal here so the
+/// deployed script is deterministic rather than dependent on a compiler's cost heuristics.
+pub fn policy_string(
+    hardware_expr: &str,
+    server_expr: &str,
+    mobile_expr: &str,
+    timelock_blocks: u16,
+) -> String {
+    format!(
+        "wsh(thresh(2,pk({hardware_expr}),s:pk({server_expr}),snj:and_v(v:pk({mobile_expr}),older({timelock_blocks}))))"
+    )
+}
+
+pub fn build_descriptor(cfg: &WalletConfig) -> Result<BuiltDescriptor> {
+    cfg.validate()?;
+
+    let hardware_expr = key_expr(&cfg.keys.hardware).context("keys.hardware")?;
+    let server_expr = key_expr(&cfg.keys.server).context("keys.server")?;
+    let mobile_expr = key_expr(&cfg.keys.mobile).context("keys.mobile")?;
+
+    let desc_str = policy_string(
+        &hardware_expr,
+        &server_expr,
+        &mobile_expr,
+        cfg.timelock_blocks,
+    );
+
+    let multipath = Descriptor::<DescriptorPublicKey>::from_str(&desc_str)
+        .with_context(|| format!("parsing generated descriptor: {desc_str}"))?;
+
+    if multipath.desc_type() != DescriptorType::Wsh {
+        bail!(
+            "expected a wsh() descriptor, got {:?}",
+            multipath.desc_type()
+        );
+    }
+    multipath
+        .sanity_check()
+        .context("generated descriptor failed miniscript sanity check")?;
+
+    let mut singles = multipath
+        .clone()
+        .into_single_descriptors()
+        .context("splitting multipath descriptor into external/internal")?;
+    if singles.len() != 2 {
+        bail!(
+            "expected exactly 2 derivation paths (external, internal) from <0;1>, got {}",
+            singles.len()
+        );
+    }
+    let internal = singles.pop().unwrap();
+    let external = singles.pop().unwrap();
+    external
+        .sanity_check()
+        .context("external descriptor failed sanity check")?;
+    internal
+        .sanity_check()
+        .context("internal descriptor failed sanity check")?;
+
+    Ok(BuiltDescriptor {
+        multipath,
+        external,
+        internal,
+        timelock_blocks: cfg.timelock_blocks,
+    })
+}
+
+/// Derives the address at `index` for a single-path (non-multipath) descriptor.
+pub fn address_at(
+    desc: &Descriptor<DescriptorPublicKey>,
+    index: u32,
+    network: ChainNetwork,
+) -> Result<Address> {
+    let definite = desc
+        .at_derivation_index(index)
+        .with_context(|| format!("deriving index {index}"))?;
+    definite
+        .address(network.to_bitcoin_network())
+        .with_context(|| format!("computing address at index {index}"))
+}
+
+/// Resolves a single-path descriptor to its fully concrete (non-wildcard) form at `index`,
+/// for invariant analysis and satisfaction.
+pub fn at_index(
+    desc: &Descriptor<DescriptorPublicKey>,
+    index: u32,
+) -> Result<Descriptor<DefiniteDescriptorKey>> {
+    desc.at_derivation_index(index)
+        .with_context(|| format!("deriving index {index}"))
+}
+
+/// Which chain (receive/external or change/internal) a derived scriptPubkey was found on.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum Chain {
+    External,
+    Internal,
+}
+
+/// Where in the wallet a scriptPubkey was found, from [`find_owner`].
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub struct Owned {
+    pub chain: Chain,
+    pub index: u32,
+}
+
+/// Searches `desc` at indices `0..gap_limit` for one whose scriptPubkey equals `target`.
+///
+/// This is the only trustworthy way to answer "is this scriptPubkey ours": PSBT metadata
+/// (bip32_derivation, the "this is change" convention some wallets use) is supplied by
+/// whoever built the PSBT and must never be taken on faith - see `inspect.rs`.
+fn find_on_chain(
+    desc: &Descriptor<DescriptorPublicKey>,
+    target: &bitcoin::ScriptBuf,
+    gap_limit: u32,
+) -> Result<Option<u32>> {
+    for index in 0..gap_limit {
+        let definite = at_index(desc, index)?;
+        if &definite.script_pubkey() == target {
+            return Ok(Some(index));
+        }
+    }
+    Ok(None)
+}
+
+/// Searches both the external and internal chains of `wallet` for `target`, up to
+/// `gap_limit` indices on each. Checks external first: an address a caller is *spending
+/// from* is at least as likely to be a receive address as a change one, and either way both
+/// chains resolve to the same policy, so the order only affects which `Chain` gets reported
+/// when (pathologically) both happened to match.
+pub fn find_owner(
+    wallet: &BuiltDescriptor,
+    target: &bitcoin::ScriptBuf,
+    gap_limit: u32,
+) -> Result<Option<Owned>> {
+    if let Some(index) = find_on_chain(&wallet.external, target, gap_limit)? {
+        return Ok(Some(Owned {
+            chain: Chain::External,
+            index,
+        }));
+    }
+    if let Some(index) = find_on_chain(&wallet.internal, target, gap_limit)? {
+        return Ok(Some(Owned {
+            chain: Chain::Internal,
+            index,
+        }));
+    }
+    Ok(None)
+}
+
+/// Every key in a fully-derived (non-wildcard) descriptor, paired with its own key
+/// expression string - used to pick a specific role's key back out by matching against the
+/// xpub that role was configured with (the only stable identifier we have for "which key is
+/// HARDWARE" once everything's been derived down to raw public keys).
+pub fn definite_keys(
+    desc: &Descriptor<DefiniteDescriptorKey>,
+) -> Vec<(String, DefiniteDescriptorKey)> {
+    let mut found = Vec::new();
+    desc.for_each_key(|k| {
+        found.push((k.to_string(), k.clone()));
+        true
+    });
+    found
+}
+
+/// Picks the key belonging to `xpub` out of `keys` (as produced by [`definite_keys`]).
+pub fn find_role_key(
+    keys: &[(String, DefiniteDescriptorKey)],
+    xpub: &str,
+) -> Result<DefiniteDescriptorKey> {
+    let xpub = xpub.trim();
+    keys.iter()
+        .find(|(s, _)| s.contains(xpub))
+        .map(|(_, k)| k.clone())
+        .with_context(|| format!("key for xpub {xpub} not found in descriptor"))
+}
+
+/// The three role keys (as concrete, spendable public keys - not descriptor key
+/// expressions) at one derivation index, for matching against a PSBT's `partial_sigs`.
+pub struct RoleKeys {
+    pub hardware: bitcoin::PublicKey,
+    pub server: bitcoin::PublicKey,
+    pub mobile: bitcoin::PublicKey,
+}
+
+pub fn role_keys_at(
+    wallet: &BuiltDescriptor,
+    cfg: &WalletConfig,
+    chain: Chain,
+    index: u32,
+) -> Result<RoleKeys> {
+    let desc = match chain {
+        Chain::External => &wallet.external,
+        Chain::Internal => &wallet.internal,
+    };
+    let definite = at_index(desc, index)?;
+    let keys = definite_keys(&definite);
+    Ok(RoleKeys {
+        hardware: find_role_key(&keys, &cfg.keys.hardware.xpub)?.to_public_key(),
+        server: find_role_key(&keys, &cfg.keys.server.xpub)?.to_public_key(),
+        mobile: find_role_key(&keys, &cfg.keys.mobile.xpub)?.to_public_key(),
+    })
+}
+
+/// Parses a standalone descriptor string (e.g. loaded from a file, or produced by another
+/// tool) for `descriptor check`. Does not require key role information.
+///
+/// If the descriptor is a `<0;1>` multipath descriptor, returns its external (index 0) half -
+/// `at_derivation_index` cannot resolve a multipath key on its own, and the invariant analysis
+/// depends only on the miniscript's key/timelock structure, which is identical on both paths.
+pub fn parse_descriptor(s: &str) -> Result<Descriptor<DescriptorPublicKey>> {
+    let desc = Descriptor::<DescriptorPublicKey>::from_str(s.trim())
+        .with_context(|| "parsing descriptor")?;
+    desc.sanity_check()
+        .context("descriptor failed miniscript sanity check")?;
+
+    if desc.is_multipath() {
+        let mut singles = desc
+            .into_single_descriptors()
+            .context("splitting multipath descriptor")?;
+        if singles.is_empty() {
+            bail!("multipath descriptor split into zero single-path descriptors");
+        }
+        let external = singles.remove(0);
+        external
+            .sanity_check()
+            .context("external descriptor failed sanity check")?;
+        Ok(external)
+    } else {
+        Ok(desc)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::test_util::test_wallet_config;
+
+    #[test]
+    fn builds_expected_wsh_shape() {
+        let cfg = test_wallet_config(12960);
+        let built = build_descriptor(&cfg).expect("should build");
+
+        assert_eq!(built.multipath.desc_type(), DescriptorType::Wsh);
+        let s = built.multipath.to_string();
+        assert!(s.starts_with("wsh(thresh(2,pk("), "got: {s}");
+        assert!(s.contains(",s:pk("), "got: {s}");
+        assert!(s.contains(",snj:and_v(v:pk("), "got: {s}");
+        assert!(s.contains(",older(12960))))"), "got: {s}");
+        assert!(s.contains("<0;1>/*"), "got: {s}");
+
+        // Round-trips through the parser byte-for-byte (proves it's a valid, canonical
+        // descriptor string, not just something we happened to construct).
+        let reparsed = Descriptor::<DescriptorPublicKey>::from_str(&s).unwrap();
+        assert_eq!(reparsed.to_string(), s);
+    }
+
+    #[test]
+    fn splits_into_distinct_external_and_internal_descriptors() {
+        let cfg = test_wallet_config(12960);
+        let built = build_descriptor(&cfg).unwrap();
+        assert_ne!(built.external.to_string(), built.internal.to_string());
+        assert!(!built.external.is_multipath());
+        assert!(!built.internal.is_multipath());
+
+        let receive0 = address_at(&built.external, 0, cfg.network).unwrap();
+        let change0 = address_at(&built.internal, 0, cfg.network).unwrap();
+        assert_ne!(receive0, change0);
+    }
+
+    #[test]
+    fn address_derivation_is_deterministic() {
+        let cfg = test_wallet_config(12960);
+        let built = build_descriptor(&cfg).unwrap();
+        let a = address_at(&built.external, 5, cfg.network).unwrap();
+        let b = address_at(&built.external, 5, cfg.network).unwrap();
+        assert_eq!(a, b);
+        let c = address_at(&built.external, 6, cfg.network).unwrap();
+        assert_ne!(a, c);
+    }
+
+    #[test]
+    fn rejects_config_that_fails_validation() {
+        let mut cfg = test_wallet_config(0);
+        cfg.timelock_blocks = 0;
+        assert!(build_descriptor(&cfg).is_err());
+    }
+
+    #[test]
+    fn parse_descriptor_accepts_a_multipath_string_and_splits_it() {
+        let cfg = test_wallet_config(12960);
+        let built = build_descriptor(&cfg).unwrap();
+        let parsed = parse_descriptor(&built.multipath.to_string()).unwrap();
+        assert_eq!(parsed.to_string(), built.external.to_string());
+    }
+
+    #[test]
+    fn parse_descriptor_rejects_garbage() {
+        assert!(parse_descriptor("not a descriptor").is_err());
+    }
+
+    #[test]
+    fn parse_descriptor_rejects_wrong_checksum() {
+        let cfg = test_wallet_config(12960);
+        let built = build_descriptor(&cfg).unwrap();
+        let mut s = built.external.to_string();
+        s.push('x'); // corrupt the checksum
+        assert!(parse_descriptor(&s).is_err());
+    }
+
+    #[test]
+    fn find_owner_locates_external_and_internal_scripts() {
+        let cfg = test_wallet_config(12960);
+        let built = build_descriptor(&cfg).unwrap();
+
+        let receive3 = at_index(&built.external, 3).unwrap().script_pubkey();
+        let owned = find_owner(&built, &receive3, 10)
+            .unwrap()
+            .expect("should find it");
+        assert_eq!(
+            owned,
+            Owned {
+                chain: Chain::External,
+                index: 3
+            }
+        );
+
+        let change7 = at_index(&built.internal, 7).unwrap().script_pubkey();
+        let owned = find_owner(&built, &change7, 10)
+            .unwrap()
+            .expect("should find it");
+        assert_eq!(
+            owned,
+            Owned {
+                chain: Chain::Internal,
+                index: 7
+            }
+        );
+    }
+
+    #[test]
+    fn find_owner_respects_the_gap_limit() {
+        let cfg = test_wallet_config(12960);
+        let built = build_descriptor(&cfg).unwrap();
+        let receive50 = at_index(&built.external, 50).unwrap().script_pubkey();
+        assert!(find_owner(&built, &receive50, 10).unwrap().is_none());
+        assert!(find_owner(&built, &receive50, 51).unwrap().is_some());
+    }
+
+    #[test]
+    fn find_owner_returns_none_for_a_foreign_script() {
+        let cfg = test_wallet_config(12960);
+        let built = build_descriptor(&cfg).unwrap();
+        // A well-formed P2WSH scriptPubkey (OP_0 <32-byte hash>) that isn't ours.
+        let foreign = bitcoin::ScriptBuf::from(vec![0u8; 34]);
+        assert!(find_owner(&built, &foreign, 25).unwrap().is_none());
+    }
+}
diff --git a/docs/miniscript-reference/invariants-reference.rs b/docs/miniscript-reference/invariants-reference.rs
new file mode 100644
index 0000000..c7e973b
--- /dev/null
+++ b/docs/miniscript-reference/invariants-reference.rs
@@ -0,0 +1,403 @@
+/*
+ * BITME-ONLY REFERENCE MATERIAL
+ * The policies and flows shown in this file (e.g., exactly one immediate path, server-side hold/veto) belong to Bitme, NOT Keeper.
+ * Keeper's actual wallet policy (including Miniscript inheritance paths) and server constraints differ.
+ * Any future implementation or tests for Keeper must use the actual Keeper Miniscript policy.
+ */
+
+//! Formal, structural proof (not just a smoke test) that a descriptor's spending policy has
+//! the required shape:
+//!
+//!   - no single key, alone, ever authorizes a spend (with or without waiting)
+//!   - exactly one 2-key subset can spend immediately (the HOT path)
+//!   - the remaining 2-key subset(s) can only spend after the configured relative timelock,
+//!     and not one block earlier (exact boundary, not "eventually")
+//!   - *every* 2-key subset can eventually spend - i.e. losing any single key is survivable.
+//!     This is the invariant that makes the wallet recoverable rather than merely secure, and
+//!     it's the one an earlier revision of this descriptor failed.
+//!
+//! This works by lifting the descriptor to rust-miniscript's abstract `Semantic` policy and
+//! using its `entails` algorithm ("every satisfaction of A is also a satisfaction of B") to ask,
+//! for every key and every pair of keys, "is having just these signatures (optionally plus
+//! having waited long enough) *sufficient* to satisfy the whole descriptor?". This is a
+//! property of the policy itself, independent of any particular PSBT or transaction.
+
+use std::str::FromStr;
+
+use anyhow::{bail, Context, Result};
+use miniscript::descriptor::DefiniteDescriptorKey;
+use miniscript::policy::{Concrete, Liftable, Semantic};
+use miniscript::Descriptor;
+
+/// A key participating in the spending policy, with a human-readable role label
+/// ("hardware", "server", "mobile", or "key1"/"key2"/"key3" if roles are unknown).
+#[derive(Clone)]
+pub struct LabeledKey {
+    pub label: String,
+    pub key: DefiniteDescriptorKey,
+}
+
+#[derive(Debug, Clone)]
+pub struct PairResult {
+    pub labels: (String, String),
+    pub spends_immediately: bool,
+    pub spends_after_timelock: bool,
+}
+
+#[derive(Debug, Clone)]
+pub struct InvariantReport {
+    pub key_labels: Vec<String>,
+    pub no_single_key_can_spend: bool,
+    pub pairs: Vec<PairResult>,
+    pub exactly_one_immediate_path: bool,
+    pub at_least_one_timelocked_path: bool,
+    pub timelock_boundary_holds: bool,
+    /// Every 2-key subset can spend, immediately or after the timelock - so the loss of any
+    /// single key still leaves a way to move the funds. See the module doc.
+    pub every_pair_can_eventually_spend: bool,
+}
+
+impl InvariantReport {
+    pub fn all_invariants_hold(&self) -> bool {
+        self.no_single_key_can_spend
+            && self.exactly_one_immediate_path
+            && self.at_least_one_timelocked_path
+            && self.timelock_boundary_holds
+            && self.every_pair_can_eventually_spend
+    }
+}
+
+fn lift_fragment(fragment: &str) -> Result<Semantic<DefiniteDescriptorKey>> {
+    Concrete::<DefiniteDescriptorKey>::from_str(fragment)
+        .with_context(|| format!("parsing test policy fragment: {fragment}"))?
+        .lift()
+        .with_context(|| format!("lifting test policy fragment: {fragment}"))
+}
+
+/// Runs the invariant analysis against `descriptor` (already resolved to a single derivation
+/// index - the policy shape, hence every invariant below, is identical at every index since
+/// only the concrete key bytes change) using `keys` as the full set of signers in the policy.
+pub fn verify_invariants(
+    descriptor: &Descriptor<DefiniteDescriptorKey>,
+    keys: &[LabeledKey],
+    timelock_blocks: u16,
+) -> Result<InvariantReport> {
+    if keys.len() < 2 {
+        bail!("need at least two keys to analyze a multi-key spending policy");
+    }
+
+    let full_policy: Semantic<DefiniteDescriptorKey> = descriptor
+        .lift()
+        .context("lifting descriptor to a semantic policy")?;
+
+    // 1. No single key, alone, ever satisfies the descriptor - checked both with no time
+    //    constraint at all, and with an unbounded amount of elapsed time.
+    let mut no_single_key_can_spend = true;
+    for k in keys {
+        let alone = lift_fragment(&format!("pk({})", k.key))?;
+        if alone.entails(full_policy.clone()).unwrap_or(true) {
+            no_single_key_can_spend = false;
+        }
+        let alone_after_timelock =
+            lift_fragment(&format!("and(pk({}),older({timelock_blocks}))", k.key))?;
+        if alone_after_timelock
+            .entails(full_policy.clone())
+            .unwrap_or(true)
+        {
+            no_single_key_can_spend = false;
+        }
+    }
+
+    // 2. Pairwise analysis over every 2-key subset.
+    let mut pairs = Vec::new();
+    let mut immediate_count = 0usize;
+    let mut timelocked_count = 0usize;
+    let mut boundary_ok = true;
+
+    for i in 0..keys.len() {
+        for j in (i + 1)..keys.len() {
+            let (a, b) = (&keys[i], &keys[j]);
+
+            let immediate = lift_fragment(&format!("and(pk({}),pk({}))", a.key, b.key))?
+                .entails(full_policy.clone())
+                .unwrap_or(false);
+
+            let after_timelock = lift_fragment(&format!(
+                "and(pk({}),and(pk({}),older({timelock_blocks})))",
+                a.key, b.key
+            ))?
+            .entails(full_policy.clone())
+            .unwrap_or(false);
+
+            if immediate {
+                immediate_count += 1;
+            }
+            if after_timelock && !immediate {
+                timelocked_count += 1;
+                if timelock_blocks > 1 {
+                    let one_block_early = lift_fragment(&format!(
+                        "and(pk({}),and(pk({}),older({})))",
+                        a.key,
+                        b.key,
+                        timelock_blocks - 1
+                    ))?
+                    .entails(full_policy.clone())
+                    .unwrap_or(true);
+                    if one_block_early {
+                        boundary_ok = false;
+                    }
+                }
+            }
+
+            pairs.push(PairResult {
+                labels: (a.label.clone(), b.label.clone()),
+                spends_immediately: immediate,
+                spends_after_timelock: after_timelock,
+            });
+        }
+    }
+
+    let every_pair_can_eventually_spend = pairs
+        .iter()
+        .all(|p| p.spends_immediately || p.spends_after_timelock);
+
+    Ok(InvariantReport {
+        key_labels: keys.iter().map(|k| k.label.clone()).collect(),
+        pairs,
+        no_single_key_can_spend,
+        exactly_one_immediate_path: immediate_count == 1,
+        at_least_one_timelocked_path: timelocked_count >= 1,
+        timelock_boundary_holds: boundary_ok,
+        every_pair_can_eventually_spend,
+    })
+}
+
+#[cfg(test)]
+mod tests {
+    use std::collections::HashMap;
+    use std::str::FromStr;
+
+    use bitcoin::{PublicKey, Sequence};
+    use miniscript::ForEachKey;
+
+    use super::*;
+    use crate::config::WalletConfig;
+    use crate::descriptor::{at_index, build_descriptor, policy_string, BuiltDescriptor};
+    use crate::test_util::{test_signature, test_signer, test_wallet_config};
+
+    /// Labels a built descriptor's keys "hardware"/"server"/"mobile" by matching them back
+    /// against the config that produced them - mirrors what the CLI does, kept independent of
+    /// `main.rs` so these tests exercise `verify_invariants` the same way production code does.
+    fn labeled_keys(
+        cfg: &WalletConfig,
+        built: &BuiltDescriptor,
+    ) -> (Descriptor<DefiniteDescriptorKey>, Vec<LabeledKey>) {
+        let definite = at_index(&built.external, 0).unwrap();
+        let mut found: Vec<(String, DefiniteDescriptorKey)> = Vec::new();
+        definite.for_each_key(|k| {
+            found.push((k.to_string(), k.clone()));
+            true
+        });
+        let roles = [
+            ("hardware", &cfg.keys.hardware.xpub),
+            ("server", &cfg.keys.server.xpub),
+            ("mobile", &cfg.keys.mobile.xpub),
+        ];
+        let mut labeled = Vec::new();
+        for (role, xpub) in roles {
+            let (_, key) = found
+                .iter()
+                .find(|(s, _)| s.contains(xpub.trim()))
+                .cloned()
+                .unwrap_or_else(|| panic!("key for role {role} not found in descriptor"));
+            labeled.push(LabeledKey {
+                label: role.to_string(),
+                key,
+            });
+        }
+        (definite, labeled)
+    }
+
+    fn pair<'a>(report: &'a InvariantReport, a: &str, b: &str) -> &'a PairResult {
+        report
+            .pairs
+            .iter()
+            .find(|p| (p.labels.0 == a && p.labels.1 == b) || (p.labels.0 == b && p.labels.1 == a))
+            .unwrap_or_else(|| panic!("no pair ({a}, {b}) in report"))
+    }
+
+    // ---- Formal: entailment over the abstract policy, independent of any real signature ----
+
+    #[test]
+    fn formal_invariants_hold_for_the_built_descriptor() {
+        let cfg = test_wallet_config(12960);
+        let built = build_descriptor(&cfg).unwrap();
+        let (definite, keys) = labeled_keys(&cfg, &built);
+        let report = verify_invariants(&definite, &keys, 12960).unwrap();
+
+        assert!(report.no_single_key_can_spend, "{report:?}");
+        assert!(report.exactly_one_immediate_path, "{report:?}");
+        assert!(report.at_least_one_timelocked_path, "{report:?}");
+        assert!(report.timelock_boundary_holds, "{report:?}");
+        assert!(report.all_invariants_hold());
+
+        let hot = pair(&report, "hardware", "server");
+        assert!(
+            hot.spends_immediately,
+            "HOT path (hardware+server) must spend immediately"
+        );
+
+        // Recovery when THIS SERVICE is gone.
+        let no_server = pair(&report, "hardware", "mobile");
+        assert!(
+            !no_server.spends_immediately,
+            "hardware+mobile must not bypass the policy engine by spending immediately"
+        );
+        assert!(
+            no_server.spends_after_timelock,
+            "hardware+mobile must spend after the timelock (server-loss recovery)"
+        );
+
+        // Recovery when the HARDWARE is gone - the property the previous descriptor lacked,
+        // and the whole reason for the redesign.
+        let no_hardware = pair(&report, "server", "mobile");
+        assert!(
+            !no_hardware.spends_immediately,
+            "server+mobile must not spend immediately - no-hardware spends must wait"
+        );
+        assert!(
+            no_hardware.spends_after_timelock,
+            "server+mobile MUST spend after the timelock: losing the HARDWARE must be survivable"
+        );
+
+        assert!(
+            report.every_pair_can_eventually_spend,
+            "losing any single key must be survivable: {report:?}"
+        );
+    }
+
+    #[test]
+    fn formal_invariants_hold_across_a_range_of_timelocks() {
+        for n in [1u16, 2, 6, 144, 4032, 12960, 65535] {
+            let cfg = test_wallet_config(n);
+            let built = build_descriptor(&cfg).unwrap();
+            let (definite, keys) = labeled_keys(&cfg, &built);
+            let report = verify_invariants(&definite, &keys, n).unwrap();
+            assert!(
+                report.all_invariants_hold(),
+                "timelock {n} blocks failed: {report:?}"
+            );
+        }
+    }
+
+    // ---- Empirical: real secp256k1 signatures fed through rust-miniscript's own witness
+    // construction algorithm (`Descriptor::get_satisfaction`), independent of the formal
+    // entailment analysis above. Uses fresh throwaway keys via `policy_string`, the same
+    // template `build_descriptor` uses, so the shape under test can't drift from production. ----
+
+    fn concrete_descriptor(
+        hardware: PublicKey,
+        server: PublicKey,
+        mobile: PublicKey,
+        timelock: u16,
+    ) -> Descriptor<PublicKey> {
+        let s = policy_string(
+            &hardware.to_string(),
+            &server.to_string(),
+            &mobile.to_string(),
+            timelock,
+        );
+        Descriptor::<PublicKey>::from_str(&s).expect("valid miniscript")
+    }
+
+    #[test]
+    fn hot_path_witness_constructs_with_hardware_and_server_and_no_wait() {
+        let hardware = test_signer(0x11);
+        let server = test_signer(0x12);
+        let mobile = test_signer(0x13);
+        let desc = concrete_descriptor(hardware.public, server.public, mobile.public, 12960);
+
+        let mut sigs = HashMap::new();
+        sigs.insert(hardware.public, test_signature(&hardware.secret));
+        sigs.insert(server.public, test_signature(&server.secret));
+        let satisfier = (sigs, Sequence::ZERO);
+
+        desc.get_satisfaction(satisfier)
+            .expect("hardware+server should satisfy the HOT path immediately");
+    }
+
+    #[test]
+    fn recovery_path_witness_requires_hardware_and_mobile_and_the_full_timelock() {
+        let hardware = test_signer(0x21);
+        let server = test_signer(0x22);
+        let mobile = test_signer(0x23);
+        let timelock = 12960u16;
+        let desc = concrete_descriptor(hardware.public, server.public, mobile.public, timelock);
+
+        let mut sigs = HashMap::new();
+        sigs.insert(hardware.public, test_signature(&hardware.secret));
+        sigs.insert(mobile.public, test_signature(&mobile.secret));
+
+        let one_block_early = (sigs.clone(), Sequence::from_height(timelock - 1));
+        desc.get_satisfaction(one_block_early)
+            .expect_err("must not satisfy one block before the timelock elapses");
+
+        let exactly_at_timelock = (sigs, Sequence::from_height(timelock));
+        desc.get_satisfaction(exactly_at_timelock)
+            .expect("must satisfy exactly at the configured timelock");
+    }
+
+    #[test]
+    fn no_single_key_witness_constructs_even_after_unlimited_time() {
+        let hardware = test_signer(0x31);
+        let server = test_signer(0x32);
+        let mobile = test_signer(0x33);
+        let desc = concrete_descriptor(hardware.public, server.public, mobile.public, 12960);
+        let far_future = Sequence::from_height(u16::MAX);
+
+        for signer in [&hardware, &server, &mobile] {
+            let mut sigs = HashMap::new();
+            sigs.insert(signer.public, test_signature(&signer.secret));
+            desc.get_satisfaction((sigs, far_future)).expect_err(
+                "a single key must never be able to spend, no matter how long it waits",
+            );
+        }
+    }
+
+    /// The no-hardware recovery path, empirically: SERVER + MOBILE must be blocked before the
+    /// timelock and must work at it. This is what makes a destroyed HARDWARE survivable.
+    #[test]
+    fn server_and_mobile_witness_constructs_only_after_the_timelock() {
+        let hardware = test_signer(0x41);
+        let server = test_signer(0x42);
+        let mobile = test_signer(0x43);
+        let timelock = 4320u16;
+        let desc = concrete_descriptor(hardware.public, server.public, mobile.public, timelock);
+
+        let mut sigs = HashMap::new();
+        sigs.insert(server.public, test_signature(&server.secret));
+        sigs.insert(mobile.public, test_signature(&mobile.secret));
+
+        desc.get_satisfaction((sigs.clone(), Sequence::ZERO))
+            .expect_err("server+mobile must not spend immediately");
+        desc.get_satisfaction((sigs.clone(), Sequence::from_height(timelock - 1)))
+            .expect_err("server+mobile must not spend one block before the timelock");
+        desc.get_satisfaction((sigs, Sequence::from_height(timelock)))
+            .expect("server+mobile must spend exactly at the timelock: lost-HARDWARE recovery");
+    }
+
+    #[test]
+    fn server_alone_can_never_spend_even_with_a_forged_looking_satisfier_for_every_other_slot() {
+        // Belt-and-braces: SERVER's signature present, but no signature offered for any other
+        // key at all (not even an attempted/garbage one) and no elapsed time. Must still fail.
+        let hardware = test_signer(0x51);
+        let server = test_signer(0x52);
+        let mobile = test_signer(0x53);
+        let desc = concrete_descriptor(hardware.public, server.public, mobile.public, 12960);
+
+        let mut sigs = HashMap::new();
+        sigs.insert(server.public, test_signature(&server.secret));
+        desc.get_satisfaction((sigs, Sequence::ZERO))
+            .expect_err("SERVER alone must never be able to spend");
+    }
+}