diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,10 @@
 # Revision history for inspection-testing
 
+## 0.2 -- 2018-01-17
+
+* With `$(inspectTest obligation)` you can now get the result of inspection
+  testing at run-time, for integration into your test suite.
+
 ## 0.1.2 -- 2017-11-20
 
 * Make `(==-)` a bit more liberal, and look through variable redefinitions that
diff --git a/Test/Inspection.hs b/Test/Inspection.hs
--- a/Test/Inspection.hs
+++ b/Test/Inspection.hs
@@ -17,6 +17,8 @@
 
     -- * Registering obligations
     inspect,
+    inspectTest,
+    Result(..),
     -- * Defining obligations
     Obligation(..), mkObligation, Property(..),
     (===), (==-), (=/=), hasNoType,
@@ -24,8 +26,9 @@
 
 import Control.Monad
 import Language.Haskell.TH
-import Language.Haskell.TH.Syntax (getQ, putQ, liftData)
+import Language.Haskell.TH.Syntax (getQ, putQ, liftData, addTopDecls)
 import Data.Data
+import GHC.Exts (lazy)
 
 import Data.Maybe (fromMaybe)
 import qualified Data.Set as S
@@ -38,7 +41,7 @@
 
  1. enable the @TemplateHaskell@ langauge extension
  2. load the plugin using @-fplugin Test.Inspection.Plugin@
- 3. declare your proof obligations using 'inspect'
+ 3. declare your proof obligations using 'inspect' or 'inspectTest'
 
 An example module is
 
@@ -79,9 +82,13 @@
         -- ^ An optional name for the test
     , expectFail  :: Bool
         -- ^ Do we expect this property to fail?
+        -- (Only used by 'inspect', not by 'inspectTest')
     , srcLoc :: Maybe Loc
         -- ^ The source location where this obligation is defined.
         -- This is filled in by 'inspect'.
+    , storeResult :: Maybe String
+        -- ^ If this is 'Nothing', then report errors during compilation.
+        -- Otherwise, update the top-level definition with this name.
     }
     deriving Data
 
@@ -120,6 +127,7 @@
     , testName = Nothing
     , srcLoc = Nothing
     , expectFail = False
+    , storeResult = Nothing
     }
 
 -- | Convenience function to declare two functions to be equal
@@ -153,14 +161,49 @@
 
 -- The exported TH functions
 
--- | As seen in the example above, the entry point to inspection testing is the
--- 'inspect' function, to which you pass an 'Obligation'.
-inspect :: Obligation -> Q [Dec]
-inspect obl = do
+inspectCommon :: AnnTarget -> Obligation -> Q [Dec]
+inspectCommon annTarget obl = do
     loc <- location
     annExpr <- liftData (obl { srcLoc = Just loc })
     rememberDs <- concat <$> mapM rememberName (allLocalNames obl)
