diff --git a/peras-hs/src/Peras/Chain.hs b/peras-hs/src/Peras/Chain.hs
index 1a881a3b..e4b2c809 100644
--- a/peras-hs/src/Peras/Chain.hs
+++ b/peras-hs/src/Peras/Chain.hs
@@ -2,6 +2,14 @@ module Peras.Chain where
 
 import Peras.Block (Block)
 
-data Chain t
-  = Genesis
-  | Cons (Block t) (Chain t)
+data Chain t = Genesis
+             | Cons (Block t) (Chain t)
+
+asList :: Chain t -> [Block t]
+asList Genesis = []
+asList (Cons x c) = x : asList c
+
+asChain :: [Block t] -> Chain t
+asChain [] = Genesis
+asChain (x : bs) = Cons x (asChain bs)
+
diff --git a/peras-iosim/analyses/block-production/experiment.sh b/peras-iosim/analyses/block-production/experiment.sh
index 2630e8e6..e280ba8a 100755
--- a/peras-iosim/analyses/block-production/experiment.sh
+++ b/peras-iosim/analyses/block-production/experiment.sh
@@ -33,7 +33,7 @@ echo "$i: $SEED"
 
 "$PERAS_IOSIM" --parameter-file tmp-network.yaml --protocol-file tmp-protocol.yaml --result-file tmp-result.json
 
-jq -r '.exitStates.N1 | "'"$SEED","$ASC","$END_SLOT","$TOTAL_STAKE"',\(.stake),\(.preferredChain.blocks|length)"' tmp-result.json >> tmp-results.csv
+jq -r '.currentStates.N1 | "'"$SEED","$ASC","$END_SLOT","$TOTAL_STAKE"',\(.stake),\(.preferredChain.blocks|length)"' tmp-result.json >> tmp-results.csv
 
 done
 
diff --git a/peras-iosim/src/Peras/IOSim/GraphViz.hs b/peras-iosim/src/Peras/IOSim/GraphViz.hs
index 27caf508..12f63de0 100644
--- a/peras-iosim/src/Peras/IOSim/GraphViz.hs
+++ b/peras-iosim/src/Peras/IOSim/GraphViz.hs
@@ -10,7 +10,7 @@ import Control.Lens ((^.))
 import Data.List (nub)
 import Peras.Block (Block (..))
 import Peras.Chain (Chain (..))
-import Peras.IOSim.Network.Types (NetworkState, chainsSeen, exitStates)
+import Peras.IOSim.Network.Types (NetworkState, chainsSeen, currentStates)
 import Peras.IOSim.Node.Types (committeeMember, downstreams, slotLeader, stake, vrfOutput)
 
 import qualified Data.Map.Strict as M
@@ -28,7 +28,7 @@ peersGraph ::
   NetworkState v ->
   G.Graph
 peersGraph networkState =
-  let nodeStates = networkState ^. exitStates
+  let nodeStates = networkState ^. currentStates
       nodeIds = M.mapWithKey (\name _ -> G.NodeId (G.StringId $ show name) Nothing) nodeStates
       mkNode name nodeState =
         G.NodeStatement
