diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,13 @@
 
 ## UNRELEASED
 
+## 3.1.0 - 2023-04-10
+
+* **BREAKING**: Change the type of `postcondition` to allow you to
+  express property monitoring (e.g. stats or counterexamples) in the
+  postcondition itself - rather than duplicating code for counterexamples
+  in the `monitoring` function.
+
 ## 3.0.3 - 2023-04-18
 
 * Added `hasNoVariablesQ` and `forAllNonVariableDL` functions to help make
diff --git a/quickcheck-dynamic.cabal b/quickcheck-dynamic.cabal
--- a/quickcheck-dynamic.cabal
+++ b/quickcheck-dynamic.cabal
@@ -1,6 +1,6 @@
 cabal-version:   2.2
 name:            quickcheck-dynamic
-version:         3.0.3
+version:         3.1.0
 license:         Apache-2.0
 license-files:
   LICENSE
@@ -54,6 +54,7 @@
     TypeOperators
     DerivingVia
     DeriveGeneric
+    GeneralizedNewtypeDeriving
 
   ghc-options:
     -Wall -Wnoncanonical-monad-instances -Wunused-packages
diff --git a/src/Test/QuickCheck/StateModel.hs b/src/Test/QuickCheck/StateModel.hs
--- a/src/Test/QuickCheck/StateModel.hs
+++ b/src/Test/QuickCheck/StateModel.hs
@@ -11,6 +11,7 @@
   module Test.QuickCheck.StateModel.Variables,
   StateModel (..),
   RunModel (..),
+  PostconditionM (..),
   WithUsedVars (..),
   Annotated (..),
   Step (..),
@@ -22,6 +23,8 @@
   Env,
   Realized,
   Generic,
+  monitorPost,
+  counterexamplePost,
   stateAfter,
   runActions,
   lookUpVar,
@@ -37,7 +40,7 @@
 import Control.Monad.Identity
 import Control.Monad.Reader
 import Control.Monad.State
-import Control.Monad.Writer (WriterT)
+import Control.Monad.Writer (Endo (..), WriterT, runWriterT, tell)
 import Data.Data
 import Data.Kind
 import Data.List
@@ -137,6 +140,19 @@
 type instance Realized (WriterT w m) a = Realized m a
 type instance Realized Identity a = a
 
+newtype PostconditionM m a = PostconditionM {runPost :: WriterT (Endo Property, Endo Property) m a}
+  deriving (Functor, Applicative, Monad, MonadTrans)
+
+-- | Apply the property transformation to the property after evaluating
+-- the postcondition. Useful for collecting statistics while avoiding
+-- duplication between `monitoring` and `postcondition`.
+monitorPost :: Monad m => (Property -> Property) -> PostconditionM m ()
+monitorPost m = PostconditionM $ tell (Endo m, mempty)
+
+-- | Acts as `Test.QuickCheck.counterexample` if the postcondition fails.
+counterexamplePost :: Monad m => String -> PostconditionM m ()
+counterexamplePost c = PostconditionM $ tell (mempty, Endo $ counterexample c)
+
 class Monad m => RunModel state m where
   -- | Perform an `Action` in some `state` in the `Monad` `m`.  This
   -- is the function that's used to exercise the actual stateful
@@ -153,10 +169,10 @@
   -- | Postcondition on the `a` value produced at some step.
   -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
   -- to check the implementation produces expected values.
-  postcondition :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> m Bool
+  postcondition :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool
   postcondition _ _ _ _ = pure True
 
-  -- | Allows the user to attach information to the `Property` at each step of the process.
+  -- | Allows the user to attach additional information to the `Property` at each step of the process.
   -- This function is given the full transition that's been executed, including the start and ending
   -- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform`
   -- while executing this step.
@@ -381,6 +397,8 @@
           s' = computeNextState s act var
           env' = (var :== ret) : env
       monitor (monitoring @state @m (underlyingState s, underlyingState s') act (lookUpVar env') ret)
-      b <- run $ postcondition @state @m (underlyingState s, underlyingState s') act (lookUpVar env) ret
+      (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ postcondition @state @m (underlyingState s, underlyingState s') act (lookUpVar env) ret
+      monitor mon
+      unless b $ monitor onFail
       assert b
       loop s' env' as