diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,13 @@
 
 ## UNRELEASED
 
+## 2.0.0 - 2022-10-11
+
+* **BREAKING**: Add `Realized` type family to distinguish between the model- and real type of an action
+* **BREAKING**: Introduce `RunModel` type class to interpret Model-generated sequence of actions against real-world implementation
+  * Move `perform` method from `StateModel` to this new type-class
+  * Also split `postcondition` and `monitoring` out from the `StateModel` to the `RunModel` type class
+* Added Thread registry example based on io-sim concurrency simulation library
 
 ## 1.1.0 - 2022-08-27
 
diff --git a/quickcheck-dynamic.cabal b/quickcheck-dynamic.cabal
--- a/quickcheck-dynamic.cabal
+++ b/quickcheck-dynamic.cabal
@@ -1,16 +1,16 @@
 cabal-version:   2.2
 name:            quickcheck-dynamic
-version:         1.1.0
+version:         2.0.0
 license:         Apache-2.0
 license-files:
   LICENSE
   NOTICE
-  
+
 maintainer:      arnaud.bailly@iohk.io
 author:          Ulf Norell
 category:        Testing
 synopsis:
-  A library for stateful property-based testing   
+  A library for stateful property-based testing
 homepage:
   https://github.com/input-output-hk/quickcheck-dynamic#readme
 
@@ -23,7 +23,7 @@
 build-type:      Simple
 extra-doc-files: README.md
 extra-source-files: CHANGELOG.md
-                    
+
 source-repository head
   type:     git
   location: https://github.com/input-output-hk/quickcheck-dynamic
@@ -31,16 +31,23 @@
 common lang
   default-language:   Haskell2010
   default-extensions:
-    DeriveFoldable
     DeriveFunctor
-    DeriveGeneric
-    DeriveLift
-    DeriveTraversable
-    ExplicitForAll
-    GeneralizedNewtypeDeriving
+    DeriveDataTypeable
+    StandaloneDeriving
     ImportQualifiedPost
+    TupleSections
+    LambdaCase
+    PatternSynonyms
+    GADTs
+    TypeApplications
     ScopedTypeVariables
-    StandaloneDeriving
+    TypeFamilies
+    FlexibleContexts
+    FlexibleInstances
+    MultiParamTypeClasses
+    RankNTypes
+    ViewPatterns
+    TypeOperators
 
   ghc-options:
     -Wall -Wnoncanonical-monad-instances -Wunused-packages
@@ -61,4 +68,5 @@
     build-depends:
         QuickCheck -any,
         base >=4.7 && <5,
-        random -any
+        random -any,
+        mtl -any
diff --git a/src/Test/QuickCheck/DynamicLogic.hs b/src/Test/QuickCheck/DynamicLogic.hs
--- a/src/Test/QuickCheck/DynamicLogic.hs
+++ b/src/Test/QuickCheck/DynamicLogic.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE FlexibleContexts #-}
-
 -- | Monadic interface for writing /Dynamic Logic/ properties.
 --
 -- This interface offers a much nicer experience than manipulating the
@@ -64,7 +62,7 @@
 instance MonadFail (DL s) where
   fail = errorDL
 
-action :: (Show a, Typeable a, Eq (Action s a)) => Action s a -> DL s ()
+action :: (Typeable a, Eq (Action s a)) => Action s a -> DL s ()
 action cmd = DL $ \_ k -> DL.after cmd $ k ()
 
 anyAction :: DL s ()
