diff --git a/refinery.cabal b/refinery.cabal
--- a/refinery.cabal
+++ b/refinery.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 47bfe1a8a6266a80890a145e94605cb2fc4b85749382b27f0f5ed1db65241473
+-- hash: c5e5c657da3ec1e29d787f8c9eb17e054b2e5ad3a9e6420df6680e4cb31ca981
 
 name:           refinery
-version:        0.2.0.0
+version:        0.3.0.0
 synopsis:       Toolkit for building proof automation systems
 description:    Please see the README on GitHub at <https://github.com/githubuser/refinery#readme>
 category:       Language
diff --git a/src/Refinery/ProofState.hs b/src/Refinery/ProofState.hs
--- a/src/Refinery/ProofState.hs
+++ b/src/Refinery/ProofState.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wno-name-shadowing #-}
 
 {-# LANGUAGE TupleSections          #-}
@@ -34,6 +35,7 @@
 import           Control.Monad.Logic
 import           Control.Monad.Morph
 import           Control.Monad.Reader
+import           Data.Either
 
 import           GHC.Generics
 
@@ -43,6 +45,7 @@
     | Stateful (s -> (s, ProofStateT ext' ext err s m goal))
     | Alt (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)
     | Interleave (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)
+    | Commit (ProofStateT ext' ext err s m goal) (ProofStateT ext' ext err s m goal)
     | Empty
     | Failure err
     | Axiom ext
@@ -54,6 +57,7 @@
   show (Stateful _) = "(Stateful <s>)"
   show (Alt p1 p2) = "(Alt " <> show p1 <> " " <> show p2 <> ")"
   show (Interleave p1 p2) = "(Interleave " <> show p1 <> " " <> show p2 <> ")"
+  show (Commit p1 p2) = "(Commit " <> show p1 <> " " <> show p2 <> ")"
   show Empty = "Empty"
   show (Failure err) = "(Failure " <> show err <> ")"
   show (Axiom ext) = "(Axiom " <> show ext <> ")"
@@ -64,6 +68,7 @@
     fmap f (Stateful s) = Stateful $ fmap (fmap f) . s
     fmap f (Alt p1 p2) = Alt (fmap f p1) (fmap f p2)
     fmap f (Interleave p1 p2) = Interleave (fmap f p1) (fmap f p2)
+    fmap f (Commit p1 p2) = Commit (fmap f p1) (fmap f p2)
     fmap _ Empty = Empty
     fmap _ (Failure err) = Failure err
     fmap _ (Axiom ext) = Axiom ext
@@ -78,20 +83,22 @@
   hoist nat (Stateful f)    = Stateful $ fmap (hoist nat) . f
   hoist nat (Alt p1 p2)   = Alt (hoist nat p1) (hoist nat p2)
   hoist nat (Interleave p1 p2)   = Interleave (hoist nat p1) (hoist nat p2)
+  hoist nat (Commit p1 p2)   = Commit (hoist nat p1) (hoist nat p2)
   hoist _ (Failure err) = Failure err
   hoist _ Empty         = Empty
   hoist _ (Axiom ext)   = Axiom ext
 
 applyCont
     :: (Functor m)
-    => (ext -> ProofStateT ext ext err s m a)
-    -> ProofStateT ext ext err s m a
-    -> ProofStateT ext ext err s m a
+    => (ext -> ProofStateT ext' ext err s m a)
+    -> ProofStateT ext' ext err s m a
+    -> ProofStateT ext' ext err s m a
 applyCont k (Subgoal goal k') = Subgoal goal (applyCont k . k')
 applyCont k (Effect m) = Effect (fmap (applyCont k) m)
 applyCont k (Stateful s) = Stateful $ fmap (applyCont k) . s
 applyCont k (Alt p1 p2) = Alt (applyCont k p1) (applyCont k p2)
 applyCont k (Interleave p1 p2) = Interleave (applyCont k p1) (applyCont k p2)
+applyCont k (Commit p1 p2) = Commit (applyCont k p1) (applyCont k p2)
 applyCont _ Empty = Empty
 applyCont _ (Failure err) = (Failure err)
 applyCont k (Axiom ext) = k ext
@@ -103,6 +110,7 @@
     (Stateful s)  >>= f = Stateful $ fmap (>>= f) . s
     (Alt p1 p2)   >>= f = Alt (p1 >>= f) (p2 >>= f)
     (Interleave p1 p2)   >>= f = Interleave (p1 >>= f) (p2 >>= f)
+    (Commit p1 p2)   >>= f = Commit (p1 >>= f) (p2 >>= f)
     (Failure err) >>= _ = Failure err
     Empty         >>= _ = Empty
     (Axiom ext)   >>= _ = Axiom ext
@@ -131,7 +139,7 @@
 instance (MonadExtract ext m, Monoid w) => MonadExtract ext (SW.WriterT w m)
 instance (MonadExtract ext m) => MonadExtract ext (ExceptT err m)
 
-proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, [goal])]
+proofs :: forall ext err s m goal. (MonadExtract ext m) => s -> ProofStateT ext ext err s m goal -> m [Either err (ext, s, [goal])]
 proofs s p = go s [] p
     where
       go s goals (Subgoal goal k) = do
@@ -143,9 +151,12 @@
           in go s' goals p
       go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2)
       go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2)
