diff --git a/lib/mpf-write/MPF.hs b/lib/mpf-write/MPF.hs
index 91d70a8..0c1e546 100644
--- a/lib/mpf-write/MPF.hs
+++ b/lib/mpf-write/MPF.hs
@@ -19,6 +19,7 @@ module MPF
 
       -- * Re-exports from Proof
     , module MPF.Proof.Insertion
+    , module MPF.Proof.Exclusion
 
       -- * Re-exports from Backend
     , module MPF.Backend.Standalone
@@ -32,4 +33,5 @@ import MPF.Hashes.Aiken
 import MPF.Hashes.CBOR
 import MPF.Insertion
 import MPF.Interface
+import MPF.Proof.Exclusion
 import MPF.Proof.Insertion
diff --git a/lib/mpf-write/MPF/Hashes/Aiken.hs b/lib/mpf-write/MPF/Hashes/Aiken.hs
index d5eb456..e87c50f 100644
--- a/lib/mpf-write/MPF/Hashes/Aiken.hs
+++ b/lib/mpf-write/MPF/Hashes/Aiken.hs
@@ -125,7 +125,8 @@ encodeBranch branchJump (HexDigit pos) siblingHashes =
 -- | Encode a Fork step.
 --
 -- @skip@ = length of the fork's branch jump prefix.
--- Inner Neighbor: nibble (int), prefix (packed nibbles), root (32 bytes).
+-- Inner Neighbor: nibble (int), prefix (one byte per nibble),
+-- root (32 bytes).
 encodeFork
     :: HexKey -> HexDigit -> HexKey -> MPFHash -> Builder.Builder
 encodeFork branchJump (HexDigit nibble) neighborPrefix neighborRoot =
@@ -135,11 +136,20 @@ encodeFork branchJump (HexDigit nibble) neighborPrefix neighborRoot =
         <> cborTag 121
         <> listBegin
         <> cborUInt (fromIntegral nibble)
-        <> cborBytes (packHexKey neighborPrefix)
+        <> cborBytes (encodeNibblePrefix neighborPrefix)
         <> cborBytes (renderMPFHash neighborRoot)
         <> cborBreak
         <> cborBreak
 
+-- | Encode a fork prefix as one byte per nibble.
+--
+-- This matches the upstream JS/Aiken codec, where a prefix
+-- like @[1,2]@ becomes bytes @01 02@ rather than a single
+-- packed byte @12@.
+encodeNibblePrefix :: HexKey -> ByteString
+encodeNibblePrefix =
+    B.pack . map (\(HexDigit d) -> d)
+
 -- | Encode a Leaf step.
 --
 -- @skip@ = length of the leaf's branch jump prefix.
@@ -305,9 +315,15 @@ unpackFullKeyPath = concatMap byteToNibbles . B.unpack
         , HexDigit (b `mod` 16)
         ]
 
--- | Unpack nibble-packed prefix to HexKey
-unpackNibblePrefix :: ByteString -> HexKey
-unpackNibblePrefix = unpackFullKeyPath
+-- | Unpack a fork prefix encoded as one byte per nibble.
+unpackNibblePrefix :: ByteString -> Maybe HexKey
+unpackNibblePrefix =
+    mapM toNibble . B.unpack
+  where
+    toNibble :: Word8 -> Maybe HexDigit
+    toNibble w
+        | w < 16 = Just (HexDigit w)
+        | otherwise = Nothing
 
 -- | Parse a Branch step (after tag 121 and list begin)
 parseBranchStep :: Parser (MPFProofStep MPFHash)
@@ -357,12 +373,13 @@ parseForkStep bs = do
     (rootBS, bs6) <- parseCBORBytes bs5
     ((), bs7) <- parseBreak bs6
     ((), bs8) <- parseBreak bs7
