diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Revision history for quickcheck-lockstep
 
+## 0.3.0 -- 2023-10-17
+
+* BREAKING: Update `quickcheck-dynamic` dependency to `>=3.3`.
+* Add compatibility with ghc-9.6 (Javier Sagredo)
+
 ## 0.2.1 -- 2022-12-06
 
 * Expose necessary definitions for custom `Operation` instances (Joris Dral)
diff --git a/quickcheck-lockstep.cabal b/quickcheck-lockstep.cabal
--- a/quickcheck-lockstep.cabal
+++ b/quickcheck-lockstep.cabal
@@ -1,10 +1,10 @@
 cabal-version:      2.4
 name:               quickcheck-lockstep
-version:            0.2.1
+version:            0.3.0
 license:            BSD-3-Clause
 license-file:       LICENSE
 author:             Edsko de Vries
-maintainer:         edsko@well-typed.com
+maintainer:         edsko@well-typed.com, joris@well-typed.com
 extra-source-files: CHANGELOG.md
 category:           Testing
 synopsis:           Library for lockstep-style testing with 'quickcheck-dynamic'
@@ -13,7 +13,7 @@
                     APIs calls, then execute them both against the system under
                     test and against a model, and compare responses up to some
                     notion of observability.
-tested-with:        GHC ==8.10.7 || ==9.0.2 || ==9.2.4 || ==9.4.2
+tested-with:        GHC ==8.10 || ==9.0 || ==9.2 || ==9.4 || ==9.6
 
 source-repository head
   type:     git
@@ -59,12 +59,12 @@
       Test.QuickCheck.StateModel.Lockstep.GVar
   build-depends:
       -- quickcheck-dynamic requires ghc 8.10 minimum
-      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
-    , quickcheck-dynamic >= 2.0  && < 2.1
+      base               >= 4.14   && < 4.19
+    , constraints        >= 0.13   && < 0.14
+    , mtl                >= 2.2    && < 2.4
+    , containers         >= 0.6    && < 0.7
+    , QuickCheck         >= 2.14   && < 2.15
+    , quickcheck-dynamic >= 3.3.1  && < 3.4
   hs-source-dirs:
       src
 
@@ -80,7 +80,8 @@
   other-modules:
       Test.MockFS
       Test.MockFS.Mock
-      Test.IORef
+      Test.IORef.Full
+      Test.IORef.Simple
   default-extensions:
       DeriveGeneric
       EmptyCase
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
@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
 -- | Default implementations for the @quickcheck-dynamic@ class methods
 --
 -- Intended for qualified import.
@@ -18,12 +20,14 @@
 import Prelude hiding (init)
 
 import Data.Constraint (Dict(..))
-import Data.Maybe (isNothing)
+import Data.Set qualified as Set
 import Data.Typeable
 
 import Test.QuickCheck (Gen, Property)
 import Test.QuickCheck qualified as QC
-import Test.QuickCheck.StateModel (Var, Any(..), LookUp, Realized)
+import Test.QuickCheck.StateModel ( Var, Any(..), LookUp, Realized, PostconditionM
+                                  , Action, monitorPost)
+import Test.QuickCheck.StateModel.Variables (VarContext, HasVariables (..))
 
 import Test.QuickCheck.StateModel.Lockstep.API
 import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)
@@ -68,16 +72,17 @@
 -- | Default implementation for 'Test.QuickCheck.StateModel.arbitraryAction'
 arbitraryAction ::
      InLockstep state
-  => Lockstep state -> Gen (Any (LockstepAction state))
-arbitraryAction (Lockstep state env) =
+  => VarContext -> Lockstep state -> Gen (Any (LockstepAction state))
+arbitraryAction _ (Lockstep state env) =
     arbitraryWithVars (varsOfType env) state
 
 -- | Default implementation for 'Test.QuickCheck.StateModel.shrinkAction'
 shrinkAction ::
      InLockstep state
-  => Lockstep state
+  => VarContext
+  -> Lockstep state
   -> LockstepAction state a -> [Any (LockstepAction state)]