-    pure $ PragmaD (AnnP ModuleAnnotation annExpr) : rememberDs
+    pure $ PragmaD (AnnP annTarget annExpr) : rememberDs
+
+-- | As seen in the example above, the entry point to inspection testing is the
+-- 'inspect' function, to which you pass an 'Obligation'.
+-- It will report test failures at compile time.
+inspect :: Obligation -> Q [Dec]
+inspect = inspectCommon ModuleAnnotation
+
+-- | The result of 'inspectTest', which a more or less helpful text message
+data Result = Failure String | Success String
+    deriving Show
+
+didNotRunPluginError :: Result
+didNotRunPluginError = lazy (error "Test.Inspection.Plugin did not run")
+{-# NOINLINE didNotRunPluginError #-}
+
+-- | This is a variant that allows compilation to succeed in any case,
+-- and instead indicates the result as a value of type 'Result',
+-- which allows seamless integration into test frameworks.
+--
+-- This variant ignores the 'expectFail' field of the obligation. Instead,
+-- it is expected that you use the corresponding functionality in your test
+-- framework (e.g. tasty-expected-failure)
+inspectTest :: Obligation -> Q Exp
+inspectTest obl = do
+    nameS <- genName
+    name <- newName nameS
+    anns <- inspectCommon (ValueAnnotation name) obl
+    addTopDecls $
+        [ SigD name (ConT ''Result)
+        , ValD (VarP name) (NormalB (VarE 'didNotRunPluginError)) []
+        , PragmaD (InlineP name NoInline FunLike AllPhases)
+        ] ++ anns
+    return $ VarE name
+  where
+    genName = do
+        (r,c) <- loc_start <$> location
+        return $ "inspect_" ++ show r ++ "_" ++ show c
 
 -- We need to ensure that names refernced in obligations are kept alive
 -- We do so by annotating them with 'KeepAlive'
diff --git a/Test/Inspection/Internal.hs b/Test/Inspection/Internal.hs
--- a/Test/Inspection/Internal.hs
+++ b/Test/Inspection/Internal.hs
@@ -6,7 +6,9 @@
 -- Portability : GHC specifc
 --
 {-# LANGUAGE DeriveDataTypeable #-}
-module Test.Inspection.Internal (KeepAlive(..)) where
+module Test.Inspection.Internal
+    ( KeepAlive(..)
+    ) where
 
 import Data.Data
 
diff --git a/Test/Inspection/Plugin.hs b/Test/Inspection/Plugin.hs
--- a/Test/Inspection/Plugin.hs
+++ b/Test/Inspection/Plugin.hs
@@ -3,42 +3,46 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE TemplateHaskell #-}
 module Test.Inspection.Plugin (plugin) where
 
 import Control.Monad
 import System.Exit
 import Data.Either
 import Data.Maybe
+import Data.Bifunctor
 import qualified Data.Map.Strict as M
 import qualified Language.Haskell.TH.Syntax as TH
 
 import GhcPlugins hiding (SrcLoc)
 
 import Test.Inspection.Internal (KeepAlive(..))
-import Test.Inspection (Obligation(..), Property(..))
+import Test.Inspection (Obligation(..), Property(..), Result(..))
 import Test.Inspection.Core
 
--- | The plugin. It supports the option @-fplugin-opt=Test.Inspection.Plugin=keep-going@ to
+-- | The plugin. It supports the option @-fplugin-opt=Test.Inspection.Plugin:keep-going@ to
 -- ignore a failing build.
 plugin :: Plugin
 plugin = defaultPlugin { installCoreToDos = install }
 
 data UponFailure = AbortCompilation | KeepGoing deriving Eq
 
+data ResultTarget = PrintAndAbort | StoreAt Name
+
 install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
 install args passes = return $ passes ++ [pass]
   where
-    pass = CoreDoPluginPass "Test.Inspection" (proofPass upon_failure)
+    pass = CoreDoPluginPass "Test.Inspection.Plugin" (proofPass upon_failure)
     upon_failure | "keep-going" `elem` args = KeepGoing
                  | otherwise                = AbortCompilation
 
 
-extractObligations :: ModGuts -> (ModGuts, [Obligation])
-extractObligations guts = (guts { mg_rules = rules', mg_anns = anns_clean }, obligations)
+extractObligations :: ModGuts -> (ModGuts, [(ResultTarget, Obligation)])
+extractObligations guts = (guts', obligations)
   where
-    rules' = mg_rules guts
     (anns', obligations) = partitionMaybe findObligationAnn (mg_anns guts)
     anns_clean = filter (not . isKeepAliveAnn) anns'
+    guts' = guts { mg_anns = anns_clean }
 
 isKeepAliveAnn :: Annotation -> Bool
 isKeepAliveAnn (Annotation (NamedTarget _) payload)
@@ -47,10 +51,13 @@
 isKeepAliveAnn _
     = False
 
-findObligationAnn :: Annotation -> Maybe Obligation
+findObligationAnn :: Annotation -> Maybe (ResultTarget, Obligation)
 findObligationAnn (Annotation (ModuleTarget _) payload)
     | Just obl <- fromSerialized deserializeWithData payload
-    = Just obl
+    = Just (PrintAndAbort, obl)
+findObligationAnn (Annotation (NamedTarget n) payload)
+    | Just obl <- fromSerialized deserializeWithData payload
+    = Just (StoreAt n, obl)
 findObligationAnn _
     = Nothing
 
@@ -74,34 +81,48 @@
     | moduleNameString (moduleName mod) == TH.modString m = TH.occString occ
 showTHName _ n = show n
 
-data Stat = ExpSuccess | ExpFailure | UnexpSuccess | UnexpFailure
+data Stat = ExpSuccess | ExpFailure | UnexpSuccess | UnexpFailure | StoredResult
     deriving (Enum, Eq, Ord, Bounded)
 type Stats = M.Map Stat Int
 
+type Updates = [(Name, Result)]
+
 tick :: Stat -> Stats
 tick s = M.singleton s 1
 
-checkObligation :: ModGuts -> Obligation -> CoreM Stats
-checkObligation guts obl = do
+checkObligation :: ModGuts -> (ResultTarget, Obligation) -> CoreM (Updates, Stats)
+checkObligation guts (reportTarget, obl) = do
 
     res <- checkProperty guts (target obl) (property obl)
+    case reportTarget of
+        PrintAndAbort -> do
+            category <- case (res, expectFail obl) of
+                -- Property holds
+                (Nothing, False) -> do
+                    putMsgS $ prettyObligation (mg_module guts) obl expSuccess
+                    return ExpSuccess
+                (Nothing, True) -> do
+                    putMsgS $ prettyObligation (mg_module guts) obl unexpSuccess
+                    return UnexpSuccess
+                -- Property does not hold
+                (Just reportDoc, False) -> do
+                    putMsgS $ prettyObligation (mg_module guts) obl unexpFailure
+                    putMsg $ reportDoc
+                    return UnexpFailure
+                (Just _, True) -> do
+                    putMsgS $ prettyObligation (mg_module guts) obl expFailure
+                    return ExpFailure
+            return ([], tick category)
+        StoreAt name -> do
+            dflags <- getDynFlags
+            let result = case res of
+                    Nothing -> Success $ showSDoc dflags $
+                        text (prettyObligation (mg_module guts) obl expSuccess)
+                    Just reportMsg -> Failure $ showSDoc dflags $
+                        text (prettyObligation (mg_module guts) obl unexpFailure) $$
+                        reportMsg
+            pure ([(name, result)], tick StoredResult)
 
-    case (res, expectFail obl) of
-        -- Property holds
-        (Nothing, False) -> do
-            putMsgS $ prettyObligation (mg_module guts) obl expSuccess
-            return (tick ExpSuccess)
-        (Nothing, True) -> do
-            putMsgS $ prettyObligation (mg_module guts) obl unexpSuccess
-            return (tick UnexpSuccess)
-        -- Property does not hold
-        (Just reportMsg, False) -> do
-            putMsgS $ prettyObligation (mg_module guts) obl unexpFailure
-            reportMsg
-            return (tick UnexpFailure)
-        (Just _, True) -> do
-            putMsgS $ prettyObligation (mg_module guts) obl expFailure
-            return (tick ExpFailure)
   where
     expSuccess   = "passed."
     unexpSuccess = "passed unexpectedly!"
@@ -109,7 +130,7 @@
     expFailure   = "failed expectedly."
 
 
-type Result =  Maybe (CoreM ())
+type CheckResult = Maybe SDoc
 
 lookupNameInGuts :: ModGuts -> Name -> Maybe (Var, CoreExpr)
 lookupNameInGuts guts n = listToMaybe
@@ -118,7 +139,15 @@
     , getName v == n
     ]
 
-checkProperty :: ModGuts -> TH.Name -> Property -> CoreM Result
+updateNameInGuts :: Name -> CoreExpr -> ModGuts -> ModGuts
+updateNameInGuts n expr guts =
+    guts {mg_binds = map (updateNameInGut n expr) (mg_binds guts) }
+
+updateNameInGut :: Name -> CoreExpr -> CoreBind -> CoreBind
+updateNameInGut n e (NonRec v _) | getName v == n = NonRec v e
+updateNameInGut _ _ bind                          = bind
+
+checkProperty :: ModGuts -> TH.Name -> Property -> CoreM CheckResult
 checkProperty guts thn1 (EqualTo thn2 ignore_types) = do
     Just n1 <- thNameToGhcName thn1
     Just n2 <- thNameToGhcName thn2
@@ -141,13 +170,11 @@
           -- OK if they have the same expression
           then return Nothing
           -- Not ok if the expression differ
-          else pure . Just $ putMsg $
-            pprSliceDifference slice1 slice2
+          else pure . Just $ pprSliceDifference slice1 slice2
        -- Not ok if both names are bound externally
        | Nothing <- p1
        , Nothing <- p2
-       -> pure . Just $ do
-            putMsg $ ppr n1 <+> text " and " <+> ppr n2 <+>
+       -> pure . Just $ ppr n1 <+> text " and " <+> ppr n2 <+>
                 text "are different external names"
   where
     binds = flattenBinds (mg_binds guts)
@@ -156,23 +183,39 @@
     Just n <- thNameToGhcName thn
     Just t <- thNameToGhcName tht
     case lookupNameInGuts guts n of
-        Nothing -> pure . Just $ do
-            putMsg $ ppr n <+> text "is not a local name"
+        Nothing -> pure . Just $ ppr n <+> text "is not a local name"
         Just (v, _) -> case freeOfType (slice binds v) t of
-            Just _ -> pure . Just $ putMsg $ pprSlice (slice binds v)
+            Just _ -> pure . Just $ pprSlice (slice binds v)
             Nothing -> pure Nothing
   where binds = flattenBinds (mg_binds guts)
 
 checkProperty guts thn NoAllocation = do
     Just n <- thNameToGhcName thn
     case lookupNameInGuts guts n of
-        Nothing -> pure . Just $ do
-            putMsg $ ppr n <+> text "is not a local name"
+        Nothing -> pure . Just $ ppr n <+> text "is not a local name"
         Just (v, _) -> case doesNotAllocate (slice binds v) of
-            Just (v',e') -> pure . Just $ putMsg $ nest 4 (ppr v' <+> text "=" <+> ppr e')
+            Just (v',e') -> pure . Just $ nest 4 (ppr v' <+> text "=" <+> ppr e')
             Nothing -> pure Nothing
   where binds = flattenBinds (mg_binds guts)
 
+storeResults :: Updates -> ModGuts -> CoreM ModGuts
+storeResults = flip (foldM (flip (uncurry go)))
+  where
+    go :: Name -> Result -> ModGuts -> CoreM ModGuts
+    go name res guts = do
+        e <- resultToExpr res
+        pure $ updateNameInGuts name e guts
+
+dcExpr :: TH.Name -> CoreM CoreExpr
+dcExpr thn = do
+    Just name <- thNameToGhcName thn
+    dc <- lookupDataCon name
+    pure $ Var (dataConWrapId dc)
+
+resultToExpr :: Result -> CoreM CoreExpr
+resultToExpr (Success s) = App <$> dcExpr 'Success <*> mkStringExpr s
+resultToExpr (Failure s) = App <$> dcExpr 'Failure <*> mkStringExpr s
+
 proofPass :: UponFailure -> ModGuts -> CoreM ModGuts
 proofPass upon_failure guts = do
     dflags <- getDynFlags
@@ -180,9 +223,12 @@
         warnMsg $ fsep $ map text $ words "Test.Inspection: Compilation without -O detected. Expect optimizations to fail."
 
     let (guts', obligations) = extractObligations guts
-    stats <- M.unionsWith (+) <$> mapM (checkObligation guts') obligations
+    (toStore, stats) <- (concat `bimap` M.unionsWith (+)) . unzip <$>
+        mapM (checkObligation guts') obligations
     let n = sum stats :: Int
 
+    guts'' <- storeResults toStore  guts'
+
     let q :: Stat -> Int
         q s = fromMaybe 0 $ M.lookup s stats
 
@@ -190,16 +236,18 @@
             vcat [ nest 2 (desc s) <> colon <+> ppr (q s)
                  | s <- [minBound..maxBound], q s > 0 ]
 
-    if q ExpSuccess + q ExpFailure == n
-    then putMsg $ text "inspection testing successful" $$ summary_message
-    else case upon_failure of
-        AbortCompilation -> do
-            errorMsg $ text "inspection testing unsuccessful" $$ summary_message
-            liftIO $ exitFailure -- kill the compiler. Is there a nicer way?
-        KeepGoing -> do
-            warnMsg $ text "inspection testing unsuccessful" $$ summary_message
+    -- Only print a message if there are some compile-time results to report
+    unless (q StoredResult == n) $ do
+        if q ExpSuccess + q ExpFailure + q StoredResult == n
+        then putMsg $ text "inspection testing successful" $$ summary_message
+        else case upon_failure of
+            AbortCompilation -> do
+                errorMsg $ text "inspection testing unsuccessful" $$ summary_message
+                liftIO $ exitFailure -- kill the compiler. Is there a nicer way?
+            KeepGoing -> do
+                warnMsg $ text "inspection testing unsuccessful" $$ summary_message
 
-    return guts'
+    return guts''
 
 
 desc :: Stat -> SDoc
@@ -207,6 +255,7 @@
 desc UnexpSuccess = text "unexpected successes"
 desc ExpFailure   = text "   expected failures"
 desc UnexpFailure = text " unexpected failures"
+desc StoredResult = text "      results stored"
 
 partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])
 partitionMaybe f = partitionEithers . map (\x -> maybe (Left x) Right (f x))
diff --git a/examples/SimpleTest.hs b/examples/SimpleTest.hs
new file mode 100644
--- /dev/null
+++ b/examples/SimpleTest.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# OPTIONS_GHC -O -fplugin=Test.Inspection.Plugin #-}
+module Main where
+
+import Test.Inspection
+import Data.Maybe
+import System.Exit
+
+lhs, rhs, something_else :: (a -> b) -> Maybe a -> Bool
+
+lhs f x = isNothing (fmap f x)
+
+rhs _ Nothing = True
+rhs _ (Just _) = False
+
+something_else _ _ = False
+
+printResult :: Result -> IO ()
+printResult (Success s) = putStrLn s
+printResult (Failure s) = putStrLn s
+
+isSuccess :: Result -> Bool
+isSuccess (Success _) = True
+isSuccess (Failure _) = False
+
+results :: [Result]
+results =
+    [ $(inspectTest $ 'lhs === 'rhs)
+    , $(inspectTest $ 'lhs === 'something_else)
+    ]
+
+main :: IO ()
+main = do
+    mapM_ printResult results
+    if map isSuccess results == [True, False]
+    then exitSuccess
+    else exitFailure
diff --git a/inspection-testing.cabal b/inspection-testing.cabal
--- a/inspection-testing.cabal
+++ b/inspection-testing.cabal
@@ -1,5 +1,5 @@
 name:                inspection-testing
-version:             0.1.2
+version:             0.2
 synopsis:            GHC plugin to do inspection testing
 description:         Some carefully crafted libraries make promises to their
                      users beyond functionality and performance.
@@ -72,6 +72,14 @@
   build-depends:       base >=4.9 && <4.12
   default-language:    Haskell2010
   ghc-options:         -main-is Simple
+
+test-suite simple-test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      examples
+  main-is:             SimpleTest.hs
+  build-depends:       inspection-testing
+  build-depends:       base >=4.9 && <4.12
+  default-language:    Haskell2010
 
 test-suite fusion
   type:                exitcode-stdio-1.0