diff --git a/Test/Tasty/DejaFu.hs b/Test/Tasty/DejaFu.hs
--- a/Test/Tasty/DejaFu.hs
+++ b/Test/Tasty/DejaFu.hs
@@ -1,38 +1,121 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE GADTs              #-}
-{-# LANGUAGE RankNTypes         #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeSynonymInstances #-}
 
 -- | This module allows using Deja Fu predicates with Tasty to test
 -- the behaviour of concurrent systems.
 module Test.Tasty.DejaFu
-  ( -- * Testing
+  ( -- * Unit testing
+
+  -- | This is supported by the 'IsTest' instances for 'ConcST' and
+  -- 'ConcIO'. These instances try all executions, reporting as
+  -- failures the cases which return a 'Just' string.
+  --
+  -- @instance Typeable t => IsTest (ConcST t (Maybe String))@
+  -- @instance               IsTest (ConcIO   (Maybe String))@
+  -- @instance IsOption Bounds@
+  -- @instance IsOption MemType@
+
+  -- * Property testing
     testAuto
   , testDejafu
   , testDejafus
+
+  , testAuto'
+  , testDejafu'
+  , testDejafus'
+
+  -- ** @IO@
   , testAutoIO
   , testDejafuIO
   , testDejafusIO
 
-  -- * Testing under Alternative Memory Models
-  , MemType(..)
-  , testAuto'
   , testAutoIO'
-  , testDejafu'
-  , testDejafus'
   , testDejafuIO'
   , testDejafusIO'
+
+  -- * Re-exports
+  , Bounds(..)
+  , MemType(..)
   ) where
 
+import Data.Char (toUpper)
+import Data.List (intercalate, intersperse)
+import Data.Proxy (Proxy(..))
+import Data.Tagged (Tagged(..))
 import Data.Typeable (Typeable)
 import Test.DejaFu
-import Test.DejaFu.Deterministic (ConcST, ConcIO, Trace, showFail, showTrace)
+import Test.DejaFu.Deterministic (ConcST, ConcIO, Trace, ThreadId, ThreadAction, Lookahead, showFail, showTrace)
 import Test.DejaFu.SCT (sctBound, sctBoundIO)
 import Test.Tasty (TestName, TestTree, testGroup)
+import Test.Tasty.Options (OptionDescription(..), IsOption(..), lookupOption)
 import Test.Tasty.Providers (IsTest(..), singleTest, testPassed, testFailed)
 
+-- Can't put the necessary forall in the @IsTest ConcST t@
+-- instance :(
+import Unsafe.Coerce (unsafeCoerce)
+
+#if MIN_VERSION_dejafu(0,3,0)
+type Trc = Trace ThreadId ThreadAction Lookahead
+#else
+type Trc = Trace
+#endif
+
 --------------------------------------------------------------------------------
--- Automated testing
+-- Unit testing
 
+instance Typeable t => IsTest (ConcST t (Maybe String)) where
+  testOptions = Tagged concOptions
+
+  run options conc callback = do
+    let memtype = lookupOption options :: MemType
+    let bounds  = lookupOption options :: Bounds
+    let sctBound' :: ConcST t (Maybe String) -> [(Either Failure (Maybe String), Trc)]
+        sctBound' = unsafeCoerce $ sctBound memtype bounds
+    let traces = sctBound' conc
+    run options (ConcTest traces assertableP) callback
+
+instance IsTest (ConcIO (Maybe String)) where
+  testOptions = Tagged concOptions
+
+  run options conc callback = do
+    let memtype = lookupOption options
+    let bounds  = lookupOption options
+    let traces = sctBoundIO memtype bounds conc
+    run options (ConcIOTest traces assertableP) callback
+
+concOptions :: [OptionDescription]
+concOptions =
+  [ Option (Proxy :: Proxy Bounds)
+  , Option (Proxy :: Proxy MemType)
+  ]
+
+assertableP :: Predicate (Maybe String)
+assertableP = alwaysTrue $ \r -> case r of
+  Right (Just _) -> False
+  _ -> True
+
+instance IsOption Bounds where
+  defaultValue = defaultBounds
+  parseValue = const Nothing
+  optionName = Tagged "schedule-bounds"
+  optionHelp = Tagged "The schedule bounds to use. This cannot be set on the command line."
+
+instance IsOption MemType where
+  defaultValue = defaultMemType
+  parseValue str = shortName (map toUpper str) where
+    shortName "SC"  = Just SequentialConsistency
+    shortName "TSO" = Just TotalStoreOrder
+    shortName "PSO" = Just PartialStoreOrder
+    shortName _ = Nothing
+  optionName = Tagged "memory-model"
+  optionHelp = Tagged "The memory model to use. This should be one of \"SC\", \"TSO\", or \"PSO\"."
+
+--------------------------------------------------------------------------------
+-- Property testing
+
 -- | Automatically test a computation. In particular, look for
 -- deadlocks, uncaught exceptions, and multiple return values.
 -- 
@@ -71,9 +154,6 @@
   , ("Consistent Result", alwaysSame)
   ]
 
---------------------------------------------------------------------------------
--- Manual testing
-
 -- | Check that a predicate holds.
 testDejafu :: Show a
   => (forall t. ConcST t a)
@@ -124,7 +204,7 @@
   -> [(TestName, Predicate a)]
   -- ^ The list of predicates (with names) to check
   -> TestTree
-testDejafus' = test
+testDejafus' = testst
 
 -- | Variant of 'testDejafu' for computations which do 'IO'.
 testDejafuIO :: Show a => ConcIO a -> TestName -> Predicate a -> TestTree
@@ -146,11 +226,11 @@
 -- Tasty integration
 
 data ConcTest where
-  ConcTest   :: Show a => [(Either Failure a, Trace)] -> Predicate a -> ConcTest
+  ConcTest   :: Show a => [(Either Failure a, Trc)] -> Predicate a -> ConcTest
   deriving Typeable
 
 data ConcIOTest where
-  ConcIOTest :: Show a => IO [(Either Failure a, Trace)] -> Predicate a -> ConcIOTest
+  ConcIOTest :: Show a => IO [(Either Failure a, Trc)] -> Predicate a -> ConcIOTest
   deriving Typeable
 
 instance IsTest ConcTest where
@@ -169,8 +249,8 @@
     return $ if null err then testPassed "" else testFailed err
 
 -- | Produce a Tasty 'TestTree' from a Deja Fu test.
-test :: Show a => MemType -> Bounds -> (forall t. ConcST t a) -> [(TestName, Predicate a)] -> TestTree
-test memtype cb conc tests = case map toTest tests of
+testst :: Show a => MemType -> Bounds -> (forall t. ConcST t a) -> [(TestName, Predicate a)] -> TestTree
+testst memtype cb conc tests = case map toTest tests of
   [t] -> t
   ts  -> testGroup "Deja Fu Tests" ts
 
@@ -201,7 +281,7 @@
 
   msg = if null (_failureMsg res) then "" else _failureMsg res ++ "\n"
 
-  failures = map (\(r, t) -> "\t" ++ either showFail show r ++ " " ++ showTrace t) . take 5 $ _failures res
+  failures = intersperse "" . map (\(r, t) -> indent $ either showFail show r ++ " " ++ showTrace t) . take 5 $ _failures res
 
   rest = if moreThan (_failures res) 5 then "\n\t..." else ""
 
@@ -211,3 +291,6 @@
 moreThan _ 0  = True
 moreThan (_:xs) n = moreThan xs (n-1)
 
+-- | Indent every line of a string.
+indent :: String -> String
+indent = intercalate "\n" . map ('\t':) . lines
diff --git a/tasty-dejafu.cabal b/tasty-dejafu.cabal
--- a/tasty-dejafu.cabal
+++ b/tasty-dejafu.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                tasty-dejafu
-version:             0.2.0.0
+version:             0.3.0.0
 synopsis:            Deja Fu support for the Tasty test framework.
 
 description:
@@ -30,12 +30,18 @@
   type:     git
   location: https://github.com/barrucadu/dejafu.git
 
+source-repository this
+  type:     git
+  location: https://github.com/barrucadu/dejafu.git
+  tag:      tasty-dejafu-0.3.0.0
+
 library
   exposed-modules:     Test.Tasty.DejaFu
   -- other-modules:       
   -- other-extensions:    
   build-depends:       base >=4.5 && <5
-                     , dejafu == 0.2.*
+                     , dejafu >= 0.2
+                     , tagged
                      , tasty
   -- hs-source-dirs:      
   default-language:    Haskell2010