diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,14 @@
 # Revision history for quickcheck-lockstep
 
+## 0.2.0 -- 2022-11-11
+
+* Relax bounds on `base` (support up to ghc 9.4)
+* Show real/mock response in addition to observable response
+  (see `showRealResponse`)
+* Add `labelActions` function
+* Generalise `runActionsBracket` (Joris Dral)
+* Expose getter for the model in `Lockstep` (Joris Dral)
+
 ## 0.1.0 -- 2022-10-11
 
 * First release
diff --git a/quickcheck-lockstep.cabal b/quickcheck-lockstep.cabal
--- a/quickcheck-lockstep.cabal
+++ b/quickcheck-lockstep.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               quickcheck-lockstep
-version:            0.1.0
+version:            0.2.0
 license:            BSD-3-Clause
 license-file:       LICENSE
 author:             Edsko de Vries
@@ -32,6 +32,7 @@
       RankNTypes
       ScopedTypeVariables
       StandaloneDeriving
+      TupleSections
       TypeApplications
       TypeFamilies
   other-extensions:
@@ -57,7 +58,8 @@
       Test.QuickCheck.StateModel.Lockstep.Op
   build-depends:
       -- quickcheck-dynamic requires ghc 8.10 minimum
-      base               >= 4.14 && < 4.15
+      base               >= 4.14 && < 4.18
+    , constraints        >= 0.13 && < 0.14
     , mtl                >= 2.2  && < 2.3
     , containers         >= 0.6  && < 0.7
     , QuickCheck         >= 2.14 && < 2.15
@@ -84,6 +86,7 @@
   build-depends:
       -- Version bounds determined by main lib
       base
+    , constraints
     , containers
     , directory
     , filepath
