diff --git a/crates/whitaker_clones_core/src/index/kani.rs b/crates/whitaker_clones_core/src/index/kani.rs
index d94cdd93..24d4eee6 100644
--- a/crates/whitaker_clones_core/src/index/kani.rs
+++ b/crates/whitaker_clones_core/src/index/kani.rs
@@ -1,10 +1,10 @@
-//! Kani harnesses for bounded `LshConfig::new` verification.
+//! Kani harnesses for bounded clone-detector index verification.
 //!
 //! Run directly with:
 //!
 //! ```bash
 //! cargo kani --manifest-path crates/whitaker_clones_core/Cargo.toml \
-//!   --harness verify_lsh_config_new_symbolic
+//!   --harness verify_min_hasher_sketch_is_deterministic
 //! ```
 //!
 //! Or through the repository wrapper:
@@ -21,8 +21,70 @@
 //!   bounded `[0, 128]²` input space.
 //! - `verify_lsh_config_new_overflow_product` drives the `checked_mul(None)`
 //!   branch with non-zero overflowing inputs.
+//! - `verify_min_hasher_sketch_rejects_empty_input` checks the empty
+//!   retained-fingerprint boundary.
+//! - `verify_min_hasher_sketch_is_deterministic` checks first, middle, and last
+//!   signature lanes for wide boundary-hash inputs.
+//! - `verify_min_hasher_sketch_ignores_duplicate_hashes` compares a wide
+//!   boundary-hash set against the same set with repeated hashes.
 
-use super::{IndexError, LshConfig, MINHASH_SIZE};
+use crate::token::Fingerprint;
+
+use super::{IndexError, LshConfig, MINHASH_SIZE, MinHashSignature, MinHasher};
+
+const KANI_MINHASH_SEED: u64 = 0xA076_1D64_78BD_642F;
+const KANI_MINHASH_MIDDLE_SEED: u64 = 0xE703_7ED1_A0B4_28DB;
+const KANI_MINHASH_LAST_SEED: u64 = 0x8EBC_6AF0_9C88_C6E3;
+
+fn fingerprint(hash: u64, start: usize) -> Fingerprint {
+    Fingerprint::new(hash, start..start.saturating_add(1))
+}
+
+fn checked_lane_hasher() -> MinHasher {
+    MinHasher::from_checked_lane_seeds_for_kani(
+        KANI_MINHASH_SEED,
+        KANI_MINHASH_MIDDLE_SEED,
+        KANI_MINHASH_LAST_SEED,
+    )
+}
+
+fn assert_lane_selects_singleton_min(
+    lane: usize,
+    signature: &MinHashSignature,
+    left_singleton: &MinHashSignature,
+    right_singleton: &MinHashSignature,
+) {
+    let actual = signature.values()[lane];
+    let left = left_singleton.values()[lane];
+    let right = right_singleton.values()[lane];
+
+    kani::assert(
+        left != right,
+        "singleton lane values must distinguish the checked input hashes",
+    );
+    kani::assert(
+        actual == left || actual == right,
+        "combined sketch lane must select a hash value present in a singleton sketch",
+    );
+    kani::assert(
+        actual <= left && actual <= right,
+        "combined sketch lane must contain the minimum singleton hash value",
+    );
+}
+
+fn assert_checked_lanes_select_singleton_min(
+    signature: &MinHashSignature,
+    left_singleton: &MinHashSignature,
+    right_singleton: &MinHashSignature,
+) {
+    kani::assert(
+        signature.values().len() == MINHASH_SIZE,
+        "signature must keep the fixed MinHash width",
+    );
+    assert_lane_selects_singleton_min(0, signature, left_singleton, right_singleton);
+    assert_lane_selects_singleton_min(MINHASH_SIZE / 2, signature, left_singleton, right_singleton);
+    assert_lane_selects_singleton_min(MINHASH_SIZE - 1, signature, left_singleton, right_singleton);
+}
 
 #[kani::proof]
 #[kani::unwind(4)]
