diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,35 @@
 ## [Unreleased]
 
 
+## [0.5.0.0] — 2026-07-31
+
+### Added
+
+- `Natural` now has a pinned `CanonicalTypeName` and belongs to the curated
+  symbolic equality/ordering registry. Its unbounded integer representation is
+  constrained non-negative whenever Keiki allocates a symbolic variable.
+- `Sym.constrainSymDomain` lets refined scalar instances state the validity
+  invariant for their solver representation. `symFree`, structural register
+  and input reads, field projections, and opaque term fallbacks all apply it.
+
+### Changed
+
+- `Natural` is deliberately absent from the symbolic arithmetic registry.
+  Haskell subtraction on `Natural` throws `Underflow` when its mathematical
+  result would be negative, whereas ordinary SMT integer subtraction returns
+  that negative value.
+- The opt-in opaque-guard audit now reports `TArith` whose carrier is absent
+  from the symbolic numeric registry, including `Natural` arithmetic.
+- The fast pure overlap validator treats `Natural` as the exact integral
+  interval `[0, infinity)`, so it can find non-literal interior witnesses.
+- The `OpaqueGuard` warning detail no longer names `TApp` specifically, since
+  the audit now covers unsupported `TArith` carriers too. Consumers asserting
+  on the exact message text will need to update.
+- PVP major bump: the `Sym` class definition gained `constrainSymDomain`. The
+  method has a default, so existing hand-written instances continue to compile
+  unchanged.
+
+
 ## [0.4.0.0] — 2026-07-28
 
 ### Added
diff --git a/keiki.cabal b/keiki.cabal
--- a/keiki.cabal
+++ b/keiki.cabal
@@ -1,6 +1,6 @@
 cabal-version:   3.0
 name:            keiki
-version:         0.4.0.0
+version:         0.5.0.0
 synopsis:        Pure core for symbolic-register transducer event sourcing.
 description:
   A Haskell library for the pure core of event sourcing, workflow
diff --git a/src/Keiki/Core.hs b/src/Keiki/Core.hs
--- a/src/Keiki/Core.hs
+++ b/src/Keiki/Core.hs
@@ -220,8 +220,10 @@
 import Keiki.Internal.SymbolicTypes
   ( discoverSymbolicType,
     symbolicTypeSupportsEquality,
+    symbolicTypeSupportsNumeric,
     symbolicTypeSupportsOrdering,
   )
+import Numeric.Natural (Natural)
 import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))
 
 -- | A register slot is a label paired with the type of its value.
@@ -2049,13 +2051,12 @@
       { tvwEdge :: EdgeRef s,
         tvwDetail :: String
       }
-  | -- | An edge whose guard contains an opaque 'TApp' term. The symbolic
-    --       single-valuedness and dead-edge analyses translate such a term to an
-    --       unconstrained free variable ('Keiki.Symbolic.translateTermSym' emits
-    --       @SBV.free "app1"@), so they cannot see through the guard and silently
-    --       under-verify it. Most often this is a collection-content condition
-    --       (membership, "all resolved", size) lifted through a closure because the
-    --       structural predicate language has no node for it; see the user guide and
+  | -- | An edge whose guard contains a term the symbolic translator must make
+    --       opaque. This includes 'TApp' closures and 'TArith' at a carrier outside
+    --       the symbolic numeric registry (for example 'Natural'). The solver uses
+    --       a fresh domain-valid variable for such a term, so the result remains
+    --       sound but loses precision. Most opaque guards are collection-content
+    --       conditions lifted through a closure; see the user guide and
     --       @docs\/plans\/60-first-class-collection-registers-design-gated.md@ for the
     --       options. Advisory, not a soundness error: opt in via 'warnOpaqueGuards'.
     OpaqueGuard
@@ -2103,9 +2104,9 @@
     -- | run the (structural) dead-edge check
     checkReachability :: Bool,
     -- | run the opaque-guard audit (opt-in; default off). Flags edges whose
