diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,12 @@
 As a minor extension, we also keep a semantic version for the `UNRELEASED`
 changes.
 
+## UNRELEASED
+
+## 3.4.1 - 2024-03-22
+
+* [#70](https://github.com/input-output-hk/quickcheck-dynamic/pull/70) Expose `IsPerformResult` typeclass
+
 ## 3.4.0 - 2024-03-01
 
 * Added some lightweight negative-shrinking based on a simple dependency analysis.
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.4.0
+version:            3.4.1
 license:            Apache-2.0
 license-files:
   LICENSE
@@ -90,10 +90,11 @@
   main-is:        Spec.hs
   hs-source-dirs: test
   other-modules:
-    Spec.DynamicLogic.CounterModel
+    Spec.DynamicLogic.Counters
     Spec.DynamicLogic.Registry
     Spec.DynamicLogic.RegistryModel
     Test.QuickCheck.DynamicLogic.QuantifySpec
+    Test.QuickCheck.StateModelSpec
 
   ghc-options:    -rtsopts
   build-depends:
@@ -104,4 +105,5 @@
     , quickcheck-dynamic
     , stm
     , tasty
+    , tasty-hunit
     , tasty-quickcheck
diff --git a/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs b/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs
--- a/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs
+++ b/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs
@@ -3,12 +3,16 @@
 import Test.QuickCheck
 
 -- | This combinator captures the 'smart shrinking' implemented for the
--- Smart type wrapper in Test.QuickCheck.Modifiers.
+-- `Smart` type wrapper in [Test.QuickCheck.Modifiers](https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Modifiers.html#t:Smart).
+-- It interleaves the output of the given shrinker to try to converge to more
+-- interesting values faster.
 shrinkSmart :: (a -> [a]) -> Smart a -> [Smart a]
-shrinkSmart shr (Smart i x) = take i' ys `ilv` drop i' ys
+shrinkSmart shrinker (Smart i x) = take i' ys `interleave` drop i' ys
   where
-    ys = [Smart j y | (j, y) <- [0 ..] `zip` shr x]
+    ys = [Smart j y | (j, y) <- [0 ..] `zip` shrinker x]
+
     i' = 0 `max` (i - 2)
-    [] `ilv` bs = bs
-    as `ilv` [] = as
-    (a : as) `ilv` (b : bs) = a : b : (as `ilv` bs)
+
+    [] `interleave` bs = bs
+    as `interleave` [] = as
+    (a : as) `interleave` (b : bs) = a : b : (as `interleave` bs)
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
@@ -2,7 +2,7 @@
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
 
--- | Simple (stateful) Model-Based Testing library for use with Haskell QuickCheck.
+-- | Model-Based Testing library for use with Haskell QuickCheck.
 --
 -- This module provides the basic machinery to define a `StateModel` from which /traces/ can
 -- be generated and executed against some /actual/ implementation code to define monadic `Property`
@@ -25,12 +25,14 @@
   Env,
   Realized,
   Generic,
+  IsPerformResult,
   monitorPost,
   counterexamplePost,
   stateAfter,
   runActions,
   lookUpVar,
   lookUpVarMaybe,
+  viewAtType,
   initialAnnotatedState,
   computeNextState,
   computePrecondition,
@@ -191,6 +193,13 @@
 instance MonadTrans PostconditionM where
   lift = PostconditionM . lift
 
+evaluatePostCondition :: Monad m => PostconditionM m Bool -> PropertyM m ()
+evaluatePostCondition post = do
+  (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ post
+  monitor mon
+  unless b $ monitor onFail
+  assert b
+
 -- | Apply the property transformation to the property after evaluating
 -- the postcondition. Useful for collecting statistics while avoiding
 -- duplication between `monitoring` and `postcondition`.
@@ -238,23 +247,6 @@
   monitoringFailure :: state -> Action state a -> LookUp m -> Error state -> Property -> Property
   monitoringFailure _ _ _ _ prop = prop
 
-computePostcondition
-  :: forall m state a
-   . RunModel state m
-  => (state, state)
-  -> ActionWithPolarity state a
-  -> LookUp m
-  -> Either (Error state) (Realized m a)
-  -> PostconditionM m Bool
-computePostcondition ss (ActionWithPolarity a p) l r
-  | p == PosPolarity = case r of
-      Right ra -> postcondition ss a l ra
-      -- NOTE: this is actually redundant as this handled
-      -- at the call site for this function, but this is
-      -- good hygiene?
-      Left _ -> pure False
-  | otherwise = postconditionOnFailure ss a l r
-
 type LookUp m = forall a. Typeable a => Var a -> Realized m a
 
 type Env m = [EnvEntry m]
@@ -514,47 +506,82 @@
      )
   => Actions state
   -> PropertyM m (Annotated state, Env m)
-runActions (Actions_ rejected (Smart _ actions)) = loop initialAnnotatedState [] actions
+runActions (Actions_ rejected (Smart _ actions)) = do
+  (finalState, env) <- runSteps initialAnnotatedState [] actions
+  unless (null rejected) $
+    monitor $
+      tabulate "Actions rejected by precondition" rejected
+  return (finalState, env)
+
+-- | Core function to execute a sequence of `Step` given some initial `Env`ironment
+-- and `Annotated` state.
+runSteps
+  :: forall state m e
+   . ( StateModel state
+     , RunModel state m
+     , e ~ Error state
+     , forall a. IsPerformResult e a
+     )
+  => Annotated state
+  -> Env m
+  -> [Step state]
+  -> PropertyM m (Annotated state, Env m)
+runSteps s env [] = return (s, reverse env)
+runSteps s env ((v := act) : as) = do
+  pre $ computePrecondition s act
+  ret <- run $ performResultToEither <$> perform (underlyingState s) action (lookUpVar env)
+  let name = show polar ++ actionName action
+  monitor $ tabulate "Actions" [name]
+  monitor $ tabulate "Action polarity" [show polar]
+  case (polar, ret) of
+    (PosPolarity, Left err) ->
+      positiveActionFailed err
+    (PosPolarity, Right val) -> do
+      (s', env') <- positiveActionSucceeded ret val
+      runSteps s' env' as
+    (NegPolarity, _) -> do
+      (s', env') <- negativeActionResult ret
+      runSteps s' env' as
   where
-    loop :: Annotated state -> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
-    loop _s env [] = do
-      unless (null rejected) $
-        monitor $
-          tabulate "Actions rejected by precondition" rejected
-      return (_s, reverse env)
-    loop s env ((v := act) : as) = do
-      pre $ computePrecondition s act
-      ret <- run $ performResultToEither <$> perform (underlyingState s) (polarAction act) (lookUpVar env)
-      let name = show (polarity act) ++ actionName (polarAction act)
-      monitor $ tabulate "Actions" [name]
-      monitor $ tabulate "Action polarity" [show $ polarity act]
-      if
-        | polarity act == PosPolarity
-        , Left err <- ret -> do
-            monitor $
-              monitoringFailure @state @m
-                (underlyingState s)
-                (polarAction act)
-                (lookUpVar env)
-                err
-            stop False
-        | otherwise -> do
-            let var = unsafeCoerceVar v
-                s' = computeNextState s act var
-                env'
-                  | Right val <- ret = (var :== val) : env
-                  | otherwise = env
-            monitor $ monitoring @state @m (underlyingState s, underlyingState s') (polarAction act) (lookUpVar env') ret
-            (b, (Endo mon, Endo onFail)) <-
-              run
-                . runWriterT
-                . runPost
-                $ computePostcondition @m
-                  (underlyingState s, underlyingState s')
-                  act
-                  (lookUpVar env)
-                  ret
-            monitor mon
-            unless b $ monitor onFail
-            assert b
-            loop s' env' as
+    polar = polarity act
+
+    action = polarAction act
+
+    positiveActionFailed err = do
+      monitor $
+        monitoringFailure @state @m
+          (underlyingState s)
+          action
+          (lookUpVar env)
+          err
+      stop False
+
+    positiveActionSucceeded ret val = do
+      (s', env', stateTransition) <- computeNewState ret
+      evaluatePostCondition $
+        postcondition
+          stateTransition
+          action
+          (lookUpVar env)
+          val
+      pure (s', env')
+
+    negativeActionResult ret = do
+      (s', env', stateTransition) <- computeNewState ret
+      evaluatePostCondition $
+        postconditionOnFailure
+          stateTransition
+          action
+          (lookUpVar env)
+          ret
+      pure (s', env')
+
+    computeNewState ret = do
+      let var = unsafeCoerceVar v
+          s' = computeNextState s act var
+          env'
+            | Right val <- ret = (var :== val) : env
+            | otherwise = env
+          stateTransition = (underlyingState s, underlyingState s')
+      monitor $ monitoring @state @m stateTransition action (lookUpVar env') ret
+      pure (s', env', stateTransition)
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -2,9 +2,9 @@
 
 module Main (main) where
 
-import Spec.DynamicLogic.CounterModel qualified
 import Spec.DynamicLogic.RegistryModel qualified
 import Test.QuickCheck.DynamicLogic.QuantifySpec qualified
+import Test.QuickCheck.StateModelSpec qualified
 import Test.Tasty
 
 main :: IO ()
@@ -15,6 +15,6 @@
   testGroup
     "dynamic logic"
     [ Spec.DynamicLogic.RegistryModel.tests
-    , Spec.DynamicLogic.CounterModel.tests
     , Test.QuickCheck.DynamicLogic.QuantifySpec.tests
+    , Test.QuickCheck.StateModelSpec.tests
     ]
diff --git a/test/Spec/DynamicLogic/CounterModel.hs b/test/Spec/DynamicLogic/CounterModel.hs
deleted file mode 100644
--- a/test/Spec/DynamicLogic/CounterModel.hs
+++ /dev/null
@@ -1,57 +0,0 @@
-module Spec.DynamicLogic.CounterModel where
-
-import Control.Monad.Reader
-import Data.IORef
-import Test.QuickCheck
-import Test.QuickCheck.Extras
-import Test.QuickCheck.Monadic
-import Test.QuickCheck.StateModel
-import Test.Tasty hiding (after)
-import Test.Tasty.QuickCheck
-
-data Counter = Counter Int
-  deriving (Show, Generic)
-
-deriving instance Show (Action Counter a)
-deriving instance Eq (Action Counter a)
-instance HasVariables (Action Counter a) where
-  getAllVariables _ = mempty
-
-instance StateModel Counter where
-  data Action Counter a where
-    Inc :: Action Counter ()
-    Reset :: Action Counter Int
-
-  initialState = Counter 0
-
-  arbitraryAction _ _ = frequency [(5, pure $ Some Inc), (1, pure $ Some Reset)]
-
-  nextState (Counter n) Inc _ = Counter (n + 1)
-  nextState _ Reset _ = Counter 0
-
-instance RunModel Counter (ReaderT (IORef Int) IO) where
-  perform _ Inc _ = do
-    ref <- ask
-    lift $ modifyIORef ref succ
-  perform _ Reset _ = do
-    ref <- ask
-    lift $ do
-      n <- readIORef ref
-      writeIORef ref 0
-      pure n
-
-  postcondition (Counter n, _) Reset _ res = pure $ n == res
-  postcondition _ _ _ _ = pure True
-
-prop_counter :: Actions Counter -> Property
-prop_counter as = monadicIO $ do
-  ref <- lift $ newIORef (0 :: Int)
-  runPropertyReaderT (runActions as) ref
-  assert True
-
-tests :: TestTree
-tests =
-  testGroup
-    "counter tests"
-    [ testProperty "prop_conter" $ prop_counter
-    ]
diff --git a/test/Spec/DynamicLogic/Counters.hs b/test/Spec/DynamicLogic/Counters.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec/DynamicLogic/Counters.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE NamedFieldPuns #-}
+
+-- | Define several variant models of /counters/ which are useful to
+-- test or use examples for various behaviours of the runtime.
+module Spec.DynamicLogic.Counters where
+
+import Control.Monad.Reader
+import Data.IORef
+import Test.QuickCheck
+import Test.QuickCheck.StateModel
+
+-- A very simple model with a single action that always succeed in
+-- predictable way. This model is useful for testing the runtime.
+newtype SimpleCounter = SimpleCounter {count :: Int}
+  deriving (Eq, Show, Generic)
+
+deriving instance Eq (Action SimpleCounter a)
+deriving instance Show (Action SimpleCounter a)
+instance HasVariables (Action SimpleCounter a) where
+  getAllVariables _ = mempty
+
+instance StateModel SimpleCounter where
+  data Action SimpleCounter a where
+    IncSimple :: Action SimpleCounter Int
+
+  arbitraryAction _ _ = pure $ Some IncSimple
+
+  initialState = SimpleCounter 0
+
+  nextState SimpleCounter{count} IncSimple _ = SimpleCounter (count + 1)
+
+instance RunModel SimpleCounter (ReaderT (IORef Int) IO) where
+  perform _ IncSimple _ = do
+    ref <- ask
+    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+
+-- A very simple model with a single action whose postcondition fails in a
+-- predictable way. This model is useful for testing the runtime.
+newtype FailingCounter = FailingCounter {failingCount :: Int}
+  deriving (Eq, Show, Generic)
+
+deriving instance Eq (Action FailingCounter a)
+deriving instance Show (Action FailingCounter a)
+instance HasVariables (Action FailingCounter a) where
+  getAllVariables _ = mempty
+
+instance StateModel FailingCounter where
+  data Action FailingCounter a where
+    Inc' :: Action FailingCounter Int
+
+  arbitraryAction _ _ = pure $ Some Inc'
+
+  initialState = FailingCounter 0
+
+  nextState FailingCounter{failingCount} Inc' _ = FailingCounter (failingCount + 1)
+
+instance RunModel FailingCounter (ReaderT (IORef Int) IO) where
+  perform _ Inc' _ = do
+    ref <- ask
+    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+
+  postcondition (_, FailingCounter{failingCount}) _ _ _ = pure $ failingCount < 4
+
+-- A generic but simple counter model
+data Counter = Counter Int
+  deriving (Show, Generic)
+
+deriving instance Show (Action Counter a)
+deriving instance Eq (Action Counter a)
+instance HasVariables (Action Counter a) where
+  getAllVariables _ = mempty
+
+instance StateModel Counter where
+  data Action Counter a where
+    Inc :: Action Counter ()
+    Reset :: Action Counter Int
+
+  initialState = Counter 0
+
+  arbitraryAction _ _ = frequency [(5, pure $ Some Inc), (1, pure $ Some Reset)]
+
+  nextState (Counter n) Inc _ = Counter (n + 1)
+  nextState _ Reset _ = Counter 0
+
+instance RunModel Counter (ReaderT (IORef Int) IO) where
+  perform _ Inc _ = do
+    ref <- ask
+    lift $ modifyIORef ref succ
+  perform _ Reset _ = do
+    ref <- ask
+    lift $ do
+      n <- readIORef ref
+      writeIORef ref 0
+      pure n
+
+  postcondition (Counter n, _) Reset _ res = pure $ n == res
+  postcondition _ _ _ _ = pure True
diff --git a/test/Test/QuickCheck/StateModelSpec.hs b/test/Test/QuickCheck/StateModelSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/QuickCheck/StateModelSpec.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Test.QuickCheck.StateModelSpec where
+
+import Control.Monad.Reader (lift)
+import Data.IORef (newIORef)
+import Data.List (isInfixOf)
+import Spec.DynamicLogic.Counters (Counter (..), FailingCounter, SimpleCounter (..))
+import Test.QuickCheck (Property, Result (..), Testable, chatty, choose, counterexample, noShrinking, property, stdArgs)
+import Test.QuickCheck.Extras (runPropertyReaderT)
+import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick)
+import Test.QuickCheck.StateModel (
+  Actions,
+  lookUpVarMaybe,
+  mkVar,
+  runActions,
+  underlyingState,
+  viewAtType,
+  pattern Actions,
+ )
+import Test.QuickCheck.Test (test, withState)
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@?))
+import Test.Tasty.QuickCheck (testProperty)
+
+tests :: TestTree
+tests =
+  testGroup
+    "Running actions"
+    [ testProperty "simple counter" $ prop_counter
+    , testProperty "returns final state updated from actions" prop_returnsFinalState
+    , testProperty "environment variables indices are 1-based " prop_variablesIndicesAre1Based
+    , testCase "prints distribution of actions and polarity" $ do
+        Success{output} <- captureTerminal prop_returnsFinalState
+        "100.00% +Inc" `isInfixOf` output @? "Output does not contain '100.00% +Inc'"
+        "Action polarity" `isInfixOf` output @? "Output does not contain 'Action polarity'"
+    , testCase "prints counterexample as sequence of steps when postcondition fails" $ do
+        Failure{output} <- captureTerminal prop_failsOnPostcondition
+        "do action $ Inc'" `isInfixOf` output @? "Output does not contain \"do action $ Inc'\": " <> output
+    ]
+
+captureTerminal :: Testable p => p -> IO Result
+captureTerminal p =
+  withState stdArgs{chatty = False} $ \st ->
+    test st (property p)
+
+prop_counter :: Actions Counter -> Property
+prop_counter as = monadicIO $ do
+  ref <- lift $ newIORef (0 :: Int)
+  runPropertyReaderT (runActions as) ref
+  assert True
+
+prop_returnsFinalState :: Actions SimpleCounter -> Property
+prop_returnsFinalState actions@(Actions as) =
+  monadicIO $ do
+    ref <- lift $ newIORef (0 :: Int)
+    (s, _) <- runPropertyReaderT (runActions actions) ref
+    assert $ count (underlyingState s) == length as
+
+prop_variablesIndicesAre1Based :: Actions SimpleCounter -> Property
+prop_variablesIndicesAre1Based actions@(Actions as) =
+  noShrinking $ monadicIO $ do
+    ref <- lift $ newIORef (0 :: Int)
+    (_, env) <- runPropertyReaderT (runActions actions) ref
+    act <- pick $ choose (0, length as - 1)
+    monitor $
+      counterexample $
+        unlines
+          [ "Env:  " <> show (viewAtType @Int <$> env)
+          , "Actions:  " <> show as
+          , "Act:  " <> show act
+          ]
+    assert $ null as || lookUpVarMaybe env (mkVar $ act + 1) == Just act
+
+prop_failsOnPostcondition :: Actions FailingCounter -> Property
+prop_failsOnPostcondition actions =
+  monadicIO $ do
+    ref <- lift $ newIORef (0 :: Int)
+    runPropertyReaderT (runActions actions) ref
+    assert True