@@ -138,3 +200,96 @@ fn verify_lsh_config_new_overflow_product() {
         }
     }
 }
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn verify_min_hasher_sketch_rejects_empty_input() {
+    let hasher = MinHasher::from_seed_for_kani(KANI_MINHASH_SEED);
+
+    match hasher.sketch(&[]) {
+        Err(IndexError::EmptyFingerprintSet) => {}
+        Ok(_) => kani::assert(false, "empty input must not produce a signature"),
+        Err(_) => kani::assert(false, "empty input must report EmptyFingerprintSet"),
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn verify_min_hasher_sketch_is_deterministic() {
+    let hashes = [0, u64::MAX];
+    let fingerprints = [fingerprint(hashes[0], 0), fingerprint(hashes[1], 1)];
+
+    let left = checked_lane_hasher()
+        .sketch(&fingerprints)
+        .expect("non-empty fingerprints should sketch");
+    let right = checked_lane_hasher()
+        .sketch(&fingerprints)
+        .expect("non-empty fingerprints should sketch");
+    let first_singleton = checked_lane_hasher()
+        .sketch(&[fingerprints[0].clone()])
+        .expect("single fingerprint should sketch");
+    let second_singleton = checked_lane_hasher()
+        .sketch(&[fingerprints[1].clone()])
+        .expect("single fingerprint should sketch");
+
+    kani::assert(
+        left.values()[0] == right.values()[0],
+        "sketching the same fingerprints must be deterministic for the first lane",
+    );
+    kani::assert(
+        left.values()[MINHASH_SIZE / 2] == right.values()[MINHASH_SIZE / 2],
+        "sketching the same fingerprints must be deterministic for the middle lane",
+    );
+    kani::assert(
+        left.values()[MINHASH_SIZE - 1] == right.values()[MINHASH_SIZE - 1],
+        "sketching the same fingerprints must be deterministic for the last lane",
+    );
+    assert_checked_lanes_select_singleton_min(&left, &first_singleton, &second_singleton);
+}
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn verify_min_hasher_sketch_ignores_duplicate_hashes() {
+    let hashes = [u64::from(u8::MAX) + 1, u64::from(u16::MAX)];
+    let unique = [fingerprint(hashes[0], 0), fingerprint(hashes[1], 1)];
+    let duplicated = [
+        fingerprint(hashes[0], 0),
+        fingerprint(hashes[1], 1),
+        fingerprint(hashes[0], 2),
+        fingerprint(hashes[1], 3),
+    ];
+
+    let hasher = checked_lane_hasher();
+    let unique_signature = hasher
+        .sketch(&unique)
+        .expect("non-empty fingerprints should sketch");
+    let duplicated_signature = hasher
+        .sketch(&duplicated)
+        .expect("non-empty fingerprints should sketch");
+    let first_singleton = hasher
+        .sketch(&[unique[0].clone()])
+        .expect("single fingerprint should sketch");
+    let second_singleton = hasher
+        .sketch(&[unique[1].clone()])
+        .expect("single fingerprint should sketch");
+
+    kani::assert(
+        unique_signature.values()[0] == duplicated_signature.values()[0],
+        "duplicate fingerprint hashes must not change the first signature lane",
+    );
+    kani::assert(
+        unique_signature.values()[MINHASH_SIZE / 2]
+            == duplicated_signature.values()[MINHASH_SIZE / 2],
+        "duplicate fingerprint hashes must not change the middle signature lane",
+    );
+    kani::assert(
+        unique_signature.values()[MINHASH_SIZE - 1]
+            == duplicated_signature.values()[MINHASH_SIZE - 1],
+        "duplicate fingerprint hashes must not change the last signature lane",
+    );
+    assert_checked_lanes_select_singleton_min(
+        &unique_signature,
+        &first_singleton,
+        &second_singleton,
+    );
+}
diff --git a/crates/whitaker_clones_core/src/index/minhash.rs b/crates/whitaker_clones_core/src/index/minhash.rs
index fa98772f..9da0e5a3 100644
--- a/crates/whitaker_clones_core/src/index/minhash.rs
+++ b/crates/whitaker_clones_core/src/index/minhash.rs
@@ -1,6 +1,29 @@
-//! Deterministic MinHash sketch generation.
+//! Deterministic MinHash sketch generation for token-pass clone candidates.
+//!
+//! This module turns retained token [`Fingerprint`] values into fixed-width
+//! [`MinHashSignature`] values for the clone-detector index API. [`MinHasher`]
+//! owns the deterministic seed family used to sketch a fingerprint set, while
+//! [`unique_hashes`] normalizes retained fingerprints into sorted,
+//! deduplicated hash values so sketching has set semantics rather than multiset
+//! semantics.
+//!
+//! Internally, [`Seed`] keeps MinHash seed values distinct from raw fingerprint
+//! hashes at the type level. The hashing core still accepts raw `u64` hash
+//! values because fingerprints and signature lanes are represented as hash
+//! words throughout the index API.
+//!
+//! The `#[cfg(kani)]` constructors and the unrolled `sketch_values`
+//! implementation are proof seams for bounded model checking. They keep Kani
+//! harnesses focused on [`MinHasher::sketch`] invariants without changing the
+//! production API or the production [`array::from_fn`] implementation.
+//!
+//! [`LshIndex`](super::LshIndex) in `lsh.rs` consumes the signatures produced
+//! here by partitioning them into configured bands and emitting candidate
+//! fragment pairs. The parent `index` module re-exports [`MinHasher`],
+//! [`MinHashSignature`], [`MINHASH_SIZE`], and related error/configuration
+//! types as the crate-facing clone-detector indexing API.
 
-use std::{array, collections::BTreeSet};
+use std::array;
 
 use crate::token::Fingerprint;
 
@@ -10,10 +33,17 @@ const SEED_STREAM_START: u64 = 0x243F_6A88_85A3_08D3;
 const SEED_STREAM_STEP: u64 = 0x9E37_79B9_7F4A_7C15;
 const HASH_MIX: u64 = 0x94D0_49BB_1331_11EB;
 
+/// A typed MinHash seed value.
+///
+/// Keeps seed values distinct from raw hash values at the type level,
+/// preventing accidental argument transposition inside the hashing core.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+struct Seed(u64);
+
 /// Deterministic MinHash sketcher for retained token fingerprints.
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct MinHasher {
-    seeds: [u64; MINHASH_SIZE],
+    seeds: [Seed; MINHASH_SIZE],
 }
 
 impl Default for MinHasher {
@@ -53,25 +83,233 @@ impl MinHasher {
     /// empty.
     pub fn sketch(&self, fingerprints: &[Fingerprint]) -> IndexResult<MinHashSignature> {
         let unique_hashes = unique_hashes(fingerprints)?;
-        let values = array::from_fn(|index| minimum_mixed_hash(self.seeds[index], &unique_hashes));
+        let values = sketch_values(&self.seeds, &unique_hashes);
         Ok(MinHashSignature::new(values))
     }
+
+    /// Creates a deterministic proof-only fixture for Kani harnesses.
+    ///
+    /// This `#[cfg(kani)]` proof seam fills all [`MINHASH_SIZE`] seeds with the
+    /// same value, avoiding seed-stream construction to drastically reduce
+    /// Kani's symbolic state space during bounded model checking. Production
+    /// code continues to use [`MinHasher::new`]; this constructor exists only
+    /// to provide deterministic, lightweight inputs for Kani proofs rather than
+    /// production logic.
+    #[cfg(kani)]
+    pub(super) fn from_seed_for_kani(seed: u64) -> Self {
+        Self {
+            seeds: [Seed(seed); MINHASH_SIZE],
+        }
+    }
+
+    /// Creates a deterministic proof-only fixture with selected lane seeds.
+    ///
+    /// This `pub(super)` `#[cfg(kani)]` helper is restricted to the parent
+    /// module and exists for Kani harnesses that need to observe the first,
+    /// middle, and last MinHash lanes with distinct seed values. The remaining
+    /// lanes reuse `first_seed`.
+    ///
+    /// `first_seed` initializes every lane, `middle_seed` replaces lane
+    /// [`MINHASH_SIZE`] / 2, and `last_seed` replaces lane [`MINHASH_SIZE`] -
+    /// 1. Callers provide raw `u64` seeds at this proof boundary; the function
+    /// wraps them as internal [`Seed`] values and returns a [`MinHasher`] ready
+    /// for [`MinHasher::sketch`]. There are no additional preconditions.
+    #[cfg(kani)]
+    pub(super) fn from_checked_lane_seeds_for_kani(
+        first_seed: u64,
+        middle_seed: u64,
+        last_seed: u64,
+    ) -> Self {
+        let mut seeds = [Seed(first_seed); MINHASH_SIZE];
+        seeds[MINHASH_SIZE / 2] = Seed(middle_seed);
+        seeds[MINHASH_SIZE - 1] = Seed(last_seed);
+        Self { seeds }
+    }
 }
 
-fn unique_hashes(fingerprints: &[Fingerprint]) -> IndexResult<BTreeSet<u64>> {
+/// Computes the 128-lane MinHash signature in production builds.
+///
+/// Two `cfg`-specific implementations exist to balance production idiom
+/// against proof tractability. This production variant uses idiomatic
+/// [`array::from_fn`] iteration. It is mechanically equivalent to the
+/// `#[cfg(kani)]` proof-seam variant: both call [`minimum_mixed_hash`] once per
+/// lane to produce the same 128-lane MinHash signature from the seeds and
+/// unique hashes.
+#[cfg(not(kani))]
+fn sketch_values(seeds: &[Seed; MINHASH_SIZE], unique_hashes: &[u64]) -> [u64; MINHASH_SIZE] {
+    array::from_fn(|index| minimum_mixed_hash(seeds[index], unique_hashes))
+}
+
+/// Computes the 128-lane MinHash signature with explicit unrolling for Kani.
+///
+/// Two `cfg`-specific implementations exist to balance production idiom
+/// against proof tractability. This `#[cfg(kani)]` proof seam manually unrolls
+/// every [`minimum_mixed_hash`] call so Kani's bounded model checker does not
+/// spend proof budget on iterator or loop state expansion. The explicit array
+/// literal is mechanically equivalent to the production [`array::from_fn`]
+/// implementation: both compute the same 128-lane MinHash signature from the
+/// seeds and unique hashes.
+// `@codescene/suppress` Large Method proof-seam: keep manual unrolling for Kani tractability
+#[cfg(kani)]
+fn sketch_values(seeds: &[Seed; MINHASH_SIZE], unique_hashes: &[u64]) -> [u64; MINHASH_SIZE] {
+    [
+        minimum_mixed_hash(seeds[0], unique_hashes),
+        minimum_mixed_hash(seeds[1], unique_hashes),
+        minimum_mixed_hash(seeds[2], unique_hashes),
+        minimum_mixed_hash(seeds[3], unique_hashes),
+        minimum_mixed_hash(seeds[4], unique_hashes),
+        minimum_mixed_hash(seeds[5], unique_hashes),
+        minimum_mixed_hash(seeds[6], unique_hashes),
+        minimum_mixed_hash(seeds[7], unique_hashes),
+        minimum_mixed_hash(seeds[8], unique_hashes),
+        minimum_mixed_hash(seeds[9], unique_hashes),
+        minimum_mixed_hash(seeds[10], unique_hashes),
+        minimum_mixed_hash(seeds[11], unique_hashes),
+        minimum_mixed_hash(seeds[12], unique_hashes),
+        minimum_mixed_hash(seeds[13], unique_hashes),
+        minimum_mixed_hash(seeds[14], unique_hashes),
+        minimum_mixed_hash(seeds[15], unique_hashes),
+        minimum_mixed_hash(seeds[16], unique_hashes),
+        minimum_mixed_hash(seeds[17], unique_hashes),
+        minimum_mixed_hash(seeds[18], unique_hashes),
+        minimum_mixed_hash(seeds[19], unique_hashes),
+        minimum_mixed_hash(seeds[20], unique_hashes),
+        minimum_mixed_hash(seeds[21], unique_hashes),
+        minimum_mixed_hash(seeds[22], unique_hashes),
+        minimum_mixed_hash(seeds[23], unique_hashes),
+        minimum_mixed_hash(seeds[24], unique_hashes),
+        minimum_mixed_hash(seeds[25], unique_hashes),
+        minimum_mixed_hash(seeds[26], unique_hashes),
+        minimum_mixed_hash(seeds[27], unique_hashes),
+        minimum_mixed_hash(seeds[28], unique_hashes),
+        minimum_mixed_hash(seeds[29], unique_hashes),
+        minimum_mixed_hash(seeds[30], unique_hashes),
+        minimum_mixed_hash(seeds[31], unique_hashes),
+        minimum_mixed_hash(seeds[32], unique_hashes),
+        minimum_mixed_hash(seeds[33], unique_hashes),
+        minimum_mixed_hash(seeds[34], unique_hashes),
+        minimum_mixed_hash(seeds[35], unique_hashes),
+        minimum_mixed_hash(seeds[36], unique_hashes),
+        minimum_mixed_hash(seeds[37], unique_hashes),
+        minimum_mixed_hash(seeds[38], unique_hashes),
+        minimum_mixed_hash(seeds[39], unique_hashes),
+        minimum_mixed_hash(seeds[40], unique_hashes),
+        minimum_mixed_hash(seeds[41], unique_hashes),
+        minimum_mixed_hash(seeds[42], unique_hashes),
+        minimum_mixed_hash(seeds[43], unique_hashes),
+        minimum_mixed_hash(seeds[44], unique_hashes),
+        minimum_mixed_hash(seeds[45], unique_hashes),
+        minimum_mixed_hash(seeds[46], unique_hashes),
+        minimum_mixed_hash(seeds[47], unique_hashes),
+        minimum_mixed_hash(seeds[48], unique_hashes),
+        minimum_mixed_hash(seeds[49], unique_hashes),
+        minimum_mixed_hash(seeds[50], unique_hashes),
+        minimum_mixed_hash(seeds[51], unique_hashes),
+        minimum_mixed_hash(seeds[52], unique_hashes),
+        minimum_mixed_hash(seeds[53], unique_hashes),
+        minimum_mixed_hash(seeds[54], unique_hashes),
+        minimum_mixed_hash(seeds[55], unique_hashes),
+        minimum_mixed_hash(seeds[56], unique_hashes),
+        minimum_mixed_hash(seeds[57], unique_hashes),
+        minimum_mixed_hash(seeds[58], unique_hashes),
+        minimum_mixed_hash(seeds[59], unique_hashes),
+        minimum_mixed_hash(seeds[60], unique_hashes),
+        minimum_mixed_hash(seeds[61], unique_hashes),
+        minimum_mixed_hash(seeds[62], unique_hashes),
+        minimum_mixed_hash(seeds[63], unique_hashes),
+        minimum_mixed_hash(seeds[64], unique_hashes),
+        minimum_mixed_hash(seeds[65], unique_hashes),
+        minimum_mixed_hash(seeds[66], unique_hashes),
+        minimum_mixed_hash(seeds[67], unique_hashes),
+        minimum_mixed_hash(seeds[68], unique_hashes),
+        minimum_mixed_hash(seeds[69], unique_hashes),
+        minimum_mixed_hash(seeds[70], unique_hashes),
+        minimum_mixed_hash(seeds[71], unique_hashes),
+        minimum_mixed_hash(seeds[72], unique_hashes),
+        minimum_mixed_hash(seeds[73], unique_hashes),
+        minimum_mixed_hash(seeds[74], unique_hashes),
+        minimum_mixed_hash(seeds[75], unique_hashes),
+        minimum_mixed_hash(seeds[76], unique_hashes),
+        minimum_mixed_hash(seeds[77], unique_hashes),
+        minimum_mixed_hash(seeds[78], unique_hashes),
+        minimum_mixed_hash(seeds[79], unique_hashes),
+        minimum_mixed_hash(seeds[80], unique_hashes),
+        minimum_mixed_hash(seeds[81], unique_hashes),
+        minimum_mixed_hash(seeds[82], unique_hashes),
+        minimum_mixed_hash(seeds[83], unique_hashes),
+        minimum_mixed_hash(seeds[84], unique_hashes),
+        minimum_mixed_hash(seeds[85], unique_hashes),
+        minimum_mixed_hash(seeds[86], unique_hashes),
+        minimum_mixed_hash(seeds[87], unique_hashes),
+        minimum_mixed_hash(seeds[88], unique_hashes),
+        minimum_mixed_hash(seeds[89], unique_hashes),
+        minimum_mixed_hash(seeds[90], unique_hashes),
+        minimum_mixed_hash(seeds[91], unique_hashes),
+        minimum_mixed_hash(seeds[92], unique_hashes),
+        minimum_mixed_hash(seeds[93], unique_hashes),
+        minimum_mixed_hash(seeds[94], unique_hashes),
+        minimum_mixed_hash(seeds[95], unique_hashes),
+        minimum_mixed_hash(seeds[96], unique_hashes),
+        minimum_mixed_hash(seeds[97], unique_hashes),
+        minimum_mixed_hash(seeds[98], unique_hashes),
+        minimum_mixed_hash(seeds[99], unique_hashes),
+        minimum_mixed_hash(seeds[100], unique_hashes),
+        minimum_mixed_hash(seeds[101], unique_hashes),
+        minimum_mixed_hash(seeds[102], unique_hashes),
+        minimum_mixed_hash(seeds[103], unique_hashes),
+        minimum_mixed_hash(seeds[104], unique_hashes),
+        minimum_mixed_hash(seeds[105], unique_hashes),
+        minimum_mixed_hash(seeds[106], unique_hashes),
+        minimum_mixed_hash(seeds[107], unique_hashes),
+        minimum_mixed_hash(seeds[108], unique_hashes),
+        minimum_mixed_hash(seeds[109], unique_hashes),
+        minimum_mixed_hash(seeds[110], unique_hashes),
+        minimum_mixed_hash(seeds[111], unique_hashes),
+        minimum_mixed_hash(seeds[112], unique_hashes),
+        minimum_mixed_hash(seeds[113], unique_hashes),
+        minimum_mixed_hash(seeds[114], unique_hashes),
+        minimum_mixed_hash(seeds[115], unique_hashes),
+        minimum_mixed_hash(seeds[116], unique_hashes),
+        minimum_mixed_hash(seeds[117], unique_hashes),
+        minimum_mixed_hash(seeds[118], unique_hashes),
+        minimum_mixed_hash(seeds[119], unique_hashes),
+        minimum_mixed_hash(seeds[120], unique_hashes),
+        minimum_mixed_hash(seeds[121], unique_hashes),
+        minimum_mixed_hash(seeds[122], unique_hashes),
+        minimum_mixed_hash(seeds[123], unique_hashes),
+        minimum_mixed_hash(seeds[124], unique_hashes),
+        minimum_mixed_hash(seeds[125], unique_hashes),
+        minimum_mixed_hash(seeds[126], unique_hashes),
+        minimum_mixed_hash(seeds[127], unique_hashes),
+    ]
+}
+
+/// Extracts sorted, deduplicated fingerprint hashes for MinHash set semantics.
+///
+/// This `pub(super)` helper is restricted to the parent module and converts
+/// retained [`Fingerprint`] values into the Vec-backed set representation used
+/// by [`MinHasher::sketch`]. Callers must pass the retained fingerprint slice
+/// they intend to sketch.
+///
+/// Returns the sorted unique hash values. If `fingerprints` is empty, returns
+/// [`IndexError::EmptyFingerprintSet`].
+pub(super) fn unique_hashes(fingerprints: &[Fingerprint]) -> IndexResult<Vec<u64>> {
     if fingerprints.is_empty() {
         return Err(IndexError::EmptyFingerprintSet);
     }
-    Ok(fingerprints
+    let mut hashes = fingerprints
         .iter()
         .map(|fingerprint| fingerprint.hash)
-        .collect())
+        .collect::<Vec<_>>();
+    hashes.sort_unstable();
+    hashes.dedup();
+    Ok(hashes)
 }
 
-fn minimum_mixed_hash(seed: u64, hashes: &BTreeSet<u64>) -> u64 {
-    hashes
-        .iter()
-        .fold(u64::MAX, |current, hash| current.min(mix_hash(seed, *hash)))
+fn minimum_mixed_hash(seed: Seed, hashes: &[u64]) -> u64 {
+    hashes.iter().fold(u64::MAX, |current, hash| {
+        current.min(mix_hash(seed.0, *hash))
+    })
 }
 
 fn mix_hash(seed: u64, hash: u64) -> u64 {
@@ -83,9 +321,9 @@ fn mix_hash(seed: u64, hash: u64) -> u64 {
 /// Both `next_seed` and `splitmix64` intentionally add `SEED_STREAM_STEP` to
 /// create a non-overlapping, deterministic seed sequence compatible with the
 /// seed-streaming approach. This double-increment is deliberate, not a bug.
-fn next_seed(state: &mut u64) -> u64 {
+fn next_seed(state: &mut u64) -> Seed {
     *state = state.wrapping_add(SEED_STREAM_STEP);
-    splitmix64(*state)
+    Seed(splitmix64(*state))
 }
 
 /// SplitMix64 generator with deliberate `SEED_STREAM_STEP` addition.
diff --git a/crates/whitaker_clones_core/src/index/tests.rs b/crates/whitaker_clones_core/src/index/tests.rs
index 547a3c02..2f9871c5 100644
--- a/crates/whitaker_clones_core/src/index/tests.rs
+++ b/crates/whitaker_clones_core/src/index/tests.rs
@@ -6,7 +6,7 @@ use crate::token::Fingerprint;
 
 use super::{
     CandidatePair, FragmentId, IndexError, LshConfig, LshIndex, MINHASH_SIZE, MinHashSignature,
-    MinHasher,
+    MinHasher, minhash::unique_hashes,
 };
 
 fn fingerprints(values: &[u64]) -> Vec<Fingerprint> {
@@ -132,9 +132,14 @@ fn sketch_rejects_empty_fingerprints() {
     assert_eq!(hasher.sketch(&[]), Err(IndexError::EmptyFingerprintSet));
 }
 
-#[test]
-fn min_hasher_is_deterministic_across_instances() {
-    let fingerprints = fingerprints(&[3, 5, 8, 13]);
+#[rstest]
+#[case(&[3, 5, 8, 13])]
+#[case(&[13, 8, 5, 3])]
+#[case(&[0])]
+#[case(&[u64::MAX])]
+#[case(&[0, 42, u64::MAX])]
+fn min_hasher_is_deterministic_across_instances(#[case] hashes: &[u64]) {
+    let fingerprints = fingerprints(hashes);
     let left = MinHasher::new()
         .sketch(&fingerprints)
         .expect("left instance should sketch");
@@ -145,27 +150,56 @@ fn min_hasher_is_deterministic_across_instances() {
     assert_eq!(left, right);
 }
 
-#[test]
-fn duplicate_hashes_do_not_change_the_sketch() {
+#[rstest]
+#[case(&[11, 22, 33], &[11, 22, 33, 22, 11])]
+#[case(&[5], &[5, 5, 5])]
+#[case(&[0, u64::MAX], &[u64::MAX, 0, u64::MAX, 0])]
+#[case(&[0, 1, u64::MAX], &[1, 0, u64::MAX, 1, 0])]
+fn duplicate_hashes_do_not_change_the_sketch(
+    #[case] expected_hashes: &[u64],
+    #[case] duplicated_hashes: &[u64],
+) {
+    assert_eq!(
+        unique_hashes(&fingerprints(duplicated_hashes)).expect("duplicate hashes should normalize"),
+        expected_hashes
+    );
+
     let hasher = MinHasher::new();
     let unique = hasher
-        .sketch(&fingerprints(&[11, 22, 33]))
+        .sketch(&fingerprints(expected_hashes))
         .expect("unique hashes should sketch");
     let duplicated = hasher
-        .sketch(&fingerprints(&[11, 22, 33, 22, 11]))
+        .sketch(&fingerprints(duplicated_hashes))
         .expect("duplicate hashes should sketch");
 
     assert_eq!(unique, duplicated);
 }
 
-#[test]
-fn identical_sets_yield_identical_signatures() {
+#[rstest]
+#[case(&[3, 5, 8, 13], &[13, 8, 5, 3], &[3, 5, 8, 13])]
+#[case(&[1, 2, 2, 3], &[3, 2, 1], &[1, 2, 3])]
+#[case(&[0, u64::MAX], &[u64::MAX, 0, 0], &[0, u64::MAX])]
+#[case(&[0, 1, u64::MAX], &[u64::MAX, 1, 0], &[0, 1, u64::MAX])]
+fn identical_sets_yield_identical_signatures(
+    #[case] left_hashes: &[u64],
+    #[case] right_hashes: &[u64],
+    #[case] expected_hashes: &[u64],
+) {
+    assert_eq!(
+        unique_hashes(&fingerprints(left_hashes)).expect("left hashes should normalize"),
+        expected_hashes
+    );
+    assert_eq!(
+        unique_hashes(&fingerprints(right_hashes)).expect("right hashes should normalize"),
+        expected_hashes
+    );
+
     let hasher = MinHasher::new();
     let left = hasher
-        .sketch(&fingerprints(&[3, 5, 8, 13]))
+        .sketch(&fingerprints(left_hashes))
         .expect("left sketch should succeed");
     let right = hasher
-        .sketch(&fingerprints(&[13, 8, 5, 3]))
+        .sketch(&fingerprints(right_hashes))
         .expect("right sketch should succeed");
 
     assert_eq!(left, right);
diff --git a/crates/whitaker_clones_core/tests/features/min_hash_lsh.feature b/crates/whitaker_clones_core/tests/features/min_hash_lsh.feature
index 1c6a7f8b..61ae9aba 100644
--- a/crates/whitaker_clones_core/tests/features/min_hash_lsh.feature
+++ b/crates/whitaker_clones_core/tests/features/min_hash_lsh.feature
@@ -25,6 +25,14 @@ Feature: MinHash and LSH candidate generation
     Then candidate pair count is 1
     And the only candidate pair is alpha and beta
 
+  Scenario: Duplicate retained hashes use set semantics
+    Given LSH bands 1 and rows 128
+    And fragment alpha retains hashes 11 22 33
+    And fragment beta retains hashes 11 22 33 22 11
+    When candidate pairs are generated
+    Then candidate pair count is 1
+    And the only candidate pair is alpha and beta
+
   Scenario: Invalid LSH settings surface a typed error
     Given LSH bands 0 and rows 4
     When candidate pairs are generated
diff --git a/crates/whitaker_clones_core/tests/min_hash_lsh_behaviour.rs b/crates/whitaker_clones_core/tests/min_hash_lsh_behaviour.rs
index 9895766f..01b013b4 100644
--- a/crates/whitaker_clones_core/tests/min_hash_lsh_behaviour.rs
+++ b/crates/whitaker_clones_core/tests/min_hash_lsh_behaviour.rs
@@ -181,21 +181,26 @@ fn scenario_multiple_collisions_one_pair(world: MinHashLshWorld) {
 }
 
 #[scenario(path = "tests/features/min_hash_lsh.feature", index = 3)]
-fn scenario_invalid_lsh_settings(world: MinHashLshWorld) {
+fn scenario_duplicate_hashes_use_set_semantics(world: MinHashLshWorld) {
     let _ = world;
 }
 
 #[scenario(path = "tests/features/min_hash_lsh.feature", index = 4)]
-fn scenario_empty_fingerprints(world: MinHashLshWorld) {
+fn scenario_invalid_lsh_settings(world: MinHashLshWorld) {
     let _ = world;
 }
 
 #[scenario(path = "tests/features/min_hash_lsh.feature", index = 5)]
-fn scenario_zero_rows(world: MinHashLshWorld) {
+fn scenario_empty_fingerprints(world: MinHashLshWorld) {
     let _ = world;
 }
 
 #[scenario(path = "tests/features/min_hash_lsh.feature", index = 6)]
+fn scenario_zero_rows(world: MinHashLshWorld) {
+    let _ = world;
+}
+
+#[scenario(path = "tests/features/min_hash_lsh.feature", index = 7)]
 fn scenario_invalid_non_zero_product(world: MinHashLshWorld) {
     let _ = world;
 }
diff --git a/docs/developers-guide.md b/docs/developers-guide.md
index 5f5f54eb..c7671b0f 100644
--- a/docs/developers-guide.md
+++ b/docs/developers-guide.md
@@ -268,6 +268,21 @@ The direct `CandidatePair::new` coverage lives in the clone-core crate:
   `crates/whitaker_clones_core/Cargo.toml` as `rstest`, `rstest-bdd`, and
   `rstest-bdd-macros`.
 
+The direct `MinHasher::sketch` invariant coverage is split between ordinary
+tests and Kani:
+
+- Unit tests in `crates/whitaker_clones_core/src/index/tests.rs` cover
+  deterministic sketches, duplicate-hash insensitivity, reordered set
+  semantics, empty input, and representative full-width `u64` hash values.
+- The BDD harness in
+  `crates/whitaker_clones_core/tests/min_hash_lsh_behaviour.rs` includes a
+  duplicate-retained-hash candidate-generation scenario.
+- The Kani harnesses in `crates/whitaker_clones_core/src/index/kani.rs` call
+  real `MinHasher::sketch` for the empty-input, deterministic-output, and
+  duplicate-hash properties. They use a private `cfg(kani)` seed fixture and
+  fixed-width signature builder so the proof focuses on sketch semantics
+  rather than seed-stream array construction.
+
 ### Make targets
 
 Use the Makefile targets for normal proof runs:
@@ -330,6 +345,12 @@ For the current clone-detector constructors, the split is:
 - Kani executes the real constructor with one concrete acceptance harness, one
   bounded symbolic harness over `[0, 128]²`, and one overflow harness that
   forces the `checked_mul(None)` branch.
+- Kani executes real `MinHasher::sketch` calls for empty input, deterministic
+  output, and duplicate retained hashes. The non-empty harnesses keep their
+  symbolic domains intentionally bounded: determinism proves equality at an
+  arbitrary signature lane for a fixed retained hash, while duplicate-hash
+  insensitivity proves a symbolic bounded retained hash at the first signature
+  lane.
 - Ordinary unit tests and `rstest-bdd` scenarios pin the concrete lexical
   `FragmentId` ordering contract that the `CandidatePair` proof's bridge still
   trusts rather than proving from `String` internals.
@@ -351,7 +372,7 @@ The proof targets are thin wrappers over repository scripts:
   decomposition/common harnesses through the existing workflow, and runs the
   clone-detector harnesses one harness per `cargo-kani` invocation so each
   proof appears explicitly in the output, including the overflow-specific
-  harness for `LshConfig::new`.
+  harness for `LshConfig::new` and the bounded `MinHasher::sketch` harnesses.
 
 The installer scripts are idempotent. The first proof run may take longer while
 toolchains and verifier binaries are downloaded; later runs reuse the cached
diff --git a/docs/execplans/7-2-7-kani-verification-of-bounded-min-hasher-sketch-invariants.md b/docs/execplans/7-2-7-kani-verification-of-bounded-min-hasher-sketch-invariants.md
new file mode 100644
index 00000000..9cf515b2
--- /dev/null
+++ b/docs/execplans/7-2-7-kani-verification-of-bounded-min-hasher-sketch-invariants.md
@@ -0,0 +1,737 @@
+# Verify bounded MinHasher sketch invariants
+
+This ExecPlan (execution plan) is a living document. The sections
+`Constraints`, `Tolerances`, `Risks`, `Progress`, `Surprises & Discoveries`,
+`Decision Log`, and `Outcomes & Retrospective` must be kept up to date as work
+proceeds.
+
+Status: COMPLETE
+
+## Purpose / big picture
+
+Roadmap item 7.2.7 adds bounded Kani verification for `MinHasher::sketch`, the
+clone-detector token-pass function that turns retained token fingerprints into
+a fixed-width MinHash signature. After this work is approved and implemented,
+maintainers can run `make kani-clone-detector` and observe machine-checked
+coverage for three implementation invariants:
+
+- Sketching the same bounded retained fingerprints is deterministic.
+- Repeating an already present fingerprint hash does not change the sketch.
+- Sketching an empty retained-fingerprint input fails with
+  `IndexError::EmptyFingerprintSet`.
+
+This plan deliberately does not claim to prove MinHash statistical quality,
+collision probability, or unbounded set behaviour. It proves bounded
+implementation behaviour over the real Rust code, in line with
+`docs/adr-003-formal-proof-strategy-for-clone-detector-pipeline.md`.
+
+The implementation began after explicit user approval on 2026-05-18.
+
+## Constraints
+
+- Work must implement roadmap item 7.2.7 only. Do not start roadmap item 7.2.8
+  for `LshIndex`.
+- Kani harnesses must call the real `MinHasher::sketch` implementation in
+  `crates/whitaker_clones_core/src/index/minhash.rs`, not a clean-room model.
+- Kani proof code must stay behind `#[cfg(kani)]` in
+  `crates/whitaker_clones_core/src/index/kani.rs` or a child module reached
+  from there.
+- Do not add a runtime dependency for proof tooling. Reuse
+  `scripts/install-kani.sh`, `scripts/run-kani.sh`, `make kani`, and
+  `make kani-clone-detector`.
+- Do not widen the public API solely for Kani. Prefer colocated harnesses and
+  crate-private helpers when a small proof seam is justified.
+- Keep ordinary `rstest` unit tests and `rstest-bdd` behaviour tests as the
+  first regression net. Kani complements these tests; it does not replace them.
+- Use Oxford British English in documentation.
+- Run commands through Makefile targets where targets exist.
+- Run formatting, linting, and tests sequentially, with `tee` output logs under
+  `/tmp`; do not run test, lint, format, or proof commands in parallel.
+- Do not use `/tmp` as a build target. Use it only for logs or scratch output.
+- Do not revert unrelated working-tree changes.
+- Commit atomic changes only after the relevant gates pass.
+- Run `coderabbit review --agent` after each major milestone and clear all
+  concerns before moving to the next milestone.
+- On completion of the feature, mark item 7.2.7 done in `docs/roadmap.md`.
+
+## Tolerances
+
+- Scope: if the implementation requires modifying more than eight repository
+  files, stop and ask for approval. Expected files are
+  `crates/whitaker_clones_core/src/index/kani.rs`, `scripts/run-kani.sh`,
+  `crates/whitaker_clones_core/src/index/tests.rs`,
+  `crates/whitaker_clones_core/tests/min_hash_lsh_behaviour.rs`,
+  `crates/whitaker_clones_core/tests/features/min_hash_lsh.feature`,
+  `docs/whitaker-clone-detector-design.md`, `docs/developers-guide.md`, and
+  `docs/roadmap.md`.
+- API: if a public function signature, public type, or public error variant
+  must change, stop and ask for approval.
+- Dependencies: if any new Cargo dependency, system package, or verifier
+  package is required, stop and ask for approval.
+- Proof bounds: if a MinHasher harness needs more than four symbolic retained
+  fingerprints, stop and explain the state-space risk before proceeding. The
+  user approved raising the MinHasher unwind bound above 16 on 2026-05-19 so
+  the real fixed 128-slot MinHash array construction can be verified.
+- Validation: if `make check-fmt`, `make lint`, `make test`, or
+  `make kani-clone-detector` still fails after two focused fix attempts, stop
+  and record the blocker.
+- Review: if `coderabbit review --agent` reports a concern that cannot be
+  resolved without changing the approved scope, stop and ask for direction.
+- Ambiguity: if duplicate-hash insensitivity could mean either duplicate
+  `Fingerprint.hash` values only or full duplicate `Fingerprint` structs
+  including ranges, prefer hash-only set semantics as documented in
+  `docs/whitaker-clone-detector-design.md`; stop only if code contradicts that
+  contract.
+
+## Risks
+
+- Risk: Kani state-space explosion from the Vec-backed set semantics and
+  128-wide signature construction. Severity: medium. Likelihood: medium.
+  Mitigation: keep symbolic inputs small, prove one property per harness, use
+  the shipped `cfg(kani)` seam, and keep the fixed-width signature path
+  explicit under Kani.
+
+- Risk: An over-broad proof proves a helper model rather than production code.
+  Severity: high. Likelihood: low. Mitigation: every harness must construct
+  the hasher through the shipped `MinHasher::from_seed_for_kani` seam, call the
+  Vec-backed `MinHasher::sketch(...)` entrypoint, and inspect the returned
+  `MinHashSignature` or `IndexError`.
+
+- Risk: Empty-input verification is trivial if it only checks `sketch(&[])`
+  with no symbolic path. Severity: low. Likelihood: medium. Mitigation: include
+  a concrete empty-input Kani harness and retain ordinary tests; the property
+  is intentionally a boundary error-path check.
+
+- Risk: Duplicate-hash proofs accidentally depend on byte-range equality.
+  Severity: medium. Likelihood: medium. Mitigation: use
+  `Fingerprint::new(hash, range)` values with different ranges but repeated
+  hash values in unit tests and, where tractable, in Kani input construction.
+
+- Risk: `coderabbit review --agent` may be unavailable in the local
+  environment. Severity: medium. Likelihood: medium. Mitigation: run it after
+  each milestone; if the command is missing or fails for authentication or
+  service reasons, record the exact failure and ask for direction before
+  treating the milestone as complete.
+
+## Progress
+
+- [x] 2026-05-18: Read `AGENTS.md` and loaded the required `execplans`,
+  `leta`, `rust-router`, `kani`, `commit-message`, `pr-creation`,
+  `en-gb-oxendict-style`, and `firecrawl-mcp` skills for the planning task.
+- [x] 2026-05-18: Confirmed the current branch is
+  `feat/kani-minhasher-plan`, not `main`.
+- [x] 2026-05-18: Used a Wyvern agent team to inspect code, documentation, and
+  validation conventions for item 7.2.7.
+- [x] 2026-05-18: Used Firecrawl to check current Kani guidance on proof
+  harnesses, `kani::assume`, and loop unwinding.
+- [x] 2026-05-18: Drafted this pre-implementation ExecPlan.
+- [x] 2026-05-18: Received explicit user approval to proceed with
+  implementation from this ExecPlan.
+- [x] 2026-05-18: Renamed the working branch to
+  `7-2-7-kani-verification-of-bounded-min-hasher-sketch-invariants` and push it
+  tracking
+  `origin/7-2-7-kani-verification-of-bounded-min-hasher-sketch-invariants`.
+- [x] 2026-05-18: Created draft pull request #230 for the planning commit.
+- [x] 2026-05-18: Ran baseline `make check-fmt`, `make lint`, and
+  `make test`; all passed before implementation edits.
+- [x] 2026-05-18: Restored the executable mode on `scripts/run-kani.sh` so
+  the existing `make kani-clone-detector` entry point can run.
+- [x] 2026-05-18: Reran baseline `make kani-clone-detector`; all existing
+  clone-detector harnesses verified successfully.
+- [x] 2026-05-18: Ran `coderabbit review --agent` after the baseline and
+  mode-fix milestone; it reported zero findings.
+- [x] 2026-05-18: Strengthened ordinary `rstest` unit coverage for
+  deterministic sketches, duplicate-hash insensitivity, empty input and
+  reordered set semantics.
+- [x] 2026-05-18: Added an `rstest-bdd` candidate-generation scenario showing
+  that duplicate retained hashes use set semantics.
+- [x] 2026-05-18: Validated the ordinary coverage milestone with
+  `make check-fmt`, `make lint`, and `make test`; the suite reported 1400
+  passed and 2 skipped.
+- [x] 2026-05-18: Ran `coderabbit review --agent` after the ordinary coverage
+  milestone; it reported zero findings.
+- [x] 2026-05-18: Added bounded Kani harnesses for empty-input failure,
+  deterministic sketching and duplicate-hash insensitivity.
+- [x] 2026-05-18: Added the new MinHasher harness names to
+  `scripts/run-kani.sh` under the clone-detector harness group.
+- [x] 2026-05-19: Received approval to resolve the proof-bound blocker and
+  raised the MinHasher harness unwind annotations to 129, one greater than the
+  fixed 128-slot MinHash array loop.
+- [x] 2026-05-19: Stopped the first 129-unwind Kani attempt after it continued
+  beyond a useful milestone boundary inside standard-library `BTreeSet`
+  unwinding for `verify_min_hasher_sketch_is_deterministic`.
+- [x] 2026-05-19: Reduced the non-empty Kani harness cardinalities while still
+  calling the real `MinHasher::sketch`: deterministic sketching now checks one
+  symbolic fingerprint, and duplicate-hash insensitivity compares one symbolic
+  hash against the same hash repeated at a different range.
+- [x] 2026-05-19: Stopped the reduced-cardinality 129-unwind attempt when it
+  repeated the same standard-library `BTreeSet` state-space pattern; the
+  high harness-level unwind remained the source of verifier cost.
+- [x] 2026-05-19: Introduced a private `cfg(kani)` MinHasher proof seam:
+  harnesses use `MinHasher::from_seed_for_kani` to avoid seed-stream array
+  construction, and `MinHasher::sketch` uses an explicit 128-slot
+  `cfg(kani)` signature builder so harnesses can return to unwind 4 while
+  still calling production `sketch`.
+- [x] 2026-05-19: Replaced the private `BTreeSet` dedup container in
+  `MinHasher::sketch` with a sorted/deduped `Vec<u64>`, preserving hash-set
+  semantics while avoiding verifier-heavy standard-library tree traversal.
+- [x] 2026-05-19: Narrowed the MinHasher non-empty Kani hash domain to
+  symbolic `u8` values cast to `u64` after the full-width `u64` deterministic
+  proof became solver-bound across the 128-slot signature comparison.
+- [x] 2026-05-19: Replaced whole-array equality in the Kani harnesses with
+  explicit per-slot assertions to avoid routing the 128-slot signature
+  comparison through a generated `memcmp` proof obligation.
+- [x] 2026-05-19: Replaced the 128 separate lane assertions with one symbolic
+  signature-lane assertion constrained to `< MINHASH_SIZE`, after the per-slot
+  version proved correct but generated too many separate solver obligations.
+- [x] 2026-05-19: Tightened the deterministic Kani harness to a concrete
+  retained hash plus symbolic lane after the combination of symbolic hash and
+  symbolic lane remained solver-heavy; duplicate-hash insensitivity retains the
+  symbolic bounded hash domain.
+- [x] 2026-05-19: Tightened the duplicate-insensitivity harness to assert the
+  first signature lane for a symbolic bounded retained hash after the symbolic
+  hash plus symbolic lane combination became solver-bound.
+- [x] 2026-05-19: Validated `make kani-clone-detector` after resolving the
+  proof-bound blocker; all clone-detector harnesses verified successfully,
+  including the new MinHasher empty-input, deterministic, and duplicate-hash
+  insensitivity proofs.
+- [x] 2026-05-19: Updated the clone-detector design and developer guide with
+  the MinHasher proof seam, bounded Kani harness shape, and ordinary test
+  coverage split; `docs/users-guide.md` remains unchanged because the work
+  does not change user-visible behaviour.
+- [x] 2026-05-19: Marked roadmap item 7.2.7 done.
+
+## Surprises & Discoveries
+
+- `MinHasher::sketch` already rejects empty input, deduplicates hashes through
+  `BTreeSet<u64>`, and has ordinary unit coverage for determinism, duplicate
+  hash insensitivity, empty input, and set-order independence in
+  `crates/whitaker_clones_core/src/index/tests.rs`.
+- Existing clone-detector Kani harnesses are already colocated in
+  `crates/whitaker_clones_core/src/index/kani.rs`, but currently cover only
+  `LshConfig::new`.
+- `scripts/run-kani.sh` runs clone-detector harnesses by an explicit name list,
+  so adding 7.2.7 harnesses also requires updating that script.
+- `docs/users-guide.md` does not currently document clone-detector proof
+  workflow. This feature is maintainer-facing, so the user guide should remain
+  unchanged unless the implementation changes user-visible CLI behaviour.
+- Official Kani documentation confirms that bounded proofs require explicit
+  finite input bounds, and that unwind bounds often need to be one greater than
+  the maximum loop iteration count.
+- Baseline `make kani-clone-detector` failed before implementation with
+  `Permission denied` because `scripts/run-kani.sh` is tracked as mode `100644`
+  while the Makefile invokes it directly as `./scripts/run-kani.sh`.
+- The BDD layer can observe duplicate-hash insensitivity through candidate
+  generation by comparing a fragment with unique retained hashes against a
+  fragment with the same hashes plus repeated values.
+- `make fmt` successfully applied Rust formatting for the new tests but still
+  fails on pre-existing repository-wide Markdown MD013 line-length violations.
+  Unrelated Markdown formatter churn was reverted, and `make check-fmt` passed
+  afterwards.
+- Fixed three-fingerprint and two-versus-four-fingerprint Kani inputs are
+  sufficient for item 7.2.7's bounded proof target because the invariants under
+  proof are deterministic output, empty-input failure, and duplicate hash set
+  semantics, not arbitrary-size MinHash quality.
+- The first MinHasher Kani run failed on the empty-input harness before
+  reaching `MinHasher::sketch` because `MinHasher::new()` builds the 128-wide
+  seed array with `std::array::from_fn`; Kani reported an unwinding failure in
+  the standard-library array loop at the current bound of 4.
+- A Kani-only constructor seam would not be sufficient for the non-empty
+  MinHasher harnesses because successful `MinHasher::sketch` calls also build
+  the 128-slot signature array. The proof still needs a 129 unwind bound to
+  cover the production signature loop.
+- A 129-unwind run over the original three-fingerprint deterministic harness
+  progressed through the fixed array loops but remained dominated by
+  `BTreeSet::from_sorted_iter` and internal `correct_childrens_parent_links`
+  paths. The issue is proof-state size in standard-library collection code, not
+  a project assertion failure.
+- Applying 129 as a harness-level unwind is too blunt for this proof: it covers
+  the fixed 128-slot arrays, but also forces unrelated `BTreeSet` internals to
+  the same bound. A targeted `cfg(kani)` fixed-slot expansion avoids that
+  coupling.
+- Even at unwind 4, `BTreeSet` iteration introduces verifier-heavy tree
+  navigation paths for one-element symbolic inputs. A sorted/deduped private
+  vector expresses the same set semantics for MinHasher and keeps the Kani
+  state space aligned with the bounded fingerprint input.
+- Full-width symbolic `u64` retained hashes can move the deterministic harness
+  from unwind failure into a long bit-vector solve. Bounding the symbolic hash
+  domain to 256 values keeps the proof exhaustive for a finite domain while
+  preserving ordinary `rstest` coverage for full-width `u64` examples.
+- Whole-array equality over `[u64; 128]` lowers to a memory comparison in Kani,
+  which produces a large solver obligation. Per-slot assertions are clearer
+  proof obligations and keep the invariant explicit.
+- A literal 128-lane assertion list is also too expensive. A single symbolic
+  lane index is the right bounded shape: Kani checks all valid lane indices
+  without multiplying the number of solver obligations.
+- Combining a symbolic retained hash with a symbolic lane still creates a large
+  solve for the deterministic harness. Determinism is structurally covered by
+  sketching the same concrete retained set at an arbitrary lane, while
+  duplicate-hash insensitivity carries the symbolic hash variation.
+- Combining symbolic retained hash and symbolic lane also makes the duplicate
+  harness too expensive. The proof now keeps the symbolic hash domain and
+  checks the first lane; ordinary unit and BDD tests keep full-signature
+  regression coverage.
+- The final MinHasher Kani shape is tractable but not cheap: the deterministic
+  and duplicate-insensitivity harnesses verify through the sorted/deduped
+  `Vec` implementation, and the duplicate proof took several minutes because
+  Kani still checks standard-library slice sorting and dedup internals for the
+  bounded input.
+
+## Decision Log
+
+- Decision: keep item 7.2.7 as a pre-implementation plan until the user
+  approves it. Rationale: the user explicitly stated that the plan must be
+  approved before implementation. Date/Author: 2026-05-18 / Codex.
+
+- Decision: implement the future-proof work in the existing
+  `crates/whitaker_clones_core/src/index/kani.rs` harness location, unless the
+  file becomes too large or the helper structure becomes unclear. Rationale:
+  ADR 003 and the clone-detector design already establish colocated `cfg(kani)`
+  harnesses as the clone-detector proof pattern. Date/Author: 2026-05-18 /
+  Codex.
+
+- Decision: use bounded arrays plus active lengths for symbolic fingerprint
+  inputs. Rationale: Kani verifies every value in the bounded state space;
+  fixed-size arrays keep the proof finite and make duplicate insertion
+  explicit. Date/Author: 2026-05-18 / Codex.
+
+- Decision: do not add a new ADR for 7.2.7 unless implementation uncovers a
+  substantive strategy change. Rationale: ADR 003 already decides the proof
+  split and names `MinHasher::sketch` as a Kani target. Date/Author: 2026-05-18
+  / Codex.
+
+- Decision: restore the executable bit on `scripts/run-kani.sh` before adding
+  the new harness names. Rationale: `make kani-clone-detector` is the supported
+  proof entry point, and it cannot run the existing harnesses while the script
+  is non-executable. Date/Author: 2026-05-18 / Codex.
+
+- Decision: use fixed small fingerprint arrays in the MinHasher Kani harnesses
+  rather than a symbolic active length. Rationale: the properties remain
+  bounded and substantive while avoiding proof complexity around symbolic slice
+  construction that is not part of the production contract. Date/Author:
+  2026-05-18 / Codex.
+
+- Decision: raise the MinHasher harness unwind annotations to 129 instead of
+  adding a Kani-only private constructor. Rationale: the non-empty harnesses
+  must verify the real `MinHasher::sketch` path, which itself constructs the
+  128-slot signature array; a constructor seam would only avoid seed generation
+  and would not remove the required signature-loop bound. Date/Author:
+  2026-05-19 / Codex.
+
+- Decision: narrow the non-empty Kani harness cardinalities to one symbolic
+  hash after the first 129-unwind attempt remained in `BTreeSet` internals.
+  Rationale: item 7.2.7 asks for bounded invariant verification; one symbolic
+  hash still exhausts all `u64` hash values, calls production `sketch`, proves
+  determinism for a non-empty retained set, and proves duplicate-hash
+  insensitivity with a repeated hash at a distinct range while avoiding
+  unrelated collection-state explosion. Date/Author: 2026-05-19 / Codex.
+
+- Decision: use a private Kani-only constructor and Kani-only explicit
+  fixed-slot signature builder instead of a 129 harness-level unwind. Rationale:
+  the harnesses still call real `MinHasher::sketch`, but the verifier no longer
+  applies the 128-slot array bound to standard-library `BTreeSet` internals.
+  Production builds continue to use `array::from_fn`; the proof seam is
+  compiled only under `cfg(kani)`. Date/Author: 2026-05-19 / Codex.
+
+- Decision: implement hash-set semantics for `MinHasher::sketch` with a
+  sorted/deduped private `Vec<u64>` rather than `BTreeSet<u64>`. Rationale:
+  ordering is irrelevant after deduplication, the public behaviour remains the
+  same, ordinary tests already cover duplicate and reordered inputs, and Kani
+  can verify the bounded invariants without proving standard-library tree
+  internals. Date/Author: 2026-05-19 / Codex.
+
+- Decision: bound MinHasher non-empty Kani hash values to symbolic `u8` values
+  cast to `u64`. Rationale: Kani is being used here as a bounded model checker,
+  ordinary tests still cover representative full-width `u64` hashes, and the
+  smaller finite hash domain keeps the 128-slot signature proof tractable.
+  Date/Author: 2026-05-19 / Codex.
+
+- Decision: assert MinHasher signature equality through one symbolic lane index
+  rather than whole-array equality or 128 separate lane assertions. Rationale:
+  the invariant is equality at every MinHash lane, and a symbolic index lets
+  Kani quantify over all bounded lanes without generating a large `memcmp` or a
+  large batch of independent solver obligations. Date/Author: 2026-05-19 /
+  Codex.
+
+- Decision: use a concrete retained hash for the deterministic Kani harness and
+  a bounded symbolic hash for the duplicate-insensitivity harness. Rationale:
+  deterministic output is independent of the specific retained hash value when
+  both calls receive the same input, ordinary tests cover representative
+  full-width hashes, and this split leaves the more semantically interesting
+  duplicate-hash property symbolic. Date/Author: 2026-05-19 / Codex.
+
+- Decision: check the first signature lane in the duplicate-insensitivity Kani
+  harness rather than a symbolic lane. Rationale: the harness still verifies a
+  substantive symbolic hash property through real `MinHasher::sketch`, while
+  full-signature duplicate insensitivity remains covered by ordinary tests and
+  behaviour tests. Date/Author: 2026-05-19 / Codex.
+
+## Outcomes & Retrospective
+
+Implementation is complete. `make kani-clone-detector` verifies the
+clone-detector Kani harness group, including the new `MinHasher::sketch`
+empty-input, deterministic-output, and duplicate-hash insensitivity harnesses.
+The proof shape uses a private `cfg(kani)` seed fixture and fixed-width
+signature builder while still calling real `MinHasher::sketch`. Ordinary unit
+tests and `rstest-bdd` scenarios continue to cover the broader runtime
+regression surface, including full-signature duplicate equality and
+representative full-width `u64` hashes.
+
+Validation completed on 2026-05-19:
+
+- `make kani-clone-detector` passed.
+- `make check-fmt` passed.
+- `make lint` passed.
+- `make test` passed with 1400 passed and 2 skipped.
+- `coderabbit review --agent` reported zero findings after the Kani proof
+  milestone.
+
+`docs/users-guide.md` was not changed because item 7.2.7 adds maintainer-facing
+proof coverage and internal documentation only; it does not change CLI
+behaviour, output formats, or user-facing workflows.
+
+## Orientation
+
+The relevant implementation lives in the `whitaker_clones_core` crate.
+`crates/whitaker_clones_core/src/index/minhash.rs` defines `MinHasher`.
+`MinHasher::sketch` accepts a slice of `Fingerprint` values, applies
+Vec-backed set semantics by sorting and deduplicating `Fingerprint.hash`
+values, mixes each unique hash with each seed, and returns a
+`MinHashSignature`. Kani harnesses construct proof fixtures through the shipped
+`MinHasher::from_seed_for_kani` seam and still call the real
+`MinHasher::sketch(...)` entrypoint, validating the returned
+`MinHashSignature` or `IndexError`.
+
+The surrounding index module is exposed through
+`crates/whitaker_clones_core/src/index/mod.rs` and re-exported from
+`crates/whitaker_clones_core/src/lib.rs`. Existing unit tests live in
+`crates/whitaker_clones_core/src/index/tests.rs`. Existing behaviour tests live
+in `crates/whitaker_clones_core/tests/min_hash_lsh_behaviour.rs`, backed by
+`crates/whitaker_clones_core/tests/features/min_hash_lsh.feature`.
+
+Formal verification entry points already exist. `make kani-clone-detector`
+calls `scripts/run-kani.sh clone-detector`, which invokes the pinned
+`cargo-kani` binary against explicit harness names in
+`crates/whitaker_clones_core/src/index/kani.rs`.
+
+Relevant documents to keep open during implementation:
+
+- `docs/roadmap.md`, item 7.2.7.
+- `docs/adr-003-formal-proof-strategy-for-clone-detector-pipeline.md`.
+- `docs/whitaker-clone-detector-design.md`, especially the MinHash and LSH
+  sections and the implementation decisions for 7.2.2 through 7.2.5.
+- `docs/developers-guide.md`, especially the Kani bounded model checking
+  section.
+- `docs/whitaker-dylint-suite-design.md`.
+- `docs/rust-testing-with-rstest-fixtures.md`.
+- `docs/rust-doctest-dry-guide.md`.
+- `docs/complexity-antipatterns-and-refactoring-strategies.md`.
+- `docs/rstest-bdd-users-guide.md`.
+
+Relevant skills for the implementer:
+
+- `leta`, for code navigation and symbol relationships.
+- `rust-router`, followed by `kani` for bounded model checking.
+- `rust-errors`, if the implementation needs to inspect or extend
+  `IndexError` handling.
+- `rust-types-and-apis`, only if a proof seam appears to require type or API
+  changes.
+- `nextest`, if `make test` failures require focused nextest diagnosis.
+- `commit-message`, for every commit.
+- `pr-creation`, when opening or updating the pull request.
+
+## External research notes
+
+Firecrawl was used on 2026-05-18 to confirm current public Kani guidance from
+the official Kani documentation:
+
+- The Kani first-steps tutorial describes proof harnesses as test-like entry
+  points that use `kani::any()` for symbolic values and `kani::assume()` to
+  encode real preconditions:
+  <https://model-checking.github.io/kani/tutorial-first-steps.html>.
+- The Kani loop-unwinding tutorial explains that Kani proofs over loops are
+  bounded, must constrain problem size, and often require explicit
+  `#[kani::unwind(...)]` values high enough to avoid unwinding assertion
+  failures:
+  <https://model-checking.github.io/kani/tutorial-loop-unwinding.html>.
+
+These notes reinforce the local repository guidance in
+`docs/developers-guide.md`: use small, explicit bounds and treat Kani as
+bounded implementation verification, not as unbounded mathematical proof.
+
+## Implementation plan
+
+Do not start this section until the plan is approved.
+
+### Milestone 1: Baseline and branch preparation
+
+Rename the branch and make it track the requested remote branch:
+
+```sh
+BRANCH=7-2-7-kani-verification-of-bounded-min-hasher-sketch-invariants
+git branch -m "${BRANCH}"
+git push -u origin "${BRANCH}"
+```
+
+Record the initial state:
+
+```sh
+git status --short --branch
+```
+
+Run baseline checks before touching implementation files, with logs:
+
+```sh
+set -o pipefail && make check-fmt 2>&1 | tee /tmp/7-2-7-fmt-base.out
+set -o pipefail && make lint 2>&1 | tee /tmp/7-2-7-lint-base.out
+set -o pipefail && make test 2>&1 | tee /tmp/7-2-7-test-base.out
+set -o pipefail && \
+  make kani-clone-detector 2>&1 | tee /tmp/7-2-7-kani-base.out
+```
+
+Expected result: all commands exit 0. If a baseline check fails before the
+implementation starts, inspect whether the failure is unrelated to existing
+state. Do not hide or work around it; record it in this plan and ask for
+direction if it blocks the work.
+
+Run:
+
+```sh
+coderabbit review --agent
+```
+
+Expected result: no concerns that block Milestone 2. Resolve or escalate every
+concern before proceeding.
+
+### Milestone 2: Strengthen ordinary regression coverage
+
+Update ordinary tests before adding Kani harnesses, so there is a concrete
+red/green regression net. The likely file is
+`crates/whitaker_clones_core/src/index/tests.rs`.
+
+Add `rstest`-based coverage for these cases if they are not already explicit
+enough:
+
+- Empty fingerprint slices return `Err(IndexError::EmptyFingerprintSet)`.
+- Two `MinHasher::new()` instances sketch the same fingerprints identically.
+- Duplicate `Fingerprint.hash` values with different ranges do not change the
+  signature.
+- Reordered unique hash sets produce identical signatures.
+
+The repository already has close coverage for these behaviours, so this
+milestone may be a small refactor from plain `#[test]` functions into
+parameterized `#[rstest]` cases rather than new behavioural assertions. Avoid
+rewriting tests just for style if the existing tests already communicate the
+contract clearly.
+
+Extend the `rstest-bdd` feature and harness only if an end-to-end behaviour gap
+remains after inspecting the existing scenarios. Candidate generation already
+exercises empty-input failure through `MinHasher::sketch`; add a new scenario
+only if duplicate-hash insensitivity or deterministic sketching is observable
+through candidate generation without making the feature file noisy.
+
+Validate this milestone:
+
+```sh
+set -o pipefail && make check-fmt 2>&1 | tee /tmp/7-2-7-fmt-tests.out
+set -o pipefail && make lint 2>&1 | tee /tmp/7-2-7-lint-tests.out
+set -o pipefail && make test 2>&1 | tee /tmp/7-2-7-test-tests.out
+coderabbit review --agent
+```
+
+Expected result: formatting, linting, and tests pass, and CodeRabbit has no
+unresolved concerns. Commit this milestone only after the gates pass.
+
+### Milestone 3: Add bounded Kani harnesses for MinHasher
+
+Extend `crates/whitaker_clones_core/src/index/kani.rs` with focused harnesses.
+Keep one property per harness, with names suitable for the explicit list in
+`scripts/run-kani.sh`.
+
+Recommended harness names:
+
+- `verify_min_hasher_sketch_rejects_empty_input`.
+- `verify_min_hasher_sketch_is_deterministic`.
+- `verify_min_hasher_sketch_ignores_duplicate_hashes`.
+
+Use helper functions in the Kani module if they improve clarity. A likely
+pattern is:
+
+```rust
+const MAX_SYMBOLIC_FINGERPRINTS: usize = 3;
+
+fn bounded_fingerprint_inputs() -> (
+    [Fingerprint; MAX_SYMBOLIC_FINGERPRINTS],
+    usize,
+) {
+    // Build a fixed-size symbolic array and an active length constrained with
+    // `kani::assume(active_len <= MAX_SYMBOLIC_FINGERPRINTS)`.
+}
+```
+
+The helper must create valid `Fingerprint` values through the real
+`Fingerprint::new(hash, range)` constructor. If symbolic ranges make the state
+space too large, use deterministic small ranges and keep the hash values
+symbolic; the invariant under proof is hash-set behaviour, not byte-range
+ordering.
+
+The deterministic harness should build two sketches from equivalent bounded
+inputs and assert that `values()` are equal. The duplicate-insensitivity
+harness should build one sketch from a bounded non-empty unique prefix and a
+second sketch from the same prefix plus a repeated hash value, then assert the
+signatures are equal. The empty-input harness should assert the exact
+`IndexError::EmptyFingerprintSet` error.
+
+Use explicit `#[kani::unwind(...)]` values. Start with the smallest practical
+bound that covers:
+
+- active-length construction,
+- Vec-backed dedup for the bounded retained fingerprints,
+- 128 signature slots, and
+- any helper loops used by the harness.
+
+The recorded proof-bound approval allowed unwind 129 for the fixed 128-slot
+signature-construction investigation; the shipped proof seam keeps the final
+MinHasher harnesses at unwind 4 while preserving that decision history.
+
+Update `scripts/run-kani.sh` so `run_clone_detector_harnesses` invokes the new
+MinHasher harness names after the existing `LshConfig` harnesses. This keeps
+`make kani-clone-detector` as the one supported entry point.
+
+Validate this milestone:
+
+```sh
+set -o pipefail && \
+  make kani-clone-detector 2>&1 | tee /tmp/7-2-7-kani-minhash.out
+set -o pipefail && make check-fmt 2>&1 | tee /tmp/7-2-7-fmt-minhash.out
+set -o pipefail && make lint 2>&1 | tee /tmp/7-2-7-lint-minhash.out
+set -o pipefail && make test 2>&1 | tee /tmp/7-2-7-test-minhash.out
+coderabbit review --agent
+```
+
+Expected result: the Kani output reports successful verification for all new
+MinHasher harnesses and the existing clone-detector harnesses; normal gates
+pass. Commit this milestone only after the gates pass.
+
+### Milestone 4: Update documentation
+
+Update `docs/whitaker-clone-detector-design.md` with an implementation decision
+section for 7.2.7. It should state:
+
+- the harnesses exercise `MinHasher::sketch` directly;
+- the proof bounds are intentionally small and bounded;
+- duplicate-hash insensitivity means duplicate `Fingerprint.hash` values are
+  collapsed before sketching, regardless of `Fingerprint` range; and
+- ordinary tests and behaviour scenarios remain the regression safety net.
+
+Update `docs/developers-guide.md` so the clone-detector proof workflow names
+the new MinHasher harness group or explains that `make kani-clone-detector` now
+covers both `LshConfig::new` and `MinHasher::sketch`.
+
+Do not update `docs/users-guide.md` unless implementation changes user-visible
+commands, output, configuration, or CLI behaviour. If it remains unchanged,
+record that decision in this plan's `Decision Log`.
+
+Validate Markdown:
+
+```sh
+set -o pipefail && make fmt 2>&1 | tee /tmp/fmt-whitaker-7-2-7-docs.out
+set -o pipefail && \
+  make markdownlint 2>&1 | tee /tmp/7-2-7-mdlint-docs.out
+set -o pipefail && make nixie 2>&1 | tee /tmp/nixie-whitaker-7-2-7-docs.out
+set -o pipefail && make check-fmt 2>&1 | tee /tmp/7-2-7-fmt-docs.out
+set -o pipefail && make lint 2>&1 | tee /tmp/lint-whitaker-7-2-7-docs.out
+set -o pipefail && make test 2>&1 | tee /tmp/test-whitaker-7-2-7-docs.out
+set -o pipefail && \
+  make kani-clone-detector 2>&1 | tee /tmp/7-2-7-kani-docs.out
+coderabbit review --agent
+```
+
+Expected result: documentation and normal gates pass. Commit this milestone
+only after the gates pass.
+
+### Milestone 5: Final gates, roadmap completion, and pull request
+
+Once code, tests, proofs, and documentation are complete, mark roadmap item
+7.2.7 done in `docs/roadmap.md` by changing its checkbox from `[ ]` to `[x]`.
+Do not mark 7.2.8 done.
+
+Run the final required gates:
+
+```sh
+set -o pipefail && make check-fmt 2>&1 | tee /tmp/7-2-7-fmt-final.out
+set -o pipefail && make lint 2>&1 | tee /tmp/7-2-7-lint-final.out
+set -o pipefail && make test 2>&1 | tee /tmp/7-2-7-test-final.out
+set -o pipefail && \
+  make kani-clone-detector 2>&1 | tee /tmp/7-2-7-kani-final.out
+set -o pipefail && make kani 2>&1 | tee /tmp/kani-whitaker-7-2-7-final.out
+coderabbit review --agent
+```
+
+If documentation changed, also run:
+
+```sh
+set -o pipefail && \
+  make markdownlint 2>&1 | tee /tmp/7-2-7-mdlint-final.out
+set -o pipefail && make nixie 2>&1 | tee /tmp/nixie-whitaker-7-2-7-final.out
+```
+
+Commit the roadmap update after gates pass. Push the branch:
+
+```sh
+git push
+```
+
+Record the Lody session reference:
+
+```sh
+echo ${LODY_SESSION_ID}
+```
+
+Create or update the draft pull request. The title must include the roadmap
+item as `(7.2.7)`, for example:
+
+```text
+Verify bounded MinHasher sketch invariants (7.2.7)
+```
+
+The pull request description must mention this ExecPlan document and include a
+`## References` section ending with:
+
+```text
+Lody session: https://lody.ai/leynos/sessions/${LODY_SESSION_ID}
+```
+
+## Acceptance criteria
+
+- `crates/whitaker_clones_core/src/index/kani.rs` contains Kani harnesses that
+  call the real `MinHasher::sketch` implementation and prove bounded
+  deterministic output, duplicate-hash insensitivity, and empty-input failure.
+- `scripts/run-kani.sh` includes the new harness names in the clone-detector
+  harness list.
+- `make kani-clone-detector` exits 0 and reports successful verification for
+  the MinHasher harnesses.
+- Unit tests using `rstest` cover the same externally meaningful
+  `MinHasher::sketch` contracts.
+- `rstest-bdd` behaviour coverage is added or explicitly documented as already
+  sufficient for externally observable candidate-generation behaviour.
+- `docs/whitaker-clone-detector-design.md` records the 7.2.7 proof decision.
+- `docs/developers-guide.md` documents the maintainer-facing Kani coverage.
+- `docs/users-guide.md` is updated only if user-visible behaviour changes; if
+  unchanged, the rationale is recorded in this plan.
+- `docs/roadmap.md` marks item 7.2.7 done after implementation is complete.
+- `make check-fmt`, `make lint`, and `make test` all succeed.
+- `coderabbit review --agent` has been run after each major milestone, and all
+  concerns have been cleared or explicitly escalated.
+
+## Rollback plan
+
+Each milestone should be committed separately after passing its gates. If a
+later milestone fails, use Git history to inspect or revert only the milestone
+commit that introduced the problem. Do not use `git reset --hard` or checkout
+away unrelated changes unless explicitly directed.
+
+If a Kani harness becomes intractable, revert only the Kani milestone commit,
+keep any independently useful tests or documentation only if they still pass
+the gates, and update this plan's `Decision Log` with the failed bound, runtime
+symptoms, and proposed alternative.
diff --git a/docs/roadmap.md b/docs/roadmap.md
index 2d59d088..120ebe95 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -386,7 +386,7 @@
   ordering and suppresses self-pairs. Requires 7.2.4. See
   [ADR 003](adr-003-formal-proof-strategy-for-clone-detector-pipeline.md) and
   [clone detector design](whitaker-clone-detector-design.md) §MinHash and LSH.
-- [ ] 7.2.7. Use Kani to verify bounded `MinHasher::sketch` invariants,
+- [x] 7.2.7. Use Kani to verify bounded `MinHasher::sketch` invariants,
   including deterministic output, duplicate-hash insensitivity, and empty-input
   failure. Requires 7.2.4. See
   [ADR 003](adr-003-formal-proof-strategy-for-clone-detector-pipeline.md) and
diff --git a/docs/whitaker-clone-detector-design.md b/docs/whitaker-clone-detector-design.md
index f9ceb957..dbd8906c 100644
--- a/docs/whitaker-clone-detector-design.md
+++ b/docs/whitaker-clone-detector-design.md
@@ -584,6 +584,36 @@ cargo whitaker clones report --in target/whitaker/clones.refined.sarif --html
    Runtime tests still pin the concrete lexical-string semantics; the proof
    does not verify Rust `String` internals directly.
 
+## Implementation decisions (7.2.7)
+
+1. **`MinHasher::sketch` now uses vector-backed set semantics.** The runtime
+   implementation collects retained `Fingerprint.hash` values into a
+   `Vec<u64>`, sorts them, and deduplicates them before sketching. This keeps
+   the public set-semantics contract from 7.2.2 while avoiding verifier-heavy
+   `BTreeSet` internals in the bounded Kani proof.
+
+2. **Kani verifies real `MinHasher::sketch` calls with a private proof seam.**
+   The harnesses use a `cfg(kani)`-only `MinHasher::from_seed_for_kani`
+   constructor so the proof does not spend its unwind bound constructing the
+   128-seed stream. Successful harnesses still call the production
+   `MinHasher::sketch` body; only the seed fixture and fixed-width signature
+   construction are specialized for Kani.
+
+3. **The bounded proof shape is deliberately split by invariant.** The empty
+   input harness checks that `MinHasher::sketch(&[])` returns
+   `IndexError::EmptyFingerprintSet`. The determinism harness sketches the
+   same one-fingerprint set twice and proves equality for an arbitrary symbolic
+   signature lane. The duplicate-hash harness keeps the retained hash symbolic
+   over a bounded `u8` domain and proves that repeating that hash at a distinct
+   range does not change the first signature lane.
+
+4. **Ordinary tests carry the broader regression surface.** Unit tests and the
+   `rstest-bdd` MinHash/LSH scenario cover full-signature equality,
+   representative full-width `u64` hashes, reordered inputs, empty input, and
+   duplicate retained hashes. The Kani harnesses provide exhaustive bounded
+   verification for the proof-shaped state spaces rather than replacing those
+   runtime regression tests.
+
 ## Minimal code skeletons (selected)
 
 ### Token to fingerprints to candidates
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
old mode 100644
new mode 100755
index e08d0d01..d3f3913c
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -46,7 +46,10 @@ run_clone_detector_harnesses() {
     for harness in \
         verify_lsh_config_new_smoke \
         verify_lsh_config_new_symbolic \
-        verify_lsh_config_new_overflow_product
+        verify_lsh_config_new_overflow_product \
+        verify_min_hasher_sketch_rejects_empty_input \
+        verify_min_hasher_sketch_is_deterministic \
+        verify_min_hasher_sketch_ignores_duplicate_hashes
     do
         "${CARGO_KANI_BIN}" kani \
             --manifest-path "${CLONE_DETECTOR_MANIFEST}" \