diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -7,6 +7,23 @@
 *de facto* standard Haskell versioning scheme.
 
 
+0.7.0.1 [2017-06-09] (git tag: [dejafu-0.7.0.1][])
+-------
+
+https://hackage.haskell.org/package/dejafu-0.7.0.1
+
+### Test.DejaFu.Refinement
+
+- `check`, `check'`, and `checkFor` are now faster if there are multiple counterexamples.
+- The above and `counterExamples` are now faster even if there is only a single counterexample in
+  some cases.
+
+[dejafu-0.7.0.1]: https://github.com/barrucadu/dejafu/releases/tag/dejafu-0.7.0.1
+
+
+---------------------------------------------------------------------------------------------------
+
+
 0.7.0.0 [2017-06-07] (git tag: [dejafu-0.7.0.0][])
 -------
 
diff --git a/Test/DejaFu/Refinement.hs b/Test/DejaFu/Refinement.hs
--- a/Test/DejaFu/Refinement.hs
+++ b/Test/DejaFu/Refinement.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeFamilies #-}
 
@@ -10,7 +11,7 @@
 -- License     : MIT
 -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
 -- Stability   : experimental
--- Portability : FlexibleContexts, FlexibleInstances, GADTs, TupleSections, TypeFamilies
+-- Portability : FlexibleContexts, FlexibleInstances, GADTs, MultiWayIf, TupleSections, TypeFamilies
 --
 -- Properties about the side-effects of concurrent functions on some
 -- shared state.
@@ -304,6 +305,9 @@
 -- | Like 'check', but take a number of cases to try, also returns the
 -- counter example found rather than printing it.
 --
+-- If multiple counterexamples exist, this will be faster than
+-- @listToMaybe@ composed with @counterExamples@.
+--
 -- @since 0.7.0.0
 checkFor :: (Testable p, Listable (X p), Eq (X p), Show (X p))
   => Int
@@ -313,7 +317,17 @@
   -> p
   -- ^ The property to check.
   -> IO (Maybe (FailedProperty (O p) (X p)))
-checkFor sn vn p = listToMaybe <$> counterExamples sn vn p
+checkFor sn vn p =  do
+    let seeds = take sn $ concat tiers
+    let cases = take vn $ concat (rpropTiers p)
+    go seeds cases
+  where
+    go seeds ((vs, p'):rest) = do
+      r <- checkWithSeeds seeds p'
+      case r of
+        Just cf -> pure (Just (cf vs))
+        Nothing -> go seeds rest
+    go _ [] = pure Nothing
 
 -- | Find all counterexamples up to a limit.
 --
@@ -336,6 +350,9 @@
 -------------------------------------------------------------------------------
 -- Internal
 
+-- | Three-valued sum, used in checking strict refinement.
+data F x = Failing x | Unknown | Refuted
+
 -- | Check a refinement property with given seed values.  Returns the
 -- counterexample if the property is false.
 checkWithSeeds
@@ -344,21 +361,33 @@
   -> RefinementProperty o x
   -- ^ The property to check.
   -> IO (Maybe ([String] -> FailedProperty o x))
-checkWithSeeds seeds (RP how l r) = do
-    ls <- mapM (\x -> (x,) <$> evalSigWithSeed l x) seeds
-    rs <- mapM (evalSigWithSeed r) seeds
-    let resultsf f = zipWith (\(x, l') r' -> (l' `f` r', x, l', r')) ls rs
-    pure . listToMaybe $ case how of
-      Weak   -> ces (resultsf S.isSubsetOf)
-      Strict ->
-        -- strict fails if (a) any left result-set is not a subset of
-        -- the corresponding right result-set, or (b) every left
-        -- result-set is equal to the corresponding right result-set
-        let equiv = null (ces (resultsf (==)))
-        in ces (resultsf S.isSubsetOf) ++ if equiv then ces (resultsf S.isProperSubsetOf) else []
-      Equiv  -> ces (resultsf (==))
+checkWithSeeds seeds (RP how l r) = case how of
+    Weak   -> go1 S.isSubsetOf seeds
+    Equiv  -> go1 (==)         seeds
+    Strict -> go2 Unknown      seeds
   where
-    ces results = [toCE x lrs rrs | (False, x, lrs, rrs) <- results]
+    -- weak and equiv need every set of pairwise result-sets to match
+    -- some predicate.
+    go1 f (x:xs) = do
+      lrs <- evalSigWithSeed l x
+      rrs <- evalSigWithSeed r x
+      if lrs `f` rrs
+        then go1 f xs
+        else pure (Just $ toCE x lrs rrs)
+    go1 _ [] = pure Nothing
+
+    -- strict fails if (a) any left result-set is not a subset of the
+    -- corresponding right result-set, or (b) every left result-set is
+    -- equal to the corresponding right result-set
+    go2 eq (x:xs) = do
+      lrs <- evalSigWithSeed l x
+      rrs <- evalSigWithSeed r x
+      let ce = toCE x lrs rrs
+      if | lrs == rrs             -> go2 (case eq of Unknown -> Failing ce; _ -> eq) xs
+         | lrs `S.isSubsetOf` rrs -> go2 Refuted xs
+         | otherwise              -> pure (Just ce)
+    go2 (Failing cf) [] = pure (Just cf)
+    go2 _ [] = pure Nothing
 
     toCE x lrs rrs args = CounterExample
       { failingSeed  = x
diff --git a/dejafu.cabal b/dejafu.cabal
--- a/dejafu.cabal
+++ b/dejafu.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                dejafu
-version:             0.7.0.0
+version:             0.7.0.1
 synopsis:            Systematic testing for Haskell concurrency.
 
 description:
@@ -37,7 +37,7 @@
 source-repository this
   type:     git
   location: https://github.com/barrucadu/dejafu.git
-  tag:      dejafu-0.7.0.0
+  tag:      dejafu-0.7.0.1
 
 library
   exposed-modules:     Test.DejaFu