-    --     guard branches on an opaque 'TApp' term the symbolic analyses cannot
-    --     see through. Off by default so 'defaultValidationOptions' keeps its
-    --     meaning for existing consumers.
+    --     guard branches on a 'TApp' term or unsupported symbolic 'TArith'
+    --     carrier the analyses cannot see through. Off by default so
+    --     'defaultValidationOptions' keeps its meaning for existing consumers.
     warnOpaqueGuards :: Bool,
     -- | require the first emitted event to recover every command field used
     --     by replay
@@ -2242,17 +2243,27 @@
 
 -- ** Opaque-guard diagnostics
 
--- | Does the term contain an opaque 'TApp1'\/'TApp2' anywhere? Mirrors the
--- structural recursion of 'termReadsInput'; 'TArith' is transparent, so it
--- recurses into its operands rather than counting as opaque.
-termHasOpaqueApp :: Term rs ci ifs r -> Bool
-termHasOpaqueApp (TLit _) = False
-termHasOpaqueApp (TReg _) = False
-termHasOpaqueApp (TInpCtorField _ _) = False
-termHasOpaqueApp (TApp1 _ _) = True
-termHasOpaqueApp (TApp2 _ _ _) = True
-termHasOpaqueApp (TArith _ a b) = termHasOpaqueApp a || termHasOpaqueApp b
-termHasOpaqueApp TFieldProj {} = False
+-- | Does the term contain a node that becomes an opaque symbolic variable?
+-- 'TApp1'\/'TApp2' are always opaque. 'TArith' is structural only when its
+-- carrier belongs to the symbolic numeric registry; otherwise the translator
+-- deliberately falls back to a fresh domain-valid value.
+termHasOpaqueFallback :: forall rs ci ifs r. Term rs ci ifs r -> Bool
+termHasOpaqueFallback (TLit _) = False
+termHasOpaqueFallback (TReg _) = False
+termHasOpaqueFallback (TInpCtorField _ _) = False
+termHasOpaqueFallback (TApp1 _ _) = True
+termHasOpaqueFallback (TApp2 _ _ _) = True
+termHasOpaqueFallback (TArith _ a b) =
+  not carrierSupportsNumeric
+    || termHasOpaqueFallback a
+    || termHasOpaqueFallback b
+  where
+    carrierSupportsNumeric =
+      maybe
+        False
+        symbolicTypeSupportsNumeric
+        (discoverSymbolicType @r)
+termHasOpaqueFallback TFieldProj {} = False
 
 -- | Does the guard predicate branch on an opaque term anywhere? The symbolic
 -- analyses cannot see through such a guard (it becomes a free SBV variable),
@@ -2263,15 +2274,15 @@
 predHasOpaqueTerm (PAnd p q) = predHasOpaqueTerm p || predHasOpaqueTerm q
 predHasOpaqueTerm (POr p q) = predHasOpaqueTerm p || predHasOpaqueTerm q
 predHasOpaqueTerm (PNot p) = predHasOpaqueTerm p
-predHasOpaqueTerm (PEq a b) = termHasOpaqueApp a || termHasOpaqueApp b
+predHasOpaqueTerm (PEq a b) = termHasOpaqueFallback a || termHasOpaqueFallback b
 predHasOpaqueTerm (PInCtor _) = False
 predHasOpaqueTerm PLeftArm = False
 predHasOpaqueTerm PRightArm = False
-predHasOpaqueTerm (PCmp _ a b) = termHasOpaqueApp a || termHasOpaqueApp b
+predHasOpaqueTerm (PCmp _ a b) = termHasOpaqueFallback a || termHasOpaqueFallback b
 
 -- | The opt-in opaque-guard audit (run by 'validateTransducer' only when
 -- 'warnOpaqueGuards' is set). For every edge whose guard contains an opaque