+      go s goals (Commit p1 p2) = go s goals p1 >>= \case
+          (rights -> []) -> go s goals p2
+          solns -> pure solns
       go _ _ Empty = pure []
       go _ _ (Failure err) = pure [throwError err]
-      go _ goals (Axiom ext) = pure [Right (ext, goals)]
+      go s goals (Axiom ext) = pure [Right (ext, s, goals)]
 
 accumEither :: (Semigroup a, Semigroup b) => Either a b -> Either a b -> Either a b
 accumEither (Left a1) (Left a2)   = Left (a1 <> a2)
@@ -165,6 +176,7 @@
     catch (Stateful s) handle = Stateful (fmap (flip catch handle) . s)
     catch (Alt p1 p2) handle = Alt (catch p1 handle) (catch p2 handle)
     catch (Interleave p1 p2) handle = Interleave (catch p1 handle) (catch p2 handle)
+    catch (Commit p1 p2) handle = Commit (catch p1 handle) (catch p2 handle)
     catch Empty _ = Empty
     catch (Failure err) _ = Failure err
     catch (Axiom e) _ = (Axiom e)
@@ -175,7 +187,8 @@
     catchError (Effect m) handle = Effect (fmap (flip catchError handle) m)
     catchError (Stateful s) handle = Stateful $ fmap (flip catchError handle) . s
     catchError (Alt p1 p2) handle = catchError p1 handle <|> catchError p2 handle
-    catchError (Interleave p1 p2) handle = catchError p1 handle <|> catchError p2 handle
+    catchError (Interleave p1 p2) handle = Interleave (catchError p1 handle) (catchError p2 handle)
+    catchError (Commit p1 p2) handle = catchError p1 handle <|> catchError p2 handle
     catchError Empty _ = Empty
     catchError (Failure err) handle = handle err
     catchError (Axiom e) _ = (Axiom e)
@@ -187,6 +200,7 @@
     local f (Stateful s) = Stateful (fmap (local f) . s)
     local f (Alt p1 p2) = Alt (local f p1) (local f p2)
     local f (Interleave p1 p2) = Interleave (local f p1) (local f p2)
+    local f (Commit p1 p2) = Commit (local f p1) (local f p2)
     local _ Empty = Empty
     local _ (Failure err) = (Failure err)
     local _ (Axiom e) = (Axiom e)
@@ -206,6 +220,7 @@
 subgoals fs (Stateful s) = Stateful (fmap (subgoals fs) . s)
 subgoals fs (Alt p1 p2) = Alt (subgoals fs p1) (subgoals fs p2)
 subgoals fs (Interleave p1 p2) = Interleave (subgoals fs p1) (subgoals fs p2)
+subgoals fs (Commit p1 p2) = Commit (subgoals fs p1) (subgoals fs p2)
 subgoals _ (Failure err) = Failure err
 subgoals _ Empty = Empty
 subgoals _ (Axiom ext) = Axiom ext
@@ -217,6 +232,7 @@
     Stateful s -> Stateful (fmap (mapExtract into out) . s)
     Alt t1 t2 -> Alt (mapExtract into out t1) (mapExtract into out t2)
     Interleave t1 t2 -> Interleave (mapExtract into out t1) (mapExtract into out t2)
+    Commit t1 t2 -> Commit (mapExtract into out t1) (mapExtract into out t2)
     Empty -> Empty
     Failure err -> Failure err
     Axiom ext -> Axiom $ into ext