diff --git a/src/Test/QuickCheck/DynamicLogic/Core.hs b/src/Test/QuickCheck/DynamicLogic/Core.hs
--- a/src/Test/QuickCheck/DynamicLogic/Core.hs
+++ b/src/Test/QuickCheck/DynamicLogic/Core.hs
@@ -1,10 +1,3 @@
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-
 module Test.QuickCheck.DynamicLogic.Core (
   module Test.QuickCheck.DynamicLogic.Quantify,
   DynLogic,
@@ -95,7 +88,7 @@
 -- | Given `f` must be `True` after /some/ action.
 -- `f` is passed the state resulting from executing the `Action`.
 after ::
-  (Show a, Typeable a, Eq (Action s a)) =>
+  (Typeable a, Eq (Action s a)) =>
   Action s a ->
   (s -> DynFormula s) ->
   DynFormula s
@@ -474,8 +467,8 @@
  where
   shrink' _ [] _ = []
   shrink' d (step : as) s =
-    [] :
-    reverse (takeWhile (not . null) [drop (n - 1) as | n <- iterate (* 2) 1])
+    []
+      : reverse (takeWhile (not . null) [drop (n - 1) as | n <- iterate (* 2) 1])
       ++ case step of
         Do (Var i := act) ->
           [Do (Var i := act') : as | Some act' <- shrinkAction s act]
@@ -513,13 +506,13 @@
   prune _ _ [] = []
   prune ds s (Do (var := act) : rest)
     | precondition s act =
-      case [d' | d <- ds, d' <- stepDL d s (Do $ var := act)] of
-        [] -> prune ds s rest
-        ds' ->
-          Do (var := act) :
-          prune ds' (nextState s act var) rest
+        case [d' | d <- ds, d' <- stepDL d s (Do $ var := act)] of
+          [] -> prune ds s rest
+          ds' ->
+            Do (var := act)
+              : prune ds' (nextState s act var) rest
     | otherwise =
-      prune ds s rest
+        prune ds s rest
   prune ds s (Witness a : rest) =
     case [d' | d <- ds, d' <- stepDL d s (Witness a)] of
       [] -> prune ds s rest
diff --git a/src/Test/QuickCheck/DynamicLogic/Quantify.hs b/src/Test/QuickCheck/DynamicLogic/Quantify.hs
--- a/src/Test/QuickCheck/DynamicLogic/Quantify.hs
+++ b/src/Test/QuickCheck/DynamicLogic/Quantify.hs
@@ -1,6 +1,3 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
 
 -- | This module defines Quantifications, which are used together with
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
@@ -1,16 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- | Simple (stateful) Model-Based Testing library for use with Haskell QuickCheck.
@@ -28,17 +17,21 @@
   Actions (..),
   pattern Actions,
   EnvEntry (..),
+  pattern (:=?),
   Env,
+  Realized,
   stateAfter,
   runActions,
   runActionsInState,
   lookUpVar,
   lookUpVarMaybe,
-  invertLookupVarMaybe,
 ) where
 
 import Control.Monad
+import Control.Monad.Reader
+import Control.Monad.State
 import Data.Data
+import Data.Kind
 import Test.QuickCheck as QC
 import Test.QuickCheck.DynamicLogic.SmartShrinking
 import Test.QuickCheck.Monadic
@@ -61,8 +54,6 @@
 --    the action is /rejected/ and a new one is tried. This is also useful when shrinking a trace
 --    in order to ensure that removing some `Action` still produces a valid trace. The `precondition` can be
 --    somewhat redundant with the generator's conditions,
---  * `postcondition`: This function is evaluated during test execution after `perform`ing the action, it allows
---    the model to express expectations about the output of actual code given some "transition".
 class
   ( forall a. Show (Action state a)
   , Show state
@@ -103,7 +94,7 @@
   -- | Shrinker for `Action`.
   -- Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness
   -- of property-based testing.
-  shrinkAction :: (Show a, Typeable a) => state -> Action state a -> [Any (Action state)]
+  shrinkAction :: Typeable a => state -> Action state a -> [Any (Action state)]
   shrinkAction _ _ = []
 
   -- | Initial state of generated traces.
@@ -114,7 +105,7 @@
   -- by `perform`ing the `Action` inside the `state` so that further actions can use `Lookup`
   -- to retrieve that data. This allows the model to be ignorant of those values yet maintain
   -- some references that can be compared and looked for.
-  nextState :: state -> Action state a -> Var a -> state
+  nextState :: Typeable a => state -> Action state a -> Var a -> state
   nextState s _ _ = s
 
   -- | Precondition for filtering generated `Action`.
@@ -123,63 +114,70 @@
   precondition :: state -> Action state a -> Bool
   precondition _ _ = True
 
+-- TODO: maybe it makes sense to write
+-- out a long list of these instances
+type family Realized (m :: Type -> Type) a :: Type
+type instance Realized IO a = a
+type instance Realized (StateT s m) a = Realized m a
+type instance Realized (ReaderT r m) a = Realized m a
+
+class Monad m => RunModel state m where
+  -- | Perform an `Action` in some `state` in the `Monad` `m`.  This
+  -- is the function that's used to exercise the actual stateful
+  -- implementation, usually through various side-effects as permitted
+  -- by `m`. It produces a value of type `a`, eg. some observable
+  -- output from the `Action` that should later be kept in the
+  -- environment through a `Var a` also passed to the `nextState`
+  -- function.
+  --
+  -- The `Lookup` parameter provides an /environment/ to lookup `Var
+  -- a` instances from previous steps.
+  perform :: forall a. Typeable a => state -> Action state a -> LookUp m -> m (Realized m a)
+
   -- | Postcondition on the `a` value produced at some step.
   -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
   -- to check the implementation produces expected values.
-  postcondition :: state -> Action state a -> LookUp -> a -> Bool
-  postcondition _ _ _ _ = True
+  postcondition :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> m Bool
+  postcondition _ _ _ _ = pure True
 
   -- | Allows the user to attach information to the `Property` at each step of the process.
   -- This function is given the full transition that's been executed, including the start and ending
   -- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform`
   -- while executing this step.
-  monitoring :: Show a => (state, state) -> Action state a -> LookUp -> a -> Property -> Property
-  monitoring _ _ _ _ = id
-
--- | Perform an `Action` in some `state` in the `Monad` `m`.  This
--- is the function that's used to exercise the actual stateful
--- implementation, usually through various side-effects as permitted
--- by `m`. It produces a value of type `a`, eg. some observable
--- output from the `Action` that should later be kept in the
--- environment through a `Var a` also passed to the `nextState`
--- function.
---
--- The `Lookup` parameter provides an /environment/ to lookup `Var
--- a` instances from previous steps.
-newtype RunModel state m = RunModel {perform :: forall a. state -> Action state a -> LookUp -> m a}
+  monitoring :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property
+  monitoring _ _ _ _ prop = prop
 
-type LookUp = forall a. Typeable a => Var a -> a
+type LookUp m = forall a. Typeable a => Var a -> Realized m a
 
-type Env = [EnvEntry]
+type Env m = [EnvEntry m]
 
-data EnvEntry where
-  (:==) :: (Show a, Typeable a) => Var a -> a -> EnvEntry
+data EnvEntry m where
+  (:==) :: Typeable a => Var a -> Realized m a -> EnvEntry m
 
 infix 5 :==
 
-deriving instance Show EnvEntry
+pattern (:=?) :: forall a m. Typeable a => Var a -> Realized m a -> EnvEntry m
+pattern v :=? val <- (viewAtType -> Just (v, val))
 
-lookUpVarMaybe :: Typeable a => Env -> Var a -> Maybe a
+viewAtType :: forall a m. Typeable a => EnvEntry m -> Maybe (Var a, Realized m a)
+viewAtType ((v :: Var b) :== val)
+  | Just Refl <- eqT @a @b = Just (v, val)
+  | otherwise = Nothing
+
+lookUpVarMaybe :: forall a m. Typeable a => Env m -> Var a -> Maybe (Realized m a)
 lookUpVarMaybe [] _ = Nothing
-lookUpVarMaybe ((v' :== a) : env) v =
-  case cast (v', a) of
-    Just (v'', a') | v == v'' -> Just a'
+lookUpVarMaybe (((v' :: Var b) :== a) : env) v =
+  case eqT @a @b of
+    Just Refl | v == v' -> Just a
     _ -> lookUpVarMaybe env v
 
-lookUpVar :: Typeable a => Env -> Var a -> a
+lookUpVar :: Typeable a => Env m -> Var a -> Realized m a
 lookUpVar env v = case lookUpVarMaybe env v of
   Nothing -> error $ "Variable " ++ show v ++ " is not bound!"
   Just a -> a
 
-invertLookupVarMaybe :: (Typeable a, Eq a) => Env -> a -> Maybe (Var a)
-invertLookupVarMaybe [] _ = Nothing
-invertLookupVarMaybe ((v :== a) : env) a' =
-  case cast (v, a) of
-    Just (v', a'') | a' == a'' -> Just v'
-    _ -> invertLookupVarMaybe env a'
-
 data Any f where
-  Some :: (Show a, Typeable a, Eq (f a)) => f a -> Any f
+  Some :: (Typeable a, Eq (f a)) => f a -> Any f
   Error :: String -> Any f
 
 deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))
@@ -194,7 +192,7 @@
 
 data Step state where
   (:=) ::
-    (Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>
+    (Typeable a, Eq (Action state a), Show (Action state a)) =>
     Var a ->
     Action state a ->
     Step state
@@ -238,11 +236,11 @@
     | d > 10 = ("(" ++) . shows (Actions as) . (")" ++)
     | null as = ("Actions []" ++)
     | otherwise =
-      ("Actions \n [" ++)
-        . foldr
-          (.)
-          (shows (last as) . ("]" ++))
-          [shows a . (",\n  " ++) | a <- init as]
+        ("Actions \n [" ++)
+          . foldr
+            (.)
+            (shows (last as) . ("]" ++))
+            [shows a . (",\n  " ++) | a <- init as]
 
 instance (StateModel state) => Arbitrary (Actions state) where
   arbitrary = do
@@ -272,14 +270,14 @@
       go m n rej
         | m > n = return (Nothing, rej)
         | otherwise = do
-          a <- resize m $ arbitraryAction s
-          case a of
-            Some act ->
-              if precondition s act
-                then return (Just (Some act), rej)
-                else go (m + 1) n (actionName act : rej)
-            Error _ ->
-              go (m + 1) n rej
+            a <- resize m $ arbitraryAction s
+            case a of
+              Some act ->
+                if precondition s act
+                  then return (Just (Some act), rej)
+                  else go (m + 1) n (actionName act : rej)
+              Error _ ->
+                go (m + 1) n rej
 
   shrink (Actions_ rs as) =
     map (Actions_ rs) (shrinkSmart (map (prune . map fst) . shrinkList shrinker . withStates) as)
@@ -292,9 +290,9 @@
   loop _s [] = []
   loop s ((var := act) : as)
     | precondition s act =
-      (var := act) : loop (nextState s act var) as
+        (var := act) : loop (nextState s act var) as
     | otherwise =
-      loop s as
+        loop s as
 
 withStates :: StateModel state => [Step state] -> [(Step state, state)]
 withStates = loop initialState
@@ -311,20 +309,18 @@
 
 runActions ::
   forall state m.
-  (StateModel state, Monad m) =>
-  RunModel state m ->
+  (StateModel state, RunModel state m) =>
   Actions state ->
-  PropertyM m (state, Env)
+  PropertyM m (state, Env m)
 runActions = runActionsInState @_ @m initialState
 
 runActionsInState ::
   forall state m.
-  (StateModel state, Monad m) =>
+  (StateModel state, RunModel state m) =>
   state ->
-  RunModel state m ->
   Actions state ->
-  PropertyM m (state, Env)
-runActionsInState state RunModel{..} (Actions_ rejected (Smart _ actions)) = loop state [] actions
+  PropertyM m (state, Env m)
+runActionsInState st (Actions_ rejected (Smart _ actions)) = loop st [] actions
  where
   loop _s env [] = do
     unless (null rejected) $
@@ -335,8 +331,10 @@
     ret <- run (perform s act (lookUpVar env))
     let name = actionName act
     monitor (tabulate "Actions" [name])
-    let s' = nextState s act (Var n)
-        env' = (Var n :== ret) : env
-    monitor (monitoring (s, s') act (lookUpVar env') ret)
-    assert $ postcondition s act (lookUpVar env) ret
+    let var = Var n
+        s' = nextState s act var
+        env' = (var :== ret) : env
+    monitor (monitoring @state @m (s, s') act (lookUpVar env') ret)
+    b <- run $ postcondition (s, s') act (lookUpVar env) ret
+    assert b
     loop s' env' as