diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs
index d413601769..770eced3eb 100644
--- a/kore/src/Kore/Exec.hs
+++ b/kore/src/Kore/Exec.hs
@@ -30,6 +30,7 @@ import Control.Error.Util
     )
 import Control.Monad.Catch
     ( MonadCatch
+    , MonadThrow
     )
 import Control.Monad.Trans.Except
     ( runExceptT
@@ -167,6 +168,9 @@ import Kore.Unparser
     ( unparseToText
     , unparseToText2
     )
+import Log
+    ( MonadLog
+    )
 import qualified Log
 import SMT
     ( MonadSMT
@@ -197,10 +201,11 @@ data Execution =
 
 -- | Symbolic execution
 exec
-    ::  ( Log.WithLog Log.LogMessage smt
+    ::  ( MonadIO smt
+        , MonadLog smt
         , MonadProfiler smt
         , MonadSMT smt
-        , MonadIO smt
+        , MonadThrow smt
         )
     => Limit Natural
     -> VerifiedModule StepperAttributes
@@ -234,10 +239,11 @@ exec breadthLimit verifiedModule strategy initialTerm =
 
 -- | Project the value of the exit cell, if it is present.
 execGetExitCode
-    ::  ( Log.WithLog Log.LogMessage smt
+    ::  ( MonadIO smt
+        , MonadLog smt
         , MonadProfiler smt
         , MonadSMT smt
-        , MonadIO smt
+        , MonadThrow smt
         )
     => VerifiedModule StepperAttributes
     -- ^ The main module
@@ -262,10 +268,11 @@ execGetExitCode indexedModule strategy' finalTerm =
 
 -- | Symbolic search
 search
-    ::  ( Log.WithLog Log.LogMessage smt
+    ::  ( MonadIO smt
+        , MonadLog smt
         , MonadProfiler smt
         , MonadSMT smt
-        , MonadIO smt
+        , MonadThrow smt
         )
     => Limit Natural
     -> VerifiedModule StepperAttributes
@@ -404,6 +411,7 @@ boundedModelCheck
         , MonadProfiler smt
         , MonadSMT smt
         , MonadIO smt
+        , MonadThrow smt
         )
     => Limit Natural
     -> Limit Natural
@@ -584,7 +592,7 @@ simplifyReachabilityRule rule = do
 
 -- | Construct an execution graph for the given input pattern.
 execute
-    :: MonadSimplify simplifier
+    :: (MonadSimplify simplifier, MonadThrow simplifier)
     => Limit Natural
     -> VerifiedModule StepperAttributes
     -- ^ The main module
diff --git a/kore/src/Kore/ModelChecker/Bounded.hs b/kore/src/Kore/ModelChecker/Bounded.hs
index cfa1c3f15c..3caa164677 100644
--- a/kore/src/Kore/ModelChecker/Bounded.hs
+++ b/kore/src/Kore/ModelChecker/Bounded.hs
@@ -14,6 +14,9 @@ module Kore.ModelChecker.Bounded
 
 import Prelude.Kore
 
+import Control.Monad.Catch
+    ( MonadThrow
+    )
 import qualified Control.Monad.State.Strict as State
 import qualified Data.Foldable as Foldable
 import qualified Data.Graph.Inductive.Graph as Graph
@@ -100,7 +103,7 @@ bmcStrategy
 
 checkClaim
     :: forall m
-    .  MonadSimplify m
+    .  (MonadSimplify m, MonadThrow m)
     => Limit Natural
     ->  (  CommonModalPattern
         -> [Strategy (Prim CommonModalPattern (RewriteRule Variable))]
@@ -133,14 +136,14 @@ checkClaim
                         , predicate = Predicate.makeTruePredicate_
                         , substitution = mempty
                         }
-        executionGraph <- State.evalStateT
-                            (runStrategyWithSearchOrder
-                                breadthLimit
-                                transitionRule'
-                                strategy
-                                searchOrder
-                                startState)
-                            Nothing
+        executionGraph <-
+            runStrategyWithSearchOrder
+                breadthLimit
+                transitionRule'
+                strategy
+                searchOrder
+                startState
+            & flip State.evalStateT Nothing
 
         Log.logInfo . Text.pack
             $ ("searched states: " ++ (show . Graph.order . graph $ executionGraph))
diff --git a/kore/src/Kore/Profiler/Data.hs b/kore/src/Kore/Profiler/Data.hs
index 641c57e45e..8e76bfbf2c 100644
--- a/kore/src/Kore/Profiler/Data.hs
+++ b/kore/src/Kore/Profiler/Data.hs
@@ -17,6 +17,10 @@ import Prelude.Kore
 import Control.Monad
     ( when
     )
+import Control.Monad.Catch.Pure
+    ( CatchT
+    , mapCatchT
+    )
 import Control.Monad.Morph
     ( MFunctor (..)
     )
@@ -25,8 +29,8 @@ import Control.Monad.Reader
     )
 import qualified Control.Monad.State.Strict as Strict
 import Control.Monad.Trans.Accum
-    ( AccumT (AccumT)
-    , runAccumT
+    ( AccumT
+    , mapAccumT
     )
 import Control.Monad.Trans.Except
     ( ExceptT
@@ -55,12 +59,10 @@ import System.Clock
 import Control.Monad.Counter
 import ListT
     ( ListT (..)
-    )
-import qualified ListT
-    ( mapListT
+    , mapListT
     )
 
-{- Monad that can also handle profiling events.
+{- | Monad that can also handle profiling events.
 -}
 class Monad profiler => MonadProfiler profiler where
     profile
@@ -257,24 +259,27 @@ profileGhcEventsAnalyze event action = do
     liftIO $ traceEventIO ("STOP " ++ List.intercalate "/" event)
     return a
 
-instance (MonadProfiler m) => MonadProfiler (ReaderT thing m )
-
-instance MonadProfiler m => MonadProfiler (Strict.StateT s m)
+instance (MonadProfiler m, Monoid w) => MonadProfiler (AccumT w m)
+  where
+    profile a = mapAccumT (profile a)
+    {-# INLINE profile #-}
 
-instance MonadProfiler m => MonadProfiler (MaybeT m)
+instance MonadProfiler m => MonadProfiler (CatchT m) where
+    profile a = mapCatchT (profile a)
+    {-# INLINE profile #-}
 
-instance MonadProfiler m => MonadProfiler (IdentityT m)
+instance MonadProfiler m => MonadProfiler (CounterT m)
 
 instance MonadProfiler m => MonadProfiler (ExceptT e m)
 
+instance MonadProfiler m => MonadProfiler (IdentityT m)
+
 instance MonadProfiler m => MonadProfiler (ListT m) where
-    profile a action =
-        ListT.mapListT (profile a) action
+    profile a = mapListT (profile a)
     {-# INLINE profile #-}
 
-instance (MonadProfiler m, Monoid w) => MonadProfiler (AccumT w m)
-  where
-    profile a action = AccumT (profile a . runAccumT action)
-    {-# INLINE profile #-}
+instance MonadProfiler m => MonadProfiler (MaybeT m)
 
-instance MonadProfiler m => MonadProfiler (CounterT m)
+instance MonadProfiler m => MonadProfiler (ReaderT thing m )
+
+instance MonadProfiler m => MonadProfiler (Strict.StateT s m)
diff --git a/kore/src/Kore/Profiler/Profile.hs b/kore/src/Kore/Profiler/Profile.hs
index 6e2da4531a..3ef60d5a3c 100644
--- a/kore/src/Kore/Profiler/Profile.hs
+++ b/kore/src/Kore/Profiler/Profile.hs
@@ -237,11 +237,7 @@ smtDecision (sexpr :| _) action = do
         then profile ["SMT", show $ length $ show sexpr] action
         else action
 
-executionQueueLength
-    :: MonadProfiler profiler
-    => Int -> profiler result -> profiler result
-executionQueueLength len action = do
-    Configuration {logStrategy} <- profileConfiguration
-    when logStrategy
-        (profileValue ["ExecutionQueueLength"] len)
-    action
+executionQueueLength :: MonadProfiler profiler => Int -> profiler ()
+executionQueueLength len = do
+    Configuration { logStrategy } <- profileConfiguration
+    when logStrategy (profileValue ["ExecutionQueueLength"] len)
diff --git a/kore/src/Kore/Step.hs b/kore/src/Kore/Step.hs
index 61371f5884..a8ba8cec0c 100644
--- a/kore/src/Kore/Step.hs
+++ b/kore/src/Kore/Step.hs
@@ -61,7 +61,9 @@ import qualified Kore.Step.SMT.Evaluator as SMT.Evaluator
     ( filterMultiOr
     )
 import qualified Kore.Step.Step as Step
-import Kore.Step.Strategy
+import Kore.Step.Strategy hiding
+    ( transitionRule
+    )
 import qualified Kore.Step.Strategy as Strategy
 import qualified Kore.Step.Transition as Transition
 import Kore.Syntax.Variable
diff --git a/kore/src/Kore/Step/Strategy.hs b/kore/src/Kore/Step/Strategy.hs
index 4156d7fe14..74f50fdf13 100644
--- a/kore/src/Kore/Step/Strategy.hs
+++ b/kore/src/Kore/Step/Strategy.hs
@@ -30,6 +30,13 @@ module Kore.Step.Strategy
     , stuck
     , continue
       -- * Running strategies
+    , leavesM
+    , unfoldM_
+    , applyBreadthLimit
+    , unfoldBreadthFirst
+    , unfoldDepthFirst
+    , unfoldSearchOrder
+    , unfoldTransition
     , GraphSearchOrder(..)
     , constructExecutionGraph
     , ExecutionGraph(..)
@@ -43,6 +50,7 @@ module Kore.Step.Strategy
     , pickStar
     , pickPlus
     , assert
+    , transitionRule
     , executionHistoryStep
     , emptyExecutionGraph
     , module Kore.Step.Transition
@@ -60,17 +68,27 @@ import Prelude.Kore hiding
     , some
     )
 
-import qualified Control.Exception as Exception
+import Control.Error
+    ( maybeT
+    )
+import qualified Control.Lens as Lens
 import Control.Monad
-    ( when
+    ( guard
     , (>=>)
     )
+import Control.Monad.Catch
+    ( Exception (..)
+    , MonadThrow
+    )
+import qualified Control.Monad.Catch as Exception
 import Control.Monad.State.Strict
     ( MonadState
-    , StateT
     )
 import qualified Control.Monad.State.Strict as State
 import qualified Data.Foldable as Foldable
+import Data.Generics.Product
+    ( field
+    )
 import qualified Data.Graph.Inductive.Graph as Graph
 import Data.Graph.Inductive.PatriciaTree
     ( Gr
@@ -87,13 +105,11 @@ import Data.Sequence
     ( Seq
     )
 import qualified Data.Sequence as Seq
+import qualified GHC.Generics as GHC
 import Kore.Profiler.Data
     ( MonadProfiler
     )
 import qualified Kore.Profiler.Profile as Profile
-    ( executionQueueLength
-    )
-
 import Kore.Step.Transition
 import Numeric.Natural
 
@@ -251,7 +267,8 @@ data ExecutionGraph config rule = ExecutionGraph
     { root :: Graph.Node
     , graph :: Gr config (Seq rule)
     }
-    deriving(Eq, Show)
+    deriving (Eq, Show)
+    deriving (GHC.Generic)
 
 -- | A temporary data structure used to construct the 'ExecutionGraph'.
 -- Well, it was intended to be temporary, but for the purpose of making
@@ -377,11 +394,43 @@ emptyExecutionGraph config =
 -}
 data GraphSearchOrder = BreadthFirst | DepthFirst deriving Eq
 
-newtype LimitExceeded instr = LimitExceeded (Seq (Graph.Node, [instr]))
+newtype LimitExceeded a = LimitExceeded (Seq a)
     deriving (Show, Typeable)
 
-instance (Show instr, Typeable instr)
-    => Exception.Exception (LimitExceeded instr)
+instance (Show a, Typeable a) => Exception (LimitExceeded a)
+
+updateGraph
+    :: forall instr config rule m
+    .  MonadState (ExecutionGraph config rule) m
+    => (instr -> config -> TransitionT rule m config)
+    -> ([instr], Graph.Node) -> m [([instr], Graph.Node)]
+updateGraph _ ([], _) = return []
+updateGraph transit (instr : instrs, node) = do
+    config <- getConfig node
+    transitions <- runTransitionT (transit instr config)
+    nodes <- traverse (insTransition node) transitions
+    pure ((,) instrs <$> nodes)
+
+getConfig
+    :: MonadState (ExecutionGraph config rule) m
+    => Graph.Node
+    -> m config
+getConfig node = do
+    graph <- Lens.use (field @"graph")
+    pure $ fromMaybe (error "Node does not exist") (Graph.lab graph node)
+
+insTransition
+    :: MonadState (ExecutionGraph config rule) m
+    => Graph.Node  -- ^ parent node
+    -> (config, Seq rule)
+    -> m Graph.Node
+insTransition node (config, rules) = do
+    graph <- Lens.use (field @"graph")
+    let node' = (succ . snd) (Graph.nodeRange graph)
+    Lens.modifying (field @"graph") $ Graph.insNode (node', config)
+    Lens.modifying (field @"graph") $ Graph.insEdges [(node, node', rules)]
+    pure node'
+
 
 {- | Execute a 'Strategy'.
 
@@ -401,7 +450,7 @@ See also: 'pickLongest', 'pickFinal', 'pickOne', 'pickStar', 'pickPlus'
 
 constructExecutionGraph
     :: forall m config rule instr
-    .  MonadProfiler m
+    .  (MonadProfiler m, MonadThrow m)
     => Show instr
     => Typeable instr
     => Limit Natural
@@ -410,68 +459,123 @@ constructExecutionGraph
     -> GraphSearchOrder
     -> config
     -> m (ExecutionGraph config rule)
-constructExecutionGraph breadthLimit transit instrs0 searchOrder0 config0 = do
-    finalGraph <- State.execStateT
-                    (unfoldWorker initialSeed searchOrder0)
-                    initialGraph
-    return exe { graph = finalGraph }
+constructExecutionGraph breadthLimit transit instrs0 searchOrder0 config0 =
+    unfoldM_ mkQueue transit' (instrs0, root execGraph)
+    & flip State.execStateT execGraph
   where
-    exe@ExecutionGraph { root, graph = initialGraph } =
-        emptyExecutionGraph config0
-    initialSeed = Seq.singleton (root, instrs0)
-
-    transit' instr config = (lift . runTransitionT) (transit instr config)
-
-    unfoldWorker
-        :: Seq (Graph.Node, [instr])
-        -> GraphSearchOrder
-        -> StateT (Gr config (Seq rule)) m ()
-    unfoldWorker Seq.Empty _ = return ()
-    unfoldWorker ((node, instrs) Seq.:<| rest) searchOrder
-      | []              <- instrs = unfoldWorker rest searchOrder
-      | instr : instrs' <- instrs
-      = Profile.executionQueueLength (Seq.length rest) $ do
-        when (exeedsLimit rest)
-            $ Exception.throw $ LimitExceeded rest
-        nodes' <- applyInstr instr node
-        let seeds = map (withInstrs instrs') nodes'
-        case searchOrder of
-            -- The graph is unfolded breadth-first by appending the new seeds
-            -- to the end of the todo list. The next seed is always taken from
-            -- the beginning of the sequence, so that all the pending seeds
-            -- are unfolded once before the new seeds are unfolded.
-            BreadthFirst -> unfoldWorker
-                                (rest <> Seq.fromList seeds)
-                                searchOrder
-            -- The graph is unfolded depth-first by putting the new seeds to
-            -- the head of the todo list.
-            DepthFirst -> unfoldWorker
-                              (Seq.fromList seeds <> rest)
-                              searchOrder
-
-    exeedsLimit = not . withinLimit breadthLimit . fromIntegral . Seq.length
-
-    withInstrs instrs nodes = (nodes, instrs)
-
-    applyInstr instr node = do
-        config <- getNodeConfig node
-        configs' <- transit' instr config
-        traverse insChildNode (childOf node <$> configs')
-
-    getNodeConfig node =
-        fromMaybe (error "Node does not exist")
-        <$> State.gets (`Graph.lab` node)
-
-    childOf
-        :: Graph.Node
-        -> (config, Seq rule)
-        -- ^ Child node identifier and configuration
-        -> ChildNode config rule
-    childOf node (config, rules) =
-        ChildNode
-            { config
-            , parents = [(rules, node)]
-            }
+    execGraph = emptyExecutionGraph config0
+
+    mkQueue = \as ->
+        unfoldSearchOrder searchOrder0 as
+        >=> applyBreadthLimit breadthLimit
+        >=> profileQueueLength
+
+    profileQueueLength queue = do
+        Profile.executionQueueLength (Seq.length queue)
+        pure queue
+
+    transit' =
+        updateGraph $ \instr config ->
+            mapTransitionT lift $ transit instr config
+
+{- | Unfold the function from the initial vertex.
+
+@leavesM@ returns a disjunction of leaves (vertices without descendants) rather
+than constructing the entire graph.
+
+The queue updating function should be 'unfoldBreadthFirst' or
+'unfoldDepthFirst', optionally composed with 'applyBreadthLimit'.
+
+ -}
+leavesM
+    :: forall m a
+    .  Monad m
+    => Alternative m
+    => ([a] -> Seq a -> m (Seq a))  -- ^ queue updating function
+    -> (a -> m [a])  -- ^ unfolding function
+    -> a  -- ^ initial vertex
+    -> m a
+leavesM mkQueue next a0 =
+    mkQueue [a0] Seq.empty >>= worker
+  where
+    worker Seq.Empty = empty
+    worker (a Seq.:<| as) =
+        do
+            as' <- lift (next a)
+            (guard . not) (null as')
+            lift (mkQueue as' as)
+        & maybeT (return a <|> worker as) worker
+
+{- | Unfold the function from the initial vertex.
+
+@unfoldM_@ visits every descendant in the graph, but unlike 'leavesM' does not
+return any values.
+
+The queue updating function should be 'unfoldBreadthFirst' or
+'unfoldDepthFirst', optionally composed with 'applyBreadthLimit'.
+
+See also: 'leavesM'
+
+ -}
+unfoldM_
+    :: forall m a
+    .  Monad m
+    => ([a] -> Seq a -> m (Seq a))  -- ^ queue updating function
+    -> (a -> m [a])  -- ^ unfolding function
+    -> a  -- ^ initial vertex
+    -> m ()
+unfoldM_ mkQueue next = \a ->
+    mkQueue [a] Seq.empty >>= worker
+  where
+    worker Seq.Empty = return ()
+    worker (a Seq.:<| as) = do
+        as' <- next a
+        mkQueue as' as >>= worker
+
+unfoldBreadthFirst :: Applicative f => [a] -> Seq a -> f (Seq a)
+unfoldBreadthFirst as' as = pure (as <> Seq.fromList as')
+
+unfoldDepthFirst :: Applicative f => [a] -> Seq a -> f (Seq a)
+unfoldDepthFirst as' as = pure (Seq.fromList as' <> as)
+
+unfoldSearchOrder
+    :: Applicative f
+    => GraphSearchOrder
+    -> [a] -> Seq a -> f (Seq a)
+unfoldSearchOrder DepthFirst = unfoldDepthFirst
+unfoldSearchOrder BreadthFirst = unfoldBreadthFirst
+
+applyBreadthLimit
+    :: Exception (LimitExceeded a)
+    => MonadThrow m
+    => Limit Natural
+    -> Seq a
+    -> m (Seq a)
+applyBreadthLimit breadthLimit as
+  | _ Seq.:<| as' <- as, exceedsLimit as' =
+    Exception.throwM (LimitExceeded as)
+  | otherwise = pure as
+  where
+    exceedsLimit = not . withinLimit breadthLimit . fromIntegral . Seq.length
+
+{- | Turn a transition rule into an unfolding function.
+
+@unfoldTransition@ applies the transition rule to the first @instr@ and threads
+the tail of the list to the results. The result is @[]@ if the @[instr]@ is
+empty.
+
+ -}
+unfoldTransition
+    :: Monad m
+    => (instr -> config -> m [config])  -- ^ transition rule
+    -> ([instr], config)
+    -> m [([instr], config)]
+unfoldTransition transit (instrs, config) =
+    case instrs of
+        [] -> pure []
+        instr : instrs' -> do
+            configs' <- transit instr config
+            pure ((,) instrs' <$> configs')
 
 {- | Transition rule for running a 'Strategy'.
 
@@ -532,7 +636,7 @@ See also: 'pickLongest', 'pickFinal', 'pickOne', 'pickStar', 'pickPlus'
 
 runStrategy
     :: forall m prim rule config
-    .  MonadProfiler m
+    .  (MonadProfiler m, MonadThrow m)
     => Show prim
     => Typeable prim
     => Limit Natural
@@ -548,7 +652,7 @@ runStrategy breadthLimit applyPrim instrs0 config0 =
 
 runStrategyWithSearchOrder
     :: forall m prim rule config
-    .  MonadProfiler m
+    .  (MonadProfiler m, MonadThrow m)
     => Show prim
     => Typeable prim
     => Limit Natural
diff --git a/kore/src/Kore/Step/Transition.hs b/kore/src/Kore/Step/Transition.hs
index f62b0a2cfa..a304090aac 100644
--- a/kore/src/Kore/Step/Transition.hs
+++ b/kore/src/Kore/Step/Transition.hs
@@ -133,10 +133,10 @@ tryTransitionT
 tryTransitionT = lift . runTransitionT
 
 mapTransitionT
-    :: Monad m
-    => (forall x. m x -> m x)
-    -> TransitionT rule m a
+    :: (Monad m, Monad n)
+    => (forall x. m x -> n x)
     -> TransitionT rule m a
+    -> TransitionT rule n a
 mapTransitionT mapping =
     TransitionT . mapAccumT (mapListT mapping) . getTransitionT
 
diff --git a/kore/src/Kore/Strategies/Verification.hs b/kore/src/Kore/Strategies/Verification.hs
index ff1d7159fa..d77a036b90 100644
--- a/kore/src/Kore/Strategies/Verification.hs
+++ b/kore/src/Kore/Strategies/Verification.hs
@@ -21,6 +21,9 @@ module Kore.Strategies.Verification
 import Prelude.Kore
 
 import qualified Control.Lens as Lens
+import Control.Monad
+    ( (>=>)
+    )
 import qualified Control.Monad as Monad
     ( foldM_
     )
@@ -53,6 +56,7 @@ import Kore.Internal.Pattern
     ( Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
+import qualified Kore.Profiler.Profile as Profile
 import Kore.Step.RulePattern
     ( AllPathRule (..)
     , OnePathRule (..)
@@ -66,8 +70,8 @@ import Kore.Step.Strategy
     , GraphSearchOrder
     , Strategy
     , executionHistoryStep
-    , runStrategyWithSearchOrder
     )
+import qualified Kore.Step.Strategy as Strategy
 import Kore.Step.Transition
     ( TransitionT
     , runTransitionT
@@ -82,6 +86,9 @@ import Kore.Syntax.Variable
     ( Variable
     )
 import Kore.Unparser
+import ListT
+    ( ListT (..)
+    )
 
 -- TODO (thomas.tuegel): (Pattern Variable) should be ReachabilityRule.
 type CommonProofState = ProofState.ProofState (Pattern Variable)
@@ -221,20 +228,51 @@ verifyClaim
     let
         startPattern = ProofState.Goal $ getConfiguration goal
         limitedStrategy =
-            Limit.takeWithin
-                depthLimit
-                (Foldable.toList $ strategy goal claims axioms)
-    executionGraph <-
-        runStrategyWithSearchOrder
-            breadthLimit
-            modifiedTransitionRule
-            limitedStrategy
-            searchOrder
-            startPattern
-    -- Throw the first unproven configuration as an error.
-    Foldable.traverse_ Monad.Except.throwError (unprovenNodes executionGraph)
+            strategy goal claims axioms
+            & Foldable.toList
+            & Limit.takeWithin depthLimit
+    Strategy.leavesM
+        updateQueue
+        (Strategy.unfoldTransition transit)
+        (limitedStrategy, startPattern)
+        & fmap discardStrategy
+        & throwUnproven
   where
     destination = getDestination goal
+    discardStrategy = snd
+
+    updateQueue = \as ->
+        Strategy.unfoldSearchOrder searchOrder as
+        >=> Strategy.applyBreadthLimit breadthLimit
+        >=> profileQueueLength
+
+    profileQueueLength queue = do
+        Profile.executionQueueLength (length queue)
+        pure queue
+
+    throwUnproven
+        :: ListT (Verifier simplifier) CommonProofState
+        -> Verifier simplifier ()
+    throwUnproven acts =
+        foldListT acts throwUnprovenOrElse done
+      where
+        done = return ()
+
+    throwUnprovenOrElse
+        :: ProofState.ProofState (Pattern Variable)
+        -> Verifier simplifier ()
+        -> Verifier simplifier ()
+    throwUnprovenOrElse proofState acts = do
+        ProofState.extractUnproven proofState
+            & Foldable.traverse_ Monad.Except.throwError
+        acts
+
+    transit instr config =
+        Strategy.transitionRule modifiedTransitionRule instr config
+        & runTransitionT
+        & fmap (map fst)
+        & lift
+
     modifiedTransitionRule
         ::  Prim ReachabilityRule
         ->  CommonProofState
diff --git a/kore/src/ListT.hs b/kore/src/ListT.hs
index fd3be1358a..db71d0d2ee 100644
--- a/kore/src/ListT.hs
+++ b/kore/src/ListT.hs
@@ -27,6 +27,7 @@ import Prelude
 
 import Control.Applicative
 import Control.Monad
+import Control.Monad.Catch
 import Control.Monad.IO.Class
 import Control.Monad.Morph
 import Control.Monad.RWS.Class
@@ -152,6 +153,10 @@ instance (Monad f, Foldable f) => Foldable (ListT f) where
         fold $ foldListT as (\a r -> mappend (f a) <$> r) (pure mempty)
     {-# INLINE foldMap #-}
 
+instance MonadThrow m => MonadThrow (ListT m) where
+    throwM = lift . throwM
+    {-# INLINE throwM #-}
+
 cons :: a -> ListT m a -> ListT m a
 cons a as = ListT $ \yield -> yield a . foldListT as yield
 {-# INLINE cons #-}
diff --git a/kore/test/Test/Kore/Exec.hs b/kore/test/Test/Kore/Exec.hs
index 690b1efd3d..a3ddab1c3e 100644
--- a/kore/test/Test/Kore/Exec.hs
+++ b/kore/test/Test/Kore/Exec.hs
@@ -3,7 +3,7 @@ module Test.Kore.Exec
     , test_execPriority
     , test_search
     , test_searchPriority
-    , test_searchExeedingBreadthLimit
+    , test_searchExceedingBreadthLimit
     , test_execGetExitCode
     ) where
 
@@ -18,10 +18,7 @@ import Control.Exception as Exception
 import Data.Default
     ( def
     )
-import Data.Limit
-    ( Limit (..)
-    )
-import qualified Data.Limit as Limit
+import qualified Data.Graph.Inductive.Graph as Graph
 import qualified Data.Map.Strict as Map
 import Data.Set
     ( Set
@@ -34,6 +31,10 @@ import System.Exit
     ( ExitCode (..)
     )
 
+import Data.Limit
+    ( Limit (..)
+    )
+import qualified Data.Limit as Limit
 import Kore.ASTVerifier.DefinitionVerifier
     ( verifyAndIndexDefinition
     )
@@ -273,23 +274,24 @@ test_search =
                 PLUS -> Set.fromList [b, c, d]
                 FINAL -> Set.fromList [b, d]
 
-test_searchExeedingBreadthLimit :: [TestTree]
-test_searchExeedingBreadthLimit =
+test_searchExceedingBreadthLimit :: [TestTree]
+test_searchExceedingBreadthLimit =
     [ makeTestCase searchType | searchType <- [ ONE, STAR, PLUS, FINAL] ]
   where
     unlimited :: Limit Integer
     unlimited = Unlimited
     makeTestCase searchType =
         testCase
-            ("Exceed bredth limit: " <> show searchType)
+            ("Exceed breadth limit: " <> show searchType)
             (assertion searchType)
 
     assertion searchType =
-        shouldExeedBreadthLimit searchType `catch`
-            \(_ :: LimitExceeded (Strategy (Prim Rewrite))) -> pure ()
+        catch (shouldExceedBreadthLimit searchType)
+        $ \(_ :: LimitExceeded ([Strategy (Prim Rewrite)], Graph.Node)) ->
+            pure ()
 
-    shouldExeedBreadthLimit :: SearchType -> IO ()
-    shouldExeedBreadthLimit searchType = do
+    shouldExceedBreadthLimit :: SearchType -> IO ()
+    shouldExceedBreadthLimit searchType = do
         a <- actual searchType
         when (a == expected searchType)
             $ assertFailure "Did not exceed breadth limit"
diff --git a/kore/test/Test/Kore/Step/Strategy.hs b/kore/test/Test/Kore/Step/Strategy.hs
index d93b7eabd3..5ab3f66d93 100644
--- a/kore/test/Test/Kore/Step/Strategy.hs
+++ b/kore/test/Test/Kore/Step/Strategy.hs
@@ -30,7 +30,11 @@ import Test.Tasty
 import Test.Tasty.HUnit
 import Test.Tasty.QuickCheck
 
-import Data.Functor.Identity
+import qualified Control.Exception as Exception
+import Control.Monad.Catch.Pure
+    ( Catch
+    , runCatch
+    )
 import qualified Data.Graph.Inductive.Graph as Graph
 import qualified Data.Sequence as Seq
 import Numeric.Natural
@@ -89,7 +93,7 @@ instance Arbitrary prim => Arbitrary (Strategy prim) where
             Strategy.Stuck -> []
             Strategy.Continue -> []
 
-transitionPrim :: Prim -> Natural -> TransitionT Prim Identity Natural
+transitionPrim :: Prim -> Natural -> TransitionT Prim Catch Natural
 transitionPrim rule n = do
     Transition.addRule rule
     case rule of
@@ -129,10 +133,9 @@ runStrategy
     -> Natural
     -> ExecutionGraph Natural Prim
 runStrategy strategy z =
-    let
-        Identity rs = Strategy.runStrategy Unlimited transitionPrim strategy z
-    in
-        rs
+    Strategy.runStrategy Unlimited transitionPrim strategy z
+    & runCatch
+    & either Exception.throw id
 
 prop_SeqContinueIdentity :: Strategy Prim -> Natural -> Property
 prop_SeqContinueIdentity a n =