@@ -228,7 +244,7 @@
     Stateful s -> Stateful (fmap (mapExtract' into) . s)
     Alt t1 t2 -> Alt (mapExtract' into t1) (mapExtract' into t2)
     Interleave t1 t2 -> Interleave (mapExtract' into t1) (mapExtract' into t2)
+    Commit t1 t2 -> Commit (mapExtract' into t1) (mapExtract' into t2)
     Empty -> Empty
     Failure err -> Failure err
     Axiom ext -> Axiom $ into ext
-
diff --git a/src/Refinery/Tactic.hs b/src/Refinery/Tactic.hs
--- a/src/Refinery/Tactic.hs
+++ b/src/Refinery/Tactic.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 -----------------------------------------------------------------------------
@@ -20,11 +21,14 @@
   -- * Tactic Combinators
   , (<@>)
   , (<%>)
+  , commit
   , try
   , many_
   , choice
   , progress
-  , MonadLogic(..)
+  , gather
+  , pruning
+  , ensure
   -- * Subgoal Manipulation
   , goal
   , focus
@@ -38,24 +42,29 @@
 import Control.Applicative
 import Control.Monad.Except
 import Control.Monad.State.Strict
-import Control.Monad.Logic
 
 import Refinery.ProofState
 import Refinery.Tactic.Internal
 
--- -- | Create a tactic that applies each of the tactics in the list to one subgoal.
--- --
--- -- When the number of subgoals is greater than the number of provided tactics,
--- -- the identity tactic is applied to the remainder. When the number of subgoals is
--- -- less than the number of provided tactics, the remaining tactics are ignored.
+-- | Create a tactic that applies each of the tactics in the list to one subgoal.
+--
+-- When the number of subgoals is greater than the number of provided tactics,
+-- the identity tactic is applied to the remainder. When the number of subgoals is
+-- less than the number of provided tactics, the remaining tactics are ignored.
 (<@>) :: (Functor m) => TacticT jdg ext err s m a -> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
 t <@> ts = tactic $ \j -> subgoals (fmap (\t' (_,j') -> proofState t' j') ts) (proofState t j)
 
 infixr 3 <%>
 
+-- | @t1 <%> t2@ will interleave the execution of @t1@ and @t2@. This is useful if @t1@ will
+-- produce an infinite number of extracts, as we will still run @t2@. This is contrasted with
+-- @t1 <|> t2@, which will not ever consider @t2@ if @t1@ produces an infinite number of extracts.
 (<%>) :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
 t1 <%> t2 = tactic $ \j -> Interleave (proofState t1 j) (proofState t2 j)
 
+-- | @commit t1 t2@ will run @t1@, and then only run @t2@ if @t1@ failed to produce any extracts.
+commit :: TacticT jdg ext err s m a -> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
+commit t1 t2 = tactic $ \j -> Commit (proofState t1 j) (proofState t2 j)
 
 -- | Tries to run a tactic, backtracking on failure
 try :: (Monad m) => TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
@@ -69,13 +78,15 @@
 goal :: (Functor m) => TacticT jdg ext err s m jdg
 goal = TacticT $ get
 
+-- | @choice ts@ will run all of the tactics in the list against the current subgoals,
+-- and interleave their extracts in a manner similar to '<%>'.
 choice :: (Monad m) => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
 choice [] = empty
 choice (t:ts) = t <%> choice ts
 
--- -- | @progress eq err t@ applies the tactic @t@, and checks to see if the
--- -- resulting subgoals are all equal to the initial goal by using @eq@. If they
--- -- are, it throws @err@.
+-- | @progress eq err t@ applies the tactic @t@, and checks to see if the
+-- resulting subgoals are all equal to the initial goal by using @eq@. If they
+-- are, it throws @err@.
 progress :: (Monad m) => (jdg -> jdg -> Bool) -> err ->  TacticT jdg ext err s m a -> TacticT jdg ext err s m a
 progress eq err t = do
   j <- goal
@@ -83,12 +94,46 @@
   j' <- goal
   if j `eq` j' then pure a else throwError err
 
--- -- | Apply the first tactic, and then apply the second tactic focused on the @n@th subgoal.
+-- | @gather t f@ runs the tactic @t@, then runs @f@ with all of the generated subgoals to determine
+-- the next tactic to run.
+gather :: (MonadExtract ext m) => TacticT jdg ext err s m a -> ([(a, jdg)] -> TacticT jdg ext err s m a) -> TacticT jdg ext err s m a
+gather t f = tactic $ \j -> do
+    s <- get
+    results <- lift $ proofs s $ proofState t j
+    msum $ flip fmap results $ \case
+        Left err -> throwError err
+        Right (_, _, jdgs) -> proofState (f jdgs) j
+
+-- | @pruning t f@ runs the tactic @t@, and then applies a predicate to all of the generated subgoals.
+pruning
+    :: (MonadExtract ext m)
+    => TacticT jdg ext err s m ()
+    -> ([jdg] -> Maybe err)
+    -> TacticT jdg ext err s m ()
+pruning t p = gather t $ maybe t throwError . p . fmap snd
+
+-- | @filterT p f t@ runs the tactic @t@, and applies a predicate to the state after the execution of @t@. We also run
+-- a "cleanup" function @f@. Note that the predicate is applied to the state _before_ the cleanup function is run.
+ensure :: (Monad m) => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
+ensure p f t = check >> t
+    where
+      -- NOTE It may seem backwards to run check _before_ t, but we
+      -- need to do the predicate check after the subgoal has been resolved,
+      -- and not on every generated subgoal.
+      check = rule $ \j -> do
+          e <- subgoal j
+          s <- get
+          modify f
+          case p s of
+            Just err -> throwError err
+            Nothing -> pure e
+
+-- | Apply the first tactic, and then apply the second tactic focused on the @n@th subgoal.
 focus :: (Functor m) => TacticT jdg ext err s m () -> Int -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
 focus t n t' = t <@> (replicate n (pure ()) ++ [t'] ++ repeat (pure ()))
 
 -- | Runs a tactic, producing a list of possible extracts, along with a list of unsolved subgoals.