-shrinkAction (Lockstep state env) =
+shrinkAction _ (Lockstep state env) =
     shrinkWithVars (varsOfType env) state
 
 {-------------------------------------------------------------------------------
@@ -94,9 +99,11 @@
   -> LockstepAction state a
   -> LookUp m
   -> Realized m a
-  -> m Bool
+  -> PostconditionM m Bool
 postcondition (before, _after) action _lookUp a =
-    pure $ isNothing $ checkResponse (Proxy @m) before action a
+    case checkResponse (Proxy @m) before action a of
+      Nothing -> pure True
+      Just s  -> monitorPost (QC.counterexample s) >> pure False
 
 monitoring :: forall m state a.
      RunLockstep state m
@@ -106,9 +113,8 @@
   -> LookUp m
   -> Realized m a
   -> Property -> Property
-monitoring p (before, after) action _lookUp realResp =
+monitoring _p (before, after) action _lookUp _realResp =
       QC.counterexample ("State: " ++ show after)
-    . maybe id QC.counterexample (checkResponse p before action realResp)
     . QC.tabulate "Tags" tags
   where
     tags :: [String]
@@ -119,6 +125,24 @@
                         action
                         (lookUpEnvF $ lockstepEnv before)
                         (lockstepModel before)
+
+{-------------------------------------------------------------------------------
+  Default class instances
+-------------------------------------------------------------------------------}
+
+-- | Ignore variables for lockstep state.
+--
+-- We largely ignore @quickcheck-dynamic@'s variables in the lockstep framework,
+-- since it does its own accounting of model variables.
+instance HasVariables (Lockstep state) where
+  getAllVariables _ = Set.empty
+
+-- | Ignore variables for lockstep actions.
+--
+-- We largely ignore @quickcheck-dynamic@'s variables in the lockstep framework,
+-- since it does its own accounting of model variables.
+instance HasVariables (Action (Lockstep state) a) where
+  getAllVariables _ = Set.empty
 
 {-------------------------------------------------------------------------------
   Internal auxiliary
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs b/src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/EnvF.hs
@@ -21,7 +21,7 @@
 import Data.Maybe (mapMaybe)
 import Data.Typeable
 
-import Test.QuickCheck.StateModel (Var(..))
+import Test.QuickCheck.StateModel.Variables (Var, unsafeCoerceVar)
 
 {-------------------------------------------------------------------------------
   Types
@@ -51,8 +51,8 @@
     asum $ map (\(EnvEntry var' fa') -> aux var var' fa') env
   where
     aux :: Typeable a' => Var a -> Var a' -> f a' -> Maybe (f a)
-    aux (Var x) (Var y) fa' = do
-        guard (x == y)
+    aux v1 v2 fa' = do
+        guard (v1 == unsafeCoerceVar v2)
         cast fa'
 
 keysOfType :: Typeable a => EnvF f -> [Var a]
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs b/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/GVar.hs
@@ -21,7 +21,7 @@
 import Data.Maybe (isJust, fromJust)
 import Data.Typeable
 
-import Test.QuickCheck.StateModel (Var(..), LookUp, Realized)
+import Test.QuickCheck.StateModel (Var, LookUp, Realized)
 
 import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)
 import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF
diff --git a/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs b/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs
--- a/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs
+++ b/src/Test/QuickCheck/StateModel/Lockstep/Op/SumProd.hs
@@ -1,5 +1,10 @@
+{-# LANGUAGE CPP #-}
+
 module Test.QuickCheck.StateModel.Lockstep.Op.SumProd (Op(..), intOpId) where
 
+#if __GLASGOW_HASKELL__ >= 906
+import Control.Monad ((<=<))
+#endif
 import Control.Monad.Reader (ReaderT)
 import Control.Monad.State
 import GHC.Show (appPrec)
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
@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
 -- | Run lockstep tests
 --
 -- Intended for qualified import.
@@ -15,7 +17,11 @@
 import Prelude hiding (init)
 
 import Control.Exception
+#if __GLASGOW_HASKELL__ >= 906
+import Control.Monad (void)
+#else
 import Control.Monad.Reader
+#endif
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Typeable
@@ -63,7 +69,7 @@
   where
     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 tags  st ((v:=a) : ss) = go' tags st v (polarAction a) ss
 
     go' :: forall a.
          Typeable a
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -2,11 +2,13 @@
 
 import Test.Tasty
 
-import Test.IORef qualified
-import Test.MockFS qualified
+import Test.IORef.Full   qualified
+import Test.IORef.Simple qualified
+import Test.MockFS       qualified
 
 main :: IO ()
 main = defaultMain $ testGroup "quickcheck-lockstep" [
-      Test.IORef.tests
+      Test.IORef.Simple.tests
+    , Test.IORef.Full.tests
     , Test.MockFS.tests
     ]
diff --git a/test/Test/IORef.hs b/test/Test/IORef.hs
deleted file mode 100644
--- a/test/Test/IORef.hs
+++ /dev/null
@@ -1,273 +0,0 @@
-{-# 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
-
-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 = M {
-      mValues = Map.empty
-    , mWrites = Map.empty
-    }
-
-modelNew :: M -> (MRef, M)
-modelNew M{..} = (
-      mockRef
-    , M { mValues = Map.insert mockRef 0 mValues
-        , mWrites = mWrites
-        }
-    )
-  where
-    mockRef :: MRef
-    mockRef = Map.size mValues
-
-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{..} = (mValues Map.! v, m)
-
-{-------------------------------------------------------------------------------
-  Instances
--------------------------------------------------------------------------------}
-
-instance StateModel (Lockstep M) where
-  data Action (Lockstep M) a where
-    -- | Create new IORef
-    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)
-      -> Either Int (ModelVar M Int)
-      -> Action (Lockstep M) Int
-
-    -- | Read IORef
-    Read ::
-         ModelVar M (IORef Int)
-      -> Action (Lockstep M) Int
-
-  initialState    = Lockstep.initialState initModel
-  nextState       = Lockstep.nextState
-  precondition    = Lockstep.precondition
-  arbitraryAction = Lockstep.arbitraryAction
-  shrinkAction    = Lockstep.shrinkAction
-
-instance RunModel (Lockstep M) RealMonad where
-  perform       = \_state -> runIO
-  postcondition = Lockstep.postcondition
-  monitoring    = Lockstep.monitoring (Proxy @RealMonad)
-
-instance InLockstep M where
-  data ModelValue M a where
-    MRef  :: MRef -> ModelValue M (IORef Int)
-    MInt  :: Int  -> ModelValue M Int
-
-  data Observable M a where
-    ORef :: Observable M (IORef Int)
-    OId  :: (Show a, Eq a) => a -> Observable M a
-
-  observeModel (MRef  _) = ORef
-  observeModel (MInt  x) = OId x
-
-  usedVars New                  = []
-  usedVars (Write v (Left _))   = [SomeGVar v]
-  usedVars (Write v (Right v')) = [SomeGVar v, SomeGVar v']
-  usedVars (Read  v)            = [SomeGVar v]
-
-  modelNextState = runModel
-
-  arbitraryWithVars findVars _mock = oneof $ concat [
-        withoutVars
-      , case findVars (Proxy @(IORef Int)) of
-          []   -> []
-          vars -> withVars (elements vars)
-      ]
-    where
-      withoutVars :: [Gen (Any (LockstepAction M))]
-      withoutVars = [return $ Some New]
-
-      withVars ::
-           Gen (ModelVar M (IORef Int))
-        -> [Gen (Any (LockstepAction M))]
-      withVars genVar = [
-            fmap Some $ Write <$> genVar <*> (Left <$> choose (0, 10))
-          , fmap Some $ Read  <$> genVar
-          ]
-
-  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)
-
-deriving instance Eq (Action (Lockstep M) a)
-deriving instance Eq (Observable M a)
-deriving instance Eq (ModelValue M a)
-
-{-------------------------------------------------------------------------------
-  Interpreters against the real system and against the model
--------------------------------------------------------------------------------}
-
-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 -> brokenWrite buggy brokenRef (lookUpRef v) (lookUpInt x)
-      Read  v   -> readIORef (lookUpRef v)
-  where
-    lookUpRef :: ModelVar M (IORef Int) -> IORef Int
-    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 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 :: 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" [
-      testCase "labelledExamples" $
-        QC.labelledExamples $ Lockstep.tagActions (Proxy @M)
-    , testProperty "runActions" propIORef
-    ]
diff --git a/test/Test/IORef/Full.hs b/test/Test/IORef/Full.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/IORef/Full.hs
@@ -0,0 +1,273 @@
+{-# LANGUAGE RecordWildCards #-}
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.IORef.Full (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
+
+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 = M {
+      mValues = Map.empty
+    , mWrites = Map.empty
+    }
+
+modelNew :: M -> (MRef, M)
+modelNew M{..} = (
+      mockRef
+    , M { mValues = Map.insert mockRef 0 mValues
+        , mWrites = mWrites
+        }
+    )
+  where
+    mockRef :: MRef
+    mockRef = Map.size mValues
+
+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{..} = (mValues Map.! v, m)
+
+{-------------------------------------------------------------------------------
+  Instances
+-------------------------------------------------------------------------------}
+
+instance StateModel (Lockstep M) where
+  data Action (Lockstep M) a where
+    -- | Create new IORef
+    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)
+      -> Either Int (ModelVar M Int)
+      -> Action (Lockstep M) Int
+
+    -- | Read IORef
+    Read ::
+         ModelVar M (IORef Int)
+      -> Action (Lockstep M) Int
+
+  initialState    = Lockstep.initialState initModel
+  nextState       = Lockstep.nextState
+  precondition    = Lockstep.precondition
+  arbitraryAction = Lockstep.arbitraryAction
+  shrinkAction    = Lockstep.shrinkAction
+
+instance RunModel (Lockstep M) RealMonad where
+  perform       = \_state -> runIO
+  postcondition = Lockstep.postcondition
+  monitoring    = Lockstep.monitoring (Proxy @RealMonad)
+
+instance InLockstep M where
+  data ModelValue M a where
+    MRef  :: MRef -> ModelValue M (IORef Int)
+    MInt  :: Int  -> ModelValue M Int
+
+  data Observable M a where
+    ORef :: Observable M (IORef Int)
+    OId  :: (Show a, Eq a) => a -> Observable M a
+
+  observeModel (MRef  _) = ORef
+  observeModel (MInt  x) = OId x
+
+  usedVars New                  = []
+  usedVars (Write v (Left _))   = [SomeGVar v]
+  usedVars (Write v (Right v')) = [SomeGVar v, SomeGVar v']
+  usedVars (Read  v)            = [SomeGVar v]
+
+  modelNextState = runModel
+
+  arbitraryWithVars findVars _mock = oneof $ concat [
+        withoutVars
+      , case findVars (Proxy @(IORef Int)) of
+          []   -> []
+          vars -> withVars (elements vars)
+      ]
+    where
+      withoutVars :: [Gen (Any (LockstepAction M))]
+      withoutVars = [return $ Some New]
+
+      withVars ::
+           Gen (ModelVar M (IORef Int))
+        -> [Gen (Any (LockstepAction M))]
+      withVars genVar = [
+            fmap Some $ Write <$> genVar <*> (Left <$> choose (0, 10))
+          , fmap Some $ Read  <$> genVar
+          ]
+
+  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)
+
+deriving instance Eq (Action (Lockstep M) a)
+deriving instance Eq (Observable M a)
+deriving instance Eq (ModelValue M a)
+
+{-------------------------------------------------------------------------------
+  Interpreters against the real system and against the model
+-------------------------------------------------------------------------------}
+
+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 -> brokenWrite buggy brokenRef (lookUpRef v) (lookUpInt x)
+      Read  v   -> readIORef (lookUpRef v)
+  where
+    lookUpRef :: ModelVar M (IORef Int) -> IORef Int
+    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 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 :: 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.Full" [
+      testCase "labelledExamples" $
+        QC.labelledExamples $ Lockstep.tagActions (Proxy @M)
+    , testProperty "runActions" propIORef
+    ]
diff --git a/test/Test/IORef/Simple.hs b/test/Test/IORef/Simple.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/IORef/Simple.hs
@@ -0,0 +1,183 @@
+{-# LANGUAGE RecordWildCards #-}
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.IORef.Simple (tests) where
+
+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.QuickCheck (testProperty)
+
+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
+
+{-------------------------------------------------------------------------------
+  Model "M"
+-------------------------------------------------------------------------------}
+
+type MRef = Int
+
+data M = M {
+      -- | Value of every var
+      mValues :: Map MRef Int
+    }
+  deriving (Show)
+
+initModel :: M
+initModel = M { mValues = Map.empty }
+
+modelNew :: M -> (MRef, M)
+modelNew M{..} = (
+      mockRef
+    , M { mValues = Map.insert mockRef 0 mValues }
+    )
+  where
+    mockRef :: MRef
+    mockRef = Map.size mValues
+
+modelWrite :: MRef -> Int -> M -> ((), M)
+modelWrite v x M{..} = (
+      ()
+    , M { mValues = Map.insert v x mValues }
+    )
+
+modelRead :: MRef -> M -> (Int, M)
+modelRead v m@M{..} = (mValues Map.! v, m)
+
+{-------------------------------------------------------------------------------
+  Instances
+-------------------------------------------------------------------------------}
+
+instance StateModel (Lockstep M) where
+  data Action (Lockstep M) a where
+    -- | Create new IORef
+    New :: Action (Lockstep M) (IORef Int)
+
+    -- | Write value to IORef
+    Write ::
+         ModelVar M (IORef Int)
+      -> Int
+      -> Action (Lockstep M) ()
+
+    -- | Read IORef
+    Read ::
+         ModelVar M (IORef Int)
+      -> Action (Lockstep M) Int
+
+  initialState    = Lockstep.initialState initModel
+  nextState       = Lockstep.nextState
+  precondition    = Lockstep.precondition
+  arbitraryAction = Lockstep.arbitraryAction
+  shrinkAction    = Lockstep.shrinkAction
+
+instance RunModel (Lockstep M) RealMonad where
+  perform       = \_state -> runIO
+  postcondition = Lockstep.postcondition
+  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
+    ORef :: Observable M (IORef Int)
+    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]
+
+  modelNextState = runModel
+
+  arbitraryWithVars findVars _mock = oneof $ concat [
+        withoutVars
+      , case findVars (Proxy @(IORef Int)) of
+          []   -> []
+          vars -> withVars (elements vars)
+      ]
+    where
+      withoutVars :: [Gen (Any (LockstepAction M))]
+      withoutVars = [return $ Some New]
+
+      withVars ::
+           Gen (ModelVar M (IORef Int))
+        -> [Gen (Any (LockstepAction M))]
+      withVars genVar = [
+            fmap Some $ Write <$> genVar <*> choose (0, 10)
+          , fmap Some $ Read  <$> genVar
+          ]
+
+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)
+
+deriving instance Eq (Action (Lockstep M) a)
+deriving instance Eq (Observable M a)
+deriving instance Eq (ModelValue M a)
+
+{-------------------------------------------------------------------------------
+  Interpreters against the real system and against the model
+-------------------------------------------------------------------------------}
+
+type RealMonad = IO
+
+runIO :: Action (Lockstep M) a -> LookUp RealMonad -> RealMonad a
+runIO action lookUp =
+    case action of
+      New       -> newIORef 0
+      Write v x -> writeIORef (lookUpRef v) x
+      Read  v   -> readIORef (lookUpRef v)
+  where
+    lookUpRef :: ModelVar M (IORef Int) -> IORef Int
+    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp
+
+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)
+  where
+    lookUpRef :: ModelVar M (IORef Int) -> MRef
+    lookUpRef var = case lookUp var of MRef r -> r
+
+{-------------------------------------------------------------------------------
+  Top-level tests
+-------------------------------------------------------------------------------}
+
+propIORef :: Actions (Lockstep M) -> Property
+propIORef = Lockstep.runActions (Proxy @M)
+
+tests :: TestTree
+tests = testGroup "Test.IORef.Simple" [
+      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
@@ -32,7 +32,7 @@
 
 import Test.QuickCheck (Gen)
 import Test.QuickCheck qualified as QC
-import Test.QuickCheck.StateModel
+import Test.QuickCheck.StateModel hiding (vars)
 
 import Test.QuickCheck.StateModel.Lockstep
 import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep