diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,26 @@
 ## [Unreleased]
 
 
+## [0.6.0.0] — 2026-07-31
+
+### Added
+
+- `verifyPredicate`, `predicateTranslationExact`, and
+  `PredicateVerification` expose whether a predicate received an exact
+  structural translation and a definite solver answer. Opaque fallbacks,
+  solver `Unknown`/timeouts, and solver failures remain explicitly unverified.
+
+### Changed
+
+- **Breaking semantic fix:** structural `Natural` addition and multiplication
+  are now solver-visible, and structural subtraction is total monus in both
+  concrete and symbolic evaluation: `a - b = max 0 (a - b)`. It never invokes
+  partial Haskell `Natural` subtraction on an underflowing pair; the symbolic
+  form is `ite (a >= b) (a - b) 0`.
+- `Natural` now belongs to the curated symbolic numeric registry, so
+  `OpaqueGuard` no longer reports structural `Natural` arithmetic.
+
+
 ## [0.5.0.0] — 2026-07-31
 
 ### 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.5.0.0
+version:         0.6.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
@@ -316,8 +316,10 @@
 
 -- * Term language ----------------------------------------------------------
 
--- | A numeric operation carried by 'TArith'. @OpAdd@\/@OpSub@\/@OpMul@
--- are @+@\/@-@\/@*@ respectively. Kept as a single tag (rather than
+-- | A numeric operation carried by 'TArith'. @OpAdd@ and @OpMul@ are
+-- @+@ and @*@ respectively. @OpSub@ is ordinary subtraction except for
+-- 'Natural', where it is total monus: @a - b = max 0 (a - b)@. Kept as a
+-- single tag (rather than
 -- three 'Term' constructors) so each total 'Term' walker switches on
 -- one value; the three directions are recovered by the smart
 -- constructors 'tadd'\/'tsub'\/'tmul'.
@@ -428,7 +430,9 @@
   --     guard over a /computed/ value — a weighted sum, a derived cap — is
   --     visible to the solver. The 'Num' constraint prevents constructing
   --     arithmetic at non-numeric operand types; 'Typeable' lets the SBV
-  --     translator dispatch on @r@. Build with 'tadd'\/'tsub'\/'tmul'.
+  --     translator dispatch on @r@. 'Natural' subtraction is total monus in
+  --     both evaluators rather than the partial 'Num' method. Build with
+  --     'tadd'\/'tsub'\/'tmul'.
   TArith ::
     (Num r, Typeable r) =>
     NumOp ->
@@ -894,7 +898,9 @@
 -- build a 'TArith' over @+@\/@-@\/@*@. The operand type must be numeric
 -- ('Num') and 'Typeable'; the SBV translator reads them structurally
 -- (see 'Keiki.Symbolic.discoverSymNum'), unlike the opaque 'TApp'
--- escape hatches.
+-- escape hatches. For 'Natural', 'tsub' deliberately means total monus:
+-- @tsub a b@ evaluates to zero when @b > a@. It never calls the partial
+-- 'Natural' subtraction operation on an underflowing pair.
 tadd,
   tsub,
   tmul ::
@@ -1008,11 +1014,16 @@
               ++ icName ic
           )
 
--- | Interpret a 'NumOp' tag as the corresponding numeric operation.
--- The 'Num' evidence is supplied by matching the 'TArith' constructor.
-applyNumOp :: (Num r) => NumOp -> r -> r -> r
+-- | Interpret a 'NumOp' tag as the corresponding total operation. The 'Num'
+-- and 'Typeable' evidence is supplied by matching the 'TArith' constructor.
+-- 'Natural' subtraction is special-cased to monus before invoking @(-)@ so
+-- concrete evaluation cannot throw @Underflow@.
+applyNumOp :: forall r. (Num r, Typeable r) => NumOp -> r -> r -> r
 applyNumOp OpAdd = (+)
-applyNumOp OpSub = (-)
+applyNumOp OpSub =
+  case eqTypeRep (typeRep @r) (typeRep @Natural) of
+    Just HRefl -> \a b -> if a >= b then a - b else 0
+    Nothing -> (-)
 applyNumOp OpMul = (*)
 
 -- | Evaluate an 'OutTerm' against a register file and an input symbol.
@@ -2053,7 +2064,7 @@
       }
   | -- | 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
+    --       the symbolic numeric registry. 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
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
@@ -69,6 +69,7 @@
 symbolicTypeSupportsNumeric :: SymbolicType r -> Bool
 symbolicTypeSupportsNumeric SymbolicInt = True
 symbolicTypeSupportsNumeric SymbolicInteger = True
+symbolicTypeSupportsNumeric SymbolicNatural = True
 symbolicTypeSupportsNumeric SymbolicWord64 = True
 symbolicTypeSupportsNumeric SymbolicWord32 = True
 symbolicTypeSupportsNumeric SymbolicWord16 = True