-runTacticT :: (MonadExtract ext m) => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, [jdg])]
+runTacticT :: (MonadExtract ext m) => TacticT jdg ext err s m () -> jdg -> s -> m [Either err (ext, s, [jdg])]
 runTacticT t j s = proofs s $ fmap snd $ proofState t j
 
 -- | Turn an inference rule into a tactic.
diff --git a/src/Refinery/Tactic/Internal.hs b/src/Refinery/Tactic/Internal.hs
--- a/src/Refinery/Tactic/Internal.hs
+++ b/src/Refinery/Tactic/Internal.hs
@@ -86,9 +86,13 @@
 mapTacticT :: (Monad m) => (m a -> m b) -> TacticT jdg ext err s m a -> TacticT jdg ext err s m b
 mapTacticT f (TacticT m) = TacticT $ m >>= (lift . lift . f . return)
 
+instance MFunctor (TacticT jdg ext err s) where
+  hoist f = TacticT . (hoist (hoist f)) . unTacticT
+
 instance MonadTrans (TacticT jdg ext err s) where
   lift m = TacticT $ lift $ lift m
 
+
 instance (Monad m) => MonadState s (TacticT jdg ext err s m) where
     state f = tactic $ \j -> fmap (,j) $ state f
 
@@ -115,6 +119,7 @@
   RuleT (Stateful s)       >>= f = coerce $ Stateful $ fmap (bindAlaCoerce f) . s
   RuleT (Alt p1 p2)        >>= f = coerce $ Alt (bindAlaCoerce f p1) (bindAlaCoerce f p2)
   RuleT (Interleave p1 p2) >>= f = coerce $ Interleave (bindAlaCoerce f p1) (bindAlaCoerce f p2)
+  RuleT (Commit p1 p2) >>= f = coerce $ Commit (bindAlaCoerce f p1) (bindAlaCoerce f p2)
   RuleT Empty              >>= _ = coerce $ Empty
   RuleT (Failure err)      >>= _ = coerce $ Failure err
   RuleT (Axiom e)          >>= f = f e
@@ -131,6 +136,7 @@
     local f (RuleT (Stateful s))       = coerce $ Stateful (fmap (localAlaCoerce f) . s)
     local f (RuleT (Alt p1 p2))        = coerce $ Alt (localAlaCoerce f p1) (localAlaCoerce f p2)
     local f (RuleT (Interleave p1 p2)) = coerce $ Interleave (localAlaCoerce f p1) (localAlaCoerce f p2)
+    local f (RuleT (Commit p1 p2)) = coerce $ Commit (localAlaCoerce f p1) (localAlaCoerce f p2)
     local _ (RuleT Empty)              = coerce $ Empty
     local _ (RuleT (Failure err))      = coerce $ Failure err
     local _ (RuleT (Axiom e))          = coerce $ Axiom e
diff --git a/test/Checkers.hs b/test/Checkers.hs
--- a/test/Checkers.hs
+++ b/test/Checkers.hs
@@ -34,7 +34,7 @@
         s <- arbitrary
         pure $
           counterexample (show s) $
-            (put s >> get) =-= pure @m s
+            (put s >> get) =-= (put s >> pure @m s)
       )
     ]
   )
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -16,6 +16,7 @@
 import Control.Monad
 import Control.Monad.State.Strict (StateT (..))
 import Control.Monad.State.Class
+import Control.Monad.Error.Class
 import Data.Function
 import Data.Functor.Identity
 import Data.Monoid (Sum (..))
@@ -33,7 +34,7 @@
   foldr (>>) (return ()) (map (uncurry it) tests)
 
 
-instance (MonadExtract ext m, EqProp (m [Either err (ext, [a])]), Arbitrary s)
+instance (MonadExtract ext m, EqProp (m [Either err (ext, s, [a])]), Arbitrary s)
       => EqProp (ProofStateT ext ext err s m a) where
   (=-=) a b = property $ do
     s <- arbitrary
@@ -42,7 +43,7 @@
 instance ( Show jdg
          , MonadExtract ext m
          , Arbitrary jdg
-         , EqProp (m [Either err (ext, [jdg])])
+         , EqProp (m [Either err (ext, s, [jdg])])
          , Show s
          , Arbitrary s
          )
@@ -51,7 +52,7 @@
 
 instance ( Show jdg
          , Arbitrary jdg
-         , EqProp (m [Either err (ext, [jdg])])
+         , EqProp (m [Either err (ext, s, [jdg])])
          , MonadExtract ext m
          , Show s
          , Arbitrary s
@@ -147,6 +148,9 @@
     it "interleave - mzero" $ property $ interleaveMZero (undefined :: TacticTest Int)
     it "interleave - mplus" $ property $ interleaveMPlus (undefined :: TacticTest Int)
     it "distrib put over <|>" $ property $ distribPut (undefined :: TacticTest ())
+    it "pure absorption on commit" $ property $ absorptionPureCommit (undefined :: TacticTest Int)
+    it "empty identity on commit" $ property $ emptyIdentityCommit (undefined :: TacticTest Int)
+    it "failure identity on commit" $ property $ emptyIdentityCommit (undefined :: TacticTest Int)
 
 leftAltBind
     :: forall m a b
@@ -166,7 +170,7 @@
 
 interleaveMZero
     :: forall m a jdg ext err s
-     . (MonadExtract ext m, EqProp (m [Either err (ext, [jdg])]),
+     . (MonadExtract ext m, EqProp (m [Either err (ext, s, [jdg])]),
       Show jdg, Show s, Arbitrary jdg, Arbitrary s)
     => TacticT jdg ext err s m a  -- ^ proxy
     -> TacticT jdg ext err s m a
@@ -176,7 +180,7 @@
 
 interleaveMPlus
     :: forall m a jdg ext err s
-     . (MonadExtract ext m, EqProp (m [Either err (ext, [jdg])]),
+     . (MonadExtract ext m, EqProp (m [Either err (ext, s, [jdg])]),
       Show jdg, Show s, Arbitrary jdg, Arbitrary s)
     => TacticT jdg ext err s m a  -- ^ proxy
     -> a
@@ -207,3 +211,34 @@
     counterexample (show m2) $
       (put s >> (m1 <|> m2)) =-= ((put s >> m1) <|> (put s >> m2))
 
+absorptionPureCommit
+    :: forall m a jdg ext err s
+     . (MonadExtract ext m, EqProp (m [Either err (ext, s, [jdg])]),
+      Show jdg, Show s, Arbitrary jdg, Arbitrary s)
+    => TacticT jdg ext err s m a  -- ^ proxy
+    -> a
+    -> TacticT jdg ext err s m a
+    -> Property
+absorptionPureCommit _ a t =
+    (commit (pure a) t) =-= pure a
+
+emptyIdentityCommit
+    :: forall m a jdg ext err s
+     . (MonadExtract ext m, EqProp (m [Either err (ext, s, [jdg])]),
+      Show jdg, Show s, Arbitrary jdg, Arbitrary s)
+    => TacticT jdg ext err s m a  -- ^ proxy
+    -> TacticT jdg ext err s m a
+    -> Property
+emptyIdentityCommit _ t =
+    (commit empty t) =-= t
+
+failureIdentityCommit
+    :: forall m a jdg ext err s
+     . (MonadExtract ext m, EqProp (m [Either err (ext, s, [jdg])]),
+      Show jdg, Show s, Arbitrary jdg, Arbitrary s)
+    => TacticT jdg ext err s m a  -- ^ proxy
+    -> err
+    -> TacticT jdg ext err s m a
+    -> Property
+failureIdentityCommit _ e t =
+    (commit (throwError e) t) =-= t