--- 'TApp' term, emit an 'OpaqueGuard' warning locating the edge by its typed
+-- term fallback, emit an 'OpaqueGuard' warning locating the edge by its typed
 -- 'EdgeRef'. Specialised to the 'HsPred' carrier because it walks the predicate
 -- AST, exactly as 'validateTransducer' is.
 opaqueGuardWarnings ::
@@ -2282,8 +2293,8 @@
   [ OpaqueGuard
       { tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},
         tvwDetail =
-          "guard contains an opaque TApp term the symbolic analyses cannot "
-            ++ "see through; its single-valuedness was not verified"
+          "guard contains a term the symbolic analyses translate opaquely; "
+            ++ "its single-valuedness was not verified"
       }
   | s <- [minBound .. maxBound],
     (n, e) <- zip [(0 :: Int) ..] (edgesOut t s),
@@ -3004,6 +3015,8 @@
 discoverIntegralDomain
   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Integer) =
       Just (IntegralDomain id Nothing Nothing)
+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Natural) =
+      Just (IntegralDomain toInteger (Just 0) Nothing)
   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int) =
       Just (boundedIntegralDomain @Int)
   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word8) =
diff --git a/src/Keiki/Internal/SymbolicTypes.hs b/src/Keiki/Internal/SymbolicTypes.hs
--- a/src/Keiki/Internal/SymbolicTypes.hs
+++ b/src/Keiki/Internal/SymbolicTypes.hs
@@ -20,6 +20,7 @@
 import Data.Time (UTCTime)
 import Data.Typeable (Typeable)
 import Data.Word (Word16, Word32, Word64, Word8)
+import Numeric.Natural (Natural)
 import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))
 
 -- | Evidence that a type belongs to Keiki's closed symbolic registry.
@@ -27,6 +28,7 @@
   SymbolicBool :: SymbolicType Bool
   SymbolicInt :: SymbolicType Int
   SymbolicInteger :: SymbolicType Integer
+  SymbolicNatural :: SymbolicType Natural
   SymbolicText :: SymbolicType Text
   SymbolicUTCTime :: SymbolicType UTCTime
   SymbolicWord64 :: SymbolicType Word64
@@ -42,6 +44,7 @@
   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Bool) = Just SymbolicBool
   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int) = Just SymbolicInt
   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Integer) = Just SymbolicInteger
+  | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Natural) = Just SymbolicNatural
   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Text) = Just SymbolicText
   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @UTCTime) = Just SymbolicUTCTime
   | Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word64) = Just SymbolicWord64
diff --git a/src/Keiki/Shape.hs b/src/Keiki/Shape.hs
--- a/src/Keiki/Shape.hs
+++ b/src/Keiki/Shape.hs
@@ -63,6 +63,7 @@
 import GHC.Generics qualified as G
 import GHC.TypeLits (KnownSymbol, symbolVal)
 import Keiki.Core (Slot)
+import Numeric.Natural (Natural)
 import Type.Reflection
   ( SomeTypeRep (..),
     TypeRep,
@@ -123,6 +124,9 @@
 
 instance CanonicalTypeName Integer where
   canonicalTypeName _ = T.pack "Integer"
+
+instance CanonicalTypeName Natural where
+  canonicalTypeName _ = T.pack "Natural"
 
 instance CanonicalTypeName Word where
   canonicalTypeName _ = T.pack "Word"
diff --git a/src/Keiki/Symbolic.hs b/src/Keiki/Symbolic.hs
--- a/src/Keiki/Symbolic.hs
+++ b/src/Keiki/Symbolic.hs
@@ -18,7 +18,7 @@
 -- Milestones implemented in this revision (through M5 of EP-2):
 --
 --   * The 'Sym' typeclass and instances for 'Bool', 'Int', 'Integer',
---     'Text', 'UTCTime', and the fixed-width integers 'Word8' \/
+--     'Natural', 'Text', 'UTCTime', and the fixed-width integers 'Word8' \/
 --     'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/ 'Int64' (the
 --     last group added by EP-41 so money and count registers are
 --     solver-visible).