diff --git a/peras-iosim/src/Peras/IOSim/Message/Types.hs b/peras-iosim/src/Peras/IOSim/Message/Types.hs
index e7e49944..5148b2c7 100644
--- a/peras-iosim/src/Peras/IOSim/Message/Types.hs
+++ b/peras-iosim/src/Peras/IOSim/Message/Types.hs
@@ -97,6 +97,7 @@ data OutEnvelope v
   | Idle
       { timestamp :: UTCTime
       , source :: NodeId
+      , currentState :: NodeState v
       }
   | Exit
       { timestamp :: UTCTime
@@ -116,7 +117,7 @@ instance A.FromJSON v => A.FromJSON (OutEnvelope v) where
                 <*> o A..: "outMessage"
                 <*> o A..: "bytes"
                 <*> o A..: "destination"
-            parseIdle = Idle <$> o A..: "timestamp" <*> o A..: "source"
+            parseIdle = Idle <$> o A..: "timestamp" <*> o A..: "source" <*> o A..: "currentState"
             parseExit = Exit <$> o A..: "timestamp" <*> o A..: "source" <*> o A..: "nodeState"
          in parseMessage <|> parseIdle <|> parseExit
 
@@ -133,6 +134,7 @@ instance A.ToJSON v => A.ToJSON (OutEnvelope v) where
     A.object
       [ "timestamp" A..= timestamp
       , "source" A..= source
+      , "currentState" A..= currentState
       ]
   toJSON Exit{..} =
     A.object
diff --git a/peras-iosim/src/Peras/IOSim/Network.hs b/peras-iosim/src/Peras/IOSim/Network.hs
index 0ca1f06f..29b01483 100644
--- a/peras-iosim/src/Peras/IOSim/Network.hs
+++ b/peras-iosim/src/Peras/IOSim/Network.hs
@@ -1,18 +1,13 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections #-}
 
-module Peras.IOSim.Network (
-  connectNode,
-  createNetwork,
-  emptyTopology,
-  randomTopology,
-  runNetwork,
-) where
+module Peras.IOSim.Network where
 
-import Control.Concurrent.Class.MonadSTM (MonadSTM, atomically)
+import Control.Concurrent.Class.MonadSTM (MonadSTM, STM, TQueue, atomically)
 import Control.Concurrent.Class.MonadSTM.TQueue (flushTQueue, newTQueueIO, tryReadTQueue, writeTQueue)
 import Control.Lens (
   Field1 (_1),
@@ -23,7 +18,7 @@ import Control.Lens (
   (.=),
   (^.),
  )
-import Control.Monad (unless, void, when)
+import Control.Monad (unless, void)
 import Control.Monad.Class.MonadFork (MonadFork (forkIO))
 import Control.Monad.Class.MonadSay (MonadSay (say))
 import Control.Monad.Class.MonadTime (MonadTime)
@@ -42,7 +37,7 @@ import Peras.IOSim.Network.Types (
   Topology (..),
   activeNodes,
   chainsSeen,
-  exitStates,
+  currentStates,
   lastSlot,
   lastTime,
   pending,
@@ -114,107 +109,154 @@ runNetwork ::
   Network v m ->
   Slot ->
   RandT g m (NetworkState v)
-runNetwork parameters protocol states Network{..} endSlot =
+runNetwork parameters protocol states network@Network{..} endSlot =
   liftRandT . (. (def,)) . execStateT $
     do
       let
-        -- Find the total stake.
-        total = fromMaybe (sum $ (^. stake) <$> states) $ totalStake parameters
-        -- Start a node process.
-        forkNode (nodeId, nodeIn) =
-          do
-            gen <- use _2
-            let (gen', gen'') = split gen
-            _2 .= gen'
-            void
-              . lift
-              . forkIO
-              . runNode gen'' protocol total (states M.! nodeId)
-              $ NodeProcess nodeIn nodesOut
-        -- Send a message and mark the destination as active.
-        output destination inChannel inEnvelope =
-          do
-            lift . atomically . writeTQueue inChannel $ inEnvelope
-            _1 . activeNodes %= S.insert destination
-        -- Notify a node of the next slot.
-        notifySlot destination nodeIn =
-          output destination nodeIn . InEnvelope Nothing . NextSlot
-            =<< use (_1 . lastSlot)
         -- Notify a node to stop.
         notifyStop destination nodeIn = output destination nodeIn Stop
-        -- Route one message.
-        route out@OutEnvelope{..} =
-          do
-            _1 . lastTime %= max timestamp
-            pendings <- use $ _1 . pending
-            (r, gen') <- uniformR (0, 1) <$> use _2
-            _2 .= gen'
-            -- Send the message if it was already pending or if it was received in the current slot.
-            -- FIXME: This is an approximation.
-            if out `elem` pendings || r > messageDelay parameters
-              then case outMessage of
-                -- FIXME: Implement this.
-                FetchBlock _ -> lift $ say "Fetching blocks is not yet implemented."
-                -- Forward the message to the appropriate node.
-                SendMessage message ->
-                  do
-                    -- FIXME: Awkwardly peek at the chain.
-                    case message of
-                      NewChain chain -> _1 . chainsSeen %= S.insert chain
-                      _ -> pure ()
-                    -- Forward the message.
-                    output destination (nodesIn M.! destination) $ InEnvelope (pure source) message
-              else _1 . pending %= (out :)
-        route Idle{..} =
-          do
-            _1 . lastTime %= max timestamp
-            _1 . activeNodes %= S.delete source
-        route Exit{..} =
-          do
-            _1 . lastTime %= max timestamp
-            _1 . activeNodes %= S.delete source
-            _1 . exitStates %= M.insert source nodeState
-        -- Read all of the pending messages.
-        flush =
-          if False -- FIXME: Is it safe to use `flushTQueue`?
-            then flushTQueue nodesOut -- As of `io-classes-1.3.1.0`, the queue isn't empty after this call!
-            else tryReadTQueue nodesOut >>= maybe (pure mempty) ((<$> flush) . (:))
-        -- Wait for all nodes to exit.
-        waitForExits :: StateT (NetworkState v, g) m ()
-        waitForExits =
-          do
-            allIdle <- (_1 . activeNodes) `uses` null
-            received <- lift $ atomically flush
-            mapM_ route received
-            unless allIdle waitForExits
+
         -- Receive and send messages.
         loop :: MonadDelay m => MonadSay m => StateT (NetworkState v, g) m (NetworkState v)
         loop =
           do
-            -- Advance the slot counter and notify the nodes, if all nodes are idle.
-            allIdle <- (_1 . activeNodes) `uses` null
-            -- FIXME: This is unsafe because a node crashing or becoming unresponsive will block the slot advancement.
-            when allIdle $
-              do
-                -- FIXME: This is unsafe because a node might take more than one slot to do its computations.
-                _1 . lastSlot %= (+ 1)
-                uncurry notifySlot `mapM_` M.toList nodesIn
-                lift $ threadDelay 1000000
-                -- FIXME: Assume that pending messages are received in the next slot.
-                mapM_ route =<< use (_1 . pending)
-                _1 . pending .= mempty
-            -- Receive and route messages.
-            received <- lift $ atomically flush
-            mapM_ route received
+            stepToIdle parameters network
             -- Check on whether the simulation is ending.
             doExit <- (_1 . lastSlot) `uses` (>= endSlot)
             if doExit
               then do
                 uncurry notifyStop `mapM_` M.toList nodesIn
-                waitForExits
+                waitForExits parameters network
                 gets fst
               else loop
       -- Start the node processes.
-      mapM_ forkNode $ M.toList nodesIn
+      startNodes parameters protocol states network
       -- Run the network.
       loop
+
+startNodes ::
+  (Monad m, RandomGen g, Eq v, MonadSTM m, MonadSay m, Ord v, MonadDelay m, Default v, MonadFork m, MonadTime m) =>
+  Parameters ->
+  Protocol ->
+  M.Map NodeId (NodeState v) ->
+  Network v m ->
+  StateT (NetworkState v, g) m ()
+startNodes parameters protocol states network =
+  mapM_ forkNode $ M.toList nodesIn
+ where
+  Network{nodesIn, nodesOut} = network
+  -- Find the total stake.
+  total = fromMaybe (sum $ (^. stake) <$> states) $ totalStake parameters
+  -- Start a node process.
+  forkNode (nodeId, nodeIn) =
+    do
+      gen <- use _2
+      let (gen', gen'') = split gen
+      _2 .= gen'
+      void
+        . lift
+        . forkIO
+        . runNode gen'' protocol total (states M.! nodeId)
+        $ NodeProcess nodeIn nodesOut
+
+-- Wait for all nodes to exit.
+waitForExits ::
+  (Monad m, RandomGen g, Eq v, MonadSTM m, MonadSay m, Ord v, MonadDelay m) =>
+  Parameters ->
+  Network v m ->
+  StateT (NetworkState v, g) m ()
+waitForExits parameters network =
+  do
+    allIdle <- (_1 . activeNodes) `uses` null
+    received <- lift $ atomically (flush nodesOut)
+    mapM_ route received
+    unless allIdle $ waitForExits parameters network
+ where
+  Network{nodesOut} = network
+  route = routeEnvelope parameters network
+
+-- | Read all of the pending messages.
+flush :: MonadSTM m => TQueue m a -> STM m [a]
+flush q =
+  if False -- FIXME: Is it safe to use `flushTQueue`?
+    then flushTQueue q -- As of `io-classes-1.3.1.0`, the queue isn't empty after this call!
+    else tryReadTQueue q >>= maybe (pure mempty) ((<$> flush q) . (:))
+
+-- | Advance the network up to one single slot.
+-- This function loops until all nodes are idle
+stepToIdle ::
+  (Monad m, RandomGen g, Eq v, MonadSTM m, MonadSay m, Ord v, MonadDelay m) =>
+  Parameters ->
+  Network v m ->
+  StateT (NetworkState v, g) m ()
+stepToIdle parameters network = do
+  -- Advance the slot counter and notify the nodes, if all nodes are idle.
+  allIdle <- (_1 . activeNodes) `uses` null
+  -- FIXME: This is unsafe because a node crashing or becoming unresponsive will block the slot advancement.
+  if allIdle
+    then do
+      -- FIXME: This is unsafe because a node might take more than one slot to do its computations.
+      _1 . lastSlot %= (+ 1)
+      uncurry notifySlot `mapM_` M.toList nodesIn
+      lift $ threadDelay 1000000
+      -- FIXME: Assume that pending messages are received in the next slot.
+      mapM_ route =<< use (_1 . pending)
+      _1 . pending .= mempty
+    else do
+      -- Receive and route messages.
+      received <- lift $ atomically $ flush nodesOut
+      mapM_ route received
+      stepToIdle parameters network
+ where
+  Network{nodesIn, nodesOut} = network
+  route = routeEnvelope parameters network
+  -- Notify a node of the next slot.
+  notifySlot destination nodeIn =
+    output destination nodeIn . InEnvelope Nothing . NextSlot
+      =<< use (_1 . lastSlot)
+
+-- | Dispatch a single message through the network.
+routeEnvelope ::
+  (Monad m, RandomGen g, Eq v, MonadSTM m, MonadSay m, Ord v) =>
+  Parameters ->
+  Network v m ->
+  OutEnvelope v ->
+  StateT (NetworkState v, g) m ()
+routeEnvelope parameters Network{nodesIn} = \case
+  out@OutEnvelope{..} ->
+    do
+      _1 . lastTime %= max timestamp
+      pendings <- use $ _1 . pending
+      (r, gen') <- uniformR (0, 1) <$> use _2
+      _2 .= gen'
+      -- Send the message if it was already pending or if it was received in the current slot.
+      -- FIXME: This is an approximation.
+      if out `elem` pendings || r > messageDelay parameters
+        then case outMessage of
+          -- FIXME: Implement this.
+          FetchBlock _ -> lift $ say "Fetching blocks is not yet implemented."
+          -- Forward the message to the appropriate node.
+          SendMessage message ->
+            do
+              -- FIXME: Awkwardly peek at the chain.
+              case message of
+                NewChain chain -> _1 . chainsSeen %= S.insert chain
+                _ -> pure ()
+              -- Forward the message.
+              output destination (nodesIn M.! destination) $ InEnvelope (pure source) message
+        else _1 . pending %= (out :)
+  Idle{..} -> do
+    _1 . lastTime %= max timestamp
+    _1 . activeNodes %= S.delete source
+    _1 . currentStates %= M.insert source currentState
+  Exit{..} -> do
+    _1 . lastTime %= max timestamp
+    _1 . activeNodes %= S.delete source
+    _1 . currentStates %= M.insert source nodeState
+
+-- Send a message and mark the destination as active.
+output :: MonadSTM m => NodeId -> TQueue m p -> p -> StateT (NetworkState v, g) m ()
+output destination inChannel inEnvelope =
+  do
+    lift . atomically . writeTQueue inChannel $ inEnvelope
+    _1 . activeNodes %= S.insert destination
diff --git a/peras-iosim/src/Peras/IOSim/Network/Types.hs b/peras-iosim/src/Peras/IOSim/Network/Types.hs
index 1de9c528..dfe081a0 100644
--- a/peras-iosim/src/Peras/IOSim/Network/Types.hs
+++ b/peras-iosim/src/Peras/IOSim/Network/Types.hs
@@ -10,7 +10,7 @@ module Peras.IOSim.Network.Types (
   Topology (..),
   activeNodes,
   chainsSeen,
-  exitStates,
+  currentStates,
   lastSlot,
   lastTime,
   pending,
@@ -52,7 +52,7 @@ data NetworkState v = NetworkState
   , _lastTime :: UTCTime
   , _activeNodes :: S.Set NodeId
   , _chainsSeen :: S.Set (Chain v)
-  , _exitStates :: M.Map NodeId (NodeState v)
+  , _currentStates :: M.Map NodeId (NodeState v)
   , _pending :: [OutEnvelope v]
   }
   deriving stock (Eq, Generic, Ord, Read, Show)
@@ -67,7 +67,7 @@ instance ToJSON v => ToJSON (NetworkState v) where
       , "lastTime" A..= _lastTime
       , "activeNodes" A..= _activeNodes
       , "chainsSeen" A..= _chainsSeen
-      , "exitStates" A..= _exitStates
+      , "currentStates" A..= _currentStates
       , "pending" A..= _pending
       ]
 
diff --git a/peras-iosim/src/Peras/IOSim/Node.hs b/peras-iosim/src/Peras/IOSim/Node.hs
index 767e4e8d..7965ba2f 100644
--- a/peras-iosim/src/Peras/IOSim/Node.hs
+++ b/peras-iosim/src/Peras/IOSim/Node.hs
@@ -115,12 +115,13 @@ runNode gen0 protocol total state NodeProcess{..} =
                           runRand $ nextSlot protocol slot total
                       SomeBlock _ -> error "Block transfer not implemented."
                       NewChain chain -> runRand $ newChain protocol chain
+                  currentState <- get
                   atomically' $
                     do
                       case message of
                         Nothing -> pure ()
                         Just message' -> mapM_ (writeTQueue outgoing . OutEnvelope now nodeId' (SendMessage message') 0) downstreams'
-                      writeTQueue outgoing $ Idle now nodeId'
+                      writeTQueue outgoing $ Idle now nodeId' currentState
                   clock .= now
                   go gen'
               Stop -> atomically' . writeTQueue outgoing . Exit now nodeId' =<< get
diff --git a/peras-quickcheck/peras-quickcheck.cabal b/peras-quickcheck/peras-quickcheck.cabal
index be6ebdf9..88cc6beb 100644
--- a/peras-quickcheck/peras-quickcheck.cabal
+++ b/peras-quickcheck/peras-quickcheck.cabal
@@ -120,16 +120,21 @@ test-suite quickcheck-model-test
 
     -- Test dependencies.
     build-depends:
-                                  base ^>=4.18.1.0
+                                            base ^>=4.18.1.0
+                  , MonadRandom
                   , QuickCheck
                   , QuickCheck
                   , bytestring
+                  , containers
                   , data-default
                   , hspec
+                  , io-classes
                   , io-sim
                   , io-sim
+                  , lens
                   , mtl
                   , peras-hs
+                  , peras-iosim
                   , peras-quickcheck
                   , quickcheck-dynamic
                   , si-timers
diff --git a/peras-quickcheck/src/Peras/NetworkModel.hs b/peras-quickcheck/src/Peras/NetworkModel.hs
index 792b741f..5e0beb64 100644
--- a/peras-quickcheck/src/Peras/NetworkModel.hs
+++ b/peras-quickcheck/src/Peras/NetworkModel.hs
@@ -4,9 +4,11 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -15,24 +17,19 @@
 -- FIXME: unused for now
 module Peras.NetworkModel where
 
-import Control.Monad (replicateM)
-import Control.Monad.State (MonadState, StateT, gets, modify)
+import Control.Monad (replicateM_)
+import Control.Monad.Reader (MonadReader, ReaderT, ask)
 import Control.Monad.Trans (MonadTrans (..))
-import Data.Either (partitionEithers)
-import qualified Data.Map as Map
 import Data.Maybe (mapMaybe)
-import Data.Set (Set)
-import qualified Data.Set as Set
 import GHC.Generics (Generic)
 import Numeric.Natural (Natural)
 import Peras.Block (Block, Slot)
-import Peras.Chain (Chain)
+import Peras.Chain (Chain, asChain, asList)
 import Peras.Message (Message (..), NodeId (..))
 import Peras.Orphans ()
-import System.Random (RandomGen, mkStdGen)
-import Test.QuickCheck (choose, elements, frequency)
+import Test.QuickCheck (choose, elements, frequency, tabulate)
 import Test.QuickCheck.DynamicLogic (DynLogicModel)
-import Test.QuickCheck.StateModel (Any (..), HasVariables, Realized, RunModel (..), StateModel (..))
+import Test.QuickCheck.StateModel (Any (..), HasVariables, LookUp, PostconditionM, Realized, RunModel (..), StateModel (..), Var, counterexamplePost, monitorPost)
 import Test.QuickCheck.StateModel.Variables (HasVariables (..))
 
 -- | We model a network of nodes interconnected through a diffusion layer.
@@ -44,20 +41,22 @@ data Network = Network
 
 instance DynLogicModel Network
 
-baseNodes :: RandomGen g => g -> [NodeId]
-baseNodes g =
-  take 10 $ MkNodeId . ("N" <>) . show <$> [1 .. 10]
+baseNodes :: Int -> [NodeId]
+baseNodes n =
+  MkNodeId . ("N" <>) . show <$> [1 .. n]
 
 instance StateModel Network where
   data Action Network a where
     -- Advance the time one or more slots possibly producing blocks.
-    Tick :: Natural -> Action Network (Set (Block ()))
+    Tick :: Natural -> Action Network ()
     -- Observe a node's best chain
     ObserveBestChain :: NodeId -> Action Network (Chain ())
+    -- Ensure chains have a common prefix
+    ChainsHaveCommonPrefix :: [Var (Chain ())] -> Action Network ()
 
   arbitraryAction _ Network{nodeIds} =
     frequency
-      [ (10, Some . Tick . fromInteger <$> choose (1, 100))
+      [ (10, Some . Tick . fromInteger <$> choose (10, 200))
       , (1, observeNode)
       ]
    where
@@ -65,14 +64,15 @@ instance StateModel Network where
 
   initialState =
     Network
-      { nodeIds = baseNodes (mkStdGen 42)
+      { nodeIds = baseNodes 10
       , slot = 0
       }
 
   nextState currentState@Network{slot} action _var =
     case action of
-      Tick n -> currentState{slot = slot + 1}
+      Tick n -> currentState{slot = slot + n}
       ObserveBestChain{} -> currentState
+      ChainsHaveCommonPrefix{} -> currentState
 
 deriving instance Eq (Action Network a)
 deriving instance Show (Action Network a)
@@ -83,25 +83,18 @@ instance HasVariables Network where
 instance HasVariables (Action Network a) where
   getAllVariables = const mempty
 
--- | Basic interface to a `Node` instance.
-data Node m = Node
-  { nodeId :: NodeId
-  , deliver :: Message () -> m ()
-  , step :: m [Message ()]
-  -- ^ Nodes are assumed to progress in steps
-  , inbox :: [(Slot, Message ())]
-  -- ^ New inputs to be delivered to the node at some `Slot`
-  , bestChain :: m (Chain ())
+-- | An interface to a  simulator for a network
+data Simulator m = Simulator
+  { step :: m ()
+  -- ^ Step the network one slot
+  , preferredChain :: NodeId -> m (Chain ())
+  -- ^ Return preferred chain for a specific node in the network.
+  , stop :: m ()
+  -- ^ Stop all nodes in the network
   }
 
--- | All known nodes in the network.
--- FIXME: Atm we assume fully connected topology, this will evolve as we refine the model.
-data Nodes m = Nodes
-  { nodes :: Map.Map NodeId (Node m)
-  }
-
-newtype RunMonad m a = RunMonad {runMonad :: StateT (Nodes m) m a}
-  deriving newtype (Functor, Applicative, Monad, MonadState (Nodes m))
+newtype RunMonad m a = RunMonad {runMonad :: ReaderT (Simulator m) m a}
+  deriving newtype (Functor, Applicative, Monad, MonadReader (Simulator m))
 
 instance MonadTrans RunMonad where
   lift = RunMonad . lift
@@ -112,29 +105,50 @@ instance Monad m => RunModel Network (RunMonad m) where
   perform network@Network{slot} action _context =
     case action of
       Tick n ->
-        Set.fromList . mconcat <$> replicateM (fromIntegral n) performTick
+        replicateM_ (fromIntegral n) performTick
       ObserveBestChain nodeId ->
         currentChain nodeId
+      ChainsHaveCommonPrefix{} ->
+        pure ()
    where
-    performTick :: RunMonad m [Block ()]
-    performTick = do
-      allNodes <- gets (Map.elems . nodes)
-      selectBlocks . mconcat <$> traverse tick allNodes
-
-    tick :: Node m -> RunMonad m [Message ()]
-    tick node@Node{nodeId, step, deliver, inbox} = do
-      let (pending, deliverables) = partitionEithers $ map (deliverableAt slot) inbox
-      -- deliver all messages in inbox
-      mapM_ (lift . deliver) deliverables
-      -- update the node's state
-      modify $ Nodes . Map.insert nodeId (node{inbox = pending}) . nodes
-      -- then let the node advance one slot and return the messages it sends
-      lift step
+    performTick :: RunMonad m ()
+    performTick =
+      ask >>= lift . step
 
     currentChain :: NodeId -> RunMonad m (Chain ())
     currentChain nodeId =
-      gets (Map.lookup nodeId . nodes)
-        >>= maybe (error $ "Invalid node id:" <> show nodeId) (lift . bestChain)
+      ask
+        >>= lift . flip preferredChain nodeId
+
+  postcondition ::
+    Monad m =>
+    (Network, Network) ->
+    Action Network a ->
+    LookUp (RunMonad m) ->
+    Realized (RunMonad m) a ->
+    PostconditionM (RunMonad m) Bool
+  postcondition (_, Network{slot}) (ChainsHaveCommonPrefix chainVars) env () = do
+    let chains = fmap env chainVars
+        prefix = commonPrefix chains
+        chainLength = length $ asList prefix
+        chainDensity = floor $ fromIntegral chainLength * 1000 / fromIntegral slot
+    counterexamplePost $ "Chains:  " <> show chains
+    counterexamplePost $ "Common prefix:  " <> show prefix
+    monitorPost $ tabulate "Prefix length" ["<= " <> show ((chainLength `div` 100 + 1) * 100)]
+    monitorPost $ tabulate "Prefix density" ["<= " <> show (chainDensity `div` 10 + 1) <> "%"]
+    pure $ not (null (asList prefix))
+  postcondition _ _ _ _ = pure True
+
+commonPrefix :: [Chain ()] -> Chain ()
+commonPrefix chains =
+  asChain . reverse $ foldl1 prefix blocks
+ where
+  blocks = reverse . asList <$> chains
+
+  prefix :: [Block ()] -> [Block ()] -> [Block ()]
+  prefix (a : as) (b : bs)
+    | a == b = a : prefix as bs
+  prefix _ _ = []
 
 selectBlocks :: [Message ()] -> [Block ()]
 selectBlocks = mapMaybe $ \case
diff --git a/peras-quickcheck/test/Peras/NetworkModelSpec.hs b/peras-quickcheck/test/Peras/NetworkModelSpec.hs
index 9336c360..d0e93031 100644
--- a/peras-quickcheck/test/Peras/NetworkModelSpec.hs
+++ b/peras-quickcheck/test/Peras/NetworkModelSpec.hs
@@ -1,33 +1,57 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -Wno-unused-do-bind #-}
 
 module Peras.NetworkModelSpec where
 
-import Control.Monad (forM_)
-import Peras.NetworkModel (Action (..), Network (..), nodes, runMonad)
-import Peras.Util (runPropInIOSim)
+import Control.Concurrent.Class.MonadSTM (MonadSTM, TVar, atomically, modifyTVar, modifyTVar', newTVarIO, readTVarIO, writeTVar)
+import Control.Lens (Field1 (_1), use, uses, (^.))
+import Control.Monad (forM, forM_)
+import Control.Monad.Class.MonadTime.SI (getCurrentTime)
+import Control.Monad.IOSim (IOSim, runSimTrace, selectTraceEventsSayWithTime', traceResult)
+import Control.Monad.Random (evalRand, mkStdGen, runRand, runRandT)
+import Control.Monad.Reader (ReaderT (..))
+import Control.Monad.State (StateT (..), gets)
+import Data.Bifunctor (second)
+import Data.Default (def)
+import Data.Functor (void)
+import qualified Data.Map as Map
+import Peras.Chain (Chain (Genesis))
+import Peras.IOSim.Network (createNetwork, randomTopology, startNodes, stepToIdle)
+import Peras.IOSim.Network.Types (NetworkState, chainsSeen, currentStates)
+import Peras.IOSim.Node (initializeNodes)
+import qualified Peras.IOSim.Node.Types as Node
+import Peras.IOSim.Protocol.Types (Protocol (PseudoPraos))
+import Peras.IOSim.Simulate.Types (Parameters (..))
+import Peras.Message (NodeId)
+import Peras.NetworkModel (Action (..), Network (..), RunMonad, Simulator (..), runMonad)
 import Test.Hspec (Spec)
-import Test.Hspec.QuickCheck (modifyMaxShrinks, prop)
-import Test.QuickCheck (Property, property, within)
-import Test.QuickCheck.DynamicLogic (DL, action, anyActions_, forAllDL, getModelStateDL)
-import Test.QuickCheck.Monadic (assert)
+import Test.Hspec.QuickCheck (modifyMaxShrinks, modifyMaxSuccess, prop)
+import Test.QuickCheck (Gen, Property, Testable, counterexample, property, within)
+import Test.QuickCheck.DynamicLogic (DL, action, anyAction, anyActions_, forAllDL, getModelStateDL)
+import Test.QuickCheck.Gen.Unsafe (Capture (..), capture)
+import Test.QuickCheck.Monadic (PropertyM, assert, monadic')
 import Test.QuickCheck.StateModel (Actions, runActions)
 
 spec :: Spec
 spec =
-  modifyMaxShrinks (const 0) $ prop "Chain progress" prop_chain_progress
+  modifyMaxSuccess (const 10) $ prop "Chain progress" prop_chain_progress
 
 prop_chain_progress :: Property
 prop_chain_progress =
-  within 5000000 $
+  within 50000000 $
     forAllDL chainProgress propNetworkModel
 
 chainProgress :: DL Network ()
 chainProgress = do
   anyActions_
-  getModelStateDL >>= \Network{nodeIds} ->
-    forM_ nodeIds (action . ObserveBestChain)
+  getModelStateDL >>= \Network{nodeIds} -> do
+    -- we need at least on run
+    anyAction
+    chains <- forM nodeIds (action . ObserveBestChain)
+    void $ action $ ChainsHaveCommonPrefix chains
 
 propNetworkModel :: Actions Network -> Property
 propNetworkModel actions =
@@ -35,3 +59,65 @@ propNetworkModel actions =
     runPropInIOSim $ do
       _ <- runActions actions
       assert True
+
+runPropInIOSim :: Testable a => (forall s. PropertyM (RunMonad (IOSim s)) a) -> Gen Property
+runPropInIOSim p = do
+  Capture eval <- capture
+  let simTrace =
+        runSimTrace $
+          mkPerasNetwork >>= runReaderT (runMonad $ eval $ monadic' p)
+      traceDump = map (\(t, s) -> show t <> " : " <> s) $ selectTraceEventsSayWithTime' simTrace
+      logsOnError = counterexample ("trace:\n" <> unlines traceDump)
+  case traceResult False simTrace of
+    Right x ->
+      pure $ logsOnError x
+    Left ex ->
+      pure $ counterexample (show ex) $ logsOnError $ property False
+ where
+  gen = mkStdGen 42
+
+  mkPerasNetwork :: IOSim s (Simulator (IOSim s))
+  mkPerasNetwork = do
+    let initState :: NetworkState () = def
+    let (topology, gen') = runRand (randomTopology parameters) gen
+    now <- getCurrentTime
+    let (states, gen'') = runRand (initializeNodes parameters now topology) gen'
+    network <- createNetwork topology
+    networkState <- newTVarIO (initState, gen'')
+    runWithState networkState $ startNodes parameters protocol states network
+    pure $
+      Simulator
+        { step = runWithState networkState $ stepToIdle parameters network
+        , preferredChain = runWithState networkState . getPreferredChain
+        , stop = pure ()
+        }
+
+getPreferredChain :: Monad m => NodeId -> StateT (NetworkState (), g) m (Chain ())
+getPreferredChain nodeId = do
+  nodeState <- (_1 . currentStates) `uses` (Map.! nodeId)
+  pure $ nodeState ^. Node.preferredChain
+
+runWithState :: (Monad m, MonadSTM m) => TVar m (NetworkState (), g) -> StateT (NetworkState (), g) m a -> m a
+runWithState stateVar act = do
+  st <- readTVarIO stateVar
+  (res, st') <- runStateT act st
+  atomically $ writeTVar stateVar st'
+  pure res
+
+protocol :: Protocol
+protocol = PseudoPraos defaultActiveSlotCoefficient
+
+defaultActiveSlotCoefficient :: Double
+defaultActiveSlotCoefficient = 0.05
+
+parameters :: Parameters
+parameters =
+  Parameters
+    { randomSeed = 12345
+    , peerCount = 10
+    , downstreamCount = 3
+    , totalStake = Just 5000
+    , maximumStake = 1000
+    , endSlot = 1000
+    , messageDelay = 0.35
+    }
diff --git a/peras-quickcheck/test/Peras/Util.hs b/peras-quickcheck/test/Peras/Util.hs
index 7536bb23..774ffcc4 100644
--- a/peras-quickcheck/test/Peras/Util.hs
+++ b/peras-quickcheck/test/Peras/Util.hs
@@ -4,39 +4,14 @@
 
 module Peras.Util where
 
-import Control.Monad.IOSim (IOSim, runSimTrace, selectTraceEventsSayWithTime', traceResult)
-import Control.Monad.State (evalStateT, get, lift)
-import Peras.NetworkModel (Nodes (..), RunMonad, nodes, runMonad)
-import Test.QuickCheck (Gen, Property, Testable, counterexample, property)
-import Test.QuickCheck.Gen.Unsafe (Capture (..), capture)
-import Test.QuickCheck.Monadic (PropertyM (..), monadic', run)
+import Control.Monad.Reader (ReaderT (..))
+import Control.Monad.State (lift)
+import Peras.NetworkModel (RunMonad, Simulator, runMonad)
+import Test.QuickCheck.Monadic (PropertyM (..))
 
 -- Stolen from https://github.com/input-output-hk/quickcheck-dynamic/blob/c309099aa30333a34d3f70ad7acc87d033dd5cdc/quickcheck-dynamic/src/Test/QuickCheck/Extras.hs#L7
 -- TODO: generalise the combinators in Extra to arbitrary natural transformations ?
-runPropInIO :: Monad m => Nodes m -> PropertyM (RunMonad m) a -> PropertyM m (a, Nodes m)
+runPropInIO :: Monad m => Simulator m -> PropertyM (RunMonad m) a -> PropertyM m a
 runPropInIO s0 p = MkPropertyM $ \k -> do
-  m <-
-    unPropertyM
-      ( do
-          a <- p
-          s <- run get
-          return (a, s)
-      )
-      $ fmap lift . k
-  return $ evalStateT (runMonad m) s0
-
-runPropInIOSim :: Testable a => (forall s. PropertyM (RunMonad (IOSim s)) a) -> Gen Property
-runPropInIOSim p = do
-  Capture eval <- capture
-  let simTrace =
-        runSimTrace $
-          evalStateT (runMonad $ eval $ monadic' p) nodes
-      traceDump = map (\(t, s) -> show t <> " : " <> s) $ selectTraceEventsSayWithTime' simTrace
-      logsOnError = counterexample ("trace:\n" <> unlines traceDump)
-  case traceResult False simTrace of
-    Right x ->
-      pure $ logsOnError x
-    Left ex ->
-      pure $ counterexample (show ex) $ logsOnError $ property False
- where
-  nodes = Nodes{nodes = mempty}
+  m <- unPropertyM p $ fmap lift . k
+  return $ runReaderT (runMonad m) s0
diff --git a/src/Peras/Chain.agda b/src/Peras/Chain.agda
index dfd60113..67db3a46 100644
--- a/src/Peras/Chain.agda
+++ b/src/Peras/Chain.agda
@@ -1,7 +1,9 @@
 module Peras.Chain where
 
+open import Agda.Builtin.List
 open import Agda.Builtin.Word
 open import Data.Bool
+open import Data.List
 open import Data.Nat using (ℕ)
 open import Level
 open import Data.Tree.AVL.Sets renaming (⟨Set⟩ to set) hiding (foldr)
@@ -60,6 +62,20 @@ open Chain public
 
 {-# COMPILE AGDA2HS Chain #-}
 
+-- | View of a `Chain` as a mere `List` of blocks.
+asList : {t : Set} -> (c : Chain t) -> List (Block t)
+asList Genesis = []
+asList (Cons x c) = x ∷ (asList c)
+
+{-# COMPILE AGDA2HS asList #-}
+
+-- | View of a `List` of blocks as a `Chain` anchored in `Genesis`.
+asChain : {t : Set} -> (blocks : List (Block t)) -> Chain t
+asChain [] = Genesis
+asChain (x ∷ bs) = Cons x (asChain bs)
+
+{-# COMPILE AGDA2HS asChain #-}
+
 -- Chain⋆ = Chain (set BlockO)
 
 -- | Chain validity