diff --git a/src/Test/QuickCheck/StateModel/Lockstep.hs b/src/Test/QuickCheck/StateModel/Lockstep.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep.hs
@@ -13,6 +13,7 @@
 module Test.QuickCheck.StateModel.Lockstep (
     -- * Main abstraction
     Lockstep -- opaque
+  , getModel
   , InLockstep(..)
   , RunLockstep(..)
     -- ** Convenience aliases
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/API.hs b/src/Test/QuickCheck/StateModel/Lockstep/API.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/API.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/API.hs
@@ -4,6 +4,7 @@
 module Test.QuickCheck.StateModel.Lockstep.API (
     -- * State
     Lockstep(..)
+  , getModel
     -- * Main abstraction
   , InLockstep(..)
   , RunLockstep(..)
@@ -14,6 +15,7 @@
   , ModelVar
   ) where
 
+import Data.Constraint (Dict(..))
 import Data.Kind
 import Data.Typeable
 
@@ -55,6 +57,10 @@
 instance Show state => Show (Lockstep state) where
   show = show . lockstepModel
 
+-- | Inspect the model that resides inside the Lockstep state
+getModel :: Lockstep state -> state
+getModel = lockstepModel
+
 {-------------------------------------------------------------------------------
   Main lockstep abstraction
 -------------------------------------------------------------------------------}
@@ -147,6 +153,16 @@
   observeReal ::
        Proxy m
     -> LockstepAction state a -> Realized m a -> Observable state a
+
+  -- | Show responses from the real system
+  --
+  -- This method does not need to be implemented, but if it is, counter-examples
+  -- can include the real response in addition to the observable response.
+  showRealResponse ::
+       Proxy m
+    -> LockstepAction state a
+    -> Maybe (Dict (Show (Realized m a)))
+  showRealResponse _ _ = Nothing
 
 {-------------------------------------------------------------------------------
   Convenience aliases
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs b/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/Defaults.hs
@@ -17,6 +17,7 @@
 
 import Prelude hiding (init)
 
+import Data.Constraint (Dict(..))
 import Data.Maybe (isNothing)
 import Data.Typeable
 
@@ -137,19 +138,32 @@
   => Proxy m
   -> Lockstep state -> LockstepAction state a -> Realized m a -> Maybe String
 checkResponse p (Lockstep state env) action a =
-    compareEquality (observeReal p action a) (observeModel modelResp)
+    compareEquality
+      (a         , observeReal p action a)
+      (modelResp , observeModel modelResp)
   where
     modelResp :: ModelValue state a
     modelResp = fst $ modelNextState action (lookUpEnvF env) state
 
-    compareEquality ::  Observable state a -> Observable state a -> Maybe String
-    compareEquality real mock
-      | real == mock = Nothing
-      | otherwise    = Just $ concat [
+    compareEquality ::
+         (Realized m a, Observable state a)
+      -> (ModelValue state a, Observable state a) -> Maybe String
+    compareEquality (realResp, obsRealResp) (mockResp, obsMockResp)
+      | obsRealResp == obsMockResp = Nothing
+      | otherwise                  = Just $ concat [
             "System under test returned: "
-          , show real
+          , case showRealResponse (Proxy @m) action of
+              Nothing   -> show obsRealResp
+              Just Dict -> concat [
+                  show obsRealResp
+                , " ("
+                , show realResp
+                , ")"
+                ]
           , "\nbut model returned:         "
-          , show mock
+          , show obsMockResp
+          , " ("
+          , show mockResp
+          , ")"
           ]
-
 
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Run.hs b/src/Test/QuickCheck/StateModel/Lockstep/Run.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/Run.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/Run.hs
@@ -6,6 +6,7 @@
 module Test.QuickCheck.StateModel.Lockstep.Run (
     -- * Finding labelled examples
     tagActions
+  , labelActions
     -- * Run tests
   , runActions
   , runActionsBracket
@@ -51,14 +52,17 @@
 -- executed against the model /only/.
 tagActions :: forall state.
      InLockstep state
-  => Proxy state
-  -> Actions (Lockstep state)
-  -> Property
-tagActions _p (Actions steps) =
+  => Proxy state -> Actions (Lockstep state) -> Property
+tagActions _p actions = QC.label ("Tags: " ++ show (labelActions actions)) True
+
+labelActions :: forall state.
+     InLockstep state
+  => Actions (Lockstep state) -> [String]
+labelActions (Actions steps) =
     go Set.empty Test.QuickCheck.StateModel.initialState steps
   where
-    go :: Set String -> Lockstep state -> [Step (Lockstep state)] -> Property
-    go tags _st []            = QC.label ("Tags: " ++ show (Set.toList tags)) True
+    go :: Set String -> Lockstep state -> [Step (Lockstep state)] -> [String]
+    go tags _st []            = Set.toList tags
     go tags  st ((v:=a) : ss) = go' tags st v a ss
 
     go' :: forall a.
@@ -68,7 +72,7 @@
       -> Var a                      -- variable for the result of this action
       -> Action (Lockstep state) a  -- action to execute
       -> [Step (Lockstep state)]    -- remaining steps to execute
-      -> Property
+      -> [String]
     go' tags (Lockstep before env) var action ss =
         go (Set.union (Set.fromList tags') tags) st' ss
       where
@@ -94,16 +98,21 @@
 
 -- | Convenience runner with support for state initialization
 --
--- This is less general than 'Test.QuickCheck.StateModel.runActions', but
--- will be useful in many scenarios.
+-- This is less general than 'Test.QuickCheck.StateModel.runActions', but will
+-- be useful in many scenarios.
+--
+-- For most lockstep-style tests, a suitable monad to run the tests in is
+-- @'ReaderT' r 'IO'@. In this case, using @'runReaderT'@ as the runner argument
+-- is a reasonable choice.
 runActionsBracket ::
-     RunLockstep state (ReaderT st IO)
+     RunLockstep state m
   => Proxy state
   -> IO st         -- ^ Initialisation
   -> (st -> IO ()) -- ^ Cleanup
+  -> (m Property -> st -> IO Property) -- ^ Runner
   -> Actions (Lockstep state) -> Property
-runActionsBracket _ init cleanup actions =
-    monadicBracketIO init cleanup $
+runActionsBracket _ init cleanup runner actions =
+    monadicBracketIO init cleanup runner $
       void $ StateModel.runActions actions
 
 {-------------------------------------------------------------------------------
@@ -114,22 +123,24 @@
      Testable a
   => IO st
   -> (st -> IO ())
-  -> ReaderT st IO a
+  -> (m a -> st -> IO a)
+  -> m a
   -> Property
-ioPropertyBracket init cleanup (ReaderT prop) = do
+ioPropertyBracket init cleanup runner prop =
     QC.ioProperty $ mask $ \restore -> do
       st <- init
-      a  <- restore (prop st) `onException` cleanup st
+      a <- restore (runner prop st) `onException` cleanup st
       cleanup st
       return a
 
 -- | Variation on 'monadicIO' that allows for state initialisation/cleanup
-monadicBracketIO :: forall st a.
-     Testable a
+monadicBracketIO :: forall st a m.
+     (Monad m, Testable a)
   => IO st
   -> (st -> IO ())
-  -> (PropertyM (ReaderT st IO) a)
+  -> (m Property -> st -> IO Property)
+  -> PropertyM m a
   -> Property
-monadicBracketIO init cleanup =
-    monadic (ioPropertyBracket init cleanup)
+monadicBracketIO init cleanup runner =
+    monadic (ioPropertyBracket init cleanup runner)
 
diff --git a/test/Test/IORef.hs b/test/Test/IORef.hs
--- a/test/Test/IORef.hs
+++ b/test/Test/IORef.hs
@@ -1,42 +1,77 @@
+{-# LANGUAGE RecordWildCards #-}
+
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Test.IORef (tests) where
 
+import Control.Monad.Reader
 import Data.Bifunctor
+import Data.Constraint (Dict(..))
 import Data.IORef
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Proxy
 import Test.QuickCheck
 import Test.Tasty
+import Test.Tasty.HUnit
 import Test.Tasty.QuickCheck (testProperty)
 
+import Test.QuickCheck qualified as QC
+
 import Test.QuickCheck.StateModel
 import Test.QuickCheck.StateModel.Lockstep
 import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep
 import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep
+import Test.QuickCheck.StateModel.Lockstep.Run (labelActions)
 
 {-------------------------------------------------------------------------------
   Model "M"
 -------------------------------------------------------------------------------}
 
 type MRef = Int
-type M    = Map MRef Int
 
+data M = M {
+      -- | Value of every var
+      mValues :: Map MRef Int
+
+      -- | Often did we write each value to each var?
+      --
+      -- This is used for tagging.
+    , mWrites :: Map (MRef, Int) Int
+    }
+  deriving (Show)
+
 initModel :: M
-initModel = Map.empty
+initModel = M {
+      mValues = Map.empty
+    , mWrites = Map.empty
+    }
 
 modelNew :: M -> (MRef, M)
-modelNew m = (mockRef, Map.insert mockRef 0 m)
+modelNew M{..} = (
+      mockRef
+    , M { mValues = Map.insert mockRef 0 mValues
+        , mWrites = mWrites
+        }
+    )
   where
     mockRef :: MRef
-    mockRef = Map.size m
+    mockRef = Map.size mValues
 
-modelWrite :: MRef -> Int -> M -> ((), M)
-modelWrite v x m = ((), Map.insert v x m)
+modelWrite :: MRef -> Int -> M -> (Int, M)
+modelWrite v x M{..} = (
+      x
+    , M { mValues = Map.insert v x mValues
+        , mWrites = Map.alter recordWrite (v, x) mWrites
+        }
+    )
+  where
+    recordWrite :: Maybe Int -> Maybe Int
+    recordWrite Nothing  = Just 1 -- First write
+    recordWrite (Just n) = Just (n + 1)
 
 modelRead :: MRef -> M -> (Int, M)
-modelRead v m = (m Map.! v, m)
+modelRead v m@M{..} = (mValues Map.! v, m)
 
 {-------------------------------------------------------------------------------
   Instances
@@ -48,10 +83,13 @@
     New :: Action (Lockstep M) (IORef Int)
 
     -- | Write value to IORef
+    --
+    -- The value is specified either as a concrete value or by reference
+    -- to a previous write.
     Write ::
          ModelVar M (IORef Int)
-      -> Int
-      -> Action (Lockstep M) ()
+      -> Either Int (ModelVar M Int)
+      -> Action (Lockstep M) Int
 
     -- | Read IORef
     Read ::
@@ -64,15 +102,14 @@
   arbitraryAction = Lockstep.arbitraryAction
   shrinkAction    = Lockstep.shrinkAction
 
-instance RunModel (Lockstep M) IO where
+instance RunModel (Lockstep M) RealMonad where
   perform       = \_state -> runIO
   postcondition = Lockstep.postcondition
-  monitoring    = Lockstep.monitoring (Proxy @IO)
+  monitoring    = Lockstep.monitoring (Proxy @RealMonad)
 
 instance InLockstep M where
   data ModelValue M a where
     MRef  :: MRef -> ModelValue M (IORef Int)
-    MUnit :: ()   -> ModelValue M ()
     MInt  :: Int  -> ModelValue M Int
 
   data Observable M a where
@@ -80,12 +117,12 @@
     OId  :: (Show a, Eq a) => a -> Observable M a
 
   observeModel (MRef  _) = ORef
-  observeModel (MUnit x) = OId x
   observeModel (MInt  x) = OId x
 
-  usedVars New         = []
-  usedVars (Write v _) = [SomeGVar v]
-  usedVars (Read  v)   = [SomeGVar v]
+  usedVars New                  = []
+  usedVars (Write v (Left _))   = [SomeGVar v]
+  usedVars (Write v (Right v')) = [SomeGVar v, SomeGVar v']
+  usedVars (Read  v)            = [SomeGVar v]
 
   modelNextState = runModel
 
@@ -103,17 +140,40 @@
            Gen (ModelVar M (IORef Int))
         -> [Gen (Any (LockstepAction M))]
       withVars genVar = [
-            fmap Some $ Write <$> genVar <*> arbitrary
+            fmap Some $ Write <$> genVar <*> (Left <$> choose (0, 10))
           , fmap Some $ Read  <$> genVar
           ]
 
-instance RunLockstep M IO where
+  shrinkWithVars findVars _mock = \case
+      New               -> []
+      Write v (Left x)  -> concat [
+                               Some . Write v . Left  <$> shrink x
+                             , Some . Write v . Right <$> findVars (Proxy @Int)
+                             ]
+      Write _ (Right _) -> []
+      Read  _           -> []
+
+  tagStep (_stBefore, stAfter) _action _result = concat [
+        [ "WriteSameVarTwice"
+        | not
+        . Map.null
+        . Map.filter (\numWrites -> numWrites > 1)
+        $ mWrites stAfter
+        ]
+      ]
+
+instance RunLockstep M RealMonad where
   observeReal _ action result =
       case (action, result) of
         (New     , _) -> ORef
         (Write{} , x) -> OId x
         (Read{}  , x) -> OId x
 
+  showRealResponse _ = \case
+    New{}   -> Nothing
+    Write{} -> Just Dict
+    Read{}  -> Just Dict
+
 deriving instance Show (Action (Lockstep M) a)
 deriving instance Show (Observable M a)
 deriving instance Show (ModelValue M a)
@@ -126,37 +186,88 @@
   Interpreters against the real system and against the model
 -------------------------------------------------------------------------------}
 
-runIO :: Action (Lockstep M) a -> LookUp IO -> IO a
-runIO action lookUp =
+data Buggy = Buggy | NotBuggy
+  deriving (Show, Eq)
+
+instance Arbitrary Buggy where
+  arbitrary = elements [Buggy, NotBuggy]
+
+  shrink Buggy    = [NotBuggy]
+  shrink NotBuggy = []
+
+-- | We trigger a bug if we write the /same/ value to the /same/ variable
+type BrokenRef = [(IORef Int, Int)]
+
+type RealMonad = ReaderT (Buggy, IORef BrokenRef) IO
+
+runIO :: Action (Lockstep M) a -> LookUp RealMonad -> RealMonad a
+runIO action lookUp = ReaderT $ \(buggy, brokenRef) ->
     case action of
       New       -> newIORef 0
-      Write v x -> writeIORef (lookUpRef v) x
-      Read  v   -> readIORef  (lookUpRef v)
+      Write v x -> brokenWrite buggy brokenRef (lookUpRef v) (lookUpInt x)
+      Read  v   -> readIORef (lookUpRef v)
   where
     lookUpRef :: ModelVar M (IORef Int) -> IORef Int
-    lookUpRef = lookUpGVar (Proxy @IO) lookUp
+    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp
 
+    lookUpInt :: Either Int (ModelVar M Int) -> Int
+    lookUpInt (Left  x) = x
+    lookUpInt (Right v) = lookUpGVar (Proxy @RealMonad) lookUp v
+
+-- | The second write to the same variable will be broken
+brokenWrite :: Buggy -> IORef BrokenRef -> IORef Int -> Int -> IO Int
+brokenWrite NotBuggy _         v x = writeIORef v x >> return x
+brokenWrite Buggy    brokenRef v x = do
+    broken <- readIORef brokenRef
+    if (v, x) `elem` broken then
+      writeIORef v 123456789
+    else
+      writeIORef v x
+    modifyIORef brokenRef ((v, x) :)
+    return x
+
 runModel ::
      Action (Lockstep M) a
   -> ModelLookUp M
   -> M -> (ModelValue M a, M)
 runModel action lookUp =
     case action of
-      New       -> first MRef  . modelNew
-      Write v x -> first MUnit . modelWrite (lookUpRef v) x
-      Read  v   -> first MInt  . modelRead  (lookUpRef v)
+      New       -> first MRef . modelNew
+      Write v x -> first MInt . modelWrite (lookUpRef v) (lookUpInt x)
+      Read  v   -> first MInt . modelRead  (lookUpRef v)
   where
     lookUpRef :: ModelVar M (IORef Int) -> MRef
     lookUpRef var = case lookUp var of MRef r -> r
 
+    lookUpInt :: Either Int (ModelVar M Int) -> Int
+    lookUpInt (Left  x) = x
+    lookUpInt (Right v) = case lookUp v of MInt x -> x
+
 {-------------------------------------------------------------------------------
   Top-level tests
 -------------------------------------------------------------------------------}
 
-propIORef :: Actions (Lockstep M) -> Property
-propIORef = Lockstep.runActions (Proxy @M)
+propIORef :: Buggy -> Actions (Lockstep M) -> Property
+propIORef buggy actions =
+      (if triggersBug then expectFailure  else id)
+    $ Lockstep.runActionsBracket
+        (Proxy @M)
+        initBroken
+        (\_ -> return ())
+        runReaderT
+        actions
+  where
+    triggersBug :: Bool
+    triggersBug =
+           buggy == Buggy
+        && "WriteSameVarTwice" `elem` labelActions actions
 
+    initBroken :: IO (Buggy, IORef BrokenRef)
+    initBroken = (buggy,) <$> newIORef []
+
 tests :: TestTree
 tests = testGroup "Test.IORef" [
-      testProperty "runActions" propIORef
+      testCase "labelledExamples" $
+        QC.labelledExamples $ Lockstep.tagActions (Proxy @M)
+    , testProperty "runActions" propIORef
     ]
diff --git a/test/Test/MockFS.hs b/test/Test/MockFS.hs
--- a/test/Test/MockFS.hs
+++ b/test/Test/MockFS.hs
@@ -369,6 +369,7 @@
         Lockstep.runActionsBracket (Proxy @FsState)
           (createTempDirectory tmpDir "QSM")
           removeDirectoryRecursive
+          runReaderT
     ]
   where
     -- TODO: tmpDir should really be a parameter to the test suite