diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,28 @@
 # Revision history for quickcheck-lockstep
 
+## 0.7.0 -- 2025-05-09
+
+* BREAKING: Rename `lookupGVar` to `realLookupVar`, and add a `RealLookup`
+  convenience alias that is used in the type of `RealLookupVar`. The type of
+  `realLookupVar` is slightly different than the type of `lookupGVar`, but only
+  in the positions of universal quantification over types.
+* NON-BREAKING: improved error messages for `realLookupVar` and `lookupVar`,
+  which might throw an error when variables are ill-defined or unevaluable.
+* PATCH: some documentation is moved from convenience aliases like
+  `ModelFindVariables` to the functions have these aliases in their type, like
+  `findVars`.
+* BREAKING: Enable verbose counterexamples by default in the 'postcondition'
+  function using 'postconditionWith'.
+* NON-BREAKING: Add a new 'postconditionWith' function that can be configured to
+  produce more verbose counterexamples. With verbosity disabled, all states of
+  the model are printed in a counterexample. If verbosity is enabled, the
+  counterexample will also include all responses from the real system and the
+  model.
+* NON-BREAKING: Add a new `shrinkVar` function and `ModelShrinkVar` type alias.
+  Use `shrinkVar` to shrink variables to earlier variables of the same type.
+* PATCH: allow building with `ghc-9.12`
+* PATCH: support `containers-0.8`
+
 ## 0.6.0 -- 2024-12-03
 
 * BREAKING: Generalise `ModelFindVariables` and `ModelLookup` to
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.6.0
+version:         0.7.0
 license:         BSD-3-Clause
 license-file:    LICENSE
 author:          Edsko de Vries
@@ -21,7 +21,14 @@
   notion of observability.
 
 tested-with:
-  GHC ==8.10 || ==9.0 || ==9.2 || ==9.4 || ==9.6 || ==9.8 || ==9.10
+  GHC ==8.10
+   || ==9.0
+   || ==9.2
+   || ==9.4
+   || ==9.6
+   || ==9.8
+   || ==9.10
+   || ==9.12
 
 source-repository head
   type:     git
@@ -65,9 +72,9 @@
 
   -- quickcheck-dynamic requires ghc 8.10 minimum
   build-depends:
-    , base                >=4.14   && <4.21
+    , base                >=4.14   && <4.22
     , constraints         ^>=0.13  || ^>=0.14
-    , containers          ^>=0.6   || ^>=0.7
+    , containers          ^>=0.6   || ^>=0.7  || ^>=0.8
     , mtl                 ^>=2.2   || ^>=2.3
     , QuickCheck          ^>=2.14  || ^>=2.15
     , quickcheck-dynamic  ^>=3.4.1
@@ -80,6 +87,7 @@
   hs-source-dirs:     test
   main-is:            Main.hs
   other-modules:
+    Test.Golden
     Test.IORef.Full
     Test.IORef.Simple
     Test.MockFS
@@ -91,7 +99,7 @@
 
   -- Version bounds determined by main lib
   build-depends:
-    , base
+    , base < 5
     , constraints
     , containers
     , directory
@@ -101,6 +109,31 @@
     , quickcheck-dynamic
     , quickcheck-lockstep
     , tasty
+    , tasty-golden
     , tasty-hunit
     , tasty-quickcheck
     , temporary
+
+test-suite test-internals
+  import:         lang
+  type:           exitcode-stdio-1.0
+  hs-source-dirs: test-internals src
+  main-is:        Main.hs
+  other-modules:
+    Test.QuickCheck.StateModel.Lockstep.EnvF
+    Test.QuickCheck.StateModel.Lockstep.GVar
+    Test.QuickCheck.StateModel.Lockstep.Op
+    Test.QuickCheck.StateModel.Lockstep.Op.SumProd
+    Test.Test.QuickCheck.StateModel.Lockstep.GVar
+
+  ghc-options:
+    -Wno-prepositive-qualified-module
+
+  -- Version bounds determined by main lib
+  build-depends:
+    , base < 5
+    , quickcheck-dynamic
+    , tasty
+    , mtl
+    , tasty-quickcheck
+    , QuickCheck
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
@@ -20,16 +20,19 @@
   , LockstepAction
   , ModelFindVariables
   , ModelLookUp
+  , ModelShrinkVar
   , ModelVar
+  , RealLookUp
     -- * Variable context
   , ModelVarContext
   , lookupVar
   , findVars
+  , shrinkVar
+  , realLookupVar
     -- * Variables
   , GVar -- opaque
   , AnyGVar(..)
   , unsafeMkGVar
-  , lookUpGVar
   , mapGVar
     -- ** Operations
   , Operation(..)
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
@@ -15,10 +15,14 @@
   , ModelFindVariables
   , ModelLookUp
   , ModelVar
+  , ModelShrinkVar
+  , RealLookUp
     -- * Variable context
   , ModelVarContext
   , findVars
   , lookupVar
+  , shrinkVar
+  , realLookupVar
   ) where
 
 import Data.Constraint (Dict(..))
@@ -26,7 +30,7 @@
 import Data.Typeable
 
 import Test.QuickCheck (Gen)
-import Test.QuickCheck.StateModel (StateModel, Any, RunModel, Realized, Action)
+import Test.QuickCheck.StateModel (StateModel, Any, RunModel, Realized, Action, LookUp)
 
 import Test.QuickCheck.StateModel.Lockstep.EnvF (EnvF)
 import Test.QuickCheck.StateModel.Lockstep.GVar (GVar, AnyGVar(..), fromVar)
@@ -179,20 +183,20 @@
 -- | An action in the lock-step model
 type LockstepAction state = Action (Lockstep state)
 
--- | Look up a variable for model execution
---
--- The type of the variable is the type in the /real/ system.
+-- | See 'lookupVar'.
 type ModelLookUp state = forall a. ModelVar state a -> ModelValue state a
 
--- | Find variables of the appropriate type
---
--- The type you pass must be the result type of (previously executed) actions.
--- If you want to change the type of the variable, see
--- 'StateModel.Lockstep.GVar.map'.
+-- | See 'findVars'.
 type ModelFindVariables state = forall a.
           Typeable a
        => Proxy a -> [GVar (ModelOp state) a]
 
+-- | See 'shrinkVar'.
+type ModelShrinkVar state = forall a. ModelVar state a -> [ModelVar state a]
+
+-- | See 'realLookupVar'.
+type RealLookUp m op = forall a. Proxy m -> LookUp m -> GVar op a -> Realized m a
+
 -- | Variables with a "functor-esque" instance
 type ModelVar state = GVar (ModelOp state)
 
@@ -203,18 +207,45 @@
 -- | The environment of known variables and their (model) values.
 --
 -- This environment can be queried for information about known variables through
--- 'findVars' and 'lookupVar'. This environment is updated automically by the
--- lockstep framework.
+-- 'findVars', 'lookupVar', and 'shrinkVar'. This environment is updated
+-- automically by the lockstep framework.
 type ModelVarContext state = EnvF (ModelValue state)
 
--- | See 'ModelFindVariables'.
+-- | Find variables of the appropriate type
+--
+-- The type you pass must be the result type of (previously executed) actions.
+-- If you want to change the type of the variable, see 'EnvF.mapGVar'.
 findVars ::
      InLockstep state
   => ModelVarContext state -> ModelFindVariables state
 findVars env _ = map fromVar $ EnvF.keysOfType env
 
--- | See 'ModelLookUp'.
+-- | Look up a variable for execution of the model.
+--
+-- The type of the variable is the type in the /real/ system.
 lookupVar ::
      InLockstep state
   => ModelVarContext state -> ModelLookUp state
-lookupVar env = EnvF.lookUpEnvF env
+lookupVar env gvar = case EnvF.lookUpEnvF env gvar of
+    Just x -> x
+    Nothing -> error
+      "lookupVar: the variable (ModelVar) must be well-defined and evaluable, \
+      \but this requirement was violated. Normally, this is guaranteed by the \
+      \default test 'precondition'."
+
+-- | Shrink variables to /earlier/ variables of the same type.
+shrinkVar ::
+     (Typeable state, InterpretOp (ModelOp state) (ModelValue state))
+  => ModelVarContext state -> ModelShrinkVar state
+shrinkVar env var = EnvF.shrinkGVar env var
+
+-- | Look up a variable for execution of the real system.
+--
+-- The type of the variable is the type in the /real/ system.
+realLookupVar :: InterpretOp op (WrapRealized m) => RealLookUp m op
+realLookupVar p lookUp gvar = case EnvF.lookUpGVar p lookUp gvar of
+    Just x -> x
+    Nothing -> error
+      "realLookupVar: the variable (GVar) must be well-defined and evaluable, \
+      \but this requirement was violated. Normally, this is guaranteed by the \
+      \default test 'precondition'."
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
@@ -14,6 +14,7 @@
   , shrinkAction
     -- * Default implementations for methods of 'RunModel'
   , postcondition
+  , postconditionWith
   , monitoring
   ) where
 
@@ -99,10 +100,27 @@
   -> LookUp m
   -> Realized m a
   -> PostconditionM m Bool
-postcondition (before, _after) action _lookUp a =
+postcondition = postconditionWith True
+
+-- | Like 'postcondition', but with configurable verbosity.
+--
+-- By default, all states of the model are printed when a property
+-- counterexample is printed. If verbose output is enabled, the counterexample
+-- will also print all responses from the real system and the model.
+postconditionWith :: forall m state a.
+     RunLockstep state m
+  => Bool -- ^ Verbose output
+  -> (Lockstep state, Lockstep state)
+  -> LockstepAction state a
+  -> LookUp m
+  -> Realized m a
+  -> PostconditionM m Bool
+postconditionWith verbose (before, _after) action _lookUp a =
     case checkResponse (Proxy @m) before action a of
-      Nothing -> pure True
-      Just s  -> monitorPost (QC.counterexample s) >> pure False
+      Right s
+        | verbose -> monitorPost (QC.counterexample s) >> pure True
+        | otherwise -> pure True
+      Left s  -> monitorPost (QC.counterexample s) >> pure False
 
 monitoring :: forall m state a.
      RunLockstep state m
@@ -155,7 +173,7 @@
 checkResponse :: forall m state a.
      RunLockstep state m
   => Proxy m
-  -> Lockstep state -> LockstepAction state a -> Realized m a -> Maybe String
+  -> Lockstep state -> LockstepAction state a -> Realized m a -> Either String String
 checkResponse p (Lockstep state env) action a =
     compareEquality
       (a         , observeReal p action a)
@@ -166,23 +184,34 @@
 
     compareEquality ::
          (Realized m a, Observable state a)
-      -> (ModelValue state a, Observable state a) -> Maybe String
+      -> (ModelValue state a, Observable state a) -> Either String String
     compareEquality (realResp, obsRealResp) (mockResp, obsMockResp)
-      | obsRealResp == obsMockResp = Nothing
-      | otherwise                  = Just $ concat [
+      | obsRealResp == obsMockResp = Right $ concat [
             "System under test returned: "
-          , case showRealResponse (Proxy @m) action of
-              Nothing   -> show obsRealResp
-              Just Dict -> concat [
-                  show obsRealResp
-                , " ("
-                , show realResp
-                , ")"
-                ]
+          , sutReturned
+          , "\nModel returned:             "
+          , modelReturned
+          ]
+      | otherwise                  = Left $ concat [
+            "System under test returned: "
+          , sutReturned
           , "\nbut model returned:         "
-          , show obsMockResp
-          , " ("
-          , show mockResp
-          , ")"
+          , modelReturned
           ]
 
+      where
+        sutReturned = case showRealResponse (Proxy @m) action of
+            Nothing   -> show obsRealResp
+            Just Dict -> concat [
+                show obsRealResp
+              , " ("
+              , show realResp
+              , ")"
+              ]
+
+        modelReturned = concat [
+              show obsMockResp
+            , " ("
+            , show mockResp
+            , ")"
+            ]
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
@@ -1,3 +1,5 @@
+{-# LANGUAGE PatternSynonyms #-}
+
 -- | Environment parameterised by functor @f@
 --
 -- Intended for qualified import:
@@ -12,6 +14,10 @@
     -- * Query
   , lookup
   , keysOfType
+  , shrinkVar
+    -- * Internal: exposed for testing
+  , pattern EnvF
+  , EnvEntry (..)
   ) where
 
 import Prelude hiding (lookup)
@@ -57,3 +63,11 @@
 
 keysOfType :: Typeable a => EnvF f -> [Var a]
 keysOfType (EnvF env) = mapMaybe (\(EnvEntry var _) -> cast var) env
+
+-- | Shrink a variable to variables of the same type, but with a smaller
+-- variable number.
+--
+-- The numbering of variables is according to their age, meaning that this
+-- function shrinks a variable to /earlier/ variables.
+shrinkVar :: Typeable a => EnvF f -> Var a -> [Var a]
+shrinkVar envf v = [ v' | v' <- keysOfType envf, v' < v ]
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
@@ -1,3 +1,4 @@
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- | Generalized variables
@@ -15,11 +16,14 @@
     -- * Interop with 'EnvF'
   , lookUpEnvF
   , definedInEnvF
+  , shrinkGVar
+    -- * Internal: exposed for testing
+  , pattern GVar
   ) where
 
 import Prelude hiding (map)
 
-import Data.Maybe (isJust, fromJust)
+import Data.Maybe (isJust)
 import Data.Typeable
 
 import GHC.Show
@@ -37,7 +41,7 @@
 -- | Generalized variables
 --
 -- The key difference between 'GVar' and the standard 'Var' type is that
--- 'GVar' have a functor-esque structure: see 'map'.
+-- 'GVar' have a functor-esque structure: see 'mapGVar'.
 data GVar op f where
   GVar :: Typeable x => Var x -> op x y -> GVar op y
 
@@ -92,13 +96,13 @@
 
 -- | Lookup 'GVar' given a lookup function for 'Var'
 --
--- The variable must be in the environment and evaluation must succeed.
--- This is normally guaranteed by the default test 'precondition'.
+-- The result is 'Just' if the variable is in the environment and evaluation
+-- succeeds. This is normally guaranteed by the default test 'precondition'.
 lookUpGVar ::
      InterpretOp op (WrapRealized m)
-  => Proxy m -> LookUp m -> GVar op a -> Realized m a
+  => Proxy m -> LookUp m -> GVar op a -> Maybe (Realized m a)
 lookUpGVar p lookUp (GVar var op) =
-    unwrapRealized $ fromJust $ intOp op (lookUpWrapped p lookUp var)
+    unwrapRealized <$> intOp op (lookUpWrapped p lookUp var)
 
 {-------------------------------------------------------------------------------
   Interop with EnvF
@@ -106,13 +110,22 @@
 
 -- | Lookup 'GVar'
 --
--- The variable must be in the environment and evaluation must succeed.
--- This is normally guaranteed by the default test 'precondition'.
-lookUpEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> f a
-lookUpEnvF env (GVar var op) = fromJust $
+-- The result is 'Just' if the variable is in the environment and evaluation
+-- succeeds. This is normally guaranteed by the default test 'precondition'.
+lookUpEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> Maybe (f a)
+lookUpEnvF env (GVar var op) =
     EnvF.lookup var env >>= intOp op
 
 -- | Check if the variable is well-defined and evaluation will succeed.
 definedInEnvF :: (Typeable f, InterpretOp op f) => EnvF f -> GVar op a -> Bool
-definedInEnvF env (GVar var op) = isJust $
-    EnvF.lookup var env >>= intOp op
+definedInEnvF env gvar = isJust (lookUpEnvF env gvar)
+
+-- | Shrink a 'GVar' to earlier 'GVar's of the same type. It is guaranteed that
+-- the shrunk variables are in the environment and that evaluation will succeed.
+shrinkGVar :: (Typeable f, InterpretOp op f)  => EnvF f -> GVar op a -> [GVar op a]
+shrinkGVar env (GVar var op) =
+    [ gvar'
+    | var' <- EnvF.shrinkVar env var
+    , let gvar' = GVar var' op
+    , definedInEnvF env gvar'
+    ]
diff --git a/test-internals/Main.hs b/test-internals/Main.hs
new file mode 100644
--- /dev/null
+++ b/test-internals/Main.hs
@@ -0,0 +1,9 @@
+module Main (main) where
+
+import           Test.Tasty
+import qualified Test.Test.QuickCheck.StateModel.Lockstep.GVar
+
+main :: IO ()
+main = defaultMain $ testGroup "quickcheck-lockstep-internals" [
+      Test.Test.QuickCheck.StateModel.Lockstep.GVar.tests
+    ]
diff --git a/test-internals/Test/Test/QuickCheck/StateModel/Lockstep/GVar.hs b/test-internals/Test/Test/QuickCheck/StateModel/Lockstep/GVar.hs
new file mode 100644
--- /dev/null
+++ b/test-internals/Test/Test/QuickCheck/StateModel/Lockstep/GVar.hs
@@ -0,0 +1,176 @@
+{-# LANGUAGE DerivingStrategies #-}
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.Test.QuickCheck.StateModel.Lockstep.GVar where
+
+import           Data.Data                                      (eqT,
+                                                                 (:~:) (Refl))
+import           Data.Functor.Identity
+import           Test.QuickCheck.StateModel.Lockstep.EnvF       hiding
+                                                                (shrinkVar)
+import           Test.QuickCheck.StateModel.Lockstep.GVar
+import           Test.QuickCheck.StateModel.Lockstep.Op
+import           Test.QuickCheck.StateModel.Lockstep.Op.SumProd
+import           Test.QuickCheck.StateModel.Variables           hiding
+                                                                (shrinkVar)
+import           Test.Tasty
+import           Test.Tasty.QuickCheck
+
+tests :: TestTree
+tests = testGroup "Test.Test.QuickCheck.StateModel.Lockstep.GVar" [
+      testProperty "prop_shrinkGVar_wellDefined" $
+        forAllShrinkShow genEnvironment shrinkEnvironment showEnvironment $ \env ->
+        forAllShrink genGVar shrinkGVar' $ \gvar ->
+        prop_shrinkGVar_wellDefinedAndEvaluable env gvar
+    ]
+
+{-------------------------------------------------------------------------------
+  Well-defined and evaluable shrinks
+-------------------------------------------------------------------------------}
+
+-- | Verify that 'GVar's are only shrunk to 'GVar's that are well-defined and
+-- evaluable wth respect to the environment.
+prop_shrinkGVar_wellDefinedAndEvaluable :: EnvF Identity -> GVar Op Int -> Property
+prop_shrinkGVar_wellDefinedAndEvaluable env gvar =
+    -- It's not important for the test that the input GVar is well-defined, but
+    -- we label the test case anyway to see that the input GVar is /sometimes/
+    -- well-defined.
+    tabulate "Input GVar is well-defined" [show (definedInEnvF env gvar)] $
+    tabulate "Number of shrinks" [show (length shrinks)] $
+    conjoin [ prop gvar' | gvar' <- shrinks]
+  where
+    shrinks = shrinkGVar env gvar
+
+    prop gvar' =
+      counterexample ("Shrunk GVar is not in the environment: " ++ show gvar')
+        (definedInEnvF env gvar')
+
+{-------------------------------------------------------------------------------
+  Well-defined and evaluable shrinks: generators, shrinkers, printers
+-------------------------------------------------------------------------------}
+
+instance InterpretOp Op Identity where
+  intOp op = traverse (intOpId op)
+
+-- NOTE: both the environment and variables contain/are existential types, which
+-- can get a little bit complicated when writing generators, shrinkers and
+-- printers. Thus for simplicity, we take a dynamic typing approach that throws
+-- errors once we encounter a type that we did not expect. It does make
+-- functions partial and the code a little bit ugly, but it works well enough
+-- for testing well-defined and evaluable shrinks.
+
+-- With just two types of 'Var's, we can test most interesting cases of
+-- (non-)well-defined and (non-)successful evaluation.
+type T1 = Either Int Char
+type T2 = Either Char Int
+
+-- | Generate an environment that maps 'T1' and 'T2' variables to 'T1' and 'T2' values
+-- respectively.
+genEnvironment :: Gen (EnvF Identity)
+genEnvironment = do
+    NonNegative (Small n) <- arbitrary
+    genInsert empty n
+  where
+    genInsert :: EnvF Identity -> Int -> Gen (EnvF Identity)
+    genInsert acc 0 = pure acc
+    genInsert acc n = do
+        b <- elements [True, False]
+        if b then do
+          var <- genVar
+          x <- genValue1
+          genInsert (insert var (Identity x) acc) (n-1)
+        else do
+          var <- genVar
+          x <- genValue2
+          genInsert (insert var (Identity x) acc) (n-1)
+
+shrinkEnvironment :: EnvF Identity -> [EnvF Identity]
+shrinkEnvironment (EnvF xs) = EnvF <$> liftShrink shrinkEntry xs
+
+-- | Shrink each entry individually, but also shrink T1 entries towards T2 entries
+shrinkEntry :: EnvEntry Identity -> [EnvEntry Identity]
+shrinkEntry (EnvEntry (var :: Var a) (Identity x))
+    -- A T1 entry
+    | Just Refl <- eqT @a @T1
+    = -- Shrink either the variable, or shrink the value, or ...
+      [ EnvEntry var' (Identity x')
+      | (var', x') <- liftShrink2 shrinkVar shrinkValue1 (var, x)
+      ] ++
+      -- ... shrink towards a T2 entry
+      [ EnvEntry (unsafeCoerceVar var :: Var T2) (Identity x')
+      | x' <- case x of
+                Left y  -> [Right y]
+                Right{} -> []
+      ]
+    -- A T2 entry
+    | Just Refl <- eqT @a @T2
+    =  -- Shrink either the variable, or shrink the value
+      [ EnvEntry var' (Identity x')
+      | (var', x') <- liftShrink2 shrinkVar shrinkValue2 (var, x)
+      ]
+    | otherwise
+    = error "shrinkEntry"
+
+showEnvironment :: EnvF Identity -> String
+showEnvironment (EnvF xs) = "EnvF " ++ "[" ++ concatMap showEntry xs ++ "]"
+
+showEntry :: EnvEntry Identity -> String
+showEntry (EnvEntry (var :: Var a) x)
+    | Just Refl <- eqT @a @T1
+    = "EnvEntry " ++ show var ++ " (" ++ show x ++ ")"
+    | Just Refl <- eqT @a @T2
+    = "EnvEntry " ++ show var ++ " (" ++ show x ++ ")"
+    | otherwise
+    = error "showEntry"
+
+-- | Generate a T1 or T2 variable
+genGVar :: Gen (GVar Op Int)
+genGVar = oneof [
+      do var <- genVar
+         pure (unsafeMkGVar (var :: Var T1) OpLeft)
+    , do var <- genVar
+         pure (unsafeMkGVar (var :: Var T2) OpRight)
+    ]
+
+shrinkGVar' :: GVar Op Int -> [GVar Op Int]
+shrinkGVar' (GVar (var :: Var a) op)
+  | Just Refl <- eqT @a @T1
+  = [ unsafeMkGVar var' op
+    | var' <- shrinkVar var
+    ] ++ [
+      unsafeMkGVar (unsafeCoerceVar var :: Var T2) OpRight
+    ]
+  | Just Refl <- eqT @a @T2
+  = [ unsafeMkGVar var' op
+    | var' <- shrinkVar var
+    ]
+  | otherwise
+  = error "shrink'GVar"
+
+genVar :: Gen (Var a)
+genVar = mkVar <$> arbitrary
+
+shrinkVar :: Var a -> [Var a]
+shrinkVar var = [ mkVar x' | x' <- shrink x]
+  where
+    -- Hacky: the constructor for 'Var' is not exposed, but we can obtain the
+    -- wrapped integer by reading it from the show output.
+    --
+    -- The show instance looks like:
+    --
+    -- > data Var = Var Int
+    -- > show (Var x) = "var" ++ show x
+    x = read (drop 3 (show var))
+
+genValue1 :: Gen T1
+genValue1 = arbitrary
+
+shrinkValue1 :: T1 -> [T1]
+shrinkValue1 = shrink
+
+genValue2 :: Gen T2
+genValue2 = arbitrary
+
+shrinkValue2 :: T2 -> [T2]
+shrinkValue2 = shrink
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,14 +1,16 @@
 module Main (main) where
 
-import Test.Tasty
+import           Test.Tasty
 
-import Test.IORef.Full   qualified
-import Test.IORef.Simple qualified
-import Test.MockFS       qualified
+import           Test.Golden
+import           Test.IORef.Full
+import           Test.IORef.Simple
+import           Test.MockFS
 
 main :: IO ()
 main = defaultMain $ testGroup "quickcheck-lockstep" [
-      Test.IORef.Simple.tests
+      Test.Golden.tests
+    , Test.IORef.Simple.tests
     , Test.IORef.Full.tests
     , Test.MockFS.tests
     ]
diff --git a/test/Test/Golden.hs b/test/Test/Golden.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Golden.hs
@@ -0,0 +1,107 @@
+{- HLINT ignore "Use camelCase" -}
+
+module Test.Golden where
+
+import           Control.Exception      (bracket_)
+import           System.Directory
+import           System.FilePath
+import           Test.MockFS            as MockFS
+import           Test.QuickCheck
+import           Test.QuickCheck.Random (mkQCGen)
+import           Test.Tasty
+import           Test.Tasty.Golden
+
+tests :: TestTree
+tests = testGroup "Test.Golden" [
+      golden_success_propLockstep_MockFS
+    , golden_failure_default_propLockstep_MockFS
+    , golden_failure_nonVerbose_propLockstep_MockFS
+    , golden_failure_verbose_propLockstep_MockFS
+    ]
+
+goldenDir :: FilePath
+goldenDir = "test" </> "golden"
+
+tmpDir :: FilePath
+tmpDir = "_tmp"
+
+-- | Golden test for a successful lockstep test
+golden_success_propLockstep_MockFS :: TestTree
+golden_success_propLockstep_MockFS =
+    goldenVsFile testName goldenPath outputPath $ do
+      createDirectoryIfMissing False tmpDir
+      r <- quickCheckWithResult args MockFS.propLockstep
+      writeFile outputPath (output r)
+  where
+    testName = "golden_success_propLockstep_MockFS"
+    goldenPath = goldenDir </> testName <.> "golden"
+    outputPath = tmpDir </> testName <.> "golden"
+
+    args = stdArgs {
+        replay = Just (mkQCGen 17, 32)
+      , chatty = False
+      }
+
+-- | Golden test for a failing lockstep test that produces a counterexample
+-- using the default postcondition.
+golden_failure_default_propLockstep_MockFS :: TestTree
+golden_failure_default_propLockstep_MockFS =
+    goldenVsFile testName goldenPath outputPath $ do
+      createDirectoryIfMissing False tmpDir
+      r <-
+        bracket_
+          MockFS.setInduceFault
+          MockFS.setNoInduceFault
+          (quickCheckWithResult args MockFS.propLockstep)
+      writeFile outputPath (output r)
+  where
+    testName = "golden_failure_default_propLockstep_MockFS"
+    goldenPath = goldenDir </> testName <.> "golden"
+    outputPath = tmpDir </> testName <.> "golden"
+
+    args = stdArgs {
+        replay = Just (mkQCGen 17, 32)
+      , chatty = False
+      }
+
+-- | Golden test for a failing lockstep test that produces a /non-verbose/ counterexample
+golden_failure_nonVerbose_propLockstep_MockFS :: TestTree
+golden_failure_nonVerbose_propLockstep_MockFS =
+    goldenVsFile testName goldenPath outputPath $ do
+      createDirectoryIfMissing False tmpDir
+      r <-
+        bracket_
+          (MockFS.setInduceFault >> MockFS.setPostconditionNonVerbose)
+          (MockFS.setNoInduceFault >> MockFS.setPostconditionDefault)
+          (quickCheckWithResult args MockFS.propLockstep)
+      writeFile outputPath (output r)
+  where
+    testName = "golden_failure_nonVerbose_propLockstep_MockFS"
+    goldenPath = goldenDir </> testName <.> "golden"
+    outputPath = tmpDir </> testName <.> "golden"
+
+    args = stdArgs {
+        replay = Just (mkQCGen 17, 32)
+      , chatty = False
+      }
+
+-- | Golden test for a failing lockstep test that produces a /verbose/ counterexample
+golden_failure_verbose_propLockstep_MockFS :: TestTree
+golden_failure_verbose_propLockstep_MockFS =
+    goldenVsFile testName goldenPath outputPath $ do
+      createDirectoryIfMissing False tmpDir
+      r <-
+        bracket_
+          (MockFS.setInduceFault >> MockFS.setPostconditionVerbose)
+          (MockFS.setNoInduceFault >> MockFS.setPostconditionDefault)
+          (quickCheckWithResult args MockFS.propLockstep)
+      writeFile outputPath (output r)
+  where
+    testName = "golden_failure_verbose_propLockstep_MockFS"
+    goldenPath = goldenDir </> testName <.> "golden"
+    outputPath = tmpDir </> testName <.> "golden"
+
+    args = stdArgs {
+        replay = Just (mkQCGen 17, 32)
+      , chatty = False
+      }
diff --git a/test/Test/IORef/Full.hs b/test/Test/IORef/Full.hs
--- a/test/Test/IORef/Full.hs
+++ b/test/Test/IORef/Full.hs
@@ -208,11 +208,11 @@
       Read  v   -> readIORef (lookUpRef v)
   where
     lookUpRef :: ModelVar M (IORef Int) -> IORef Int
-    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp
+    lookUpRef = realLookupVar (Proxy @RealMonad) lookUp
 
     lookUpInt :: Either Int (ModelVar M Int) -> Int
     lookUpInt (Left  x) = x
-    lookUpInt (Right v) = lookUpGVar (Proxy @RealMonad) lookUp v
+    lookUpInt (Right v) = realLookupVar (Proxy @RealMonad) lookUp v
 
 -- | The second write to the same variable will be broken
 brokenWrite :: Buggy -> IORef BrokenRef -> IORef Int -> Int -> IO Int
diff --git a/test/Test/IORef/Simple.hs b/test/Test/IORef/Simple.hs
--- a/test/Test/IORef/Simple.hs
+++ b/test/Test/IORef/Simple.hs
@@ -155,7 +155,7 @@
       Read  v   -> readIORef (lookUpRef v)
   where
     lookUpRef :: ModelVar M (IORef Int) -> IORef Int
-    lookUpRef = lookUpGVar (Proxy @RealMonad) lookUp
+    lookUpRef = realLookupVar (Proxy @RealMonad) lookUp
 
 runModel ::
      Action (Lockstep M) a
diff --git a/test/Test/MockFS.hs b/test/Test/MockFS.hs
--- a/test/Test/MockFS.hs
+++ b/test/Test/MockFS.hs
@@ -11,14 +11,27 @@
 {-# LANGUAGE TypeApplications      #-}
 {-# LANGUAGE TypeFamilies          #-}
 
-module Test.MockFS (tests) where
+module Test.MockFS (
+    tests
+  , propLockstep
+    -- * Unsafe: induce test failure
+  , setInduceFault
+  , setNoInduceFault
+    -- * Unsafe: set postcondition
+  , setPostconditionDefault
+  , setPostconditionNonVerbose
+  , setPostconditionVerbose
+  ) where
 
 import Prelude hiding (init)
 
 import Control.Exception (catch, throwIO)
 import Control.Monad (replicateM, (<=<))
 import Control.Monad.Reader (ReaderT (..))
+import Control.Monad.Trans (lift)
 import Data.Bifunctor
+import Data.Constraint
+import Data.IORef
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Typeable
@@ -26,6 +39,7 @@
 import System.Directory qualified as IO
 import System.IO qualified as IO
 import System.IO.Temp (createTempDirectory, getCanonicalTemporaryDirectory)
+import System.IO.Unsafe (unsafePerformIO)
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit
 import Test.Tasty.QuickCheck (testProperty)
@@ -83,7 +97,9 @@
 
 instance RunModel (Lockstep FsState) RealMonad where
   perform       = \_st -> runIO
-  postcondition = Lockstep.postcondition
+  postcondition states action lookUp result = do
+      pc <- lift $ lift getPostcondition
+      runPostcondition pc states action lookUp result
   monitoring    = Lockstep.monitoring (Proxy @RealMonad)
 
 deriving instance Show (Action (Lockstep FsState) a)
@@ -203,6 +219,13 @@
       Close{} -> OEither . bimap OId OId
       Read{}  -> OEither . bimap OId OId
 
+  showRealResponse _ = \case
+      MkDir{} -> Just Dict
+      Open{} -> Nothing
+      Write{} -> Just Dict
+      Close{} -> Just Dict
+      Read{} -> Just Dict
+
 {-------------------------------------------------------------------------------
   Interpreter against the model
 -------------------------------------------------------------------------------}
@@ -320,11 +343,15 @@
           IO.hPutStr (lookUp' h) s
         Close h -> catchErr $
           IO.hClose (lookUp' h)
-        Read f -> catchErr $
-          IO.readFile (Mock.fileFP root $ either lookUp' id f)
+        Read f -> catchErr $ do
+          fault <- getFaultRef
+          s <- IO.readFile (Mock.fileFP root $ either lookUp' id f)
+          case fault of
+            Fault | length s >= 3 -> pure ""
+            _                     -> pure s
       where
         lookUp' :: FsVar x -> x
-        lookUp' = lookUpGVar (Proxy @RealMonad) lookUp
+        lookUp' = realLookupVar (Proxy @RealMonad) lookUp
 
 catchErr :: forall a. IO a -> IO (Either Err a)
 catchErr act = catch (Right <$> act) handler
@@ -365,14 +392,91 @@
 tests = testGroup "Test.MockFS" [
       testCase "labelledExamples" $
         QC.labelledExamples $ Lockstep.tagActions (Proxy @FsState)
-    , testProperty "propLockstep" $
-        Lockstep.runActionsBracket (Proxy @FsState)
-          (createSystemTempDirectory "QSM")
-          removeDirectoryRecursive
-          runReaderT
+    , testProperty "propLockstep" propLockstep
     ]
 
+propLockstep :: Actions (Lockstep FsState) -> QC.Property
+propLockstep =
+    Lockstep.runActionsBracket (Proxy @FsState)
+      (createSystemTempDirectory "QSM")
+      removeDirectoryRecursive
+      runReaderT
+
 createSystemTempDirectory :: [Char] -> IO FilePath
 createSystemTempDirectory prefix = do
     systemTempDir <- getCanonicalTemporaryDirectory
     createTempDirectory systemTempDir prefix
+
+{-------------------------------------------------------------------------------
+  Unsafe: induce test failure
+-------------------------------------------------------------------------------}
+
+data Fault = Fault | NoFault
+  deriving Eq
+
+{-# NOINLINE faultRef #-}
+-- | A mutable variable that can be set globally to induce test failures in
+-- 'propLockstep'. This is used in "Test.Golden" to golden test counterexamples
+-- as produced by the @quickcheck-lockstep@.
+faultRef :: IORef Fault
+faultRef = unsafePerformIO $ newIORef NoFault
+
+{-# NOINLINE getFaultRef #-}
+getFaultRef :: IO Fault
+getFaultRef = readIORef faultRef
+
+{-# NOINLINE setFaultRef #-}
+setFaultRef :: Fault -> IO ()
+setFaultRef = writeIORef faultRef
+
+{-# NOINLINE setInduceFault #-}
+setInduceFault :: IO ()
+setInduceFault = setFaultRef Fault
+
+{-# NOINLINE setNoInduceFault #-}
+setNoInduceFault ::  IO ()
+setNoInduceFault = setFaultRef NoFault
+
+{-------------------------------------------------------------------------------
+  Unsafe: set postcondition
+-------------------------------------------------------------------------------}
+
+data Postcondition =
+    DefaultPostcondition
+  | NonVerbosePostcondition
+  | VerbosePostcondition
+
+runPostcondition ::
+     Postcondition
+  -> (Lockstep FsState, Lockstep FsState)
+  -> Action (Lockstep FsState) a
+  -> LookUp RealMonad
+  -> Realized RealMonad a
+  -> PostconditionM RealMonad Bool
+runPostcondition DefaultPostcondition = Lockstep.postcondition
+runPostcondition NonVerbosePostcondition = Lockstep.postconditionWith False
+runPostcondition VerbosePostcondition = Lockstep.postconditionWith True
+
+{-# NOINLINE postconditionRef #-}
+postconditionRef :: IORef Postcondition
+postconditionRef = unsafePerformIO $ newIORef DefaultPostcondition
+
+{-# NOINLINE getPostcondition #-}
+getPostcondition :: IO Postcondition
+getPostcondition = readIORef postconditionRef
+
+{-# NOINLINE setPostconditionDefault #-}
+setPostconditionDefault :: IO ()
+setPostconditionDefault = setPostcondition VerbosePostcondition
+
+{-# NOINLINE setPostconditionVerbose #-}
+setPostconditionVerbose :: IO ()
+setPostconditionVerbose = setPostcondition VerbosePostcondition
+
+{-# NOINLINE setPostconditionNonVerbose #-}
+setPostconditionNonVerbose :: IO ()
+setPostconditionNonVerbose = setPostcondition NonVerbosePostcondition
+
+{-# NOINLINE setPostcondition #-}
+setPostcondition :: Postcondition -> IO ()
+setPostcondition = writeIORef postconditionRef