+    neighborPrefix <- unpackNibblePrefix prefixBS
     let branchJump = replicate skip (HexDigit 0)
     Just
         ( ProofStepFork
             { psfBranchJump = branchJump
             , psfOurPosition = HexDigit 0
-            , psfNeighborPrefix = unpackNibblePrefix prefixBS
+            , psfNeighborPrefix = neighborPrefix
             , psfNeighborIndex = HexDigit (fromIntegral nibble)
             , psfMerkleRoot = MPFHash rootBS
             }
diff --git a/lib/mpf-write/MPF/Proof/Exclusion.hs b/lib/mpf-write/MPF/Proof/Exclusion.hs
new file mode 100644
index 0000000..01b2e04
--- /dev/null
+++ b/lib/mpf-write/MPF/Proof/Exclusion.hs
@@ -0,0 +1,504 @@
+{-# LANGUAGE StrictData #-}
+
+-- |
+-- Module      : MPF.Proof.Exclusion
+-- Description : MPF exclusion-proof generation and verification
+-- Copyright   : (c) Paolo Veronelli, 2024
+-- License     : Apache-2.0
+--
+-- Exclusion proofs for MPF keys. The populated proof variant reuses the
+-- existing 'MPFProofStep' structure so the current Aiken proof-step codec
+-- remains usable for exclusion mode too.
+module MPF.Proof.Exclusion
+    ( MPFExclusionProof (..)
+    , mpfExclusionProofSteps
+    , mkMPFExclusionProof
+    , foldMPFExclusionProof
+    , verifyMPFExclusionProof
+    ) where
+
+import Data.List (foldl', isPrefixOf)
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
+import Database.KV.Transaction
+    ( GCompare
+    , Selector
+    , Transaction
+    , query
+    )
+import MPF.Hashes (MPFHashing (..))
+import MPF.Interface
+    ( FromHexKV (..)
+    , HexDigit (..)
+    , HexIndirect (..)
+    , HexKey
+    , compareHexKeys
+    )
+import MPF.Proof.Insertion (MPFProofStep (..))
+
+-- | Exclusion proof for an MPF key.
+data MPFExclusionProof a
+    = MPFExclusionEmpty
+        { mpeTargetKey :: HexKey
+        }
+    | MPFExclusionWitness
+        { mpeTargetKey :: HexKey
+        , mpeProofSteps :: [MPFProofStep a]
+        }
+    deriving (Show, Eq)
+
+-- | Generate an exclusion proof for a key.
+mkMPFExclusionProof
+    :: (Monad m, GCompare d)
+    => HexKey
+    -> FromHexKV k v a
+    -> MPFHashing a
+    -> Selector d HexKey (HexIndirect a)
+    -> k
+    -> Transaction m cf d ops (Maybe (MPFExclusionProof a))
+mkMPFExclusionProof prefix FromHexKV{fromHexK} hashing sel k = do
+    let targetKey = fromHexK k
+    mRoot <- query sel prefix
+    case mRoot of
+        Nothing ->
+            pure
+                $ Just
+                    MPFExclusionEmpty
+                        { mpeTargetKey = targetKey
+                        }
+        Just root@HexIndirect{hexJump = rootJump, hexIsLeaf}
+            | hexIsLeaf -> do
+                mStep <-
+                    divergenceStep
+                        hashing
+                        sel
+                        prefix
+                        []
+                        targetKey
+                        root
+                pure $ mkWitness targetKey . pure <$> mStep
+            | not (rootJump `isPrefixOf` targetKey) -> do
+                mStep <-
+                    divergenceStep
+                        hashing
+                        sel
+                        prefix
+                        []
+                        targetKey
+                        root
+                pure $ mkWitness targetKey . pure <$> mStep
+            | otherwise ->
+                case drop (length rootJump) targetKey of
+                    [] -> pure Nothing
+                    remaining -> do
+                        mSteps <- go prefix [] rootJump remaining
+                        pure $ mkWitness targetKey <$> mSteps
+  where
+    mkWitness targetKey steps =
+        MPFExclusionWitness
+            { mpeTargetKey = targetKey
+            , mpeProofSteps = steps
+            }
+
+    go _ _ _ [] = pure Nothing
+    go dbPath logicalPath branchJump (x : ks) = do
+        let branchPath = dbPath <> branchJump
+        sibDetails <- fetchSiblingDetails sel branchPath x
+        mCurrentStep <-
+            buildBranchStep
+                hashing
+                sel
+                branchPath
+                logicalPath
+                branchJump
+                x
+                sibDetails
+        case mCurrentStep of
+            Nothing -> pure Nothing
+            Just currentStep -> do
+                mChild <- query sel (branchPath <> [x])
+                case mChild of
+                    Nothing ->
+                        pure $ Just [currentStep]
+                    Just child@HexIndirect{hexJump = childJump, hexIsLeaf}
+                        | childJump `isPrefixOf` ks ->
+                            case drop (length childJump) ks of
+                                []
+                                    | hexIsLeaf -> pure Nothing
+                                    | otherwise -> pure Nothing
+                                rest -> do
+                                    mRest <-
+                                        go
+                                            (branchPath <> [x])
+                                            (logicalPath <> branchJump <> [x])
+                                            childJump
+                                            rest
+                                    pure $ fmap (++ [currentStep]) mRest
+                        | otherwise -> do
+                            let childPath = branchPath <> [x]
+                                childLogicalPath =
+                                    logicalPath <> branchJump <> [x]
+                            mTerminal <-
+                                divergenceStep
+                                    hashing
+                                    sel
+                                    childPath
+                                    childLogicalPath
+                                    ks
+                                    child
+                            pure $ fmap (: [currentStep]) mTerminal
+
+-- | View an exclusion proof as the shared Aiken / JS proof-step list.
+--
+-- Empty-tree exclusion uses the same transport shape as upstream:
+-- an empty proof-step list verified in exclusion mode.
+mpfExclusionProofSteps
+    :: MPFExclusionProof a -> [MPFProofStep a]
+mpfExclusionProofSteps MPFExclusionEmpty{} = []
+mpfExclusionProofSteps MPFExclusionWitness{mpeProofSteps} =
+    mpeProofSteps
+
+-- | Fold an exclusion proof to the trusted root hash.
+foldMPFExclusionProof
+    :: MPFHashing a -> MPFExclusionProof a -> Maybe a
+foldMPFExclusionProof _ MPFExclusionEmpty{} = Nothing
+foldMPFExclusionProof
+    hashing
+    MPFExclusionWitness{mpeProofSteps} =
+        foldl' (step hashing) Nothing mpeProofSteps
+
+-- | Verify an exclusion proof against a trusted root.
+verifyMPFExclusionProof
+    :: Eq a
+    => MPFHashing a
+    -> Maybe a
+    -> MPFExclusionProof a
+    -> Bool
+verifyMPFExclusionProof
+    hashing
+    trustedRoot
+    proof@MPFExclusionEmpty{} =
+        trustedRoot == foldMPFExclusionProof hashing proof
+verifyMPFExclusionProof
+    hashing
+    trustedRoot
+    proof@MPFExclusionWitness{mpeTargetKey, mpeProofSteps} =
+        proofMatchesTarget mpeTargetKey mpeProofSteps
+            && trustedRoot
+                == foldMPFExclusionProof hashing proof
+
+proofMatchesTarget
+    :: HexKey -> [MPFProofStep a] -> Bool
+proofMatchesTarget targetKey steps = go targetKey (reverse steps)
+  where
+    go _ [] = True
+    go key (proofStep : rest) = case consumeStep key proofStep of
+        Just key' -> go key' rest
+        Nothing -> False
+
+consumeStep
+    :: HexKey -> MPFProofStep a -> Maybe HexKey
+consumeStep key proofStep = do
+    let (jump, position) = case proofStep of
+            ProofStepBranch{psbJump, psbPosition} ->
+                (psbJump, psbPosition)
+            ProofStepLeaf{pslBranchJump, pslOurPosition} ->
+                (pslBranchJump, pslOurPosition)
+            ProofStepFork{psfBranchJump, psfOurPosition} ->
+                (psfBranchJump, psfOurPosition)
+    if jump `isPrefixOf` key
+        then case drop (length jump) key of
+            d : ds | d == position -> Just ds
+            _ -> Nothing
+        else Nothing
+
+step :: MPFHashing a -> Maybe a -> MPFProofStep a -> Maybe a
+step hashing acc proofStep = case proofStep of
+    ProofStepBranch{psbJump, psbPosition, psbSiblingHashes} ->
+        Just
+            $ branchHash
+                hashing
+                psbJump
+                ( merkleRoot
+                    hashing
+                    [ if HexDigit n == psbPosition
+                        then acc
+                        else
+                            Map.lookup
+                                (HexDigit n)
+                                (Map.fromList psbSiblingHashes)
+                    | n <- [0 .. 15]
+                    ]
+                )
+    ProofStepLeaf
+        { pslBranchJump
+        , pslOurPosition
+        , pslNeighborNibble
+        , pslNeighborSuffix
+        , pslNeighborValueDigest
+        } ->
+            let neighborHash =
+                    leafHash
+                        hashing
+                        pslNeighborSuffix
+                        pslNeighborValueDigest
+            in  case acc of
+                    Nothing ->
+                        Just
+                            $ leafHash
+                                hashing
+                                ( pslBranchJump
+                                    <> [pslNeighborNibble]
+                                    <> pslNeighborSuffix
+                                )
+                                pslNeighborValueDigest
+                    Just subtreeHash ->
+                        Just
+                            $ branchHash
+                                hashing
+                                pslBranchJump
+                                ( merkleRoot
+                                    hashing
+                                    [ if HexDigit n == pslOurPosition
+                                        then Just subtreeHash
+                                        else
+                                            if HexDigit n
+                                                == pslNeighborNibble
+                                                then Just neighborHash
+                                                else Nothing
+                                    | n <- [0 .. 15]
+                                    ]
+                                )
+    ProofStepFork
+        { psfBranchJump
+        , psfOurPosition
+        , psfNeighborPrefix
+        , psfNeighborIndex
+        , psfMerkleRoot
+        } ->
+            let neighborHash =
+                    branchHash
+                        hashing
+                        psfNeighborPrefix
+                        psfMerkleRoot
+            in  case acc of
+                    Nothing ->
+                        Just
+                            $ branchHash
+                                hashing
+                                ( psfBranchJump
+                                    <> [psfNeighborIndex]
+                                    <> psfNeighborPrefix
+                                )
+                                psfMerkleRoot
+                    Just subtreeHash ->
+                        Just
+                            $ branchHash
+                                hashing
+                                psfBranchJump
+                                ( merkleRoot
+                                    hashing
+                                    [ if HexDigit n == psfOurPosition
+                                        then Just subtreeHash
+                                        else
+                                            if HexDigit n
+                                                == psfNeighborIndex
+                                                then Just neighborHash
+                                                else Nothing
+                                    | n <- [0 .. 15]
+                                    ]
+                                )
+
+buildBranchStep
+    :: (Monad m, GCompare d)
+    => MPFHashing a
+    -> Selector d HexKey (HexIndirect a)
+    -> HexKey
+    -> HexKey
+    -> HexKey
+    -> HexDigit
+    -> Map HexDigit (HexIndirect a)
+    -> Transaction m cf d ops (Maybe (MPFProofStep a))
+buildBranchStep
+    hashing
+    sel
+    branchPath
+    logicalPath
+    branchJump
+    x
+    sibDetails =
+        case Map.toList sibDetails of
+            [] -> pure Nothing
+            [ ( d
+                    , HexIndirect
+                        { hexJump = sibSuffix
+                        , hexValue = sibVal
+                        , hexIsLeaf = True
+                        }
+                    )
+                ] ->
+                    pure
+                        $ Just
+                            ProofStepLeaf
+                                { pslBranchJump = branchJump
+                                , pslOurPosition = x
+                                , pslNeighborKeyPath =
+                                    logicalPath
+                                        <> branchJump
+                                        <> [d]
+                                        <> sibSuffix
+                                , pslNeighborNibble = d
+                                , pslNeighborSuffix = sibSuffix
+                                , pslNeighborValueDigest = sibVal
+                                }
+            [ ( d
+                    , HexIndirect
+                        { hexJump = sibPrefix
+                        , hexIsLeaf = False
+                        }
+                    )
+                ] -> do
+                    mr <-
+                        fetchBranchMerkleRoot
+                            hashing
+                            sel
+                            (branchPath <> [d])
+                            sibPrefix
+                    pure
+                        $ Just
+                            ProofStepFork
+                                { psfBranchJump = branchJump
+                                , psfOurPosition = x
+                                , psfNeighborPrefix = sibPrefix
+                                , psfNeighborIndex = d
+                                , psfMerkleRoot = mr
+                                }
+            nonEmpty ->
+                pure
+                    $ Just
+                        ProofStepBranch
+                            { psbJump = branchJump
+                            , psbPosition = x
+                            , psbSiblingHashes =
+                                [ (d, computeNodeHash hashing hi)
+                                | (d, hi) <- nonEmpty
+                                ]
+                            }
+
+divergenceStep
+    :: (Monad m, GCompare d)
+    => MPFHashing a
+    -> Selector d HexKey (HexIndirect a)
+    -> HexKey
+    -> HexKey
+    -> HexKey
+    -> HexIndirect a
+    -> Transaction m cf d ops (Maybe (MPFProofStep a))
+divergenceStep
+    hashing
+    sel
+    dbPath
+    logicalPath
+    targetKey
+    HexIndirect
+        { hexJump = witnessJump
+        , hexValue = witnessValue
+        , hexIsLeaf
+        } =
+        case splitDivergence targetKey witnessJump of
+            Nothing -> pure Nothing
+            Just (common, ourNibble, witnessNibble, witnessSuffix) ->
+                if hexIsLeaf
+                    then
+                        pure
+                            $ Just
+                                ProofStepLeaf
+                                    { pslBranchJump = common
+                                    , pslOurPosition = ourNibble
+                                    , pslNeighborKeyPath =
+                                        logicalPath <> witnessJump
+                                    , pslNeighborNibble = witnessNibble
+                                    , pslNeighborSuffix = witnessSuffix
+                                    , pslNeighborValueDigest =
+                                        witnessValue
+                                    }
+                    else do
+                        mr <-
+                            fetchBranchMerkleRoot
+                                hashing
+                                sel
+                                dbPath
+                                witnessJump
+                        pure
+                            $ Just
+                                ProofStepFork
+                                    { psfBranchJump = common
+                                    , psfOurPosition = ourNibble
+                                    , psfNeighborPrefix = witnessSuffix
+                                    , psfNeighborIndex = witnessNibble
+                                    , psfMerkleRoot = mr
+                                    }
+
+splitDivergence
+    :: HexKey
+    -> HexKey
+    -> Maybe (HexKey, HexDigit, HexDigit, HexKey)
+splitDivergence targetKey witnessKey =
+    case compareHexKeys targetKey witnessKey of
+        (common, ourNibble : _, witnessNibble : witnessSuffix) ->
+            Just
+                ( common
+                , ourNibble
+                , witnessNibble
+                , witnessSuffix
+                )
+        _ -> Nothing
+
+fetchSiblingDetails
+    :: (Monad m, GCompare d)
+    => Selector d HexKey (HexIndirect a)
+    -> HexKey
+    -> HexDigit
+    -> Transaction m cf d ops (Map HexDigit (HexIndirect a))
+fetchSiblingDetails sel pfx exclude = do
+    pairs <- mapM fetchOne digits
+    pure
+        $ Map.fromList
+            [(d, hi) | (d, Just hi) <- pairs]
+  where
+    digits =
+        [ HexDigit n
+        | n <- [0 .. 15]
+        , HexDigit n /= exclude
+        ]
+
+    fetchOne d = do
+        mi <- query sel (pfx <> [d])
+        pure (d, mi)
+
+fetchBranchMerkleRoot
+    :: (Monad m, GCompare d)
+    => MPFHashing a
+    -> Selector d HexKey (HexIndirect a)
+    -> HexKey
+    -> HexKey
+    -> Transaction m cf d ops a
+fetchBranchMerkleRoot
+    hashing'@MPFHashing{merkleRoot}
+    sel
+    nodePath
+    nodeJump = do
+        children <- mapM fetchChild [HexDigit n | n <- [0 .. 15]]
+        pure $ merkleRoot children
+      where
+        fetchChild d = do
+            mi <- query sel (nodePath <> nodeJump <> [d])
+            pure $ fmap (computeNodeHash hashing') mi
+
+computeNodeHash :: MPFHashing a -> HexIndirect a -> a
+computeNodeHash
+    MPFHashing{leafHash}
+    HexIndirect{hexJump, hexValue, hexIsLeaf} =
+        if hexIsLeaf
+            then leafHash hexJump hexValue
+            else hexValue
diff --git a/mts.cabal b/mts.cabal
index ea6fbdd..20092f8 100644
--- a/mts.cabal
+++ b/mts.cabal
@@ -158,6 +158,7 @@ library csmt-write
     CSMT.Proof.Insertion
 
   build-depends:
+    , async                                    >=2.2  && <2.3
     , base                                     >=4.19 && <5
     , bytestring                               >=0.12 && <0.13
     , cborg                                    >=0.2  && <0.3
@@ -271,6 +272,7 @@ library mpf-write
     MPF.Interface
     MPF.MTS
     MPF.Proof.Completeness
+    MPF.Proof.Exclusion
     MPF.Proof.Insertion
 
   build-depends:
@@ -313,6 +315,7 @@ library mpf
     , MPF.Interface
     , MPF.MTS
     , MPF.Proof.Completeness
+    , MPF.Proof.Exclusion
     , MPF.Proof.Insertion
 
   build-depends:
@@ -322,6 +325,7 @@ library mpf
     , mts
     , mts:mpf-write
     , rocksdb-haskell-jprupp                   >=2.1  && <2.2
+    , rocksdb-kv-transactions                  >=0.1  && <0.2
     , rocksdb-kv-transactions:kv-transactions
     , transformers                             >=0.6  && <0.7
     , unliftio                                 >=0.2  && <0.3
@@ -487,6 +491,7 @@ test-suite unit-tests
     MPF.InsertionSpec
     MPF.InterfaceSpec
     MPF.NamespaceSpec
+    MPF.Proof.ExclusionSpec
     MPF.Proof.InsertionSpec
     MPF.ProofCompatSpec
     MPF.PropertySpec
diff --git a/specs/004-mpf-wasm-write-demo/exclusion-proof-handoff.md b/specs/004-mpf-wasm-write-demo/exclusion-proof-handoff.md
index 9de7187..6fd4e6b 100644
--- a/specs/004-mpf-wasm-write-demo/exclusion-proof-handoff.md
+++ b/specs/004-mpf-wasm-write-demo/exclusion-proof-handoff.md
@@ -7,32 +7,47 @@ This handoff is for the missing MPF exclusion-proof path needed by
 
 Dedicated blocker issue:
 
-- [#148](https://github.com/lambdasistemi/haskell-mts/issues/148) -
-  `Add MPF exclusion proof generation and verification`
+- [#149](https://github.com/lambdasistemi/haskell-mts/issues/149) -
+  `Add MPF exclusion proofs with Aiken proof-format parity`
+
+This note previously pointed at `#148`. Use `#149` as the canonical
+parallel handoff issue because it captures the upstream Aiken / JS parity
+constraints in detail.
 
 Current status on this branch:
 
 - Phase 1 is done: MPF hashes were rerouted through the pure Blake2b path.
 - Phase 2 is done: `mpf-write` was split out as the pure sublibrary.
+- `#149` core proof work is now in progress on this worktree:
+  - first-class `MPFExclusionProof`
+  - generator for absent keys
+  - pure verifier
+  - shared proof-step projection for Aiken / JS transport
+  - proof-spec parity with CSMT for both inclusion and exclusion
+    including QuickCheck-style property coverage
+  - pinned upstream JS exclusion parity vector (`melon`)
 - PR checkpoint: [#147](https://github.com/lambdasistemi/haskell-mts/pull/147)
 - Verified checkpoint commit: `f4d3201`
 
-The remaining browser/WASM mirror work from `#146` is blocked on a real
-MPF exclusion-proof API. The CSMT write demo protocol already expects the
-response envelope to carry `ptype = 0 / 1 / 0xff`, where `1` is exclusion.
+The remaining browser/WASM mirror work from `#146` is no longer blocked
+on the pure MPF proof design. The remaining gap is routing that proof
+through the shared MTS/browser interface. The CSMT write demo protocol
+already expects the response envelope to carry `ptype = 0 / 1 / 0xff`,
+where `1` is exclusion.
 
 ## What Already Exists
 
 ### MPF inclusion proofs
 
-- Generator: [lib/mpf-write/MPF/Proof/Insertion.hs](/code/haskell-mts-issue-146/lib/mpf-write/MPF/Proof/Insertion.hs:115)
-- Verifier: [lib/mpf-write/MPF/Proof/Insertion.hs](/code/haskell-mts-issue-146/lib/mpf-write/MPF/Proof/Insertion.hs:468)
-- MTS wiring: [lib/mpf-write/MPF/MTS.hs](/code/haskell-mts-issue-146/lib/mpf-write/MPF/MTS.hs:271)
+- Generator: [lib/mpf-write/MPF/Proof/Insertion.hs](/code/haskell-mts-issue-149/lib/mpf-write/MPF/Proof/Insertion.hs:115)
+- Verifier: [lib/mpf-write/MPF/Proof/Insertion.hs](/code/haskell-mts-issue-149/lib/mpf-write/MPF/Proof/Insertion.hs:468)
+- MTS wiring: [lib/mpf-write/MPF/MTS.hs](/code/haskell-mts-issue-149/lib/mpf-write/MPF/MTS.hs:271)
 
 Important current behavior:
 
 - `mkMPFInclusionProof` is membership-only.
-- Missing keys do not produce a first-class witness proof.
+- Missing keys do not produce a first-class witness proof through the
+  old inclusion API.
 - `verifyMPFInclusionProof` requires a value and checks membership only.
 
 ### Aiken inclusion-proof parity
@@ -42,7 +57,7 @@ is intended to match the Aiken / off-chain reference bytes.
 
 Primary codec:
 
-- [lib/mpf-write/MPF/Hashes/Aiken.hs](/code/haskell-mts-issue-146/lib/mpf-write/MPF/Hashes/Aiken.hs:1)
+- [lib/mpf-write/MPF/Hashes/Aiken.hs](/code/haskell-mts-issue-149/lib/mpf-write/MPF/Hashes/Aiken.hs:1)
 
 Concrete format constraints already encoded there:
 
@@ -56,12 +71,13 @@ Concrete format constraints already encoded there:
 
 Existing parity tests:
 
-- [test/MPF/Hashes/AikenSpec.hs](/code/haskell-mts-issue-146/test/MPF/Hashes/AikenSpec.hs:36)
-- [test/MPF/ProofCompatSpec.hs](/code/haskell-mts-issue-146/test/MPF/ProofCompatSpec.hs:1)
+- [test/MPF/Hashes/AikenSpec.hs](/code/haskell-mts-issue-149/test/MPF/Hashes/AikenSpec.hs:36)
+- [test/MPF/ProofCompatSpec.hs](/code/haskell-mts-issue-149/test/MPF/ProofCompatSpec.hs:1)
 
 What those tests already guarantee:
 
-- Exact byte parity for known upstream JS vectors (`mango`, `kumquat`).
+- Exact byte parity for known upstream JS vectors (`mango`,
+  `kumquat`, `melon` exclusion).
 - Round-trip parse/render for all 30 fruit proofs.
 - Constructor-shape preservation through parse/render.
 
@@ -70,30 +86,30 @@ What those tests already guarantee:
 CSMT already has the full exclusion-proof stack:
 
 - Proof type and CBOR codec:
-  [lib/csmt-core/CSMT/Core/CBOR.hs](/code/haskell-mts-issue-146/lib/csmt-core/CSMT/Core/CBOR.hs:118)
+  [lib/csmt-core/CSMT/Core/CBOR.hs](/code/haskell-mts-issue-149/lib/csmt-core/CSMT/Core/CBOR.hs:118)
 - Write-side generator:
-  [lib/csmt-write/CSMT/Proof/Exclusion.hs](/code/haskell-mts-issue-146/lib/csmt-write/CSMT/Proof/Exclusion.hs:1)
+  [lib/csmt-write/CSMT/Proof/Exclusion.hs](/code/haskell-mts-issue-149/lib/csmt-write/CSMT/Proof/Exclusion.hs:1)
 - Browser write protocol using `ptype = 0 / 1`:
-  [app/csmt-write-wasm/Main.hs](/code/haskell-mts-issue-146/app/csmt-write-wasm/Main.hs:290)
-  and [verifiers/browser-write/write.js](/code/haskell-mts-issue-146/verifiers/browser-write/write.js:256)
+  [app/csmt-write-wasm/Main.hs](/code/haskell-mts-issue-149/app/csmt-write-wasm/Main.hs:290)
+  and [verifiers/browser-write/write.js](/code/haskell-mts-issue-149/verifiers/browser-write/write.js:256)
 
 There is also an earlier product spec for CSMT exclusion proofs:
 
-- [specs/002-exclusion-proof/spec.md](/code/haskell-mts-issue-146/specs/002-exclusion-proof/spec.md:1)
+- [specs/002-exclusion-proof/spec.md](/code/haskell-mts-issue-149/specs/002-exclusion-proof/spec.md:1)
 
 ## What Is Missing
 
-There is no MPF equivalent yet for:
+There is still no MPF equivalent yet for:
 
-- a first-class exclusion-proof type
-- an exclusion-proof generator for absent keys
-- a pure verifier for non-membership
-- a stable serialized wire format for exclusion proofs
 - MTS-level routing that can distinguish inclusion from exclusion
+- browser write-path plumbing that emits `ptype = 1`
+- transport-level handling of the explicit empty-tree witness in the
+  higher-level protocol
 
-Right now, absent keys effectively collapse to "no proof":
+The pure proof API is now present, but absent keys still collapse to
+"no proof" at the MTS layer:
 
-- [test/MPF/Proof/InsertionSpec.hs](/code/haskell-mts-issue-146/test/MPF/Proof/InsertionSpec.hs:45)
+- [test/MPF/Proof/InsertionSpec.hs](/code/haskell-mts-issue-149/test/MPF/Proof/InsertionSpec.hs:45)
 
 ## Research Constraint: Aiken Proof Format Parity
 
@@ -140,6 +156,9 @@ Implication for the Haskell work:
   verifiable in exclusion mode.
 - The browser/WASM protocol can still carry `ptype = 1`; that tag can stay
   outside the proof bytes, matching the current demo envelope design.
+- On this branch, the pure API now exposes the shared step-list view via
+  `mpfExclusionProofSteps`; empty-tree exclusion maps to `[]`, so the
+  existing `renderAikenProof` transport can still be used.
 
 ## Likely Witness Material Already Present
 
@@ -152,14 +171,14 @@ shape to make non-membership plausible:
 
 Relevant code:
 
-- [lib/mpf-write/MPF/Proof/Insertion.hs](/code/haskell-mts-issue-146/lib/mpf-write/MPF/Proof/Insertion.hs:47)
+- [lib/mpf-write/MPF/Proof/Insertion.hs](/code/haskell-mts-issue-149/lib/mpf-write/MPF/Proof/Insertion.hs:47)
 
 That does not mean an exclusion proof already exists. It only means there
 is likely reusable witness structure for designing one.
 
 ## Expected Deliverables
 
-1. Track implementation in [#148](https://github.com/lambdasistemi/haskell-mts/issues/148).
+1. Track implementation in [#149](https://github.com/lambdasistemi/haskell-mts/issues/149).
 2. Define an MPF exclusion-proof type with at least:
    - empty-tree case
    - populated-tree witness case
diff --git a/specs/005-mpf-exclusion-proof-aiken-parity/plan.md b/specs/005-mpf-exclusion-proof-aiken-parity/plan.md
new file mode 100644
index 0000000..c661011
--- /dev/null
+++ b/specs/005-mpf-exclusion-proof-aiken-parity/plan.md
@@ -0,0 +1,66 @@
+# Implementation Plan: MPF Exclusion Proofs with Aiken Parity
+
+## Design Choice
+
+Use a dedicated Haskell exclusion-proof type, but keep the proof payload
+itself on the existing `MPFProofStep` constructors. This preserves the
+current Aiken proof-step codec while avoiding a broad `MTS.Interface`
+change in the first patch.
+
+## Proof Model
+
+```haskell
+data MPFExclusionProof a
+  = MPFExclusionEmpty { mpeTargetKey :: HexKey }
+  | MPFExclusionWitness
+      { mpeTargetKey :: HexKey
+      , mpeProofSteps :: [MPFProofStep a]
+      }
+```
+
+The wire-format constraint is satisfied because the serializable payload
+for populated proofs remains `mpeProofSteps`.
+
+## Generation Strategy
+
+Walk the existing trie while following the target key:
+
+1. No root: return `MPFExclusionEmpty`
+2. Root jump diverges: synthesize a terminal `Fork` or `Leaf` proof step
+   describing the existing root as the witness
+3. Existing branch path matches:
+   - missing child: finish with a `Branch` step
+   - child jump diverges: finish with a terminal `Fork` or `Leaf` step
+   - child jump matches: recurse and append the current branch step
+4. Exact existing leaf path: return `Nothing`
+
+## Verification Strategy
+
+Verification has two checks:
+
+1. The target key must be structurally compatible with the proof path
+2. Folding the proof in exclusion mode must reproduce the trusted root
+
+The fold carries `Maybe a` for the target subtree:
+
+- `Nothing` means "the target subtree is absent here"
+- `Just h` means "a deeper witness subtree reconstructed to node hash `h`"
+
+`Leaf` and `Fork` steps collapse to the single neighbor node when the
+target subtree is absent. `Branch` steps rebuild the branch root with the
+target position left empty.
+
+## Scope Of First Patch
+
+- Create spec artifacts for `#149`
+- Add `MPF.Proof.Exclusion`
+- Add focused unit tests in the pure backend
+- Expose the new module through `mpf-write`, `mpf`, and the MPF test lib
+
+## Deferred Work
+
+- Widen `MTS.Interface` so inclusion and exclusion can share a top-level
+  proof type
+- Thread `ptype = 1` through `MPF.MTS` and the browser/WASM write path
+- Add explicit upstream JS exclusion vectors once the core proof shape is
+  stable
diff --git a/specs/005-mpf-exclusion-proof-aiken-parity/spec.md b/specs/005-mpf-exclusion-proof-aiken-parity/spec.md
new file mode 100644
index 0000000..af90d11
--- /dev/null
+++ b/specs/005-mpf-exclusion-proof-aiken-parity/spec.md
@@ -0,0 +1,132 @@
+# Feature Specification: MPF Exclusion Proofs with Aiken Parity
+
+**Feature Branch**: `feat/mpf-exclusion-proof-aiken-parity`
+**Created**: 2026-04-22
+**Status**: Draft
+**Input**: User description: "Implement
+`lambdasistemi/haskell-mts#149` on top of the `mpf-write` layout from
+PR `#147`."
+
+## User Scenarios & Testing *(mandatory)*
+
+### User Story 1 - Prove an absent MPF key (Priority: P1)
+
+A library consumer wants to prove that a key is absent from an MPF trie
+without inventing a second proof-step wire format. They request an
+exclusion proof for an absent key and verify it against a trusted root.
+
+**Why this priority**: This is the blocker for `#146`'s `ptype = 1`
+browser/WASM path.
+
+**Independent Test**: Insert known keys, generate an exclusion proof for
+an absent key, and verify it against the current root.
+
+**Acceptance Scenarios**:
+
+1. **Given** a populated trie and an absent key, **When** exclusion proof
+   generation runs, **Then** it returns a proof instead of `Nothing`.
+2. **Given** a valid exclusion proof and trusted root, **When**
+   verification runs, **Then** it succeeds without needing tree access.
+3. **Given** a valid exclusion proof, **When** its proof steps are
+   serialized with the existing Aiken proof-step codec, **Then** the
+   bytes remain parseable by the current step parser.
+
+---
+
+### User Story 2 - Handle empty trees and present keys correctly (Priority: P2)
+
+A library consumer needs clean behavior at the two boundary cases:
+empty trees and keys that are actually present.
+
+**Why this priority**: These are the easiest ways to return a proof that
+lies.
+
+**Independent Test**: Generate proof on an empty trie and on a present
+key.
+
+**Acceptance Scenarios**:
+
+1. **Given** an empty trie, **When** exclusion proof generation runs,
+   **Then** it returns an explicit empty-tree proof.
+2. **Given** an empty-tree proof, **When** verification runs against an
+   empty root, **Then** it succeeds.
+3. **Given** a present key, **When** exclusion proof generation runs,
+   **Then** it returns `Nothing`.
+
+---
+
+### User Story 3 - Reject tampered exclusion proofs (Priority: P2)
+
+A verifier receives an exclusion proof whose target key or proof steps
+have been modified.
+
+**Why this priority**: The proof is only useful if tampering is
+detectable.
+
+**Independent Test**: Generate a valid proof, modify the target key or a
+proof step, and ensure verification fails.
+
+**Acceptance Scenarios**:
+
+1. **Given** a valid exclusion proof, **When** the target key is swapped,
+   **Then** verification fails.
+2. **Given** a valid exclusion proof, **When** a proof step is modified,
+   **Then** verification fails.
+
+## Edge Cases
+
+- Empty trie
+- Divergence inside the root jump
+- Missing child at a branch with multiple siblings
+- Divergence inside a compressed child jump
+- Terminal witness leaf
+- Terminal witness branch
+
+## Requirements *(mandatory)*
+
+### Functional Requirements
+
+- **FR-001**: The MPF library MUST provide a first-class exclusion-proof
+  API for absent keys.
+- **FR-002**: The exclusion-proof API MUST reuse the existing
+  `MPFProofStep` structure rather than inventing a second step encoding.
+- **FR-003**: The exclusion verifier MUST be pure and operate on trusted
+  root plus proof data only.
+- **FR-004**: The exclusion verifier MUST reject proofs whose path does
+  not match the claimed target key.
+- **FR-005**: Exclusion proof generation MUST return `Nothing` for
+  present keys.
+- **FR-006**: Empty trees MUST have an explicit exclusion-proof variant.
+- **FR-007**: The existing inclusion Aiken proof-step rendering MUST stay
+  unchanged for inclusion proofs.
+- **FR-008**: The resulting proof steps MUST remain serializable through
+  the current Aiken step codec so the `ptype = 1` browser/WASM envelope
+  can keep carrying step bytes out-of-band.
+
+### Key Entities
+
+- **MPFExclusionProof**: Proof that a target key is absent. It is either
+  an empty-tree witness or a populated proof carrying the target key plus
+  shared `MPFProofStep` data.
+- **Shared proof steps**: Existing `ProofStepBranch`, `ProofStepFork`,
+  and `ProofStepLeaf` constructors reused for exclusion mode.
+
+## Success Criteria *(mandatory)*
+
+### Measurable Outcomes
+
+- **SC-001**: Absent-key exclusion proofs verify successfully against the
+  current root.
+- **SC-002**: Present keys do not produce exclusion proofs.
+- **SC-003**: Empty-tree exclusion proofs verify only against an empty
+  root.
+- **SC-004**: Tampered target keys or tampered proof steps are rejected.
+- **SC-005**: Existing inclusion Aiken proof-step tests remain green
+  unchanged.
+
+## Assumptions
+
+- The first implementation slice may stop at the pure MPF proof API and
+  direct tests, before widening `MTS.Interface` and the browser protocol.
+- The current work targets the fixed-path `mpf-write` code layout from PR
+  `#147`.
diff --git a/specs/005-mpf-exclusion-proof-aiken-parity/tasks.md b/specs/005-mpf-exclusion-proof-aiken-parity/tasks.md
new file mode 100644
index 0000000..1747105
--- /dev/null
+++ b/specs/005-mpf-exclusion-proof-aiken-parity/tasks.md
@@ -0,0 +1,34 @@
+# Tasks: MPF Exclusion Proofs with Aiken Parity
+
+**Input**: Design documents from
+`/specs/005-mpf-exclusion-proof-aiken-parity/`
+**Prerequisites**: `plan.md`, `spec.md`
+
+## Phase 1: Core Proof API
+
+- [x] T001 Create `lib/mpf-write/MPF/Proof/Exclusion.hs` with
+  `MPFExclusionProof`, `mkMPFExclusionProof`, `foldMPFExclusionProof`,
+  and `verifyMPFExclusionProof`.
+- [x] T002 Expose `MPF.Proof.Exclusion` through `mts.cabal` and the `MPF`
+  re-export surface.
+- [x] T003 Extend `MPF.Test.Lib` with helpers for building and verifying
+  exclusion proofs in the pure backend.
+
+## Phase 2: Focused Tests
+
+- [x] T004 Add `test/MPF/Proof/ExclusionSpec.hs`.
+- [x] T005 Cover empty-tree exclusion, present-key rejection, root/leaf
+  divergence, branch missing-child exclusion, and tamper rejection.
+- [x] T006 Keep the current inclusion Aiken proof-step tests green.
+
+## Phase 3: Follow-on Integration
+
+- [ ] T007 Widen the MTS/browser-facing proof API so MPF exclusion proofs
+  can flow into the `ptype = 1` WASM protocol from `#146`.
+- [x] T008 Add explicit upstream JS/Aiken exclusion vectors once the core
+  proof shape is stable.
+
+## Verification
+
+- [x] T009 Run focused MPF unit tests
+- [x] T010 Run formatting on touched files
diff --git a/test-lib/mpf/MPF/Test/Lib.hs b/test-lib/mpf/MPF/Test/Lib.hs
index 1056bc0..01634d2 100644
--- a/test-lib/mpf/MPF/Test/Lib.hs
+++ b/test-lib/mpf/MPF/Test/Lib.hs
@@ -37,8 +37,11 @@ module MPF.Test.Lib
 
       -- * Proof Utilities
     , proofMPFM
+    , proofExcludeMPFM
     , verifyMPFM
+    , verifyExcludeMPFM
     , MPFProof
+    , MPFExclusionProof
     , MPFProofStep (..)
     , foldMPFProof
 
@@ -93,6 +96,11 @@ import MPF.Interface
     , byteStringToHexKey
     , hexKeyPrism
     )
+import MPF.Proof.Exclusion
+    ( MPFExclusionProof
+    , mkMPFExclusionProof
+    , verifyMPFExclusionProof
+    )
 import MPF.Proof.Insertion
     ( MPFProof
     , MPFProofStep (..)
@@ -284,6 +292,17 @@ proofMPFMAt prefix k =
             MPFStandaloneMPFCol
             k
 
+-- | Generate an exclusion proof for a key in the Pure monad
+proofExcludeMPFM
+    :: HexKey -> MPFPure (Maybe (MPFExclusionProof MPFHash))
+proofExcludeMPFM =
+    runTransactionUnguarded (mpfPureDatabase mpfHashCodecs)
+        . mkMPFExclusionProof
+            []
+            fromHexKVIdentity
+            mpfHashing
+            MPFStandaloneMPFCol
+
 -- | Verify a membership proof for a key-value pair in the Pure monad
 verifyMPFM :: HexKey -> MPFHash -> MPFPure Bool
 verifyMPFM = verifyMPFMAt []
@@ -310,6 +329,19 @@ verifyMPFMAt prefix k v =
                     v
                     proof
 
+-- | Verify an exclusion proof for a key in the Pure monad.
+verifyExcludeMPFM :: HexKey -> MPFPure Bool
+verifyExcludeMPFM k = do
+    mProof <- proofExcludeMPFM k
+    trustedRoot <- getRootHashM
+    pure $ case mProof of
+        Nothing -> False
+        Just proof ->
+            verifyMPFExclusionProof
+                mpfHashing
+                trustedRoot
+                proof
+
 -- | Get the root hash from the MPF trie
 getRootHashM :: MPFPure (Maybe MPFHash)
 getRootHashM = getRootHashMAt []
diff --git a/test/MPF/Proof/ExclusionSpec.hs b/test/MPF/Proof/ExclusionSpec.hs
new file mode 100644
index 0000000..bc2fd69
--- /dev/null
+++ b/test/MPF/Proof/ExclusionSpec.hs
@@ -0,0 +1,237 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module MPF.Proof.ExclusionSpec (spec) where
+
+import Data.ByteString qualified as B
+import Data.List (nub)
+import Data.Maybe (isJust)
+import Data.Word (Word8)
+import MPF.Hashes (MPFHash, mkMPFHash, mpfHashing)
+import MPF.Hashes.Aiken (parseAikenProof, renderAikenProof)
+import MPF.Interface (HexDigit (..), HexKey, byteStringToHexKey)
+import MPF.Proof.Exclusion
+    ( MPFExclusionProof (..)
+    , foldMPFExclusionProof
+    , mpfExclusionProofSteps
+    , verifyMPFExclusionProof
+    )
+import MPF.Proof.Insertion (MPFProofStep (..))
+import MPF.Test.Lib
+    ( getRootHashM
+    , insertMPFM
+    , proofExcludeMPFM
+    , runMPFPure'
+    , verifyExcludeMPFM
+    )
+import Test.Hspec
+import Test.QuickCheck
+    ( Gen
+    , Property
+    , choose
+    , counterexample
+    , elements
+    , forAll
+    , property
+    , vectorOf
+    , (===)
+    )
+
+exclusionProofFor
+    :: [(HexKey, MPFHash)]
+    -> HexKey
+    -> (Maybe (MPFExclusionProof MPFHash), Maybe MPFHash)
+exclusionProofFor inserts targetKey =
+    fst $ runMPFPure' $ do
+        mapM_ (uncurry insertMPFM) inserts
+        proof <- proofExcludeMPFM targetKey
+        root <- getRootHashM
+        pure (proof, root)
+
+isWitness :: Maybe (MPFExclusionProof a) -> Bool
+isWitness (Just MPFExclusionWitness{}) = True
+isWitness _ = False
+
+genHexDigit :: Gen HexDigit
+genHexDigit =
+    HexDigit . fromIntegral <$> choose (0, 15 :: Int)
+
+genFixedKey :: Int -> Gen [HexDigit]
+genFixedKey n = vectorOf n genHexDigit
+
+genTreeAndAbsentKey :: Gen ([HexKey], HexKey)
+genTreeAndAbsentKey = do
+    numKeys <- choose (2, 10)
+    keys <- nub <$> vectorOf numKeys (genFixedKey 16)
+    absent <- genFixedKey 16
+    if length keys < 2 || absent `elem` keys
+        then genTreeAndAbsentKey
+        else pure (keys, absent)
+
+genValueHash :: Gen MPFHash
+genValueHash =
+    mkMPFHash . B.pack <$> vectorOf 8 genWord8
+  where
+    genWord8 :: Gen Word8
+    genWord8 = fromIntegral <$> choose (0, 255 :: Int)
+
+genInserts :: [HexKey] -> Gen [(HexKey, MPFHash)]
+genInserts keys =
+    zip keys <$> vectorOf (length keys) genValueHash
+
+spec :: Spec
+spec = describe "MPF.Proof.Exclusion" $ do
+    it "builds an explicit empty-tree proof" $ do
+        let target = byteStringToHexKey "absent"
+            ((mProof, trustedRoot), _) = runMPFPure' $ do
+                proof <- proofExcludeMPFM target
+                root <- getRootHashM
+                pure (proof, root)
+        trustedRoot `shouldBe` Nothing
+        case mProof of
+            Just proof@MPFExclusionEmpty{} -> do
+                foldMPFExclusionProof mpfHashing proof `shouldBe` Nothing
+                parseAikenProof
+                    (renderAikenProof (mpfExclusionProofSteps proof))
+                    `shouldBe` Just []
+                verifyMPFExclusionProof
+                    mpfHashing
+                    trustedRoot
+                    proof
+                    `shouldBe` True
+            _ -> expectationFailure "Expected MPFExclusionEmpty"
+
+    it "returns Nothing for a present key" $ do
+        let key = byteStringToHexKey "hello"
+            value = mkMPFHash "world"
+            (mProof, _) = runMPFPure' $ do
+                insertMPFM key value
+                proofExcludeMPFM key
+        mProof `shouldBe` Nothing
+
+    it "verifies exclusion for a single-leaf divergence" $ do
+        let witnessKey = byteStringToHexKey "hello"
+            targetKey = byteStringToHexKey "hullo"
+            value = mkMPFHash "world"
+            ((mProof, trustedRoot), _) = runMPFPure' $ do
+                insertMPFM witnessKey value
+                proof <- proofExcludeMPFM targetKey
+                root <- getRootHashM
+                pure (proof, root)
+        case mProof of
+            Just proof@MPFExclusionWitness{} -> do
+                verifyMPFExclusionProof
+                    mpfHashing
+                    trustedRoot
+                    proof
+                    `shouldBe` True
+                parseAikenProof
+                    (renderAikenProof (mpfExclusionProofSteps proof))
+                    `shouldSatisfy` isJust
+            _ -> expectationFailure "Expected populated exclusion proof"
+
+    it "verifies exclusion for a missing child under a branch" $ do
+        let keyA = [HexDigit 1, HexDigit 1]
+            keyB = [HexDigit 1, HexDigit 2]
+            keyC = [HexDigit 1, HexDigit 4]
+            targetKey = [HexDigit 1, HexDigit 3, HexDigit 5]
+            valueA = mkMPFHash "a"
+            valueB = mkMPFHash "b"
+            valueC = mkMPFHash "c"
+            ((mProof, verified), _) = runMPFPure' $ do
+                insertMPFM keyA valueA
+                insertMPFM keyB valueB
+                insertMPFM keyC valueC
+                proof <- proofExcludeMPFM targetKey
+                ok <- verifyExcludeMPFM targetKey
+                pure (proof, ok)
+        verified `shouldBe` True
+        case mProof of
+            Just MPFExclusionWitness{mpeProofSteps = [ProofStepBranch{}]} ->
+                pure ()
+            _ -> expectationFailure "Expected a terminal Branch exclusion step"
+
+    it "rejects a tampered target key" $ do
+        let witnessKey = byteStringToHexKey "hello"
+            targetKey = byteStringToHexKey "hullo"
+            tamperedKey = byteStringToHexKey "hello"
+            value = mkMPFHash "world"
+            ((mProof, trustedRoot), _) = runMPFPure' $ do
+                insertMPFM witnessKey value
+                proof <- proofExcludeMPFM targetKey
+                root <- getRootHashM
+                pure (proof, root)
+        case mProof of
+            Just proof@MPFExclusionWitness{} ->
+                verifyMPFExclusionProof
+                    mpfHashing
+                    trustedRoot
+                    proof{mpeTargetKey = tamperedKey}
+                    `shouldBe` False
+            _ -> expectationFailure "Expected populated exclusion proof"
+
+    describe "property tests" $ do
+        it "absent key always produces a verifiable proof"
+            $ property propAbsentKeyProves
+
+        it "present key always returns Nothing"
+            $ property propPresentKeyFails
+
+        it "tampered target key fails verification"
+            $ property propTamperedTargetFails
+
+propAbsentKeyProves :: Property
+propAbsentKeyProves =
+    forAll genTreeAndAbsentKey $ \(keys, absent) ->
+        forAll (genInserts keys) $ \inserts ->
+            let (result, trustedRoot) =
+                    exclusionProofFor inserts absent
+            in  counterexample
+                    ( "keys="
+                        ++ show keys
+                        ++ " absent="
+                        ++ show absent
+                        ++ " result="
+                        ++ show (isWitness result)
+                        ++ " root="
+                        ++ show trustedRoot
+                    )
+                    $ case result of
+                        Just proof ->
+                            verifyMPFExclusionProof
+                                mpfHashing
+                                trustedRoot
+                                proof
+                                === True
+                        Nothing ->
+                            property False
+
+propPresentKeyFails :: Property
+propPresentKeyFails =
+    forAll genTreeAndAbsentKey $ \(keys, _) ->
+        forAll (genInserts keys) $ \inserts ->
+            forAll (elements keys) $ \present ->
+                fst (exclusionProofFor inserts present)
+                    === Nothing
+
+propTamperedTargetFails :: Property
+propTamperedTargetFails =
+    forAll genTreeAndAbsentKey $ \(keys, absent) ->
+        forAll (genInserts keys) $ \inserts ->
+            forAll (elements keys) $ \present ->
+                let (result, trustedRoot) =
+                        exclusionProofFor inserts absent
+                in  counterexample
+                        ( "present="
+                            ++ show present
+                            ++ " absent="
+                            ++ show absent
+                        )
+                        $ case result of
+                            Just proof@MPFExclusionWitness{} ->
+                                verifyMPFExclusionProof
+                                    mpfHashing
+                                    trustedRoot
+                                    proof{mpeTargetKey = present}
+                                    === False
+                            _ ->
+                                property False
diff --git a/test/MPF/Proof/InsertionSpec.hs b/test/MPF/Proof/InsertionSpec.hs
index 897a314..1e2a18c 100644
--- a/test/MPF/Proof/InsertionSpec.hs
+++ b/test/MPF/Proof/InsertionSpec.hs
@@ -2,10 +2,11 @@
 
 module MPF.Proof.InsertionSpec (spec) where
 
-import Control.Monad (forM_)
+import Control.Monad (forM, forM_)
 import Data.ByteString qualified as B
+import Data.List (nub)
 import MPF.Hashes (mkMPFHash, mpfHashing, renderMPFHash)
-import MPF.Interface (HexDigit (..), byteStringToHexKey)
+import MPF.Interface (HexDigit (..), HexKey, byteStringToHexKey)
 import MPF.Test.Lib
     ( deleteMPFM
     , foldMPFProof
@@ -17,6 +18,100 @@ import MPF.Test.Lib
     , verifyMPFM
     )
 import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy)
+import Test.QuickCheck
+    ( Gen
+    , Property
+    , choose
+    , elements
+    , forAll
+    , listOf
+    , vectorOf
+    )
+
+genHexDigit :: Gen HexDigit
+genHexDigit =
+    HexDigit . fromIntegral <$> choose (0, 15 :: Int)
+
+genFixedHexKey :: Int -> Gen HexKey
+genFixedHexKey n = vectorOf n genHexDigit
+
+fullTreeKeys :: Int -> [HexKey]
+fullTreeKeys depth =
+    sequence
+        ( replicate
+            depth
+            [HexDigit (fromIntegral n) | n <- [0 .. 15 :: Int]]
+        )
+
+genSparseKeys :: Int -> Gen [HexKey]
+genSparseKeys n = do
+    keys <- nub <$> vectorOf n (genFixedHexKey 16)
+    if length keys < max 8 (n `div` 2)
+        then genSparseKeys n
+        else pure keys
+
+valueFor :: Int -> B.ByteString
+valueFor n =
+    B.pack
+        [ fromIntegral (n `div` 256)
+        , fromIntegral (n `mod` 256)
+        ]
+
+testRandomFactsInAFullTree :: Property
+testRandomFactsInAFullTree =
+    forAll (elements [1, 2]) $ \depth ->
+        let kvs =
+                [ (key, mkMPFHash (valueFor ix))
+                | (ix, key) <- zip [1 ..] (fullTreeKeys depth)
+                ]
+        in  forAll
+                (listOf $ elements [0 .. length kvs - 1])
+                $ \indices ->
+                    let (results, _) = runMPFPure' $ do
+                            forM_ kvs $ uncurry insertMPFM
+                            forM indices $ \ix -> do
+                                let (testKey, testValue) = kvs !! ix
+                                verifyMPFM testKey testValue
+                    in  all id results
+
+testRandomFactsInASparseTree :: Property
+testRandomFactsInASparseTree =
+    forAll (choose (16, 96 :: Int)) $ \n ->
+        forAll (genSparseKeys n) $ \keys ->
+            let kvs =
+                    [ (key, mkMPFHash (valueFor ix))
+                    | (ix, key) <- zip [1 ..] keys
+                    ]
+            in  forAll
+                    (listOf $ elements [0 .. length kvs - 1])
+                    $ \indices ->
+                        let (results, _) = runMPFPure' $ do
+                                forM_ kvs $ uncurry insertMPFM
+                                forM indices $ \ix -> do
+                                    let (testKey, testValue) = kvs !! ix
+                                    verifyMPFM testKey testValue
+                        in  all id results
+
+testRandomDeletedFactsInASparseTree :: Property
+testRandomDeletedFactsInASparseTree =
+    forAll (choose (32, 128 :: Int)) $ \n ->
+        forAll (genSparseKeys n) $ \keys ->
+            let kvs =
+                    [ (key, mkMPFHash (valueFor ix))
+                    | (ix, key) <- zip [1 ..] keys
+                    ]
+            in  forAll
+                    (listOf $ elements [0 .. length kvs - 1])
+                    $ \indices ->
+                        let results =
+                                [ fst $ runMPFPure' $ do
+                                    forM_ kvs $ uncurry insertMPFM
+                                    let (testKey, testValue) = kvs !! ix
+                                    deleteMPFM testKey
+                                    verifyMPFM testKey testValue
+                                | ix <- indices
+                                ]
+                        in  all not results
 
 spec :: Spec
 spec = do
@@ -192,3 +287,16 @@ spec = do
                             wrongValue = mkMPFHash "not-apple"
                         verifyMPFM appleKey wrongValue
                 verified `shouldBe` False
+
+        describe "property tests" $ do
+            it
+                "verifies random facts in a full tree"
+                testRandomFactsInAFullTree
+
+            it
+                "verifies random facts in a sparse tree"
+                testRandomFactsInASparseTree
+
+            it
+                "rejects random deleted facts in a sparse tree"
+                testRandomDeletedFactsInASparseTree
diff --git a/test/MPF/ProofCompatSpec.hs b/test/MPF/ProofCompatSpec.hs
index 35f9979..3ca2dfd 100644
--- a/test/MPF/ProofCompatSpec.hs
+++ b/test/MPF/ProofCompatSpec.hs
@@ -1,8 +1,9 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
 
 -- | Comprehensive proof CBOR compatibility test.
 -- Verifies renderAikenProof round-trips correctly for all 30 fruits
--- and matches known JS vectors for mango and kumquat.
+-- and matches known JS vectors for inclusion and exclusion proofs.
 module MPF.ProofCompatSpec (spec) where
 
 import Control.Monad (forM_)
@@ -10,11 +11,16 @@ import Data.ByteString (ByteString)
 import MPF.Hashes (MPFHash, mkMPFHash, renderMPFHash)
 import MPF.Hashes.Aiken (parseAikenProof, renderAikenProof)
 import MPF.Interface (byteStringToHexKey)
+import MPF.Proof.Exclusion
+    ( MPFExclusionProof (..)
+    , mpfExclusionProofSteps
+    )
 import MPF.Proof.Insertion (MPFProof (..))
 import MPF.Test.Lib
     ( encodeHex
     , fruitsTestData
     , insertByteStringM
+    , proofExcludeMPFM
     , proofMPFM
     , runMPFPure'
     )
@@ -27,6 +33,22 @@ fruitProof fruitKey =
         let hexKey = byteStringToHexKey $ renderMPFHash $ mkMPFHash fruitKey
         proofMPFM hexKey
 
+fruitExclusionProof
+    :: ByteString -> Maybe (MPFExclusionProof MPFHash)
+fruitExclusionProof fruitKey =
+    fst $ runMPFPure' $ do
+        forM_ fruitsTestData $ uncurry insertByteStringM
+        let hexKey = byteStringToHexKey $ renderMPFHash $ mkMPFHash fruitKey
+        proofExcludeMPFM hexKey
+
+melonExclusionExpectedHex :: ByteString
+melonExclusionExpectedHex =
+    "9fd8799f005f5840c7bfa4472f3a98ebe0421e8f3f03adf0f7c4340dec65b4b92b1c9f0bed209eb47238ba5d16031b6bace4aee22156f5028b0ca56dc24f7247d6435292e82c039c58403490a825d2e8deddf8679ce2f95f7e3a59d9c3e1af4a49b410266d21c9344d6d08434fd717aea47d156185d589f44a59fc2e0158eab7ff035083a2a66cd3e15bffffd8799f005f5840922f17e88cc74f89e0a135af20ae55ed0cac3c74f2b948bb9bc249bda9a759dd985c311e6afc57389e6f1e94796c920f142b867df4dd9304b3b6bbcfe5972c2958400eb923b0cbd24df54401d998531feead35a47a99f4deed205de4af81120f97610000000000000000000000000000000000000000000000000000000000000000ffffff"
+
+peachExpectedHex :: ByteString
+peachExpectedHex =
+    "9fd8799f005f58404be28f4839135e1f8f5372a90b54bb7bfaf997a5d13711bb4d7d93f9d4e04fbefa63eb4576001d8658219f928172eccb5448b4d7d62cd6d95228e13ebcbd53505840be527bcfc7febe3c560057d97f4190bd24b537a322315f84daafab3ada562b50da0bdb30bf45c76153418a634f1bcecba8c601ca985fbca14b57582920d82acbffffd87a9f00d8799f0f42010258202f6b320212dd98c38a7cd074886d942d9577cdad5ef1c72d32a01df1a63ed88fffffff"
+
 spec :: Spec
 spec = describe "Proof CBOR compatibility" $ do
     describe "all 30 fruit proofs render and round-trip via Aiken CBOR"
@@ -62,3 +84,27 @@ spec = describe "Proof CBOR compatibility" $ do
                 Just proof ->
                     encodeHex (renderAikenProof (mpfProofSteps proof))
                         `shouldBe` "9fd8799f005f5840c7bfa4472f3a98ebe0421e8f3f03adf0f7c4340dec65b4b92b1c9f0bed209eb47238ba5d16031b6bace4aee22156f5028b0ca56dc24f7247d6435292e82c039c58403490a825d2e8deddf8679ce2f95f7e3a59d9c3e1af4a49b410266d21c9344d6d08434fd717aea47d156185d589f44a59fc2e0158eab7ff035083a2a66cd3e15bffffd87a9f00d8799f0041075820a1ffbc0e72342b41129e2d01d289809079b002e54b123860077d2d66added281ffffff"
+
+        -- Generated from the canonical upstream off-chain implementation.
+        -- This catches fork-prefix encoding regressions that mango/kumquat miss.
+        it "peach proof matches upstream CBOR" $ do
+            case fruitProof "peach[uid: 0]" of
+                Nothing -> expectationFailure "No peach proof"
+                Just proof ->
+                    encodeHex (renderAikenProof (mpfProofSteps proof))
+                        `shouldBe` peachExpectedHex
+
+        it "melon exclusion proof matches JS CBOR" $ do
+            case fruitExclusionProof "melon" of
+                Just proof@MPFExclusionWitness{} ->
+                    encodeHex
+                        ( renderAikenProof
+                            (mpfExclusionProofSteps proof)
+                        )
+                        `shouldBe` melonExclusionExpectedHex
+                Just MPFExclusionEmpty{} ->
+                    expectationFailure
+                        "Unexpected empty-tree exclusion proof"
+                Nothing ->
+                    expectationFailure
+                        "No exclusion proof for melon"