@@ -112,6 +112,7 @@
   ( SymbolicType (..),
     discoverSymbolicType,
   )
+import Numeric.Natural (Natural)
 import System.IO.Unsafe (unsafePerformIO)
 import Type.Reflection (SomeTypeRep (..), eqTypeRep, typeRep, type (:~~:) (HRefl))
 
@@ -137,6 +138,12 @@
   fromSym :: SymRep a -> a
   symDefault :: a
 
+  -- | Restrict a symbolic representation to values that denote a real @a@.
+  -- Most carriers use their whole SBV domain. Refined carriers such as
+  -- 'Natural' add constraints whenever Keiki allocates a symbolic variable.
+  constrainSymDomain :: SBV.SBV (SymRep a) -> SBV.Symbolic ()
+  constrainSymDomain _ = pure ()
+
 instance Sym Bool where
   type SymRep Bool = Bool
   toSym = id
@@ -149,6 +156,19 @@
   fromSym = id
   symDefault = 0
 
+-- | Arbitrary-precision non-negative integers. The representation stays an
+-- unbounded SMT integer, while every allocated variable is constrained to the
+-- actual 'Natural' domain. Numeric arithmetic is deliberately not registered:
+-- Haskell 'Natural' subtraction throws @Underflow@ when its mathematical result
+-- would be negative, while ordinary SMT integer subtraction returns that negative
+-- integer. Treating the operations as identical would not preserve concrete behavior.
+instance Sym Natural where
+  type SymRep Natural = Integer
+  toSym = fromIntegral
+  fromSym = fromInteger
+  symDefault = 0
+  constrainSymDomain value = SBV.constrain (value SBV..>= 0)
+
 -- | Encoded as 'Integer'. SBV does not provide an 'SInt'-of-arbitrary-
 -- size; using 'Integer' means machine-width 'Int' wraparound is not modeled.
 -- Guards whose truth depends on 'Int' overflow should use an explicit
@@ -234,7 +254,7 @@
 
 -- | Try to discover a 'Sym' instance for @r@ at runtime. Returns
 -- @Just SymDict@ for any of the curated supported types
--- ('Bool', 'Int', 'Integer', 'Text', 'UTCTime', and the fixed-width
+-- ('Bool', 'Int', 'Integer', 'Natural', 'Text', 'UTCTime', and the fixed-width
 -- integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/
 -- 'Int64'); 'Nothing' otherwise. The translator uses this to route
 -- 'PEq' over arbitrary types: a 'Sym' hit translates to '(.==)' on
@@ -245,6 +265,7 @@
   Just SymbolicBool -> Just SymDict
   Just SymbolicInt -> Just SymDict
   Just SymbolicInteger -> Just SymDict
+  Just SymbolicNatural -> Just SymDict
   Just SymbolicText -> Just SymDict
   Just SymbolicUTCTime -> Just SymDict
   Just SymbolicWord64 -> Just SymDict
@@ -266,7 +287,7 @@
 -- | Try to discover ordering evidence for @r@ at runtime, companion to
 -- 'discoverSym'. Returns @Just SymOrdDict@ for the numeric and time
 -- types whose 'SymRep' is an 'SBV.OrdSymbolic' 'Integer' ('Int',
--- 'Integer', the fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32'
+-- 'Integer', 'Natural', the fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32'
 -- \/ 'Word64' \/ 'Int32' \/ 'Int64', and 'UTCTime' encoded as epoch
 -- seconds); 'Nothing' otherwise. 'Bool' and 'Text' are deliberately
 -- omitted: ordering a 'Bool' guard is not meaningful, and 'SString'
@@ -277,6 +298,7 @@
 discoverSymOrd = case discoverSymbolicType @r of
   Just SymbolicInt -> Just SymOrdDict
   Just SymbolicInteger -> Just SymOrdDict
+  Just SymbolicNatural -> Just SymOrdDict
   Just SymbolicUTCTime -> Just SymOrdDict
   Just SymbolicWord64 -> Just SymOrdDict
   Just SymbolicWord32 -> Just SymOrdDict
@@ -301,8 +323,10 @@
 -- 'discoverSymOrd'. Returns @Just SymNumDict@ for the numeric types
 -- whose 'SymRep' is the SBV-'Num' 'Integer' ('Int', 'Integer', and the
 -- fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/
--- 'Int32' \/ 'Int64'); 'Nothing' otherwise. 'Bool', 'Text', and
--- 'UTCTime' are omitted — not meaningfully arithmetic here. A 'Nothing'
+-- 'Int32' \/ 'Int64'); 'Nothing' otherwise. 'Natural' is omitted because
+-- its subtraction is partial and throws @Underflow@ for a negative result,
+-- unlike ordinary SMT integer subtraction. 'Bool', 'Text', and 'UTCTime' are
+-- also omitted. A 'Nothing'
 -- makes the 'TArith' translator fall back to a fresh opaque variable,
 -- exactly as 'goEq' \/ 'goCmp' fall back for non-'Sym' operands —
 -- sound, just imprecise. (The 'Num' constraint on the 'TArith'
@@ -322,6 +346,7 @@
   Just SymbolicBool -> Nothing
   Just SymbolicText -> Nothing
   Just SymbolicUTCTime -> Nothing
+  Just SymbolicNatural -> Nothing
   Nothing -> Nothing
 
 -- | Lift a concrete value to an SBV literal of its 'SymRep'.
@@ -330,7 +355,10 @@
 
 -- | Allocate a fresh symbolic variable of the carrier's 'SymRep'.
 symFree :: forall a. (Sym a) => String -> SBV.Symbolic (SBV.SBV (SymRep a))
-symFree = SBV.free
+symFree label = do
+  value <- SBV.free label
+  constrainSymDomain @a value
+  pure value
 
 -- * Translation environment -------------------------------------------------
 
@@ -469,13 +497,13 @@
   SBV.Symbolic (SBV.SBV (SymRep r))
 translateTermSym _env (TLit r) = pure (symLit r)
 translateTermSym env (TReg ix) =
-  memoFree env (RegVar (indexName ix))
+  memoFree @r env (RegVar (indexName ix))
 translateTermSym env (TInpCtorField ic ix) =
-  memoFree env (InpVar (icName ic) (indexName ix))
-translateTermSym _env (TApp1 _f _t) = SBV.free "app1"
-translateTermSym _env (TApp2 _f _a _b) = SBV.free "app2"
+  memoFree @r env (InpVar (icName ic) (indexName ix))
+translateTermSym _env (TApp1 _f _t) = symFree @r "app1"
+translateTermSym _env (TApp2 _f _a _b) = symFree @r "app2"
 translateTermSym env (TArith op a b) = case discoverSymNum @r of
-  Nothing -> SBV.free "arith" -- sound opaque fallback
+  Nothing -> symFree @r "arith" -- sound opaque fallback within the carrier domain
   Just SymNumDict -> do
     sa <- translateTermSym env a
     sb <- translateTermSym env b
@@ -485,7 +513,7 @@
           OpMul -> (*)
     pure (apply sa sb)
 translateTermSym env (TFieldProj (witness :: FieldWitness projection) base) =
-  memoFree env (projectionVarKey witness base)
+  memoFree @r env (projectionVarKey witness base)
 
 projectionVarKey ::
   forall projection rs ci ifs.
@@ -526,7 +554,7 @@
   FieldResult projection ->
   SBV.Symbolic ()
 constrainFieldProjection env witness base concrete = do
-  symbolic <- memoFree env (projectionVarKey witness base)
+  symbolic <- memoFree @(FieldResult projection) env (projectionVarKey witness base)
   SBV.constrain (symbolic SBV..== symLit concrete)
 
 -- | Memoized symbolic-variable allocator (EP-42). Looks @name@ up in
@@ -537,14 +565,14 @@
 -- return it. This is what makes repeated reads of the same register or
 -- input field share a single solver variable.
 memoFree ::
-  forall a.
-  (SBV.SymVal a) =>
-  SymEnv -> SymVarKey -> SBV.Symbolic (SBV.SBV a)
+  forall r.
+  (Sym r) =>
+  SymEnv -> SymVarKey -> SBV.Symbolic (SBV.SBV (SymRep r))
 memoFree env key = do
   m <- liftIO (readIORef (seVarCache env))
   case Map.lookup key m of
     Just (SomeSBV (v :: SBV.SBV b)) ->
-      case eqTypeRep (typeRep @a) (typeRep @b) of
+      case eqTypeRep (typeRep @(SymRep r)) (typeRep @b) of
         Just HRefl -> pure v
         Nothing ->
           -- Unreachable: a name maps to exactly one representation type.
@@ -558,7 +586,7 @@
           ordinal <- readIORef (seProjectionOrdinal env)
           modifyIORef' (seProjectionOrdinal env) (+ 1)
           pure ("proj/" <> show ordinal)
-      v <- SBV.free label
+      v <- symFree @r label
       liftIO (modifyIORef' (seVarCache env) (Map.insert key (SomeSBV v)))
       pure v
 
@@ -831,7 +859,7 @@
 --
 -- The instance constraints @KnownSymbol s@ and @Sym t@ make this
 -- automatic for any concrete slot list whose value types are in the
--- curated 'Sym' registry ('Bool', 'Int', 'Integer', 'Text',
+-- curated 'Sym' registry ('Bool', 'Int', 'Integer', 'Natural', 'Text',
 -- 'UTCTime'). User Registration's 'UserRegRegs' shape qualifies
 -- without further user code.
 class ExtractRegFile (rs :: [Slot]) where
diff --git a/test/Keiki/ShapeSpec.hs b/test/Keiki/ShapeSpec.hs
--- a/test/Keiki/ShapeSpec.hs
+++ b/test/Keiki/ShapeSpec.hs
@@ -24,6 +24,7 @@
     sha256Hex,
     stateShapeHash,
   )
+import Numeric.Natural (Natural)
 import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy)
 import Type.Reflection (someTypeRep)
 
@@ -81,6 +82,7 @@
      '("int32", Int32),
      '("int64", Int64),
      '("integer", Integer),
+     '("natural", Natural),
      '("word", Word),
      '("word8", Word8),
      '("word16", Word16),
@@ -148,6 +150,10 @@
     it "concatenates one slot in the documented R3 form" $
       regFileShapeCanonical (Proxy @('[ '("retryCount", Int)] :: [(Symbol, Type)]))
         `shouldBe` T.pack "retryCount:Int;regfile:0"