diff --git a/src/Keiki/Symbolic.hs b/src/Keiki/Symbolic.hs
--- a/src/Keiki/Symbolic.hs
+++ b/src/Keiki/Symbolic.hs
@@ -62,6 +62,9 @@
     translateTermSym,
     translatePred,
     constrainFieldProjection,
+    PredicateVerification (..),
+    predicateTranslationExact,
+    verifyPredicate,
 
     -- * Symbolic predicate wrapper
     SymPred (..),
@@ -323,10 +326,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. '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'
+-- 'Int32' \/ 'Int64'), plus 'Natural'. Natural subtraction has the explicit
+-- total monus meaning shared with concrete 'evalTerm'; it is translated as
+-- @ite (a >= b) (a - b) 0@ rather than ordinary integer subtraction.
+-- 'Bool', 'Text', and 'UTCTime' are 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'
@@ -337,6 +340,7 @@
 discoverSymNum = case discoverSymbolicType @r of
   Just SymbolicInt -> Just SymNumDict
   Just SymbolicInteger -> Just SymNumDict
+  Just SymbolicNatural -> Just SymNumDict
   Just SymbolicWord64 -> Just SymNumDict
   Just SymbolicWord32 -> Just SymNumDict
   Just SymbolicWord16 -> Just SymNumDict
@@ -346,7 +350,6 @@
   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'.
@@ -507,11 +510,15 @@
   Just SymNumDict -> do
     sa <- translateTermSym env a
     sb <- translateTermSym env b
-    let apply = case op of
-          OpAdd -> (+)
-          OpSub -> (-)
-          OpMul -> (*)
-    pure (apply sa sb)
+    case (discoverSymbolicType @r, op) of
+      (Just SymbolicNatural, OpSub) ->
+        pure (SBV.ite (sa SBV..>= sb) (sa - sb) 0)
+      _ -> do
+        let apply = case op of
+              OpAdd -> (+)
+              OpSub -> (-)
+              OpMul -> (*)
+        pure (apply sa sb)
 translateTermSym env (TFieldProj (witness :: FieldWitness projection) base) =
   memoFree @r env (projectionVarKey witness base)
 
@@ -658,6 +665,89 @@
               CmpGt -> (SBV..>)
               CmpGe -> (SBV..>=)
         pure (apply sa sb)
+
+-- | A conservative answer from 'verifyPredicate'. The two @Verified@
+-- constructors mean every predicate node translated structurally and the
+-- solver returned a definite result. Opaque Haskell applications, unsupported
+-- carrier dictionaries, solver timeouts or @Unknown@, and solver failures are
+-- represented explicitly and must not be treated as successful verification.
+data PredicateVerification
+  = VerifiedSatisfiable
+  | VerifiedUnsatisfiable
+  | UnverifiedOpaque
+  | UnverifiedSolverUnknown String
+  | UnverifiedSolverFailure String
+  deriving stock (Eq, Show)
+
+-- | Whether every node in a predicate has an exact structural symbolic
+-- translation. This is stricter than merely being accepted by 'translatePred',
+-- whose compatibility fallback intentionally replaces unsupported pieces with
+-- fresh variables.
+predicateTranslationExact :: forall rs ci. HsPred rs ci -> Bool
+predicateTranslationExact = goPred
+  where
+    goPred :: HsPred rs ci -> Bool
+    goPred PTop = True
+    goPred PBot = True
+    goPred (PAnd p q) = goPred p && goPred q
+    goPred (POr p q) = goPred p && goPred q
+    goPred (PNot p) = goPred p
+    goPred (PEq a b) = exactEquality a b
+    goPred (PInCtor _) = True
+    goPred PLeftArm = True
+    goPred PRightArm = True
+    goPred (PCmp _ a b) = exactOrdering a b
+
+    exactEquality ::
+      forall r ifs1 ifs2.
+      (Typeable r) =>
+      Term rs ci ifs1 r ->
+      Term rs ci ifs2 r ->
+      Bool
+    exactEquality a b = case discoverSym @r of
+      Nothing -> False
+      Just SymDict -> exactTerm a && exactTerm b
+
+    exactOrdering ::
+      forall r ifs1 ifs2.
+      (Typeable r) =>
+      Term rs ci ifs1 r ->
+      Term rs ci ifs2 r ->
+      Bool
+    exactOrdering a b = case discoverSymOrd @r of
+      Nothing -> False
+      Just SymOrdDict -> exactTerm a && exactTerm b
+
+    exactTerm :: forall ifs r. (Sym r) => Term rs ci ifs r -> Bool
+    exactTerm (TLit _) = True
+    exactTerm (TReg _) = True
+    exactTerm (TInpCtorField _ _) = True
+    exactTerm (TApp1 _ _) = False
+    exactTerm (TApp2 _ _ _) = False
+    exactTerm (TArith _ a b) = case discoverSymNum @r of
+      Nothing -> False
+      Just SymNumDict -> exactTerm a && exactTerm b
+    exactTerm TFieldProj {} = True
+
+-- | Translate and solve one predicate without collapsing uncertainty into a
+-- Boolean. Exact translations produce a verified satisfiable or unsatisfiable
+-- answer. Any opaque fallback is rejected before invoking the solver, and
+-- every non-definite solver result remains visibly unverified.
+verifyPredicate :: HsPred rs ci -> IO PredicateVerification
+verifyPredicate predicate
+  | not (predicateTranslationExact predicate) = pure UnverifiedOpaque
+  | otherwise = do
+      result <- SBV.sat $ do
+        env <- mkSymEnv
+        translatePred env predicate
+      pure $ case result of
+        SBV.SatResult status -> case status of
+          SBV.Satisfiable {} -> VerifiedSatisfiable
+          SBV.Unsatisfiable {} -> VerifiedUnsatisfiable
+          SBV.Unknown {} -> UnverifiedSolverUnknown "solver returned Unknown"
+          SBV.ProofError {} -> UnverifiedSolverFailure "solver returned ProofError"
+          SBV.DeltaSat {} -> UnverifiedSolverUnknown "solver returned DeltaSat"
+          SBV.SatExtField {} -> UnverifiedSolverUnknown "solver returned SatExtField"
 
 -- * Symbolic predicate wrapper ----------------------------------------------
 
diff --git a/test/Keiki/OperatorsSpec.hs b/test/Keiki/OperatorsSpec.hs
--- a/test/Keiki/OperatorsSpec.hs
+++ b/test/Keiki/OperatorsSpec.hs
@@ -1,6 +1,7 @@
 module Keiki.OperatorsSpec (spec) where
 
 import Keiki.Core
+import Numeric.Natural (Natural)
 import Test.Hspec
 
 -- A trivial command type; the operators here never read it.
@@ -72,6 +73,9 @@
       n (lit 2 .+ lit 3 .* lit 4) `shouldBe` 14
     it "arithmetic feeds a comparison without parens" $
       p (lit (10 :: Int) .<= lit 3 .* lit 4) `shouldBe` True
+    it "Natural subtraction is total monus" $ do
+      evalTerm (lit (2 :: Natural) .- lit 5) RNil NoCmd `shouldBe` 0
+      evalTerm (lit (7 :: Natural) .- lit 5) RNil NoCmd `shouldBe` 2
 
   describe "type synonyms" $
     it "Pred is interchangeable with HsPred" $
diff --git a/test/Keiki/SymbolicSpec.hs b/test/Keiki/SymbolicSpec.hs
--- a/test/Keiki/SymbolicSpec.hs
+++ b/test/Keiki/SymbolicSpec.hs
@@ -410,7 +410,7 @@
         (PCmp CmpGt (lit (1 :: Natural)) (lit 2) :: HsPred '[] AmtCmd)
         `shouldBe` True
 
-    it "extracts a valid Natural witness and withholds generic arithmetic" $ do
+    it "extracts a valid Natural witness and exposes total arithmetic" $ do
       case symSatExt
         ( PAnd
             (PInCtor inCtorAmtTick)
@@ -421,9 +421,23 @@
         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"
+      isJust (discoverSymNum @Natural) `shouldBe` True
+
+    it "gives Natural subtraction the same total monus meaning concretely and symbolically" $ do
+      let underflowing = tsub (lit (2 :: Natural)) (lit 5)
+          ordinary = tsub (lit (9 :: Natural)) (lit 4)
+      evalTerm underflowing RNil AmtTick `shouldBe` 0
+      evalTerm ordinary RNil AmtTick `shouldBe` 5
+      verifyPredicate (underflowing .== lit 0 :: HsPred '[] AmtCmd)
+        `shouldReturn` VerifiedSatisfiable
+      proveP (underflowing .== lit 0 :: HsPred '[] AmtCmd)
+        `shouldReturn` True
+
+    it "never upgrades opaque predicate terms to verified" $ do
+      let opaque =
+            PEq (TApp1 id (lit (1 :: Integer))) (lit 1) :: HsPred '[] AmtCmd
+      predicateTranslationExact opaque `shouldBe` False
+      verifyPredicate opaque `shouldReturn` UnverifiedOpaque
 
   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
@@ -155,8 +155,8 @@
       isFinal = (== Mid)
     }
 
--- Natural equality and ordering are symbolic, but generic TArith is opaque
--- because its type-wide registry would also expose partial subtraction.
+-- Natural equality, ordering, and total arithmetic are symbolic. Subtraction
+-- is monus in both concrete and symbolic evaluation.
 type NaturalRegs = '[ '("n", Natural)]
 
 naturalIdx :: Index NaturalRegs Natural
@@ -476,9 +476,9 @@
     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" $
+    it "total Natural arithmetic remains structural" $
       validateTransducer optsOn naturalArithmeticOpaqueT
-        `shouldSatisfy` any isOpaqueStart
+        `shouldSatisfy` (not . any isOpaqueStart)
 
     it "supported Int arithmetic remains structural" $ do
       let isOpaque (OpaqueGuard {}) = True