+
+    it "pins Natural independently of its base-library representation" $
+      regFileShapeCanonical (Proxy @('[ '("revision", Natural)] :: [(Symbol, Type)]))
+        `shouldBe` T.pack "revision:Natural;regfile:0"
 
     it "keeps GHC-internal module paths out of every built-in name" $ do
       let canonical = regFileShapeCanonical (Proxy @BuiltInSlots)
diff --git a/test/Keiki/SymbolicSpec.hs b/test/Keiki/SymbolicSpec.hs
--- a/test/Keiki/SymbolicSpec.hs
+++ b/test/Keiki/SymbolicSpec.hs
@@ -12,6 +12,7 @@
 import Data.Word (Word16, Word32, Word64, Word8)
 import Keiki.FieldProjSpec qualified as FieldProj
 import Keiki.Symbolic
+import Numeric.Natural (Natural)
 import Test.Hspec
 
 -- | A two-constructor input symbol for the 'PInCtor' tests.
@@ -114,6 +115,15 @@
       isFinal = (== True)
     }
 
+-- | Natural uses an unbounded SMT integer with a non-negative domain
+-- constraint. It supports equality and ordering, but intentionally not the
+-- generic arithmetic registry because Haskell subtraction throws Underflow
+-- when its mathematical result would be negative.
+type NaturalRegs = '[ '("count", Natural)]
+
+naturalIdx :: Index NaturalRegs Natural
+naturalIdx = ZIdx
+
 -- | A two-edge transducer over a 'Word64' register. Both edges leave
 -- the @False@ vertex; the second edge carries a constant 'Word64'
 -- equality that is always false (@5 == 6@), so the pair is mutually
@@ -325,6 +335,7 @@
     it "discovers Sym Bool" $ symKnown (Proxy @Bool) `shouldBe` True
     it "discovers Sym Int" $ symKnown (Proxy @Int) `shouldBe` True
     it "discovers Sym Integer" $ symKnown (Proxy @Integer) `shouldBe` True
+    it "discovers Sym Natural" $ symKnown (Proxy @Natural) `shouldBe` True
     it "discovers Sym Text" $ symKnown (Proxy @Text) `shouldBe` True
     it "discovers Sym UTCTime" $ symKnown (Proxy @UTCTime) `shouldBe` True
     -- EP-41: fixed-width integers (money + counts).
@@ -385,6 +396,34 @@
       evalPred timeBeforeGuard runtimeRegs AmtTick `shouldBe` True
       checkTransitionDeterminismSym timePrecisionFixture `shouldSatisfy` (not . null)
       isSingleValuedSym (withSymPred timePrecisionFixture) `shouldBe` False
+
+    it "constrains Natural register variables to non-negative values" $
+      symIsBot
+        (PCmp CmpLt (proj naturalIdx) (lit (0 :: Natural)) :: HsPred NaturalRegs AmtCmd)
+        `shouldBe` True
+
+    it "keeps Natural equality and ordering solver-visible" $ do
+      symIsBot
+        (PEq (lit (1 :: Natural)) (lit 2) :: HsPred '[] AmtCmd)
+        `shouldBe` True
+      symIsBot
+        (PCmp CmpGt (lit (1 :: Natural)) (lit 2) :: HsPred '[] AmtCmd)
+        `shouldBe` True
+
+    it "extracts a valid Natural witness and withholds generic arithmetic" $ do
+      case symSatExt
+        ( PAnd
+            (PInCtor inCtorAmtTick)
+            (PCmp CmpGe (proj naturalIdx) (lit (3 :: Natural))) ::
+            HsPred NaturalRegs AmtCmd
+        ) of
+        Nothing -> expectationFailure "expected a Natural witness"
+        Just (registers, command) -> do
+          registers ! naturalIdx `shouldSatisfy` (>= 3)
+          command `shouldBe` AmtTick
+      case discoverSymNum @Natural of
+        Nothing -> pure ()
+        Just _ -> expectationFailure "Natural must not use ordinary integer arithmetic"
 
   describe "ordering predicate PCmp (EP-41 M2)" $ do
     it "constant contradiction 5 >= 10 over Word64 is symIsBot" $
diff --git a/test/Keiki/ValidationSpec.hs b/test/Keiki/ValidationSpec.hs
--- a/test/Keiki/ValidationSpec.hs
+++ b/test/Keiki/ValidationSpec.hs
@@ -6,6 +6,7 @@
 import Keiki.Core
 import Keiki.FieldProjSpec qualified as FieldProj
 import Keiki.Symbolic (checkDeadEdgesSym, checkTransitionDeterminismSym)
+import Numeric.Natural (Natural)
 import Test.Hspec
 
 -- A tiny two-constructor command for guards.
@@ -154,6 +155,37 @@
       isFinal = (== Mid)
     }
 
+-- Natural equality and ordering are symbolic, but generic TArith is opaque
+-- because its type-wide registry would also expose partial subtraction.
+type NaturalRegs = '[ '("n", Natural)]
+
+naturalIdx :: Index NaturalRegs Natural
+naturalIdx = ZIdx
+
+naturalArithmeticOpaqueT ::
+  SymTransducer (HsPred NaturalRegs Cmd) NaturalRegs V Cmd ()
+naturalArithmeticOpaqueT =
+  SymTransducer
+    { edgesOut = \case
+        Start ->
+          [ Edge
+              { guard =
+                  PCmp
+                    CmpGt
+                    (tadd (proj naturalIdx) (TLit 1))
+                    (TLit 0),
+                update = UKeep,
+                output = [],
+                target = Start,
+                mode = Live
+              }
+          ]
+        _ -> [],
+      initial = Start,
+      initialRegs = RCons (Proxy @"n") 0 RNil,
+      isFinal = const False
+    }
+
 -- A 3-slot input constructor, mirroring CoreHiddenInputsGSMSpec, used to build
 -- a hidden-input edge (its output recovers only slots a, b — never c).
 data MultiInput = Begin Int Int Int
@@ -279,6 +311,50 @@
     )
     (fooWith (PCmp CmpGt (proj xIdx) (TLit 5)))
 
+intArithmeticStructuralT ::
+  SymTransducer (HsPred OverlapRegs Cmd) OverlapRegs V Cmd ()
+intArithmeticStructuralT =
+  SymTransducer
+    { edgesOut = \case
+        Start ->
+          [ Edge
+              (PCmp CmpGt (tadd (proj xIdx) (TLit 1)) (TLit 0))
+              UKeep
+              []
+              Start
+              Live
+          ]
+        _ -> [],
+      initial = Start,
+      initialRegs = RCons (Proxy @"x") 0 RNil,
+      isFinal = const False
+    }
+
+naturalInteriorOverlapT ::
+  SymTransducer (HsPred NaturalRegs Cmd) NaturalRegs V Cmd ()
+naturalInteriorOverlapT =
+  SymTransducer
+    { edgesOut = \case
+        Start ->
+          [ Edge
+              (PCmp CmpGt (proj naturalIdx) (TLit 1))
+              UKeep
+              []
+              Start
+              Live,
+            Edge
+              (PCmp CmpLt (proj naturalIdx) (TLit 3))
+              UKeep
+              []
+              Start
+              Live
+          ]
+        _ -> [],
+      initial = Start,
+      initialRegs = RCons (Proxy @"n") 0 RNil,
+      isFinal = const False
+    }
+
 differentCtorT ::
   SymTransducer (HsPred OverlapRegs Cmd) OverlapRegs V Cmd ()
 differentCtorT =
@@ -400,6 +476,16 @@
     it "an opaque collection-style guard is flagged when the audit is on" $
       validateTransducer optsOn opaqueT `shouldSatisfy` any isOpaqueStart
 
+    it "unsupported Natural arithmetic is flagged when the audit is on" $
+      validateTransducer optsOn naturalArithmeticOpaqueT
+        `shouldSatisfy` any isOpaqueStart
+
+    it "supported Int arithmetic remains structural" $ do
+      let isOpaque (OpaqueGuard {}) = True
+          isOpaque _ = False
+      validateTransducer optsOn intArithmeticStructuralT
+        `shouldSatisfy` (not . any isOpaque)
+
     it "a fully structural transducer is never flagged, even with the audit on" $ do
       let isOpaque (OpaqueGuard {}) = True
           isOpaque _ = False
@@ -589,6 +675,12 @@
     it "uses a mentioned non-integral literal as a concrete witness" $
       checkTransitionDeterminismPure boolLiteralWitnessT
         `shouldSatisfy` (not . null)
+
+    it "finds an interior overlap in Natural's zero-bounded domain" $ do
+      let purePairs = map warningPair (checkTransitionDeterminismPure naturalInteriorOverlapT)
+          symbolicPairs = map warningPair (checkTransitionDeterminismSym naturalInteriorOverlapT)
+      purePairs `shouldBe` [(Start, 0, 1)]
+      purePairs `shouldSatisfy` all (`elem` symbolicPairs)
 
     it "does not guess through POr or an opaque TApp term" $ do
       checkTransitionDeterminismPure unknownOrT `shouldBe` []