diff --git a/plutus-core/executables/pir/Main.hs b/plutus-core/executables/pir/Main.hs
index f6591417865..bfdf2b19dcc 100644
--- a/plutus-core/executables/pir/Main.hs
+++ b/plutus-core/executables/pir/Main.hs
@@ -196,7 +196,7 @@ doOptimisations :: PirTerm PLC.SrcSpan -> Either (PirError UnitProvenance) (PirT
 doOptimisations term = do
   plcTcConfig <- PLC.getDefTypeCheckConfig PIR.noProvenance
   let ctx = getCtx plcTcConfig
-  runExcept $ flip runReaderT ctx $ runQuoteT $ PIR.simplifyTerm =<< PLC.rename (PIR.Original () <$ term)
+  runExcept $ flip runReaderT ctx $ runQuoteT $ PIR.runCompilerPass PIR.simplifier (PIR.Original () <$ term)
   where
     getCtx
         :: PLC.TypeCheckConfig PLC.DefaultUni PLC.DefaultFun
diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal
index 02a96a472c7..351baaf646d 100644
--- a/plutus-core/plutus-core.cabal
+++ b/plutus-core/plutus-core.cabal
@@ -501,6 +501,7 @@ library plutus-ir
     PlutusIR.Mark
     PlutusIR.MkPir
     PlutusIR.Parser
+    PlutusIR.Pass
     PlutusIR.Purity
     PlutusIR.Subst
     PlutusIR.Transform.Beta
@@ -537,6 +538,7 @@ library plutus-ir
     PlutusIR.Compiler.Recursion
     PlutusIR.Normalize
     PlutusIR.Transform.RewriteRules.Common
+    PlutusIR.Transform.RewriteRules.Rules
     PlutusIR.Transform.RewriteRules.UnConstrConstrData
 
   build-depends:
@@ -712,7 +714,7 @@ library plutus-core-testlib
     PlutusIR.Generators.QuickCheck.Common
     PlutusIR.Generators.QuickCheck.GenerateTerms
     PlutusIR.Generators.QuickCheck.ShrinkTerms
-    PlutusIR.Properties.Typecheck
+    PlutusIR.Pass.Test
     PlutusIR.Test
     Test.Tasty.Extras
     UntypedPlutusCore.Test.DeBruijn.Bad
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Compiler.hs b/plutus-core/plutus-ir/src/PlutusIR/Compiler.hs
index 5b6ff93e759..fe72fa03868 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Compiler.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Compiler.hs
@@ -18,6 +18,7 @@ module PlutusIR.Compiler (
     noProvenance,
     CompilationOpts (..),
     coOptimize,
+    coTypecheck,
     coPedantic,
     coVerbose,
     coDebug,
@@ -47,16 +48,26 @@ module PlutusIR.Compiler (
     PirTCConfig(..),
     AllowEscape(..),
     toDefaultCompilationCtx,
-    simplifyTerm
+    runCompilerPass,
+    simplifier
     ) where
 
+import Control.Lens
+import Control.Monad
+import Control.Monad.Except
+import Control.Monad.Extra (orM, whenM)
+import Data.Monoid
+import Data.Monoid.Extra (mwhen)
+import Debug.Trace (traceM)
+import PlutusCore qualified as PLC
+import PlutusCore.Error (throwingEither)
 import PlutusIR
-
 import PlutusIR.Compiler.Let qualified as Let
 import PlutusIR.Compiler.Lower
 import PlutusIR.Compiler.Provenance
 import PlutusIR.Compiler.Types
 import PlutusIR.Error
+import PlutusIR.Pass qualified as P
 import PlutusIR.Transform.Beta qualified as Beta
 import PlutusIR.Transform.CaseOfCase qualified as CaseOfCase
 import PlutusIR.Transform.CaseReduce qualified as CaseReduce
@@ -74,28 +85,8 @@ import PlutusIR.Transform.RewriteRules qualified as RewriteRules
 import PlutusIR.Transform.StrictifyBindings qualified as StrictifyBindings
 import PlutusIR.Transform.ThunkRecursions qualified as ThunkRec
 import PlutusIR.Transform.Unwrap qualified as Unwrap
-import PlutusIR.TypeCheck.Internal
-
-import PlutusCore qualified as PLC
-
-import Control.Lens
-import Control.Monad
-import Control.Monad.Extra (orM, whenM)
-import Control.Monad.Reader
-import Debug.Trace (traceM)
-import PlutusIR.Analysis.Builtins
 import PlutusPrelude
 
--- Simplifier passes
-data Pass uni fun =
-  Pass { _name      :: String
-       , _shouldRun :: forall m e a. Compiling m e uni fun a => m Bool
-       , _pass      :: forall m e a. Compiling m e uni fun a => Term TyName Name uni fun (Provenance a) -> m (Term TyName Name uni fun (Provenance a))
-       }
-
-onOption :: Compiling m e uni fun a => Lens' (CompilationOpts a) Bool -> m Bool
-onOption coOpt = view (ccOpts . coOpt)
-
 isVerbose :: Compiling m e uni fun a => m Bool
 isVerbose = view $ ccOpts . coVerbose
 
@@ -108,189 +99,131 @@ logVerbose = whenM (orM [isVerbose, isDebug]) . traceM
 logDebug :: Compiling m e uni fun a => String -> m ()
 logDebug = whenM isDebug . traceM
 
-applyPass :: (Compiling m e uni fun a, b ~ Provenance a) => Pass uni fun -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
-applyPass pass = runIf (_shouldRun pass) $ through check <=< \term -> do
-  let passName = _name pass
-  logVerbose $ "      !!! " ++ passName
-  logDebug   $ "        !!! Before " ++ passName ++ "\n" ++ show (pretty term)
-  term' <- _pass pass term
-  logDebug   $ "        !!! After " ++ passName ++ "\n" ++ show (pretty term')
-  pure term'
-
-availablePasses :: [Pass uni fun]
-availablePasses =
-    [ Pass "unwrap cancel"        (onOption coDoSimplifierUnwrapCancel)       (pure . Unwrap.unwrapCancel)
-    , Pass "case reduce"          (onOption coDoSimplifierCaseReduce)         (pure . CaseReduce.caseReduce)
-    , Pass "case of case"         (onOption coDoSimplifierCaseOfCase)         (\t -> do
-                                                                                  binfo <- view ccBuiltinsInfo
-                                                                                  conservative <- view (ccOpts . coCaseOfCaseConservative)
-                                                                                  CaseOfCase.caseOfCase binfo conservative noProvenance t)
-    , Pass "known constructor"    (onOption coDoSimplifierKnownCon)           KnownCon.knownCon
-    , Pass "beta"                 (onOption coDoSimplifierBeta)               (pure . Beta.beta)
-    , Pass "strictify bindings"   (onOption coDoSimplifierStrictifyBindings)  (\t -> do
-                                                                                  binfo <- view ccBuiltinsInfo
-                                                                                  pure $ StrictifyBindings.strictifyBindings binfo t
-                                                                              )
-    , Pass "evaluate builtins"    (onOption coDoSimplifierEvaluateBuiltins)   (\t -> do
-                                                                                  binfo <- view ccBuiltinsInfo
-                                                                                  costModel <- view ccBuiltinCostModel
-                                                                                  preserveLogging <- view (ccOpts . coPreserveLogging)
-                                                                                  pure $ EvaluateBuiltins.evaluateBuiltins preserveLogging binfo costModel t
-                                                                              )
-    , Pass "inline"               (onOption coDoSimplifierInline)             (\t -> do
-                                                                                  hints <- view (ccOpts . coInlineHints)
-                                                                                  binfo <- view ccBuiltinsInfo
-                                                                                  Inline.inline hints binfo t
-                                                                              )
-    , Pass "rewrite rules" (onOption coDoSimplifierRewrite) (\ t -> do
-                                                                    rules <- view ccRewriteRules
-                                                                    RewriteRules.rewriteWith rules t)
-    ]
-
--- | Actual simplifier
-simplify
-    :: forall m e uni fun a b. (Compiling m e uni fun a, b ~ Provenance a)
-    => Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
-simplify = foldl' (>=>) pure (map applyPass availablePasses)
-
--- | Perform some simplification of a 'Term'.
---
--- NOTE: simplifyTerm requires at least 1 prior dead code elimination pass
-simplifyTerm
-  :: forall m e uni fun a b. (Compiling m e uni fun a, b ~ Provenance a)
-  => Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
-simplifyTerm = runIfOpts simplify'
-    where
-        simplify' :: Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
-        simplify' t = do
-            maxIterations <- view (ccOpts . coMaxSimplifierIterations)
-            simplifyNTimes maxIterations t
-        -- Run the simplifier @n@ times
-        simplifyNTimes :: Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
-        simplifyNTimes n = foldl' (>=>) pure (map simplifyStep [1 .. n])
-        -- generate simplification step
-        simplifyStep :: Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
-        simplifyStep i term = do
-          logVerbose $ "    !!! simplifier pass " ++ show i
-          simplify term
-
-
--- | Perform floating out/merging of lets in a 'Term' to their
--- nearest lambda/Lambda/letStrictNonValue.
--- Note: It assumes globally unique names
-floatOut
-    :: (Compiling m e uni fun a, Semigroup b)
-    => Term TyName Name uni fun b
-    -> m (Term TyName Name uni fun b)
-floatOut t = do
-    binfo <- view ccBuiltinsInfo
-    runIfOpts (pure . LetMerge.letMerge . RecSplit.recSplit . LetFloatOut.floatTerm binfo) t
-
--- | Perform floating in/merging of lets in a 'Term'.
-floatIn
-    :: Compiling m e uni fun a
-    => Term TyName Name uni fun b
-    -> m (Term TyName Name uni fun b)
-floatIn t = do
-    binfo <- view ccBuiltinsInfo
-    relaxed <- view (ccOpts . coRelaxedFloatin)
-    runIfOpts (fmap LetMerge.letMerge . LetFloatIn.floatTerm binfo relaxed) t
+runCompilerPass :: (Compiling m e uni fun a, b ~ Provenance a) => m (P.Pass m tyname name uni fun b) -> Term tyname name uni fun b -> m (Term tyname name uni fun b)
+runCompilerPass mpasses t = do
+  passes <- mpasses
+  pedantic <- view (ccOpts . coPedantic)
+  res <- runExceptT $ P.runPass logVerbose pedantic passes t
+  throwingEither _Error res
+
+floatOutPasses :: Compiling m e uni fun a => m (P.Pass m TyName Name uni fun (Provenance a))
+floatOutPasses = do
+  optimize <- view (ccOpts . coOptimize)
+  tcconfig <- view ccTypeCheckConfig
+  binfo <- view ccBuiltinsInfo
+  pure $ mwhen optimize $ P.NamedPass "float-out" $ fold
+        [ LetFloatOut.floatTermPassSC tcconfig binfo
+        , RecSplit.recSplitPass tcconfig
+        , LetMerge.letMergePass tcconfig
+        ]
+
+floatInPasses :: Compiling m e uni fun a => m (P.Pass m TyName Name uni fun (Provenance a))
+floatInPasses = do
+  optimize <- view (ccOpts . coOptimize)
+  tcconfig <- view ccTypeCheckConfig
+  binfo <- view ccBuiltinsInfo
+  relaxed <- view (ccOpts . coRelaxedFloatin)
+  pure $ mwhen optimize $ P.NamedPass "float-in" $ fold
+        [ LetFloatIn.floatTermPassSC tcconfig binfo relaxed
+        , LetMerge.letMergePass tcconfig
+        ]
+
+simplifierIteration :: Compiling m e uni fun a => String -> m (P.Pass m TyName Name uni fun (Provenance a))
+simplifierIteration suffix = do
+  opts <- view ccOpts
+  tcconfig <- view ccTypeCheckConfig
+  binfo <- view ccBuiltinsInfo
+  costModel <- view ccBuiltinCostModel
+  hints <- view (ccOpts . coInlineHints)
+  preserveLogging <- view (ccOpts . coPreserveLogging)
+  cocConservative <- view (ccOpts . coCaseOfCaseConservative)
+  rules <- view ccRewriteRules
+
+  pure $ P.NamedPass ("simplifier" ++ suffix) $ fold
+      [ mwhen (opts ^. coDoSimplifierUnwrapCancel) $ Unwrap.unwrapCancelPass tcconfig
+      , mwhen (opts ^. coDoSimplifierCaseReduce) $ CaseReduce.caseReducePass tcconfig
+      , mwhen (opts ^. coDoSimplifierCaseReduce) $ CaseOfCase.caseOfCasePassSC tcconfig binfo cocConservative noProvenance
+      , mwhen (opts ^. coDoSimplifierKnownCon) $ KnownCon.knownConPassSC tcconfig
+      , mwhen (opts ^. coDoSimplifierBeta) $ Beta.betaPassSC tcconfig
+      , mwhen (opts ^. coDoSimplifierStrictifyBindings ) $ StrictifyBindings.strictifyBindingsPass tcconfig binfo
+      , mwhen (opts ^. coDoSimplifierEvaluateBuiltins) $ EvaluateBuiltins.evaluateBuiltinsPass tcconfig preserveLogging binfo costModel
+      , mwhen (opts ^. coDoSimplifierInline) $ Inline.inlinePassSC tcconfig hints binfo
+      , mwhen (opts ^. coDoSimplifierRewrite) $ RewriteRules.rewritePassSC tcconfig rules
+      ]
+
+
+simplifier :: Compiling m e uni fun a => m (P.Pass m TyName Name uni fun (Provenance a))
+simplifier = do
+  optimize <- view (ccOpts . coOptimize)
+  maxIterations <- view (ccOpts . coMaxSimplifierIterations)
+  passes <- for [1 .. maxIterations] $ \i -> simplifierIteration (" (pass " ++ show i ++ ")")
+  pure $ mwhen optimize $ P.NamedPass "simplifier" (fold passes)
 
 -- | Typecheck a PIR Term iff the context demands it.
--- Note: assumes globally unique names
-typeCheckTerm :: (Compiling m e uni fun a, b ~ Provenance a) => Term TyName Name uni fun b -> m ()
-typeCheckTerm t = do
-    mtcconfig <- asks _ccTypeCheckConfig
-    case mtcconfig of
-        Just tcconfig -> void . runTypeCheckM tcconfig $ inferTypeM t
-        Nothing       -> pure ()
-
-check :: Compiling m e uni fun b => Term TyName Name uni fun (Provenance b) -> m ()
-check arg =
-    whenM (view (ccOpts . coPedantic)) $
-         -- the typechecker requires global uniqueness, so rename here
-        typeCheckTerm =<< PLC.rename arg
-
-withBuiltinsInfo
-    :: MonadReader (CompilationCtx uni fun a) m
-    => (BuiltinsInfo uni fun -> m t)
-    -> m t
-withBuiltinsInfo = (view ccBuiltinsInfo >>=)
+typeCheckTerm :: (Compiling m e uni fun a) => m (P.Pass m TyName Name uni fun (Provenance a))
+typeCheckTerm = do
+  doTc <- view (ccOpts . coTypecheck)
+  tcconfig <- view ccTypeCheckConfig
+  pure $ mwhen doTc $ P.typecheckPass tcconfig
 
 -- | The 1st half of the PIR compiler pipeline up to floating/merging the lets.
 -- We stop momentarily here to give a chance to the tx-plugin
 -- to dump a "readable" version of pir (i.e. floated).
 compileToReadable
-  :: (Compiling m e uni fun a, b ~ Provenance a)
+  :: forall m e uni fun a b
+  . (Compiling m e uni fun a, b ~ Provenance a)
   => Program TyName Name uni fun b
   -> m (Program TyName Name uni fun b)
-compileToReadable (Program a v t) =
-  let pipeline =
-        -- We need globally unique names for typechecking, floating, and compiling non-strict bindings
-        (<$ logVerbose "  !!! rename")
-        >=> PLC.rename
-        >=> through typeCheckTerm
-        >=> (<$ logVerbose "  !!! removeDeadBindings")
-        >=> (withBuiltinsInfo . flip DeadCode.removeDeadBindings)
-        >=> (<$ logVerbose "  !!! simplifyTerm")
-        >=> simplifyTerm
-        >=> (<$ logVerbose "  !!! floatOut")
-        >=> floatOut
-        >=> through check
-  in validateOpts v >> Program a v <$> pipeline t
+compileToReadable (Program a v t) = do
+  validateOpts v
+  let
+    pipeline :: m (P.Pass m TyName Name uni fun b)
+    pipeline = getAp $ foldMap Ap
+        [ typeCheckTerm
+        , DeadCode.removeDeadBindingsPassSC <$> view ccTypeCheckConfig <*> view ccBuiltinsInfo
+        , simplifier
+        , floatOutPasses
+        ]
+  Program a v <$> runCompilerPass pipeline t
 
 -- | The 2nd half of the PIR compiler pipeline.
 -- Compiles a 'Term' into a PLC Term, by removing/translating step-by-step the PIR's language constructs to PLC.
 -- Note: the result *does* have globally unique names.
-compileReadableToPlc :: (Compiling m e uni fun a, b ~ Provenance a) => Program TyName Name uni fun b -> m (PLCProgram uni fun a)
-compileReadableToPlc (Program a v t) =
-  let pipeline =
-        (<$ logVerbose "  !!! floatIn")
-        >=> floatIn
-        >=> through check
-        >=> (<$ logVerbose "  !!! compileNonStrictBindings")
-        >=> NonStrict.compileNonStrictBindings False
-        >=> through check
-        >=> (<$ logVerbose "  !!! thunkRecursions")
-        >=> (withBuiltinsInfo . fmap pure . flip ThunkRec.thunkRecursions)
-        -- Thunking recursions breaks global uniqueness
-        >=> PLC.rename
-        >=> through check
+compileReadableToPlc :: forall m e uni fun a b . (Compiling m e uni fun a, b ~ Provenance a) => Program TyName Name uni fun b -> m (PLCProgram uni fun a)
+compileReadableToPlc (Program a v t) = do
+
+  let
+    pipeline :: m (P.Pass m TyName Name uni fun b)
+    pipeline = getAp $ foldMap Ap
+        [ floatInPasses
+        , NonStrict.compileNonStrictBindingsPassSC <$> view ccTypeCheckConfig <*> pure False
+        , ThunkRec.thunkRecursionsPass <$> view ccTypeCheckConfig <*> view ccBuiltinsInfo
         -- Process only the non-strict bindings created by 'thunkRecursions' with unit delay/forces
         -- See Note [Using unit versus force/delay]
-        >=> (<$ logVerbose "  !!! compileNonStrictBindings")
-        >=> NonStrict.compileNonStrictBindings True
-        >=> through check
-        >=> (<$ logVerbose "  !!! compileLets DataTypes")
-        >=> Let.compileLets Let.DataTypes
-        >=> through check
-        >=> (<$ logVerbose "  !!! compileLets RecTerms")
-        >=> Let.compileLets Let.RecTerms
-        >=> through check
+        , NonStrict.compileNonStrictBindingsPassSC <$> view ccTypeCheckConfig <*> pure True
+        , Let.compileLetsPassSC <$> view ccTypeCheckConfig <*> pure Let.DataTypes
+        , Let.compileLetsPassSC <$> view ccTypeCheckConfig <*> pure Let.RecTerms
         -- We introduce some non-recursive let bindings while eliminating recursive let-bindings, so we
         -- can eliminate any of them which are unused here.
-        >=> (<$ logVerbose "  !!! removeDeadBindings")
-        >=> (withBuiltinsInfo . flip DeadCode.removeDeadBindings)
-        >=> through check
-        >=> (<$ logVerbose "  !!! simplifyTerm")
-        >=> simplifyTerm
-        >=> through check
-        >=> (<$ logVerbose "  !!! compileLets Types")
-        >=> Let.compileLets Let.Types
-        >=> through check
-        >=> (<$ logVerbose "  !!! compileLets NonRecTerms")
-        >=> Let.compileLets Let.NonRecTerms
-        >=> through check
+        , DeadCode.removeDeadBindingsPassSC <$> view ccTypeCheckConfig <*> view ccBuiltinsInfo
+        , simplifier
+        , Let.compileLetsPassSC <$> view ccTypeCheckConfig <*> pure Let.Types
+        , Let.compileLetsPassSC <$> view ccTypeCheckConfig <*> pure Let.NonRecTerms
+        ]
+
+    go =
+        runCompilerPass pipeline
         >=> (<$ logVerbose "  !!! lowerTerm")
         >=> lowerTerm
-  in PLC.Program a v <$> pipeline t
+
+  PLC.Program a v <$> go t
 
 --- | Compile a 'Program' into a PLC Program. Note: the result *does* have globally unique names.
 compileProgram :: Compiling m e uni fun a
             => Program TyName Name uni fun a -> m (PLCProgram uni fun a)
 compileProgram =
   (pure . original)
-  >=> (<$ logVerbose "!!! compileToReadable")
+  >=> (<$ logDebug "!!! compileToReadable")
   >=> compileToReadable
-  >=> (<$ logVerbose "!!! compileReadableToPlc")
+  >=> (<$ logDebug "!!! compileReadableToPlc")
   >=> compileReadableToPlc
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Let.hs b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Let.hs
index 595ba164741..98145bc6772 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Let.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Let.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
 -- | Functions for compiling PIR let terms.
-module PlutusIR.Compiler.Let (compileLets, LetKind(..)) where
+module PlutusIR.Compiler.Let (compileLets, LetKind(..), compileLetsPass, compileLetsPassSC) where
 
 import PlutusIR
 import PlutusIR.Compiler.Datatype
@@ -24,6 +24,8 @@ import Data.Foldable
 import Data.List.NonEmpty hiding (partition, reverse)
 import Data.List.NonEmpty qualified as NE
 import PlutusCore.Pretty (display)
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
 {- Note [Extra definitions while compiling let-bindings]
 The let-compiling passes can generate some additional definitions, so we use the
@@ -37,6 +39,27 @@ Also we should pull out more stuff (e.g. see 'NonStrict' which uses unit).
 -}
 
 data LetKind = RecTerms | NonRecTerms | Types | DataTypes
+  deriving stock (Show, Eq, Ord)
+
+compileLetsPassSC
+  :: Compiling m e uni fun a
+  => TC.PirTCConfig uni fun
+  -> LetKind
+  -> Pass m TyName Name uni fun (Provenance a)
+compileLetsPassSC tcconfig letKind =
+    renamePass <> compileLetsPass tcconfig letKind
+
+compileLetsPass
+  :: Compiling m e uni fun a
+  => TC.PirTCConfig uni fun
+  -> LetKind
+  -> Pass m TyName Name uni fun (Provenance a)
+compileLetsPass tcconfig letKind =
+  NamedPass "compile lets" $
+    Pass
+      (compileLets letKind)
+      [Typechecks tcconfig, GloballyUniqueNames]
+      [ConstCondition (Typechecks tcconfig)]
 
 -- | Compile the let terms out of a 'Term'. Note: the result does *not* have globally unique names.
 compileLets :: Compiling m e uni fun a => LetKind -> PIRTerm uni fun a -> m (PIRTerm uni fun a)
@@ -63,7 +86,7 @@ compileRecBindings kind body bs =
     singleGroup :| [] ->
       case NE.head singleGroup of
          TermBind {} -> compileRecTermBindings kind body singleGroup
-         DatatypeBind {} ->  lift $ compileRecDataBindings kind body singleGroup
+         DatatypeBind {} -> lift $ compileRecDataBindings kind body singleGroup
          tb@TypeBind {} ->
             lift $ getEnclosing >>= \p -> throwing _Error $
                 CompilationError p
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
index 9054a9ed1c1..493aaaff67e 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs
@@ -27,7 +27,7 @@ import PlutusCore.Quote
 import PlutusCore.StdLib.Type qualified as Types
 import PlutusCore.TypeCheck.Internal qualified as PLC
 import PlutusCore.Version qualified as PLC
-import PlutusIR.Transform.RewriteRules
+import PlutusIR.Transform.RewriteRules.Rules
 import PlutusPrelude
 
 import Control.Monad.Error.Lens (throwing)
@@ -76,6 +76,7 @@ defaultDatatypeCompilationOpts = DatatypeCompilationOpts SumsOfProducts
 
 data CompilationOpts a = CompilationOpts {
     _coOptimize                        :: Bool
+    , _coTypecheck                     :: Bool
     , _coPedantic                      :: Bool
     , _coVerbose                       :: Bool
     , _coDebug                         :: Bool
@@ -105,6 +106,7 @@ makeLenses ''CompilationOpts
 defaultCompilationOpts :: CompilationOpts a
 defaultCompilationOpts = CompilationOpts
   { _coOptimize = True -- synonymous with max-simplifier-iterations=0
+  , _coTypecheck = True
   , _coPedantic = False
   , _coVerbose = False
   , _coDebug = False
@@ -130,7 +132,7 @@ data CompilationCtx uni fun a = CompilationCtx {
     _ccOpts               :: CompilationOpts a
     , _ccEnclosing        :: Provenance a
     -- | Decide to either typecheck (passing a specific tcconfig) or not by passing 'Nothing'.
-    , _ccTypeCheckConfig  :: Maybe (PirTCConfig uni fun)
+    , _ccTypeCheckConfig  :: PirTCConfig uni fun
     , _ccBuiltinsInfo     :: BuiltinsInfo uni fun
     , _ccBuiltinCostModel :: PLC.CostingPart uni fun
     , _ccRewriteRules     :: RewriteRules uni fun
@@ -145,7 +147,7 @@ toDefaultCompilationCtx
 toDefaultCompilationCtx configPlc = CompilationCtx
        { _ccOpts = defaultCompilationOpts
        , _ccEnclosing = noProvenance
-       , _ccTypeCheckConfig = Just $ PirTCConfig configPlc YesEscape
+       , _ccTypeCheckConfig = PirTCConfig configPlc YesEscape
        , _ccBuiltinsInfo = def
        , _ccBuiltinCostModel = def
        , _ccRewriteRules = def
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Error.hs b/plutus-core/plutus-ir/src/PlutusIR/Error.hs
index 577b2ccca42..80b1e997be5 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Error.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Error.hs
@@ -54,6 +54,9 @@ instance AsTypeErrorExt (Error uni fun a) uni a where
 instance PLC.AsFreeVariableError (Error uni fun a) where
     _FreeVariableError = _PLCError . PLC._FreeVariableError
 
+instance PLC.AsUniqueError (Error uni fun a) a where
+    _UniqueError = _PLCError . PLC._UniqueError
+
 -- Pretty-printing
 ------------------
 
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Pass.hs b/plutus-core/plutus-ir/src/PlutusIR/Pass.hs
new file mode 100644
index 00000000000..1b046163590
--- /dev/null
+++ b/plutus-core/plutus-ir/src/PlutusIR/Pass.hs
@@ -0,0 +1,153 @@
+{-# LANGUAGE GADTs      #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+
+module PlutusIR.Pass where
+
+import PlutusIR.Check.Uniques qualified as Uniques
+import PlutusIR.Core.Type
+import PlutusIR.Error
+import PlutusIR.TypeCheck qualified as TC
+
+import PlutusCore qualified as PLC
+import PlutusCore.Name
+
+import Control.Monad (when)
+import Control.Monad.Except
+import Control.Monad.Trans.Class (lift)
+import Data.Foldable
+import Data.Text (Text)
+import PlutusCore.Quote
+import PlutusPrelude
+
+-- | A condition on a 'Term'.
+data Condition tyname name uni fun a where
+  -- | The 'Term' typechecks.
+  Typechecks :: (PLC.Typecheckable uni fun, PLC.GEq uni)
+    => TC.PirTCConfig uni fun -> Condition TyName Name uni fun a
+  -- | The 'Term' has globally unique names.
+  GloballyUniqueNames :: (HasUnique tyname TypeUnique, HasUnique name TermUnique, Ord a)
+    => Condition tyname name uni fun a
+  -- | A custom condition. 'Nothing' indicates success, 'Just' indicates a failure at
+  -- a location with a message.
+  Custom :: (Term tyname name uni fun a -> Maybe (a, Text))
+    -> Condition tyname name uni fun a
+
+-- | A condition on a pair of 'Term's.
+data BiCondition tyname name uni fun a where
+  -- | A condition on the second 'Term'.
+  ConstCondition :: Condition tyname name uni fun a -> BiCondition tyname name uni fun a
+  -- | A custom condition. 'Nothing' indicates success, 'Just' indicates a failure at
+  -- a location with a message.
+  CustomBi :: (Term tyname name uni fun a -> Term tyname name uni fun a -> Maybe (a, Text))
+    -> BiCondition tyname name uni fun a
+
+checkCondition
+  :: MonadError (Error uni fun a) m
+  => Condition tyname name uni fun a
+  -> Term tyname name uni fun a
+  -> m ()
+checkCondition c t = case c of
+  Typechecks tcconfig -> void $ runQuoteT $ do
+    -- Typechecking requires globally unique names
+    renamed <- PLC.rename t
+    TC.inferType tcconfig renamed
+  GloballyUniqueNames -> void $ Uniques.checkTerm (const True) t
+  Custom f -> case f t of
+    Just (a, e) -> throwError $ CompilationError a e
+    Nothing     -> pure ()
+
+checkBiCondition
+  :: MonadError (Error uni fun a) m
+  => BiCondition tyname name uni fun a
+  -> Term tyname name uni fun a
+  -> Term tyname name uni fun a
+  -> m ()
+checkBiCondition c t1 t2 = case c of
+  ConstCondition c' -> checkCondition c' t2
+  CustomBi f -> case f t1 t2 of
+    Just (a, e) -> throwError $ CompilationError a e
+    Nothing     -> pure ()
+
+-- | A pass over a term, with pre- and post-conditions.
+data Pass m tyname name uni fun a =
+  -- | A basic pass. Has a function, which is the pass itself, a set of pre-conditions
+  -- which are run on the input term, and a set of post-conditions which are run on the
+  -- input and output terms (so can compare them).
+  Pass
+    (Term tyname name uni fun a -> m (Term tyname name uni fun a))
+    [Condition tyname name uni fun a]
+    [BiCondition tyname name uni fun a]
+  | CompoundPass (Pass m tyname name uni fun a) (Pass m tyname name uni fun a)
+  | NoOpPass
+  | NamedPass String (Pass m tyname name uni fun a)
+
+instance Semigroup (Pass m tyname name uni fun a) where
+  p1 <> p2 = CompoundPass p1 p2
+
+instance Monoid (Pass m tyname name uni fun a) where
+  mempty = NoOpPass
+
+hoistPass :: (forall v . m v -> n v) -> Pass m tyname name uni fun a -> Pass n tyname name uni fun a
+hoistPass f p = case p of
+  Pass mainPass pre post -> Pass (f . mainPass) pre post
+  CompoundPass p1 p2     -> CompoundPass (hoistPass f p1) (hoistPass f p2)
+  NamedPass n pass       -> NamedPass n (hoistPass f pass)
+  NoOpPass               -> NoOpPass
+
+runPass
+  :: Monad m
+  => (String -> m ())
+  -> Bool
+  -> Pass m tyname name uni fun a
+  -> Term tyname name uni fun a
+  -> ExceptT (Error uni fun a) m (Term tyname name uni fun a)
+runPass logger checkConditions (Pass mainPass pre post) t = do
+  when checkConditions $ do
+    lift $ logger "checking preconditions"
+    for_ pre $ \c -> checkCondition c t
+  t' <- lift $ mainPass t
+  when checkConditions $ do
+    lift $ logger "checking postconditions"
+    for_ post $ \c -> checkBiCondition c t t'
+  pure t'
+runPass logger checkConditions (CompoundPass p1 p2) t = do
+  t' <- runPass logger checkConditions p1 t
+  runPass logger checkConditions p2 t'
+runPass logger checkConditions (NamedPass n pass) t = do
+  lift $ logger $ n ++ ": running pass"
+  t' <- runPass logger checkConditions pass t
+  lift $ logger $ n ++ ": finished pass"
+  pure t'
+runPass _ _ NoOpPass t = pure t
+
+-- | A simple, non-monadic pass that should typecheck.
+simplePass
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
+  => String
+  -> TC.PirTCConfig uni fun
+  -> (Term TyName Name uni fun a -> Term TyName Name uni fun a)
+  -> Pass m TyName Name uni fun a
+simplePass name tcConfig f =
+  NamedPass name $
+    Pass (pure . f) [Typechecks tcConfig] [ConstCondition (Typechecks tcConfig)]
+
+-- | A pass that does renaming.
+renamePass
+  :: (HasUnique name TermUnique, HasUnique tyname TypeUnique, MonadQuote m, Ord a)
+  => Pass m tyname name uni fun a
+renamePass =
+  NamedPass "renaming" $
+    Pass PLC.rename [] [ConstCondition GloballyUniqueNames]
+
+-- | A pass that does typechecking, useful when you want to do it explicitly
+-- and not as part of a precondition check.
+typecheckPass
+  :: (TC.MonadTypeCheckPir err uni fun a m, Ord a)
+  => TC.PirTCConfig uni fun
+  -> Pass m TyName Name uni fun a
+typecheckPass tcconfig = NamedPass "typechecking" $ Pass run [GloballyUniqueNames] []
+  where
+    run t = do
+      _ <- TC.inferType tcconfig t
+      pure t
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/Beta.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/Beta.hs
index f834b180237..a0335a5cad7 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/Beta.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/Beta.hs
@@ -4,13 +4,17 @@
 A simple beta-reduction pass.
 -}
 module PlutusIR.Transform.Beta (
-  beta
+  beta,
+  betaPass,
+  betaPassSC
   ) where
 
-import PlutusIR
-
 import Control.Lens (over)
 import Data.List.NonEmpty qualified as NE
+import PlutusCore qualified as PLC
+import PlutusIR
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
 {- Note [Multi-beta]
 Consider two examples where applying beta should be helpful.
@@ -58,6 +62,10 @@ applications.
 That does mean that we need to do a manual traversal rather than doing standard bottom-up
 processing.
 
+Note that multi-beta requires globally unique names. In the example above, we end up with
+the binding for `x` outside `b`, which means it could shadow an existing `x` binding in the
+environment.
+
 Note that multi-beta cannot be used on TypeBinds. For instance, it is unsound to turn
 
 (/\a \(b : a). t) {x} (y : x)
@@ -128,3 +136,20 @@ beta = over termSubterms beta . localTransform
           let b = TypeBind a (TyVarDecl a n k) tyArg
           in Let (termAnn body) NonRec (pure b) body
       t -> t
+
+betaPassSC
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, PLC.MonadQuote m, Ord a)
+  => TC.PirTCConfig uni fun
+  -> Pass m TyName Name uni fun a
+betaPassSC tcconfig = renamePass <> betaPass tcconfig
+
+betaPass
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m, Ord a)
+  => TC.PirTCConfig uni fun
+  -> Pass m TyName Name uni fun a
+betaPass tcconfig =
+  NamedPass "beta" $
+    Pass
+      (pure . beta)
+      [Typechecks tcconfig, GloballyUniqueNames]
+      [ConstCondition (Typechecks tcconfig)]
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/CaseOfCase.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/CaseOfCase.hs
index fc365e2847b..f025ba5401f 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/CaseOfCase.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/CaseOfCase.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ViewPatterns        #-}
-module PlutusIR.Transform.CaseOfCase where
+module PlutusIR.Transform.CaseOfCase (caseOfCase, caseOfCasePass, caseOfCasePassSC) where
 
 import Control.Lens hiding (Strict, cons)
 import Control.Monad.Trans (lift)
@@ -15,13 +15,42 @@ import PlutusCore.Name qualified as PLC
 import PlutusCore.Quote
 import PlutusIR
 import PlutusIR.Analysis.Builtins
-import PlutusIR.Analysis.VarInfo
+import PlutusIR.Analysis.VarInfo (VarInfo (DatatypeConstructor, DatatypeMatcher), VarsInfo,
+                                  getConstructorArities, lookupVarInfo, termVarInfo)
 import PlutusIR.Contexts
 import PlutusIR.Core
 import PlutusIR.MkPir
+import PlutusIR.Pass
 import PlutusIR.Transform.Rename ()
+import PlutusIR.TypeCheck qualified as TC
 import PlutusPrelude
 
+caseOfCasePassSC ::
+    forall m uni fun a.
+    (PLC.Typecheckable uni fun, PLC.GEq uni, PLC.MonadQuote m, Ord a) =>
+    TC.PirTCConfig uni fun ->
+    BuiltinsInfo uni fun ->
+    Bool ->
+    a ->
+    Pass m TyName Name uni fun a
+caseOfCasePassSC tcconfig binfo conservative newAnn =
+  renamePass <> caseOfCasePass tcconfig binfo conservative newAnn
+
+caseOfCasePass ::
+    forall m uni fun a.
+    ( PLC.Typecheckable uni fun, PLC.GEq uni, MonadQuote m, Ord a) =>
+    TC.PirTCConfig uni fun ->
+    BuiltinsInfo uni fun ->
+    Bool ->
+    a ->
+    Pass m TyName Name uni fun a
+caseOfCasePass tcconfig binfo conservative newAnn =
+  NamedPass "case-of-case" $
+    Pass
+      (caseOfCase binfo conservative newAnn)
+      [Typechecks tcconfig, GloballyUniqueNames]
+      [ConstCondition (Typechecks tcconfig)]
+
 {-|
 Perform the case-of-case transformation. This pushes
 case expressions into the case branches of other case
@@ -43,7 +72,7 @@ Example:
 caseOfCase ::
     forall m tyname uni fun a.
     ( Ord fun, PLC.HasUnique tyname PLC.TypeUnique
-    , PLC.MonadQuote m
+    , PLC.MonadQuote m -- we need this because we do generate new names
     ) =>
     BuiltinsInfo uni fun ->
     Bool ->
@@ -51,10 +80,7 @@ caseOfCase ::
     Term tyname Name uni fun a ->
     m (Term tyname Name uni fun a)
 -- See Note [Case-of-case and conapps]
-caseOfCase binfo conservative newAnn t0 = do
-    -- We are going to record information about variables in a global map, so we
-    -- need global uniqueness
-    t <- PLC.rename t0
+caseOfCase binfo conservative newAnn t = do
     let vinfo = termVarInfo t
     liftQuote $ transformMOf termSubterms (processTerm binfo vinfo conservative newAnn) t
 
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/CaseReduce.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/CaseReduce.hs
index f7f3b908a1a..c0efcb8ee09 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/CaseReduce.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/CaseReduce.hs
@@ -3,6 +3,7 @@
 
 module PlutusIR.Transform.CaseReduce
     ( caseReduce
+    , caseReducePass
     ) where
 
 import PlutusCore.MkPlc
@@ -10,6 +11,15 @@ import PlutusIR.Core
 
 import Control.Lens (transformOf, (^?))
 import Data.List.Extras
+import PlutusCore qualified as PLC
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
+
+caseReducePass
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
+  => TC.PirTCConfig uni fun
+  -> Pass m TyName Name uni fun a
+caseReducePass tcconfig = simplePass "case reduce" tcconfig caseReduce
 
 caseReduce :: Term tyname name uni fun a -> Term tyname name uni fun a
 caseReduce = transformOf termSubterms processTerm
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/DeadCode.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/DeadCode.hs
index 27f80a10349..b75e0704a68 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/DeadCode.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/DeadCode.hs
@@ -4,7 +4,7 @@
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
 -- | Optimization passes for removing dead code, mainly dead let bindings.
-module PlutusIR.Transform.DeadCode (removeDeadBindings) where
+module PlutusIR.Transform.DeadCode (removeDeadBindings, removeDeadBindingsPass, removeDeadBindingsPassSC) where
 
 import PlutusIR
 import PlutusIR.Analysis.Dependencies qualified as Deps
@@ -24,12 +24,35 @@ import Data.Set qualified as Set
 import Algebra.Graph qualified as G
 import Algebra.Graph.ToGraph qualified as T
 import Data.List.NonEmpty qualified as NE
-import PlutusCore.Quote (MonadQuote, freshTyName, liftQuote)
+import PlutusCore.Quote (MonadQuote, freshTyName)
 import PlutusCore.StdLib.Data.ScottUnit qualified as Unit
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Analysis.VarInfo
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 import Witherable (Witherable (wither))
 
+removeDeadBindingsPassSC ::
+  (PLC.Typecheckable uni fun, PLC.GEq uni, Ord a, MonadQuote m)
+  => TC.PirTCConfig uni fun
+  -> BuiltinsInfo uni fun
+  -> Pass m TyName Name uni fun a
+removeDeadBindingsPassSC tcconfig binfo =
+  renamePass <> removeDeadBindingsPass tcconfig binfo
+
+removeDeadBindingsPass ::
+  (PLC.Typecheckable uni fun, PLC.GEq uni, Ord a, MonadQuote m)
+  => TC.PirTCConfig uni fun
+  -> BuiltinsInfo uni fun
+  -> Pass m TyName Name uni fun a
+removeDeadBindingsPass tcconfig binfo =
+  NamedPass "dead code elimination" $
+    Pass
+      (removeDeadBindings binfo)
+      [Typechecks tcconfig, GloballyUniqueNames]
+      [ConstCondition (Typechecks tcconfig)]
+
+-- We only need MonadQuote to make new types for bindings
 -- | Remove all the dead let bindings in a term.
 removeDeadBindings
     :: (PLC.HasUnique name PLC.TermUnique,
@@ -38,9 +61,8 @@ removeDeadBindings
     -> Term TyName name uni fun a
     -> m (Term TyName name uni fun a)
 removeDeadBindings binfo t = do
-    tRen <- PLC.rename t
-    let vinfo = termVarInfo tRen
-    liftQuote $ runReaderT (transformMOf termSubterms processTerm tRen) (calculateLiveness binfo vinfo tRen)
+    let vinfo = termVarInfo t
+    runReaderT (transformMOf termSubterms processTerm t) (calculateLiveness binfo vinfo t)
 
 type Liveness = Set.Set Deps.Node
 
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/EvaluateBuiltins.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/EvaluateBuiltins.hs
index ea5455d2784..b81e4b0d511 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/EvaluateBuiltins.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/EvaluateBuiltins.hs
@@ -7,6 +7,7 @@
 -- arbitrary builtins.
 module PlutusIR.Transform.EvaluateBuiltins
     ( evaluateBuiltins
+    , evaluateBuiltinsPass
     ) where
 
 import PlutusCore.Builtin
@@ -15,7 +16,24 @@ import PlutusIR.Core
 
 import Control.Lens (transformOf, (^.))
 import Data.Functor (void)
+import PlutusCore qualified as PLC
 import PlutusIR.Analysis.Builtins
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
+
+evaluateBuiltinsPass :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
+  => TC.PirTCConfig uni fun
+  -> Bool
+  -- ^ Whether to be conservative and try to retain logging behaviour.
+  -> BuiltinsInfo uni fun
+  -> CostingPart uni fun
+  -> Pass m TyName Name uni fun a
+evaluateBuiltinsPass tcconfig conservative binfo costModel =
+  NamedPass "evaluate builtins" $
+    Pass
+      (pure . evaluateBuiltins conservative binfo costModel)
+      [Typechecks tcconfig]
+      [ConstCondition (Typechecks tcconfig)]
 
 evaluateBuiltins
   :: forall tyname name uni fun a
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/Inline/Inline.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/Inline/Inline.hs
index ee7a6e33369..66f776bc05c 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/Inline/Inline.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/Inline/Inline.hs
@@ -10,7 +10,7 @@ in the paper 'Secrets of the GHC Inliner'.
 (2) call site inlining of fully applied functions. See `Inline.CallSiteInline.hs`
 -}
 
-module PlutusIR.Transform.Inline.Inline (inline, InlineHints (..)) where
+module PlutusIR.Transform.Inline.Inline (inline, inlinePass, inlinePassSC, InlineHints (..)) where
 import PlutusCore.Annotation
 import PlutusCore.Name
 import PlutusCore.Quote
@@ -18,6 +18,7 @@ import PlutusCore.Rename (dupable)
 import PlutusIR
 import PlutusIR.Analysis.Usages qualified as Usages
 import PlutusIR.MkPir (mkLet)
+import PlutusIR.Pass
 import PlutusIR.Transform.Inline.Utils
 import PlutusIR.Transform.Rename ()
 import PlutusPrelude
@@ -28,11 +29,13 @@ import Control.Monad.Reader (runReaderT)
 import Control.Monad.State (evalStateT, modify')
 
 import Control.Monad.State.Class (gets)
+import PlutusCore qualified as PLC
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Analysis.Size (termSize)
 import PlutusIR.Analysis.VarInfo qualified as VarInfo
 import PlutusIR.Contexts (AppContext (..), fillAppContext, splitApplication)
 import PlutusIR.Transform.Inline.CallSiteInline (callSiteInline)
+import PlutusIR.TypeCheck qualified as TC
 import Witherable (Witherable (wither))
 
 {- Note [Inlining approach and 'Secrets of the GHC Inliner']
@@ -154,6 +157,29 @@ But we don't really care about the costs listed there: it's easy for us to get a
 supply, and the performance cost does not currently seem relevant. So it's fine.
 -}
 
+inlinePassSC
+    :: forall uni fun ann m
+    . (PLC.Typecheckable uni fun, PLC.GEq uni, Ord ann, ExternalConstraints TyName Name uni fun m)
+    => TC.PirTCConfig uni fun
+    -> InlineHints Name ann
+    -> BuiltinsInfo uni fun
+    -> Pass m TyName Name uni fun ann
+inlinePassSC tcconfig hints binfo = renamePass <> inlinePass tcconfig hints binfo
+
+inlinePass
+    :: forall uni fun ann m
+    . (PLC.Typecheckable uni fun, PLC.GEq uni, Ord ann, ExternalConstraints TyName Name uni fun m)
+    => TC.PirTCConfig uni fun
+    -> InlineHints Name ann
+    -> BuiltinsInfo uni fun
+    -> Pass m TyName Name uni fun ann
+inlinePass tcconfig hints binfo =
+  NamedPass "inline" $
+    Pass
+      (inline hints binfo)
+      [GloballyUniqueNames, Typechecks tcconfig]
+      [ConstCondition GloballyUniqueNames, ConstCondition (Typechecks tcconfig)]
+
 -- | Inline non-recursive bindings. Relies on global uniqueness, and preserves it.
 -- See Note [Inlining and global uniqueness]
 inline
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/KnownCon.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/KnownCon.hs
index d2a8d931f6d..176073b2036 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/KnownCon.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/KnownCon.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE NamedFieldPuns #-}
 
-module PlutusIR.Transform.KnownCon (knownCon) where
+module PlutusIR.Transform.KnownCon (knownCon, knownConPass, knownConPassSC) where
 
 import PlutusCore qualified as PLC
 import PlutusCore.Name qualified as PLC
@@ -11,6 +11,30 @@ import PlutusIR.Transform.Rename ()
 import Control.Lens hiding (cons)
 import Data.List.Extra qualified as List
 import PlutusIR.Analysis.VarInfo
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
+
+knownConPassSC ::
+    forall m uni fun a.
+    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
+    , PLC.MonadQuote m
+    )
+    => TC.PirTCConfig uni fun
+    -> Pass m TyName Name uni fun a
+knownConPassSC tcconfig = renamePass <> knownConPass tcconfig
+
+knownConPass ::
+    forall m uni fun a.
+    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
+    , Applicative m)
+    => TC.PirTCConfig uni fun
+    -> Pass m TyName Name uni fun a
+knownConPass tcconfig =
+  NamedPass "case of known constructor" $
+    Pass
+      (pure . knownCon)
+      [Typechecks tcconfig, GloballyUniqueNames]
+      [ConstCondition (Typechecks tcconfig)]
 
 {- | Simplify destructor applications, if the scrutinee is a constructor application.
 
@@ -33,20 +57,16 @@ As an example, given
 @
 -}
 knownCon ::
-    forall m tyname name uni fun a.
+    forall tyname name uni fun a.
     ( PLC.HasUnique name PLC.TermUnique
     , PLC.HasUnique tyname PLC.TypeUnique
     , Eq name
-    , PLC.MonadQuote m
     ) =>
     Term tyname name uni fun a ->
-    m (Term tyname name uni fun a)
-knownCon t0 = do
-    -- We are going to record information about variables in a global map, so we
-    -- need global uniqueness
-    t <- PLC.rename t0
+    Term tyname name uni fun a
+knownCon t =
     let vinfo = termVarInfo t
-    pure $ transformOf termSubterms (processTerm vinfo) t
+    in transformOf termSubterms (processTerm vinfo) t
 
 processTerm ::
     forall tyname name uni fun a .
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/LetFloatIn.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/LetFloatIn.hs
index bbb31c1115b..f0fbfb15fe4 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/LetFloatIn.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/LetFloatIn.hs
@@ -7,7 +7,7 @@
 {-# LANGUAGE ViewPatterns      #-}
 
 -- | Float bindings inwards.
-module PlutusIR.Transform.LetFloatIn (floatTerm) where
+module PlutusIR.Transform.LetFloatIn (floatTerm, floatTermPass, floatTermPassSC) where
 
 import PlutusCore qualified as PLC
 import PlutusCore.Builtin qualified as PLC
@@ -28,6 +28,8 @@ import Data.Set (Set)
 import Data.Set qualified as Set
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Analysis.VarInfo
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
 {- Note [Float-in]
 
@@ -179,22 +181,49 @@ data FloatInContext = FloatInContext
 
 makeLenses ''FloatInContext
 
+floatTermPassSC ::
+    forall m uni fun a.
+    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
+    , PLC.MonadQuote m
+    ) =>
+    TC.PirTCConfig uni fun ->
+    BuiltinsInfo uni fun ->
+    Bool ->
+    Pass m TyName Name uni fun a
+floatTermPassSC tcconfig binfo relaxed =
+    renamePass <> floatTermPass tcconfig binfo relaxed
+
+floatTermPass ::
+    forall m uni fun a.
+    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
+    , Applicative m
+    ) =>
+    TC.PirTCConfig uni fun ->
+    BuiltinsInfo uni fun ->
+    -- | Whether to float-in more aggressively. See Note [Float-in] #6
+    Bool ->
+    Pass m TyName Name uni fun a
+floatTermPass tcconfig binfo relaxed =
+  NamedPass "let float-in" $
+    Pass
+      (pure . floatTerm binfo relaxed)
+      [Typechecks tcconfig, GloballyUniqueNames]
+      [ConstCondition (Typechecks tcconfig)]
+
 -- | Float bindings in the given `Term` inwards.
 floatTerm ::
-  forall m tyname name uni fun a.
+  forall tyname name uni fun a.
   ( PLC.HasUnique name PLC.TermUnique
   , PLC.HasUnique tyname PLC.TypeUnique
   , PLC.ToBuiltinMeaning uni fun
-  , PLC.MonadQuote m
   ) =>
   BuiltinsInfo uni fun ->
   -- | Whether to float-in more aggressively. See Note [Float-in] #6
   Bool ->
   Term tyname name uni fun a ->
-  m (Term tyname name uni fun a)
-floatTerm binfo relaxed t0 = do
-  t1 <- PLC.rename t0
-  pure . fmap fst $ floatTermInner (Usages.termUsages t1) (termVarInfo t1) t1
+  Term tyname name uni fun a
+floatTerm binfo relaxed t0 =
+  fmap fst $ floatTermInner (Usages.termUsages t0) (termVarInfo t0) t0
   where
     floatTermInner ::
       Usages.Usages ->
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/LetFloatOut.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/LetFloatOut.hs
index 4ec809d7fc2..b3d473da053 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/LetFloatOut.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/LetFloatOut.hs
@@ -6,7 +6,7 @@
 {-# LANGUAGE TypeOperators       #-}
 {-# LANGUAGE ViewPatterns        #-}
 {-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
-module PlutusIR.Transform.LetFloatOut (floatTerm) where
+module PlutusIR.Transform.LetFloatOut (floatTerm, floatTermPass, floatTermPassSC) where
 
 import PlutusCore qualified as PLC
 import PlutusCore.Builtin qualified as PLC
@@ -31,6 +31,8 @@ import Data.Set.Lens (setOf)
 import GHC.Generics
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Analysis.VarInfo
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
 {- Note [Let Floating pass]
 
@@ -392,6 +394,32 @@ floatBackLets term fTable =
                 -- fold the floatable groups into a *single* floatablegroup and combine that with some pir (term or bindings).
                 pure $ fold1 floatableGrps' `placeIntoFn` termOrBindings
 
+floatTermPassSC ::
+    forall m uni fun a.
+    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
+    , Semigroup a, PLC.MonadQuote m
+    ) =>
+    TC.PirTCConfig uni fun ->
+    BuiltinsInfo uni fun ->
+    Pass m TyName Name uni fun a
+floatTermPassSC tcconfig binfo =
+    renamePass <> floatTermPass tcconfig binfo
+
+floatTermPass ::
+    forall m uni fun a.
+    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
+    , Semigroup a, Applicative m
+    ) =>
+    TC.PirTCConfig uni fun ->
+    BuiltinsInfo uni fun ->
+    Pass m TyName Name uni fun a
+floatTermPass tcconfig binfo =
+  NamedPass "let float-out" $
+    Pass
+      (pure . floatTerm binfo)
+      [Typechecks tcconfig, GloballyUniqueNames]
+      [ConstCondition (Typechecks tcconfig)]
+
 -- | The compiler pass of the algorithm (comprised of 3 connected passes).
 floatTerm :: (PLC.ToBuiltinMeaning uni fun,
             PLC.HasUnique tyname PLC.TypeUnique, PLC.HasUnique name PLC.TermUnique,
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/LetMerge.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/LetMerge.hs
index e49eaa19d48..054b329f9e4 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/LetMerge.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/LetMerge.hs
@@ -4,11 +4,15 @@ A trivial simplification that merges adjacent non-recursive let terms.
 -}
 module PlutusIR.Transform.LetMerge (
   letMerge
+  , letMergePass
   ) where
 
 import PlutusIR
 
 import Control.Lens (transformOf)
+import PlutusCore qualified as PLC
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
 {-|
 A single non-recursive application of let-merging cancellation.
@@ -27,3 +31,9 @@ letMerge
     :: Term tyname name uni fun a
     -> Term tyname name uni fun a
 letMerge = transformOf termSubterms letMergeStep
+
+letMergePass
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
+  => TC.PirTCConfig uni fun
+  -> Pass m TyName Name uni fun a
+letMergePass tcconfig = simplePass "let merge" tcconfig letMerge
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/NonStrict.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/NonStrict.hs
index 87f71184f45..d5815a85727 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/NonStrict.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/NonStrict.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
 -- | Compile non-strict bindings into strict bindings.
-module PlutusIR.Transform.NonStrict (compileNonStrictBindings) where
+module PlutusIR.Transform.NonStrict (compileNonStrictBindings, compileNonStrictBindingsPass, compileNonStrictBindingsPassSC) where
 
 import PlutusIR
 import PlutusIR.Transform.Rename ()
@@ -16,6 +16,9 @@ import Control.Lens hiding (Strict)
 import Control.Monad.State
 
 import Data.Map qualified as Map
+import PlutusCore qualified as PLC
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
 {- Note [Compiling non-strict bindings]
 Given `let x : ty = rhs in body`, we
@@ -41,6 +44,25 @@ function type but `() -> x` is!
 
 type Substs uni fun a = Map.Map Name (Term TyName Name uni fun a)
 
+compileNonStrictBindingsPassSC
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, MonadQuote m, Ord a)
+  => TC.PirTCConfig uni fun
+  -> Bool
+  -> Pass m TyName Name uni fun a
+compileNonStrictBindingsPassSC tcConfig useUnit =
+    renamePass <> compileNonStrictBindingsPass tcConfig useUnit
+
+compileNonStrictBindingsPass
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, MonadQuote m)
+  => TC.PirTCConfig uni fun
+  -> Bool
+  -> Pass m TyName Name uni fun a
+compileNonStrictBindingsPass tcConfig useUnit =
+  NamedPass "compile non-strict bindings" $
+    Pass
+      (compileNonStrictBindings useUnit)
+      [Typechecks tcConfig] [ConstCondition (Typechecks tcConfig)]
+
 -- | Compile all the non-strict bindings in a term into strict bindings. Note: requires globally
 -- unique names.
 compileNonStrictBindings :: MonadQuote m => Bool -> Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/RecSplit.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/RecSplit.hs
index 6f6108b8e55..b0d4233a2dc 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/RecSplit.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/RecSplit.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
 module PlutusIR.Transform.RecSplit
-    (recSplit) where
+    (recSplit, recSplitPass) where
 
 import PlutusCore.Name qualified as PLC
 import PlutusIR
@@ -22,7 +22,10 @@ import Data.Map qualified as M
 import Data.Semigroup.Foldable
 import Data.Set qualified as S
 import Data.Set.Lens (setOf)
+import PlutusCore qualified as PLC
 import PlutusIR.MkPir (mkLet)
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 import PlutusPrelude ((<^>))
 
 {- Note [LetRec splitting pass]
@@ -66,6 +69,12 @@ and the 'principal' function arbitrarily chooses between one of these introduced
 to represent the "principal" id of the whole datatype binding so it can be used as "the key".
 -}
 
+recSplitPass
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
+  => TC.PirTCConfig uni fun
+  -> Pass m TyName Name uni fun a
+recSplitPass tcconfig = simplePass "recursive let split" tcconfig recSplit
+
 {-|
 Apply letrec splitting, recursively in bottom-up fashion.
 -}
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs
index 96cfd3e2a4f..7d969d6ca3d 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules.hs
@@ -4,22 +4,49 @@
 {-# LANGUAGE TypeOperators     #-}
 module PlutusIR.Transform.RewriteRules
     ( rewriteWith
+    , rewritePass
+    , rewritePassSC
     , RewriteRules (..)
     , defaultUniRewriteRules
     ) where
 
+import PlutusCore qualified as PLC
 import PlutusCore.Core (HasUniques)
-import PlutusCore.Default
 import PlutusCore.Name
 import PlutusCore.Quote
 import PlutusIR as PIR
 import PlutusIR.Analysis.VarInfo
-import PlutusIR.Transform.RewriteRules.CommuteFnWithConst
-import PlutusIR.Transform.RewriteRules.UnConstrConstrData
-import PlutusPrelude
+import PlutusIR.Transform.RewriteRules.Rules
 
 import Control.Lens
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
+rewritePassSC ::
+    forall m uni fun a.
+    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
+    , PLC.MonadQuote m, Monoid a
+    ) =>
+    TC.PirTCConfig uni fun ->
+    RewriteRules uni fun ->
+    Pass m TyName Name uni fun a
+rewritePassSC tcconfig rules =
+    renamePass <> rewritePass tcconfig rules
+
+rewritePass ::
+    forall m uni fun a.
+    ( PLC.Typecheckable uni fun, PLC.GEq uni, Ord a
+    , PLC.MonadQuote m, Monoid a
+    ) =>
+    TC.PirTCConfig uni fun ->
+    RewriteRules uni fun ->
+    Pass m TyName Name uni fun a
+rewritePass tcconfig rules =
+  NamedPass "rewrite rules" $
+    Pass
+      (rewriteWith rules)
+      [Typechecks tcconfig, GloballyUniqueNames]
+      [ConstCondition (Typechecks tcconfig)]
 
 {- | Rewrite a `Term` using the given `RewriteRules` (similar to functions of Term -> Term)
 Normally the rewrite rules are configured at entrypoint time of the compiler.
@@ -42,21 +69,3 @@ rewriteWith (RewriteRules rules) t =
     let vinfo = termVarInfo t
     in transformMOf termSubterms (rules vinfo) t
 
--- | A bundle of composed `RewriteRules`, to be passed at entrypoint of the compiler.
-newtype RewriteRules uni fun = RewriteRules {
-    unRewriteRules :: forall tyname m a
-                   . (MonadQuote m, Monoid a)
-                   => VarsInfo tyname Name uni a
-                   -> PIR.Term tyname Name uni fun a
-                   -> m (PIR.Term tyname Name uni fun a)
-    }
-
--- | The rules for the Default Universe/Builtin.
-defaultUniRewriteRules :: RewriteRules DefaultUni DefaultFun
-defaultUniRewriteRules = RewriteRules $ \ vinfo ->
-        -- The rules are composed from left to right.
-        pure . commuteFnWithConst
-        >=> unConstrConstrData def vinfo
-
-instance Default (RewriteRules DefaultUni DefaultFun) where
-  def = defaultUniRewriteRules
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/Rules.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/Rules.hs
new file mode 100644
index 00000000000..416cd53da1d
--- /dev/null
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/RewriteRules/Rules.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs             #-}
+{-# LANGUAGE RankNTypes        #-}
+module PlutusIR.Transform.RewriteRules.Rules where
+
+import PlutusCore.Default
+import PlutusCore.Name
+import PlutusCore.Quote
+import PlutusIR as PIR
+import PlutusIR.Analysis.VarInfo
+import PlutusIR.Transform.RewriteRules.CommuteFnWithConst
+import PlutusIR.Transform.RewriteRules.UnConstrConstrData
+import PlutusPrelude
+
+-- | A bundle of composed `RewriteRules`, to be passed at entrypoint of the compiler.
+newtype RewriteRules uni fun where
+  RewriteRules :: {unRewriteRules :: forall tyname m a.
+                                       (MonadQuote m, Monoid a) =>
+                                       VarsInfo tyname Name uni a
+                                       -> PIR.Term tyname Name uni fun a
+                                          -> m (PIR.Term tyname Name uni fun a)}
+                    -> RewriteRules uni fun
+
+-- | The rules for the Default Universe/Builtin.
+defaultUniRewriteRules :: RewriteRules DefaultUni DefaultFun
+defaultUniRewriteRules = RewriteRules $ \ vinfo ->
+        -- The rules are composed from left to right.
+        pure . commuteFnWithConst
+        >=> unConstrConstrData def vinfo
+
+instance Default (RewriteRules DefaultUni DefaultFun) where
+  def = defaultUniRewriteRules
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/StrictifyBindings.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/StrictifyBindings.hs
index 05f2e125fb0..26dcd4fd7b1 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/StrictifyBindings.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/StrictifyBindings.hs
@@ -3,7 +3,8 @@
 Pass to convert pointlessly non-strict bindings into strict bindings, which have less overhead.
 -}
 module PlutusIR.Transform.StrictifyBindings (
-  strictifyBindings
+  strictifyBindings,
+  strictifyBindingsPass
   ) where
 
 import PlutusCore.Builtin
@@ -11,9 +12,12 @@ import PlutusIR
 import PlutusIR.Purity
 
 import Control.Lens (transformOf)
+import PlutusCore qualified as PLC
 import PlutusCore.Name qualified as PLC
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Analysis.VarInfo
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
 strictifyBindingsStep
     :: (ToBuiltinMeaning uni fun, PLC.HasUnique name PLC.TermUnique)
@@ -40,3 +44,16 @@ strictifyBindings binfo term =
     termSubterms
     (strictifyBindingsStep binfo (termVarInfo term))
     term
+
+strictifyBindingsPass ::
+    forall m uni fun a.
+    (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m) =>
+    TC.PirTCConfig uni fun ->
+    BuiltinsInfo uni fun ->
+    Pass m TyName Name uni fun a
+strictifyBindingsPass tcconfig binfo =
+  NamedPass "strictify bindings" $
+    Pass
+      (pure . strictifyBindings binfo)
+      [Typechecks tcconfig]
+      [ConstCondition (Typechecks tcconfig)]
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/ThunkRecursions.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/ThunkRecursions.hs
index 1e88ee52084..732d3696fe7 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/ThunkRecursions.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/ThunkRecursions.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE LambdaCase       #-}
 -- | Implements a PIR-to-PIR transformation that makes all recursive term definitions
 -- compilable to PLC. See Note [Thunking recursions] for details.
-module PlutusIR.Transform.ThunkRecursions (thunkRecursions) where
+module PlutusIR.Transform.ThunkRecursions (thunkRecursions, thunkRecursionsPass) where
 
 import PlutusCore.Builtin
 import PlutusCore.Name qualified as PLC
@@ -15,6 +15,9 @@ import PlutusIR.Purity
 
 import Control.Lens hiding (Strict)
 import Data.List.NonEmpty qualified as NE
+import PlutusCore qualified as PLC
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
 {- Note [Thunking recursions]
 Our fixpoint combinators in Plutus Core know how to handle mutually recursive values
@@ -166,3 +169,10 @@ thunkRecursions
     -> Term tyname name uni fun a
     -> Term tyname name uni fun a
 thunkRecursions binfo t = transformOf termSubterms (thunkRecursionsStep binfo (termVarInfo t)) t
+
+thunkRecursionsPass
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
+  => TC.PirTCConfig uni fun
+  -> BuiltinsInfo uni fun
+  -> Pass m TyName Name uni fun a
+thunkRecursionsPass tcconfig binfo = simplePass "thunk recursions" tcconfig (thunkRecursions binfo)
diff --git a/plutus-core/plutus-ir/src/PlutusIR/Transform/Unwrap.hs b/plutus-core/plutus-ir/src/PlutusIR/Transform/Unwrap.hs
index 5bd70f6f266..57af11bd623 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/Transform/Unwrap.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/Transform/Unwrap.hs
@@ -8,12 +8,16 @@ and should anyway better be handled by something like case-of-known constructor.
 But it's so simple we might as well include it just in case.
 -}
 module PlutusIR.Transform.Unwrap (
-  unwrapCancel
+  unwrapCancel,
+  unwrapCancelPass
   ) where
 
 import PlutusIR
 
 import Control.Lens (transformOf)
+import PlutusCore qualified as PLC
+import PlutusIR.Pass
+import PlutusIR.TypeCheck qualified as TC
 
 {-|
 A single non-recursive application of wrap/unwrap cancellation.
@@ -32,3 +36,9 @@ unwrapCancel
     :: Term tyname name uni fun a
     -> Term tyname name uni fun a
 unwrapCancel = transformOf termSubterms unwrapCancelStep
+
+unwrapCancelPass
+  :: (PLC.Typecheckable uni fun, PLC.GEq uni, Applicative m)
+  => TC.PirTCConfig uni fun
+  -> Pass m TyName Name uni fun a
+unwrapCancelPass tcconfig = simplePass "wrap-unwrap cancel" tcconfig unwrapCancel
diff --git a/plutus-core/plutus-ir/src/PlutusIR/TypeCheck.hs b/plutus-core/plutus-ir/src/PlutusIR/TypeCheck.hs
index 9161fc6d845..a63e74735a2 100644
--- a/plutus-core/plutus-ir/src/PlutusIR/TypeCheck.hs
+++ b/plutus-core/plutus-ir/src/PlutusIR/TypeCheck.hs
@@ -14,6 +14,7 @@ module PlutusIR.TypeCheck (
   checkType,
   inferTypeOfProgram,
   checkTypeOfProgram,
+  MonadTypeCheckPir,
 ) where
 
 import PlutusCore.Rename
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Compiler/Let/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Compiler/Let/Tests.hs
index 39aef7f8ea8..4cb37e52e70 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Compiler/Let/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Compiler/Let/Tests.hs
@@ -1,9 +1,20 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies     #-}
+{-# LANGUAGE TypeOperators    #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
 module PlutusIR.Compiler.Let.Tests where
 
-import PlutusIR.Test
-
+import Control.Monad (join)
+import Control.Monad.Except
+import Control.Monad.Reader
+import Data.Bifunctor
+import Data.Functor (void)
+import PlutusCore qualified as PLC
+import PlutusIR.Compiler (Provenance (..))
+import PlutusIR.Compiler qualified as PIR
 import PlutusIR.Compiler.Let
-import PlutusIR.Properties.Typecheck
+import PlutusIR.Pass.Test
+import PlutusIR.Test
 import Test.QuickCheck
 import Test.Tasty
 import Test.Tasty.ExpectedFailure (ignoreTest)
@@ -16,30 +27,34 @@ test_lets = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Compiler"] $ test
     , goldenPlcFromPir pTermAsProg "letDep"
     ]
 
--- FIXME
--- | Check that a term typechecks after a
--- `PlutusIR.Compiler.Let.compileLets` (recursive terms) pass.
-prop_TypecheckCompileLetsRecTerms :: Property
-prop_TypecheckCompileLetsRecTerms =
-  expectFailure $ withMaxSuccess 10000 $ extraConstraintTypecheckProp (compileLets RecTerms)
-
--- | Check that a term typechecks after a
--- `PlutusIR.Compiler.Let.compileLets` (non-recursive terms) pass.
-prop_TypecheckCompileLetsNonRecTerms :: Property
-prop_TypecheckCompileLetsNonRecTerms =
-  withMaxSuccess 10000 $ extraConstraintTypecheckProp (compileLets NonRecTerms)
-
--- | Check that a term typechecks after a
--- `PlutusIR.Compiler.Let.compileLets` (types) pass.
-prop_TypecheckCompileLetsTypes :: Property
-prop_TypecheckCompileLetsTypes =
-  withMaxSuccess 10000 $ extraConstraintTypecheckProp (compileLets Types)
+-- FIXME: this fails because some of the let passes expect certain things to be
+-- gone, e.g. non-strict bindings. We should a) add pre-/post-conditions for these,
+-- and b) set up the tests to establish what is needed
+test_propLets :: TestTree
+test_propLets =
+  ignoreTest $ testProperty "lets" $ \letKind -> withMaxSuccess 40000 $
+    testPassProp' @_ @_ @_ @(Provenance ())
+      (Original ())
+      (\t -> fmap Original t)
+      runCompiling
+      (\tc -> compileLetsPassSC tc letKind)
+  where
+    -- This is rather painful, but it works
+    runCompiling ::
+      forall e m c .
+      (e ~ PIR.Error PLC.DefaultUni PLC.DefaultFun (Provenance ())
+      , c ~ PIR.CompilationCtx PLC.DefaultUni PLC.DefaultFun ()
+      , m ~ ExceptT e (ExceptT e (PLC.QuoteT (Reader c)))
+      )
+      => m () -> Either String ()
+    runCompiling v =
+      let
+        res :: Either e ()
+        res = do
+            plcConfig <- PLC.getDefTypeCheckConfig (Original ())
+            let ctx = PIR.toDefaultCompilationCtx plcConfig
+            join $ flip runReader ctx $ PLC.runQuoteT $ runExceptT $ runExceptT v
+      in convertToEitherString $ first void res
 
--- FIXME this test sometimes fails so ignoring it to make CI pass.
--- | Check that a term typechecks after a
--- `PlutusIR.Compiler.Let.compileLets` (data types) pass.
-test_TypecheckCompileLetsDataTypes :: TestTree
-test_TypecheckCompileLetsDataTypes =
-  ignoreTest $ testProperty "typechecking" $
-    withMaxSuccess 10000 $
-      extraConstraintTypecheckProp (compileLets DataTypes)
+instance Arbitrary LetKind where
+  arbitrary = elements [ RecTerms , NonRecTerms , Types , DataTypes ]
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Compiler/Recursion/factorial.golden b/plutus-core/plutus-ir/test/PlutusIR/Compiler/Recursion/factorial.golden
index e4bb3260094..fd7566fb1d2 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Compiler/Recursion/factorial.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Compiler/Recursion/factorial.golden
@@ -2,30 +2,30 @@
   1.1.0
   [
     [
-      (lam s_860 [ s_860 s_860 ])
+      (lam s_1650 [ s_1650 s_1650 ])
       (lam
-        s_861
+        s_1651
         (lam
-          x_862
+          x_1652
           [
             (lam
-              factorial_863
+              factorial_1653
               [
                 [
                   [
                     [
                       (force (builtin ifThenElse))
-                      [ [ (builtin equalsInteger) (con integer 0) ] x_862 ]
+                      [ [ (builtin equalsInteger) (con integer 0) ] x_1652 ]
                     ]
-                    (lam u_864 (con integer 1))
+                    (lam u_1654 (con integer 1))
                   ]
                   (lam
-                    u_865
+                    u_1655
                     [
-                      [ (builtin multiplyInteger) x_862 ]
+                      [ (builtin multiplyInteger) x_1652 ]
                       [
-                        factorial_863
-                        [ [ (builtin subtractInteger) x_862 ] (con integer 1) ]
+                        factorial_1653
+                        [ [ (builtin subtractInteger) x_1652 ] (con integer 1) ]
                       ]
                     ]
                   )
@@ -33,7 +33,7 @@
                 (con unit ())
               ]
             )
-            [ s_861 s_861 ]
+            [ s_1651 s_1651 ]
           ]
         )
       )
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs
index 1d086cd8465..60d09e0e35f 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Scoping/Tests.hs
@@ -38,7 +38,7 @@ test_names = testGroup "names"
       -- because the scope checking machinery doesn't create unused bindings, every binding
       -- gets referenced at some point at least once (usually very close to the binding site).
       -- So this test doesn't really test much.
-      T.test_scopingGood "dead code elimination" genTerm T.BindingRemovalNotOk T.PrerenameNo $
+      T.test_scopingGood "dead code elimination" genTerm T.BindingRemovalNotOk T.PrerenameYes $
         removeDeadBindings def
     , T.test_scopingGood "constant folding" genTerm T.BindingRemovalNotOk T.PrerenameYes $
         pure . evaluateBuiltins False def defaultBuiltinCostModel
@@ -51,10 +51,10 @@ test_names = testGroup "names"
         "match-against-known-constructor"
         genTerm
         T.BindingRemovalNotOk
-        T.PrerenameNo $
-        knownCon
-    , T.test_scopingGood "floating bindings inwards" genTerm T.BindingRemovalNotOk T.PrerenameNo $
-        In.floatTerm def True
+        T.PrerenameYes $
+        (pure . knownCon)
+    , T.test_scopingGood "floating bindings inwards" genTerm T.BindingRemovalNotOk T.PrerenameYes $
+        (pure . In.floatTerm def True)
     -- Can't test 'Out.floatTerm', because it requires the type of annotations to implement
     -- 'Semigroup' and it's not clear what that means for 'NameAnn'.
     , T.test_scopingGood "merging lets" genTerm T.BindingRemovalNotOk T.PrerenameYes $
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/Tests.hs
index c728e8e3238..17d72f900a7 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/Tests.hs
@@ -1,21 +1,19 @@
 module PlutusIR.Transform.Beta.Tests where
 
-import Test.Tasty
-import Test.Tasty.Extras
-
-import PlutusCore qualified as PLC
 import PlutusCore.Quote
 import PlutusIR.Parser
-import PlutusIR.Properties.Typecheck
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.Beta
 import Test.QuickCheck.Property (Property, withMaxSuccess)
+import Test.Tasty
+import Test.Tasty.Extras
 
 test_beta :: TestTree
 test_beta = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "Beta" $
         map
-            (goldenPir (beta . runQuote . PLC.rename) pTerm)
+            (goldenPir (runQuote . runTestPass betaPassSC) pTerm)
             [ "lamapp"
             , "lamapp2"
             , "absapp"
@@ -23,6 +21,5 @@ test_beta = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
             , "multilet"
             ]
 
--- | Check that a term typechecks after a `PlutusIR.Transform.Beta.beta` pass.
-prop_TypecheckBeta :: Property
-prop_TypecheckBeta = withMaxSuccess 3000 (pureTypecheckProp beta)
+prop_beta :: Property
+prop_beta = withMaxSuccess numTestsForPassProp $ testPassProp runQuote betaPassSC
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multiapp b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multiapp
index 6638f5bc1f7..15212a32a34 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multiapp
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multiapp
@@ -1 +1 @@
-[ (lam x (con integer) (lam y (con integer) (lam z (con integer) [ y x z ]))) (con integer 1) (con integer 2) (con integer 3) ]
+[ (lam x (con integer) (lam y (fun (con integer) (fun (con integer) (con integer))) (lam z (con integer) [ y x z ]))) (con integer 1) (lam a (con integer) (lam b (con integer) (con integer 2))) (con integer 3) ]
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multiapp.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multiapp.golden
index c9784d2f139..34381f2c541 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multiapp.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multiapp.golden
@@ -1,7 +1,11 @@
 (let
   (nonrec)
   (termbind (strict) (vardecl x (con integer)) (con integer 1))
-  (termbind (strict) (vardecl y (con integer)) (con integer 2))
+  (termbind
+    (strict)
+    (vardecl y (fun (con integer) (fun (con integer) (con integer))))
+    (lam a (con integer) (lam b (con integer) (con integer 2)))
+  )
   (termbind (strict) (vardecl z (con integer)) (con integer 3))
   [ [ y x ] z ]
 )
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multilet b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multilet
index 846a294cf68..c8fe0370dde 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multilet
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multilet
@@ -1 +1 @@
-[ (lam x (con integer) [ (lam y (con integer) [ (lam z (con integer) [ y x z ]) (con integer 3) ] ) (con integer 2) ]) (con integer 1)]
+[ (lam x (con integer) [ (lam y (fun (con integer) (fun (con integer) (con integer))) [ (lam z (con integer) [ y x z ]) (con integer 3) ] ) (lam a (con integer) (lam b (con integer) (con integer 2))) ]) (con integer 1)]
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multilet.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multilet.golden
index e4285193fec..02230c95548 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multilet.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Beta/multilet.golden
@@ -3,7 +3,11 @@
   (termbind (strict) (vardecl x (con integer)) (con integer 1))
   (let
     (nonrec)
-    (termbind (strict) (vardecl y (con integer)) (con integer 2))
+    (termbind
+      (strict)
+      (vardecl y (fun (con integer) (fun (con integer) (con integer))))
+      (lam a (con integer) (lam b (con integer) (con integer 2)))
+    )
     (let
       (nonrec)
       (termbind (strict) (vardecl z (con integer)) (con integer 3))
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/Tests.hs
index e02af1a2c68..437a700204e 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/Tests.hs
@@ -1,35 +1,29 @@
-{-# LANGUAGE TypeApplications #-}
 module PlutusIR.Transform.CaseOfCase.Tests where
 
 import Test.Tasty
 import Test.Tasty.Extras
 
-import Control.Lens
-import PlutusCore qualified as PLC
-import PlutusCore.Name
 import PlutusCore.Quote
-import PlutusIR.Analysis.Builtins
-import PlutusIR.Error as PIR
 import PlutusIR.Parser
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.CaseOfCase qualified as CaseOfCase
-import PlutusIR.TypeCheck as TC
 import PlutusPrelude
+import Test.QuickCheck.Property (Property, withMaxSuccess)
 
 test_caseOfCase :: TestTree
 test_caseOfCase = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "CaseOfCase" $
         map
-            (goldenPirM goldenCoCTC pTerm)
+            (goldenPir (runQuote . runTestPass
+                        (\tc -> CaseOfCase.caseOfCasePassSC tc def True mempty)) pTerm)
             [ "basic"
             , "builtinBool"
             , "largeExpr"
             , "exponential"
             ]
-    where
-      binfo = def & set' biMatcherLike defaultUniMatcherLike
-      goldenCoCTC t = rethrow . asIfThrown @(PIR.Error PLC.DefaultUni PLC.DefaultFun ()) $ do
-        let newT = runQuote $ CaseOfCase.caseOfCase binfo True mempty t
-        -- make sure the floated result typechecks
-        _ <- runQuoteT . flip inferType (() <$ newT) =<< TC.getDefTypeCheckConfig ()
-        pure newT
+
+prop_caseOfCase :: Property
+prop_caseOfCase =
+  withMaxSuccess numTestsForPassProp $
+    testPassProp runQuote $ \tc -> CaseOfCase.caseOfCasePassSC tc def True mempty
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/exponential b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/exponential
index d8340d97e7a..9565770d2e8 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/exponential
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/exponential
@@ -42,7 +42,7 @@
                   Bool
                 }
                 False
-                (lam i (con integer) True)
+                (lam j (con integer) True)
             ]
           ]
           (con integer)
@@ -60,7 +60,7 @@
                 Bool
               }
               False
-              (lam i (con integer) True)
+              (lam k (con integer) True)
             ]
           ]
           (con integer)
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/exponential.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/exponential.golden
index 46868f1c6a9..4305c3882e4 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/exponential.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseOfCase/exponential.golden
@@ -34,7 +34,7 @@
                 ]
               ]
               (lam
-                i
+                j
                 (con integer)
                 [
                   [ { [ match_Bool True ] (con integer) } (con integer 1) ]
@@ -52,7 +52,7 @@
               ]
             ]
             (lam
-              i
+              k
               (con integer)
               [
                 [ { [ match_Bool True ] (con integer) } (con integer 3) ]
@@ -77,7 +77,7 @@
                 ]
               ]
               (lam
-                i
+                j
                 (con integer)
                 [
                   [ { [ match_Bool True ] (con integer) } (con integer 1) ]
@@ -95,7 +95,7 @@
               ]
             ]
             (lam
-              i
+              k
               (con integer)
               [
                 [ { [ match_Bool True ] (con integer) } (con integer 3) ]
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseReduce/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseReduce/Tests.hs
index 2951f789c07..e5fb095759f 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseReduce/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/CaseReduce/Tests.hs
@@ -1,11 +1,9 @@
 module PlutusIR.Transform.CaseReduce.Tests where
 
+import Data.Functor.Identity
+import PlutusIR.Pass.Test
 import PlutusIR.Transform.CaseReduce
-
-import PlutusIR.Properties.Typecheck
 import Test.QuickCheck.Property (Property, withMaxSuccess)
 
--- | Check that a term typechecks after a `PlutusIR.Transform.CaseReduce.caseReduce` pass.
-prop_TypecheckCaseReduce :: Property
-prop_TypecheckCaseReduce =
-      withMaxSuccess 3000 (pureTypecheckProp caseReduce)
+prop_caseReduce :: Property
+prop_caseReduce = withMaxSuccess numTestsForPassProp $ testPassProp runIdentity caseReducePass
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/Tests.hs
index c418ed5caa7..4b4e74cb0af 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/Tests.hs
@@ -7,7 +7,7 @@ import PlutusCore.Default
 import PlutusCore.Quote
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Parser
-import PlutusIR.Properties.Typecheck
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.DeadCode
 import PlutusPrelude
@@ -19,7 +19,7 @@ test_deadCode :: TestTree
 test_deadCode = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "DeadCode" $
         map
-            (goldenPir (runQuote . removeDeadBindings def) pTerm)
+            (goldenPir (runQuote . runTestPass (\tc -> removeDeadBindingsPassSC tc def)) pTerm)
             [ "typeLet"
             , "termLet"
             , "strictLet"
@@ -39,11 +39,12 @@ test_deadCode = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
             ]
 
 -- FIXME this test sometimes fails so ignoring it to make CI pass.
--- | Check that a term typechecks after a `PlutusIR.Transform.DeadCode.removeDeadBindings` pass.
 typecheckRemoveDeadBindingsProp :: BuiltinSemanticsVariant DefaultFun -> Property
 typecheckRemoveDeadBindingsProp biVariant =
-  withMaxSuccess 50000 $ nonPureTypecheckProp $ removeDeadBindings $
-     def {_biSemanticsVariant = biVariant}
-test_TypecheckRemoveDeadBindings :: TestTree
-test_TypecheckRemoveDeadBindings =
-  ignoreTest $ testProperty "typechecking" typecheckRemoveDeadBindingsProp
+  withMaxSuccess (3 * numTestsForPassProp) $
+    testPassProp
+      runQuote
+      $ \tc -> removeDeadBindingsPassSC tc (def {_biSemanticsVariant = biVariant})
+test_deadCodeP :: TestTree
+test_deadCodeP =
+  ignoreTest $ testProperty "deadCode" typecheckRemoveDeadBindingsProp
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/builtinBinding b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/builtinBinding
index ed6edee687a..61337cf966c 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/builtinBinding
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/builtinBinding
@@ -1,7 +1,7 @@
 (let
   (nonrec)
   (termbind (strict)
-    (vardecl add (fun (con integer) (con integer))) (builtin addInteger)
+    (vardecl add (fun (con integer) (fun (con integer) (con integer)))) (builtin addInteger)
   )
   (abs a (type) (lam x a x))
 )
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/datatypeLiveType b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/datatypeLiveType
index 4a0a278a5a3..7e107132e06 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/datatypeLiveType
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/datatypeLiveType
@@ -8,5 +8,5 @@
       (vardecl Nothing [Maybe a]) (vardecl Just (fun a [Maybe a]))
     )
   )
-  (error Maybe)
+  (error [Maybe (con integer)])
 )
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/datatypeLiveType.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/datatypeLiveType.golden
index 8f6518246cd..81089321b1e 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/datatypeLiveType.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/datatypeLiveType.golden
@@ -4,5 +4,5 @@
     (tyvardecl Maybe (fun (type) (type)))
     (lam a (type) (all a (type) (fun a a)))
   )
-  (error Maybe)
+  (error [ Maybe (con integer) ])
 )
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/etaBuiltinBinding b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/etaBuiltinBinding
index fa2dc2fb602..effbb76ddbc 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/etaBuiltinBinding
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/DeadCode/etaBuiltinBinding
@@ -1,7 +1,7 @@
 (let
   (nonrec)
   (termbind (strict)
-    (vardecl add (fun (con integer) (con integer))) (lam arg1 (con integer) (lam arg2 (con integer) [ [ (builtin addInteger) arg1 ] arg2 ]))
+    (vardecl add (fun (con integer) (fun (con integer) (con integer)))) (lam arg1 (con integer) (lam arg2 (con integer) [ [ (builtin addInteger) arg1 ] arg2 ]))
   )
   (abs a (type) (lam x a x))
 )
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/EvaluateBuiltins/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/EvaluateBuiltins/Tests.hs
index f044776bf35..8d6aca9048d 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/EvaluateBuiltins/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/EvaluateBuiltins/Tests.hs
@@ -3,10 +3,11 @@ module PlutusIR.Transform.EvaluateBuiltins.Tests where
 import Test.Tasty
 import Test.Tasty.Extras
 
+import Data.Functor.Identity
 import PlutusCore.Default.Builtins
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Parser
-import PlutusIR.Properties.Typecheck
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.EvaluateBuiltins
 import PlutusPrelude
@@ -19,7 +20,9 @@ test_evaluateBuiltins = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Trans
     where
       conservative =
         map
-            (goldenPir (evaluateBuiltins True def def) pTerm)
+            (goldenPir
+              (runIdentity . runTestPass (\tc -> evaluateBuiltinsPass tc True def def))
+              pTerm)
             [ "addInteger"
             , "ifThenElse"
             , "traceConservative"
@@ -38,12 +41,10 @@ test_evaluateBuiltins = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Trans
             , "uncompressAndEqualBlsNonConservative"
             ]
 
--- | Check that a term typechecks after a `PlutusIR.Transform.EvaluateBuiltins`
--- pass.
-prop_TypecheckEvaluateBuiltins ::
+prop_evaluateBuiltins ::
     Bool -> BuiltinSemanticsVariant DefaultFun -> Property
-prop_TypecheckEvaluateBuiltins conservative biVariant =
-  withMaxSuccess 40000 $
-    pureTypecheckProp $
-        evaluateBuiltins conservative (def {_biSemanticsVariant = biVariant}) def
-
+prop_evaluateBuiltins conservative biVariant =
+  withMaxSuccess (2 * 3 * numTestsForPassProp) $
+    testPassProp
+      runIdentity
+      $ \tc -> evaluateBuiltinsPass tc conservative (def {_biSemanticsVariant = biVariant}) def
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/Tests.hs
index 224cfea4d3b..4dba93991c8 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/Tests.hs
@@ -1,19 +1,12 @@
-{-# LANGUAGE LambdaCase       #-}
-{-# LANGUAGE TypeApplications #-}
 module PlutusIR.Transform.Inline.Tests where
 
 import Test.Tasty.Extras
 
-import Control.Monad.Except
-import PlutusCore qualified as PLC
 import PlutusCore.Default.Builtins
 import PlutusCore.Quote
-import PlutusIR
 import PlutusIR.Analysis.Builtins
-import PlutusIR.Check.Uniques qualified as Uniques
-import PlutusIR.Core.Instance.Pretty.Readable
 import PlutusIR.Parser
-import PlutusIR.Properties.Typecheck
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.Inline.Inline
 import PlutusPrelude
@@ -23,20 +16,9 @@ import Test.Tasty (TestTree)
 -- | Tests of the inliner, include global uniqueness test.
 test_inline :: TestTree
 test_inline = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
-    let goldenInlineUnique :: Term TyName Name PLC.DefaultUni PLC.DefaultFun PLC.SrcSpan ->
-            IO (Term TyName Name PLC.DefaultUni PLC.DefaultFun PLC.SrcSpan)
-        goldenInlineUnique pir =
-            rethrow . asIfThrown @(PLC.UniqueError PLC.SrcSpan) $ do
-                let pirInlined = runQuote $ do
-                        renamed <- PLC.rename pir
-                        inline mempty def renamed
-                -- Make sure the inlined term is globally unique.
-                _ <- checkUniques pirInlined
-                pure pirInlined
-    in
     testNested "Inline" $
         map
-            (goldenPirM goldenInlineUnique pTerm)
+            (goldenPir (runQuote . runTestPass (\tc -> inlinePassSC tc mempty def)) pTerm)
             [ "var"
             , "builtin"
             , "callsite-non-trivial-body"
@@ -77,34 +59,13 @@ test_inline = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
             , "rhs-modified"
             , "partiallyApp"
             , "effectfulBuiltinArg"
+            , "nameCapture"
             ]
 
--- | Tests that the inliner doesn't incorrectly capture variable names.
-test_nameCapture :: TestTree
-test_nameCapture = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
-    let goldenNameCapture :: Term TyName Name PLC.DefaultUni PLC.DefaultFun PLC.SrcSpan ->
-            IO String
-        goldenNameCapture pir =
-            rethrow . asIfThrown @(PLC.UniqueError PLC.SrcSpan) $ do
-                let pirInlined = runQuote $ do
-                        renamed <- PLC.rename pir
-                        inline mempty def renamed
-                -- Make sure the inlined term is globally unique.
-                _ <- checkUniques pirInlined
-                pure . render $ prettyPirReadable pirInlined
-    in
-    testNested "Inline" $
-        map
-            (goldenPirMUnique goldenNameCapture pTerm)
-            [ "nameCapture"]
-
--- | Check whether a term is globally unique.
-checkUniques :: (Ord a, MonadError (PLC.UniqueError a) m) => Term TyName Name uni fun a -> m ()
-checkUniques =
-    Uniques.checkTerm (\case { Uniques.MultiplyDefined{} -> True; _ -> False})
-
--- | Check that a term typechecks after a `PlutusIR.Transform.Inline` pass.
-prop_TypecheckInline :: BuiltinSemanticsVariant DefaultFun -> Property
-prop_TypecheckInline biVariant =
-  withMaxSuccess 20000 $ nonPureTypecheckProp $
-    inline mempty (def {_biSemanticsVariant = biVariant})
+prop_inline ::
+    BuiltinSemanticsVariant DefaultFun -> Property
+prop_inline biVariant =
+  withMaxSuccess (3 * numTestsForPassProp) $
+    testPassProp
+      runQuote
+      $ \tc -> inlinePassSC tc mempty (def {_biSemanticsVariant = biVariant})
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/effectfulBuiltinArg b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/effectfulBuiltinArg
index a14512e85e5..adf162e4fa9 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/effectfulBuiltinArg
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/effectfulBuiltinArg
@@ -5,8 +5,8 @@
   (termbind
     (strict)
     (vardecl x (con integer))
-    [ (builtin trace) (con string "msg2") (con integer 1) ]
+    [ { (builtin trace) (con integer) } (con string "msg2") (con integer 1) ]
   )
-  [ {(builtin ifThenElse) (con integer) }  [ (builtin equalsInteger) [(builtin trace) (con string "msg1") (con integer 0)] x] (con integer 9) (con integer 10) ]
+  [ {(builtin ifThenElse) (con integer) }  [ (builtin equalsInteger) [ { (builtin trace) (con integer) } (con string "msg1") (con integer 0)] x] (con integer 9) (con integer 10) ]
 )
 
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/effectfulBuiltinArg.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/effectfulBuiltinArg.golden
index 729aaebf9e4..7b56bf75458 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/effectfulBuiltinArg.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/effectfulBuiltinArg.golden
@@ -3,7 +3,9 @@
   (termbind
     (strict)
     (vardecl x (con integer))
-    [ [ (builtin trace) (con string "msg2") ] (con integer 1) ]
+    [
+      [ { (builtin trace) (con integer) } (con string "msg2") ] (con integer 1)
+    ]
   )
   [
     [
@@ -12,7 +14,10 @@
         [
           [
             (builtin equalsInteger)
-            [ [ (builtin trace) (con string "msg1") ] (con integer 0) ]
+            [
+              [ { (builtin trace) (con integer) } (con string "msg1") ]
+              (con integer 0)
+            ]
           ]
           x
         ]
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/firstEffectfulTerm1 b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/firstEffectfulTerm1
index e1eea3cc157..6a5bcf12325 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/firstEffectfulTerm1
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/firstEffectfulTerm1
@@ -4,7 +4,7 @@
   (termbind
     (strict)
     (vardecl a (con integer))
-    { error (con integer) }
+    (error (con integer))
   )
   [ (lam x (con integer) x) a ]
 )
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/firstEffectfulTerm1.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/firstEffectfulTerm1.golden
index c38706c83e8..0ff66b05e7f 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/firstEffectfulTerm1.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/firstEffectfulTerm1.golden
@@ -1 +1 @@
-[ (lam x (con integer) x) { error (con integer) } ]
\ No newline at end of file
+[ (lam x (con integer) x) (error (con integer)) ]
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/nameCapture.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/nameCapture.golden
index 3371360e060..45735f41d6e 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/nameCapture.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/nameCapture.golden
@@ -1,8 +1,10 @@
-let
-  !a_4 : integer = 10
-  !c_6 : integer = addInteger a_4 a_4
-in
-let
-  !a_8 : integer = 7
-in
-addInteger (addInteger a_4 a_8) a_8
\ No newline at end of file
+(let
+  (nonrec)
+  (termbind (strict) (vardecl a (con integer)) (con integer 10))
+  (termbind (strict) (vardecl c (con integer)) [ [ (builtin addInteger) a ] a ])
+  (let
+    (nonrec)
+    (termbind (strict) (vardecl a (con integer)) (con integer 7))
+    [ [ (builtin addInteger) [ [ (builtin addInteger) a ] a ] ] a ]
+  )
+)
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/tyvar b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/tyvar
index 20428d720cf..3d79ca444a4 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/tyvar
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/tyvar
@@ -2,9 +2,7 @@
   (nonrec)
   (typebind (tyvardecl a (type)) (con integer))
   (typebind (tyvardecl b (type)) (con integer))
-  (let
-    (nonrec)
-    (termbind (strict) (vardecl y b) (con integer 1))
-    (lam z a [(lam x b x) y])
+  (lam p b
+    (lam z a [(lam x b x) p])
   )
 )
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/tyvar.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/tyvar.golden
index 1afce924f91..e0d12f496dd 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/tyvar.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Inline/tyvar.golden
@@ -1 +1 @@
-(lam z (con integer) [ (lam x (con integer) x) (con integer 1) ])
\ No newline at end of file
+(lam p (con integer) (lam z (con integer) [ (lam x (con integer) x) p ]))
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/KnownCon/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/KnownCon/Tests.hs
index 3d8d70b719a..afa0335080f 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/KnownCon/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/KnownCon/Tests.hs
@@ -1,23 +1,20 @@
-{-# LANGUAGE TypeApplications #-}
 module PlutusIR.Transform.KnownCon.Tests where
 
 import Test.Tasty
 import Test.Tasty.Extras
 
-import PlutusCore qualified as PLC
-import PlutusCore.Name
 import PlutusCore.Quote
-import PlutusIR.Error as PIR
 import PlutusIR.Parser
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.KnownCon qualified as KnownCon
-import PlutusIR.TypeCheck as TC
+import Test.QuickCheck
 
 test_knownCon :: TestTree
 test_knownCon = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "KnownCon" $
         map
-            (goldenPirM goldenKnownConTC pTerm)
+            (goldenPir (runQuote . runTestPass KnownCon.knownConPassSC) pTerm)
             [ "applicative"
             , "bool"
             , "list"
@@ -26,9 +23,6 @@ test_knownCon = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
             , "maybe-nothing"
             , "pair"
             ]
-  where
-    goldenKnownConTC pir = rethrow . asIfThrown @(PIR.Error PLC.DefaultUni PLC.DefaultFun ()) $ do
-        let simplified = runQuote $ KnownCon.knownCon pir
-        -- make sure the result typechecks
-        _ <- runQuoteT . flip inferType (() <$ simplified) =<< TC.getDefTypeCheckConfig ()
-        pure simplified
+
+prop_knownCon :: Property
+prop_knownCon = withMaxSuccess numTestsForPassProp $ testPassProp runQuote KnownCon.knownConPassSC
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/Tests.hs
index 0e132d11169..1ee11a89a51 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/Tests.hs
@@ -1,24 +1,19 @@
-{-# LANGUAGE TypeApplications #-}
 module PlutusIR.Transform.LetFloatIn.Tests where
 
 import Test.Tasty
 import Test.Tasty.Extras
 
 import PlutusCore qualified as PLC
-import PlutusCore.Name
+import PlutusCore.Builtin
 import PlutusCore.Quote
-import PlutusIR.Error as PIR
+import PlutusIR.Analysis.Builtins
 import PlutusIR.Parser
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.LetFloatIn qualified as LetFloatIn
 import PlutusIR.Transform.LetMerge qualified as LetMerge
 import PlutusIR.Transform.Rename ()
-import PlutusIR.TypeCheck as TC
 import PlutusPrelude
-
-import PlutusCore.Builtin
-import PlutusIR.Analysis.Builtins
-import PlutusIR.Properties.Typecheck
 import Test.QuickCheck.Property (Property, withMaxSuccess)
 
 test_letFloatInConservative :: TestTree
@@ -26,24 +21,21 @@ test_letFloatInConservative =
     runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform", "LetFloatIn"] $
     testNested "conservative" $
         map
-            (goldenPirM goldenFloatTC pTerm)
+            (goldenPir (runQuote . runTestPass testPass) pTerm)
             [ "avoid-floating-into-lam"
             , "avoid-floating-into-tyabs"
             ]
   where
-    goldenFloatTC pir = rethrow . asIfThrown @(PIR.Error PLC.DefaultUni PLC.DefaultFun ()) $ do
-        let pirFloated = runQuote $ LetFloatIn.floatTerm def False pir
-        -- make sure the floated result typechecks
-        _ <- runQuoteT . flip inferType (() <$ pirFloated) =<< TC.getDefTypeCheckConfig ()
-        -- letmerge is not necessary for floating, but is a nice visual transformation
-        pure $ LetMerge.letMerge pirFloated
+    testPass tcconfig =
+      LetFloatIn.floatTermPassSC tcconfig def False
+      <> LetMerge.letMergePass tcconfig
 
 test_letFloatInRelaxed :: TestTree
 test_letFloatInRelaxed =
     runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform", "LetFloatIn"] $
     testNested "relaxed" $
         map
-            (goldenPirM goldenFloatTC pTerm)
+            (goldenPir (runQuote . runTestPass testPass) pTerm)
             [ "avoid-floating-into-RHS"
             , "avoid-moving-strict-nonvalue-bindings"
             , "cannot-float-into-app"
@@ -62,18 +54,17 @@ test_letFloatInRelaxed =
             , "type"
             ]
   where
-    goldenFloatTC pir = rethrow . asIfThrown @(PIR.Error PLC.DefaultUni PLC.DefaultFun ()) $ do
-        let pirFloated = runQuote $ LetFloatIn.floatTerm def True pir
-        -- make sure the floated result typechecks
-        _ <- runQuoteT . flip inferType (() <$ pirFloated) =<< TC.getDefTypeCheckConfig ()
-        -- letmerge is not necessary for floating, but is a nice visual transformation
-        pure $ LetMerge.letMerge pirFloated
+    testPass tcconfig =
+      LetFloatIn.floatTermPassSC tcconfig def True
+      <> LetMerge.letMergePass tcconfig
 
--- | Check that a term typechecks after a
--- `PlutusIR.Transform.LetFloatIn.floatTerm` pass.
-prop_TypecheckFloatTerm ::
+prop_floatIn ::
   BuiltinSemanticsVariant PLC.DefaultFun -> Bool -> Property
-prop_TypecheckFloatTerm biVariant conservative =
-  withMaxSuccess 40000 $
-    nonPureTypecheckProp $
-      LetFloatIn.floatTerm (def {_biSemanticsVariant = biVariant}) conservative
+prop_floatIn biVariant conservative =
+  withMaxSuccess (3 * 2 * numTestsForPassProp) $ testPassProp runQuote testPass
+  where
+    testPass tcconfig =
+      LetFloatIn.floatTermPassSC
+        tcconfig
+        (def { _biSemanticsVariant = biVariant })
+        conservative
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/relaxed/type b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/relaxed/type
index 18ca0fdf9aa..672eae6fdea 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/relaxed/type
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/relaxed/type
@@ -1,19 +1,14 @@
 (let
   (nonrec)
+  (termbind (strict) (vardecl const (all a (type) (all b (type) (fun a (fun b a))))) (abs a (type) (abs b (type) (lam x a (lam y b x)))))
   (typebind (tyvardecl int (type)) (con integer))
   (lam
     n
     (con integer)
     [
-      [
-        [
-          { (builtin ifThenElse) int }
-          [ [ (builtin equalsInteger) (con integer 1) ] (con integer 0) ]
-        ]
-        (con integer 2)
-      ]
-      (con integer 3)
+      { const (con integer) int }
+      (con integer 1)
     ]
   )
 )
--- The typebind can be floated into the lambda and the application.
+-- The typebind can be floated into the lambda and the application, as can the termbind.
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/relaxed/type.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/relaxed/type.golden
index 2533a5f4c6a..9844b611adf 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/relaxed/type.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatIn/relaxed/type.golden
@@ -2,17 +2,25 @@
   n
   (con integer)
   [
-    [
-      [
-        (let
-          (nonrec)
-          (typebind (tyvardecl int (type)) (con integer))
-          { (builtin ifThenElse) int }
-        )
-        [ [ (builtin equalsInteger) (con integer 1) ] (con integer 0) ]
-      ]
-      (con integer 2)
-    ]
-    (con integer 3)
+    (let
+      (nonrec)
+      (typebind (tyvardecl int (type)) (con integer))
+      {
+        {
+          (let
+            (nonrec)
+            (termbind
+              (strict)
+              (vardecl const (all a (type) (all b (type) (fun a (fun b a)))))
+              (abs a (type) (abs b (type) (lam x a (lam y b x))))
+            )
+            const
+          )
+          (con integer)
+        }
+        int
+      }
+    )
+    (con integer 1)
   ]
 )
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatOut/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatOut/Tests.hs
index a3e5f54ad92..7eefa7ad929 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatOut/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/LetFloatOut/Tests.hs
@@ -5,28 +5,24 @@ import Test.Tasty
 import Test.Tasty.Extras
 
 import PlutusCore qualified as PLC
-import PlutusCore.Name
+import PlutusCore.Builtin
 import PlutusCore.Quote
-import PlutusIR.Error as PIR
+import PlutusIR.Analysis.Builtins
 import PlutusIR.Parser
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.LetFloatOut qualified as LetFloatOut
 import PlutusIR.Transform.LetMerge qualified as LetMerge
 import PlutusIR.Transform.RecSplit qualified as RecSplit
 import PlutusIR.Transform.Rename ()
-import PlutusIR.TypeCheck as TC
 import PlutusPrelude
-
-import PlutusCore.Builtin
-import PlutusIR.Analysis.Builtins
-import PlutusIR.Properties.Typecheck (pureTypecheckProp)
 import Test.QuickCheck.Property (Property, withMaxSuccess)
 
 test_letFloatOut :: TestTree
 test_letFloatOut = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "LetFloatOut" $
         map
-            (goldenPirM goldenFloatTC pTerm)
+            (goldenPir (runQuote . runTestPass testPass) pTerm)
             [ "letInLet"
             , "listMatch"
             , "maybe"
@@ -63,16 +59,15 @@ test_letFloatOut = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"
             , "rhsSqueezeVsNest"
             ]
   where
-    goldenFloatTC pir = rethrow . asIfThrown @(PIR.Error PLC.DefaultUni PLC.DefaultFun ()) $ do
-        let pirFloated = RecSplit.recSplit . LetFloatOut.floatTerm def . runQuote $ PLC.rename pir
-        -- make sure the floated result typechecks
-        _ <- runQuoteT . flip inferType (() <$ pirFloated) =<< TC.getDefTypeCheckConfig ()
-        -- letmerge is not necessary for floating, but is a nice visual transformation
-        pure $ LetMerge.letMerge pirFloated
+    testPass tcconfig =
+      LetFloatOut.floatTermPassSC tcconfig def
+      <> RecSplit.recSplitPass tcconfig
+      <> LetMerge.letMergePass tcconfig
 
--- | Check that a term typechecks after a
--- `PlutusIR.Transform.LetFloatOut.floatTerm` pass.
-prop_TypecheckFloatTerm :: BuiltinSemanticsVariant PLC.DefaultFun -> Property
-prop_TypecheckFloatTerm biVariant =
-  withMaxSuccess 20000 $ pureTypecheckProp $
-    LetFloatOut.floatTerm (def { _biSemanticsVariant = biVariant})
+prop_floatIn :: BuiltinSemanticsVariant PLC.DefaultFun -> Property
+prop_floatIn biVariant = withMaxSuccess (3 * numTestsForPassProp) $ testPassProp runQuote testPass
+  where
+    testPass tcconfig =
+      LetFloatOut.floatTermPassSC
+        tcconfig
+        (def { _biSemanticsVariant = biVariant })
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/NonStrict/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/NonStrict/Tests.hs
index 6f0ad17b781..e9574329bef 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/NonStrict/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/NonStrict/Tests.hs
@@ -5,15 +5,21 @@ import Test.Tasty.Extras
 
 import PlutusCore.Quote
 import PlutusIR.Parser
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.NonStrict qualified as NonStrict
 import PlutusIR.Transform.Rename ()
+import Test.QuickCheck
 
 test_nonStrict :: TestTree
 test_nonStrict = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "NonStrict" $
         map
-            (goldenPir (runQuote . NonStrict.compileNonStrictBindings False) pTerm)
+            (goldenPir (runQuote . runTestPass
+                        (\tc -> NonStrict.compileNonStrictBindingsPassSC tc False)) pTerm)
             [ "nonStrict1"
             ]
 
+prop_nonStrict :: Bool -> Property
+prop_nonStrict useUnit = withMaxSuccess (2 * numTestsForPassProp) $
+  testPassProp runQuote $ \tc -> NonStrict.compileNonStrictBindingsPassSC tc useUnit
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/RecSplit/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/RecSplit/Tests.hs
index c8809a96b6d..02cc57ad0a5 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/RecSplit/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/RecSplit/Tests.hs
@@ -3,10 +3,10 @@ module PlutusIR.Transform.RecSplit.Tests where
 import Test.Tasty
 import Test.Tasty.Extras
 
-import PlutusCore qualified as PLC
+import Data.Functor.Identity
 import PlutusCore.Quote
 import PlutusIR.Parser
-import PlutusIR.Properties.Typecheck
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.RecSplit
 import Test.Tasty.QuickCheck
@@ -15,7 +15,7 @@ test_recSplit :: TestTree
 test_recSplit = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "RecSplit" $
         map
-            (goldenPir (recSplit . runQuote . PLC.rename) pTerm)
+            (goldenPir (runQuote . runTestPass recSplitPass) pTerm)
             [ "truenonrec"
             , "mutuallyRecursiveTypes"
             , "mutuallyRecursiveValues"
@@ -24,7 +24,6 @@ test_recSplit = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
             , "big"
             ]
 
--- | Check that a term typechecks after a `PlutusIR.Transform.RecSplit.recSplit` pass.
-prop_TypecheckRecSplit :: Property
-prop_TypecheckRecSplit =
-  withMaxSuccess 3000 (pureTypecheckProp recSplit)
+prop_recSplit :: Property
+prop_recSplit =
+  withMaxSuccess numTestsForPassProp $ testPassProp runIdentity recSplitPass
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Rename/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/Rename/Tests.hs
index cf2a8d06102..5857f13358f 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Rename/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Rename/Tests.hs
@@ -5,9 +5,9 @@ import Test.Tasty.Extras
 
 import PlutusCore.Pretty qualified as PLC
 import PlutusCore.Quote
-import PlutusCore.Rename qualified as PLC
 import PlutusIR.Parser
-import PlutusIR.Properties.Typecheck
+import PlutusIR.Pass
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.Rename ()
 import Test.Tasty.QuickCheck
@@ -16,7 +16,8 @@ test_rename :: TestTree
 test_rename = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "Rename" $
         map
-            (goldenPir (PLC.AttachPrettyConfig debugConfig . runQuote . PLC.rename) pTerm)
+            (goldenPir
+             (PLC.AttachPrettyConfig debugConfig . runQuote . runTestPass (const renamePass)) pTerm)
             [ "allShadowedDataNonRec"
             , "allShadowedDataRec"
             , "paramShadowedDataNonRec"
@@ -25,7 +26,6 @@ test_rename = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
   where
     debugConfig = PLC.PrettyConfigClassic PLC.debugPrettyConfigName False
 
--- | Check that a term typechecks after a `PlutusIR.Transform.Rename.rename` pass.
-prop_TypecheckRename :: Property
-prop_TypecheckRename =
-  withMaxSuccess 5000 (nonPureTypecheckProp PLC.rename)
+prop_rename :: Property
+prop_rename =
+  withMaxSuccess numTestsForPassProp $ testPassProp runQuote (const renamePass)
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/Tests.hs
index 628a6062cd8..0cdbfc797ca 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/Tests.hs
@@ -4,17 +4,19 @@ import PlutusCore.Quote
 import PlutusCore.Test hiding (ppCatch)
 import PlutusIR.Compiler qualified as PIR
 import PlutusIR.Parser
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.RewriteRules as RewriteRules
 import PlutusPrelude
 
+import Test.QuickCheck
 import Test.Tasty
 
-test_RewriteRules :: TestTree
-test_RewriteRules = runTestNestedIn ["plutus-ir/test/PlutusIR/Transform"] $
+test_rewriteRules :: TestTree
+test_rewriteRules = runTestNestedIn ["plutus-ir/test/PlutusIR/Transform"] $
     testNested "RewriteRules" $
     (fmap
-        (goldenPirDoc (prettyPlcClassicDebug . runQuote . RewriteRules.rewriteWith def)  pTerm)
+        (goldenPir (runQuote . runTestPass (\tc -> rewritePassSC tc def)) pTerm)
         [ "equalsInt.pir" -- this tests that the function works on equalInteger
         , "divideInt.pir" -- this tests that the function excludes not commutative functions
         , "multiplyInt.pir" -- this tests that the function works on multiplyInteger
@@ -35,3 +37,7 @@ test_RewriteRules = runTestNestedIn ["plutus-ir/test/PlutusIR/Transform"] $
           -- we need traces to remain for checking the evaluation-order
           tplc <- asIfThrown $ compileWithOpts ( set (PIR.ccOpts . PIR.coPreserveLogging) True) ast
           runUPlcLogs [void tplc]
+
+prop_rewriteRules :: Property
+prop_rewriteRules =
+  withMaxSuccess numTestsForPassProp $ testPassProp runQuote $ \tc -> rewritePassSC tc def
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/let.pir.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/let.pir.golden
index 523f5b1f055..b5baf093451 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/let.pir.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/let.pir.golden
@@ -1,8 +1,8 @@
 (let
   (nonrec)
-  (termbind (strict) (vardecl x_0 (con integer)) (error (con integer)))
+  (termbind (strict) (vardecl x (con integer)) (error (con integer)))
   [
     [ (builtin equalsInteger) (con integer 5) ]
-    [ [ (builtin addInteger) (con integer 10) ] x_0 ]
+    [ [ (builtin addInteger) (con integer 10) ] x ]
   ]
 )
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/unConstrConstrDataFst.pir.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/unConstrConstrDataFst.pir.golden
index 8213f1b4f00..7dad83c70a4 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/unConstrConstrDataFst.pir.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/unConstrConstrDataFst.pir.golden
@@ -2,18 +2,18 @@
   (nonrec)
   (datatypebind
     (datatype
-      (tyvardecl MyD_1099_0 (type))
+      (tyvardecl MyD_1099 (type))
 
-      MyD_match_1102_1
-      (vardecl MyD_1100_2 (fun (con integer) MyD_1099_0))
-      (vardecl MyD_1101_3 (fun (con bytestring) MyD_1099_0))
+      MyD_match_1102
+      (vardecl MyD_1100 (fun (con integer) MyD_1099))
+      (vardecl MyD_1101 (fun (con bytestring) MyD_1099))
     )
   )
   (let
     (nonrec)
     (termbind
       (strict)
-      (vardecl generated_0 (con integer))
+      (vardecl generated (con integer))
       [
         [ { (builtin trace) (con integer) } (con string "BEFORE") ]
         (con integer 0)
@@ -23,7 +23,7 @@
       (nonrec)
       (termbind
         (strict)
-        (vardecl generated_1 [ (con list) (con data) ])
+        (vardecl generated [ (con list) (con data) ])
         [
           [ { (builtin trace) [ (con list) (con data) ] } (con string "AFTER") ]
           [
@@ -35,7 +35,7 @@
           ]
         ]
       )
-      generated_0
+      generated
     )
   )
 )
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/unConstrConstrDataSnd.pir.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/unConstrConstrDataSnd.pir.golden
index b667d06151a..a9d8728185b 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/unConstrConstrDataSnd.pir.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/RewriteRules/unConstrConstrDataSnd.pir.golden
@@ -2,11 +2,11 @@
   (nonrec)
   (datatypebind
     (datatype
-      (tyvardecl MyD_1099_0 (type))
+      (tyvardecl MyD_1099 (type))
 
-      MyD_match_1102_1
-      (vardecl MyD_1100_2 (fun (con integer) MyD_1099_0))
-      (vardecl MyD_1101_3 (fun (con bytestring) MyD_1099_0))
+      MyD_match_1102
+      (vardecl MyD_1100 (fun (con integer) MyD_1099))
+      (vardecl MyD_1101 (fun (con bytestring) MyD_1099))
     )
   )
   [
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictifyBindings/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictifyBindings/Tests.hs
index 347def86720..fc2af546710 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictifyBindings/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/StrictifyBindings/Tests.hs
@@ -3,10 +3,11 @@ module PlutusIR.Transform.StrictifyBindings.Tests where
 import Test.Tasty
 import Test.Tasty.Extras
 
+import Data.Functor.Identity
 import PlutusCore.Default.Builtins
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Parser
-import PlutusIR.Properties.Typecheck (pureTypecheckProp)
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.StrictifyBindings
 import PlutusPrelude
@@ -16,16 +17,16 @@ test_strictifyBindings :: TestTree
 test_strictifyBindings = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "StrictifyBindings" $
         map
-            (goldenPir (strictifyBindings def) pTerm)
+            (goldenPir (runIdentity . runTestPass (\tc -> strictifyBindingsPass tc def)) pTerm)
             [ "pure1"
             , "impure1"
             , "unused"
             , "conapp"
             ]
 
--- | Check that a term typechecks after a
--- `PlutusIR.Transform.StrictifyBindings` pass.
-prop_TypecheckStrictifyBindings :: BuiltinSemanticsVariant DefaultFun -> Property
-prop_TypecheckStrictifyBindings biVariant =
-  withMaxSuccess 5000 $
-    pureTypecheckProp (strictifyBindings (def {_biSemanticsVariant = biVariant}))
+prop_strictifyBindings :: BuiltinSemanticsVariant DefaultFun -> Property
+prop_strictifyBindings biVariant =
+  withMaxSuccess numTestsForPassProp $
+    testPassProp
+      runIdentity
+      $ \tc -> strictifyBindingsPass tc (def {_biSemanticsVariant = biVariant})
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/Tests.hs
index 31012cd4eea..1b80679868c 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/Tests.hs
@@ -3,14 +3,15 @@ module PlutusIR.Transform.ThunkRecursions.Tests where
 import Test.Tasty
 import Test.Tasty.Extras
 
+import Data.Functor.Identity
 import PlutusCore.Builtin
 import PlutusCore.Default
 import PlutusIR.Analysis.Builtins
 import PlutusIR.Parser
-import PlutusIR.Properties.Typecheck
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.Rename ()
-import PlutusIR.Transform.ThunkRecursions (thunkRecursions)
+import PlutusIR.Transform.ThunkRecursions
 import PlutusPrelude
 import Test.QuickCheck.Property (Property, withMaxSuccess)
 
@@ -18,7 +19,7 @@ test_thunkRecursions :: TestTree
 test_thunkRecursions = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "ThunkRecursions" $
         map
-            (goldenPir (thunkRecursions def) pTerm)
+            (goldenPir (runIdentity . runTestPass (\tc -> thunkRecursionsPass tc def)) pTerm)
             [ "listFold"
             , "listFoldTrace"
             , "monoMap"
@@ -28,8 +29,7 @@ test_thunkRecursions = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transf
             , "preserveStrictness"
             ]
 
--- | Check that a term typechecks after a `PlutusIR.Transform.ThunkRecursions.thunkRecursions` pass.
-prop_TypecheckThunkRecursions :: BuiltinSemanticsVariant DefaultFun -> Property
-prop_TypecheckThunkRecursions biVariant =
-  withMaxSuccess 5000 $ pureTypecheckProp $
-    thunkRecursions $ def {_biSemanticsVariant = biVariant}
+prop_thunkRecursions :: BuiltinSemanticsVariant DefaultFun -> Property
+prop_thunkRecursions biVariant =
+  withMaxSuccess numTestsForPassProp $
+    testPassProp runIdentity $ \tc -> thunkRecursionsPass tc (def {_biSemanticsVariant = biVariant})
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFold b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFold
index 7fa3aaef8f3..7132634ce0d 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFold
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFold
@@ -13,24 +13,29 @@
     (termbind (strict)
       (vardecl
         foldl
-        (all a (type) (all b (type) (fun (fun a (fun b a)) (fun a (fun [List b] a)))))
+        (all a (type) (all b (type) (fun (fun b (fun a b)) (fun b (fun [List a] b)))))
       )
+      (abs a (type)
+      (abs b (type)
       (lam
         f
-        (fun a (fun b a))
+        (fun b (fun a b))
         (lam
           acc
-          a
+          b
           (lam
             lst
-            [List b]
+            [List a]
             [
-              [ [ { match_List a } lst ] acc ]
-              (lam x b (lam xs [List b] [ [ [ foldl f ] [ [ f acc ] x ] ] xs ]))
+              { [ { match_List a } lst ] b }
+              acc
+              (lam x a (lam xs [List a] [ { foldl a b } f [ f acc x ] xs ]))
             ]
           )
         )
       )
+      )
+      )
     )
     foldl
   )
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFold.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFold.golden
index 74f4291b25c..5490f98189c 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFold.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFold.golden
@@ -18,24 +18,38 @@
         (all
           a
           (type)
-          (all b (type) (fun (fun a (fun b a)) (fun a (fun [ List b ] a))))
+          (all b (type) (fun (fun b (fun a b)) (fun b (fun [ List a ] b))))
         )
       )
-      (lam
-        f
-        (fun a (fun b a))
-        (lam
-          acc
-          a
+      (abs
+        a
+        (type)
+        (abs
+          b
+          (type)
           (lam
-            lst
-            [ List b ]
-            [
-              [ [ { match_List a } lst ] acc ]
+            f
+            (fun b (fun a b))
+            (lam
+              acc
+              b
               (lam
-                x b (lam xs [ List b ] [ [ [ foldl f ] [ [ f acc ] x ] ] xs ])
+                lst
+                [ List a ]
+                [
+                  [ { [ { match_List a } lst ] b } acc ]
+                  (lam
+                    x
+                    a
+                    (lam
+                      xs
+                      [ List a ]
+                      [ [ [ { { foldl a } b } f ] [ [ f acc ] x ] ] xs ]
+                    )
+                  )
+                ]
               )
-            ]
+            )
           )
         )
       )
@@ -49,7 +63,7 @@
           (all
             a
             (type)
-            (all b (type) (fun (fun a (fun b a)) (fun a (fun [ List b ] a))))
+            (all b (type) (fun (fun b (fun a b)) (fun b (fun [ List a ] b))))
           )
         )
         foldl
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFoldTrace b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFoldTrace
index 311dd29097c..d26b6d43eb8 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFoldTrace
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFoldTrace
@@ -13,28 +13,34 @@
     (termbind (strict)
       (vardecl
         foldl
-        (all a (type) (all b (type) (fun (fun a (fun b a)) (fun a (fun [List b] a)))))
+        (all a (type) (all b (type) (fun (fun b (fun a b)) (fun b (fun [List a] b)))))
       )
+      (abs a (type)
+      (abs b (type)
       (lam
         f
-        (fun a (fun b a))
+        (fun b (fun a b))
         (lam
           acc
-          a
+          b
           (lam
             lst
-            [List b]
+            [List a]
             [
-              [ [ { match_List a } lst ] acc ]
-              (lam x b (lam xs [List b]
-                [ [ { (builtin trace) a } (con string "hello") ]
-                 [ [ [ foldl f ] [ [ f acc ] x ] ] xs ]
-
-                 ]))
+              { [ { match_List a } lst ] b }
+              acc
+              (lam x a (lam xs [List a]
+                [
+                  { (builtin trace) b } (con string "hello")
+                  [ { foldl a b } f [ f acc x ] xs ]
+                ]
+              ))
             ]
           )
         )
       )
+      )
+      )
     )
     foldl
   )
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFoldTrace.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFoldTrace.golden
index ec1b6fdbe50..756d649f18e 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFoldTrace.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/listFoldTrace.golden
@@ -18,33 +18,41 @@
         (all
           a
           (type)
-          (all b (type) (fun (fun a (fun b a)) (fun a (fun [ List b ] a))))
+          (all b (type) (fun (fun b (fun a b)) (fun b (fun [ List a ] b))))
         )
       )
-      (lam
-        f
-        (fun a (fun b a))
-        (lam
-          acc
-          a
+      (abs
+        a
+        (type)
+        (abs
+          b
+          (type)
           (lam
-            lst
-            [ List b ]
-            [
-              [ [ { match_List a } lst ] acc ]
+            f
+            (fun b (fun a b))
+            (lam
+              acc
+              b
               (lam
-                x
-                b
-                (lam
-                  xs
-                  [ List b ]
-                  [
-                    [ { (builtin trace) a } (con string "hello") ]
-                    [ [ [ foldl f ] [ [ f acc ] x ] ] xs ]
-                  ]
-                )
+                lst
+                [ List a ]
+                [
+                  [ { [ { match_List a } lst ] b } acc ]
+                  (lam
+                    x
+                    a
+                    (lam
+                      xs
+                      [ List a ]
+                      [
+                        [ { (builtin trace) b } (con string "hello") ]
+                        [ [ [ { { foldl a } b } f ] [ [ f acc ] x ] ] xs ]
+                      ]
+                    )
+                  )
+                ]
               )
-            ]
+            )
           )
         )
       )
@@ -58,7 +66,7 @@
           (all
             a
             (type)
-            (all b (type) (fun (fun a (fun b a)) (fun a (fun [ List b ] a))))
+            (all b (type) (fun (fun b (fun a b)) (fun b (fun [ List a ] b))))
           )
         )
         foldl
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/monoMap b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/monoMap
index 9b1b37dfbff..d653eb284b5 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/monoMap
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/monoMap
@@ -21,11 +21,11 @@
           lst
           [List (con integer)]
           [
-            [ [ { match_List (con integer) } lst ] Nil ]
+            [ { [ { match_List (con integer) } lst ] [List (con integer)] } { Nil (con integer) } ]
             (lam
               x
               (con integer)
-              (lam xs [List (con integer)] [ [ Cons [ f x ] ] [ [ map f ] xs ] ])
+              (lam xs [List (con integer)] [ { Cons (con integer) } [ f x ] [ map f xs ] ])
             )
           ]
         )
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/monoMap.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/monoMap.golden
index b3d32df28f9..56054fc3165 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/monoMap.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/ThunkRecursions/monoMap.golden
@@ -27,12 +27,17 @@
           lst
           [ List (con integer) ]
           [
-            [ [ { match_List (con integer) } lst ] Nil ]
+            [
+              { [ { match_List (con integer) } lst ] [ List (con integer) ] }
+              { Nil (con integer) }
+            ]
             (lam
               x
               (con integer)
               (lam
-                xs [ List (con integer) ] [ [ Cons [ f x ] ] [ [ map f ] xs ] ]
+                xs
+                [ List (con integer) ]
+                [ [ { Cons (con integer) } [ f x ] ] [ [ map f ] xs ] ]
               )
             )
           ]
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/Tests.hs b/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/Tests.hs
index 5830191a885..5c4aa3a31dd 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/Tests.hs
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/Tests.hs
@@ -4,23 +4,21 @@ import Test.Tasty
 import Test.Tasty.Extras
 
 import PlutusIR.Parser
+import PlutusIR.Pass.Test
 import PlutusIR.Test
 import PlutusIR.Transform.Unwrap
 
-import PlutusIR.Properties.Typecheck
+import Data.Functor.Identity
 import Test.QuickCheck.Property (Property, withMaxSuccess)
 
 test_unwrap :: TestTree
 test_unwrap = runTestNestedIn ["plutus-ir", "test", "PlutusIR", "Transform"] $
     testNested "Unwrap" $
         map
-            (goldenPir unwrapCancel pTerm)
-            -- Note: these examples don't typecheck, but we don't care
+            (goldenPir (runIdentity . runTestPass unwrapCancelPass) pTerm)
             [ "unwrapWrap"
-            , "wrapUnwrap"
             ]
 
--- | Check that a term typechecks after a `PlutusIR.Transform.Unwrap.unwrapCancel` pass.
-prop_TypecheckUnwrap :: Property
-prop_TypecheckUnwrap =
-    withMaxSuccess 3000 (pureTypecheckProp unwrapCancel)
+prop_unwrap :: Property
+prop_unwrap =
+  withMaxSuccess numTestsForPassProp $ testPassProp runIdentity unwrapCancelPass
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/unwrapWrap b/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/unwrapWrap
index 1b9b056f5d6..15fad79bbb4 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/unwrapWrap
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/unwrapWrap
@@ -1 +1,17 @@
-(unwrap (iwrap (con integer) (con integer) (con integer 1)))
+(abs a (type)
+  (unwrap
+    (iwrap
+      (lam list (fun (type) (type)) (lam a (type) (all r (type) (fun r (fun (fun a (fun [list a] r)) r)))))
+	  a
+      (abs r (type)
+        (lam z r
+          (lam
+            f
+            (fun a (fun (ifix (lam list (fun (type) (type)) (lam a (type) (all r (type) (fun r (fun (fun a (fun [list a] r)) r))))) a) r))
+            z
+          )
+        )
+      )
+    )
+  )
+)
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/unwrapWrap.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/unwrapWrap.golden
index 132831f390c..24aebcf99ce 100644
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/unwrapWrap.golden
+++ b/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/unwrapWrap.golden
@@ -1 +1,34 @@
-(con integer 1)
\ No newline at end of file
+(abs
+  a
+  (type)
+  (abs
+    r
+    (type)
+    (lam
+      z
+      r
+      (lam
+        f
+        (fun
+          a
+          (fun
+            (ifix
+              (lam
+                list
+                (fun (type) (type))
+                (lam
+                  a
+                  (type)
+                  (all r (type) (fun r (fun (fun a (fun [ list a ] r)) r)))
+                )
+              )
+              a
+            )
+            r
+          )
+        )
+        z
+      )
+    )
+  )
+)
\ No newline at end of file
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/wrapUnwrap b/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/wrapUnwrap
deleted file mode 100644
index 6e453ccea19..00000000000
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/wrapUnwrap
+++ /dev/null
@@ -1 +0,0 @@
-(iwrap (con integer) (con integer) (unwrap (con integer 1)))
diff --git a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/wrapUnwrap.golden b/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/wrapUnwrap.golden
deleted file mode 100644
index 53abe52ddea..00000000000
--- a/plutus-core/plutus-ir/test/PlutusIR/Transform/Unwrap/wrapUnwrap.golden
+++ /dev/null
@@ -1 +0,0 @@
-(iwrap (con integer) (con integer) (unwrap (con integer 1)))
\ No newline at end of file
diff --git a/plutus-core/testlib/PlutusIR/Pass/Test.hs b/plutus-core/testlib/PlutusIR/Pass/Test.hs
new file mode 100644
index 00000000000..3af3ce71f62
--- /dev/null
+++ b/plutus-core/testlib/PlutusIR/Pass/Test.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase        #-}
+{-# LANGUAGE RankNTypes        #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+module PlutusIR.Pass.Test where
+
+import Control.Exception (throw)
+import Control.Monad.Except
+import Data.Bifunctor (first)
+import Data.Functor
+import Data.Typeable
+import PlutusCore qualified as PLC
+import PlutusCore.Builtin
+import PlutusCore.Default (BuiltinSemanticsVariant (..))
+import PlutusCore.Generators.QuickCheck (forAllDoc)
+import PlutusCore.Pretty qualified as PLC
+import PlutusIR.Core.Type
+import PlutusIR.Error qualified as PIR
+import PlutusIR.Generators.QuickCheck
+import PlutusIR.Pass
+import PlutusIR.TypeCheck
+import PlutusIR.TypeCheck qualified as TC
+import Test.QuickCheck
+
+-- Convert Either Error () to Either String () to match with the Testable (Either String ())
+-- instance.
+convertToEitherString :: Either (PIR.Error PLC.DefaultUni PLC.DefaultFun ()) ()
+  -> Either String ()
+convertToEitherString = \case
+  Left err -> Left $ show err
+  Right () -> Right ()
+
+instance Arbitrary (BuiltinSemanticsVariant PLC.DefaultFun) where
+    arbitrary = elements [DefaultFunSemanticsVariant1, DefaultFunSemanticsVariant2]
+
+-- | An appropriate number of tests for a compiler pass property, so that we get some decent
+-- exploration of the program space. If you also take other arguments, then consider multiplying
+-- this up in order to account for the larger space.
+numTestsForPassProp :: Int
+numTestsForPassProp = 3000
+
+-- | Run a 'Pass' on a 'Term', setting up the typechecking config and throwing errors.
+runTestPass
+  :: (PLC.ThrowableBuiltins uni fun
+     , PLC.Typecheckable uni fun
+     , PLC.Pretty a
+     , Typeable a
+     , Monoid a
+     , Monad m
+     )
+  => (TC.PirTCConfig uni fun -> Pass m tyname name uni fun a)
+  -> Term tyname name uni fun a
+  -> m (Term tyname name uni fun a)
+runTestPass pass t = do
+  res <- runExceptT $ do
+    tcconfig <- TC.getDefTypeCheckConfig mempty
+    runPass (\_ -> pure ()) True (pass tcconfig) t
+  case res of
+    Left e  -> throw e
+    Right v -> pure v
+
+-- | Run a 'Pass' on generated 'Terms's, setting up the typechecking config
+-- and throwing errors.
+testPassProp ::
+  Monad m
+  => (forall a . m a -> a)
+  -> (TC.PirTCConfig PLC.DefaultUni PLC.DefaultFun
+      -> Pass m TyName Name PLC.DefaultUni PLC.DefaultFun ())
+  -> Property
+testPassProp exitMonad pass =
+  testPassProp'
+    ()
+    id
+    after
+    pass
+  where
+    after res = convertToEitherString $ first void $ exitMonad $ runExceptT res
+
+-- | A version of 'testPassProp' with more control, allowing some pre-processing
+-- of the term, and a more specific "exit" function.
+testPassProp' ::
+  forall m tyname name a prop
+  . (Monad m, Testable prop)
+  => a
+  -> (Term TyName Name PLC.DefaultUni PLC.DefaultFun ()
+      -> Term tyname name PLC.DefaultUni PLC.DefaultFun a)
+  -> (ExceptT (PIR.Error PLC.DefaultUni PLC.DefaultFun a) m () -> prop)
+  -> (TC.PirTCConfig PLC.DefaultUni PLC.DefaultFun
+      -> Pass m tyname name PLC.DefaultUni PLC.DefaultFun a)
+  -> Property
+testPassProp' ann before after pass =
+  forAllDoc "ty,tm" genTypeAndTerm_ (const []) $ \ (_ty, tm) ->
+    let
+      res :: ExceptT (PIR.Error PLC.DefaultUni PLC.DefaultFun a) m ()
+      res = do
+        tcconfig <- getDefTypeCheckConfig ann
+        let tm' = before tm
+        _ <- runPass (\_ -> pure ()) True (pass tcconfig) tm'
+        pure ()
+    in after res
diff --git a/plutus-core/testlib/PlutusIR/Properties/Typecheck.hs b/plutus-core/testlib/PlutusIR/Properties/Typecheck.hs
deleted file mode 100644
index f8977b7b109..00000000000
--- a/plutus-core/testlib/PlutusIR/Properties/Typecheck.hs
+++ /dev/null
@@ -1,97 +0,0 @@
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE LambdaCase        #-}
-{-# LANGUAGE TypeFamilies      #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
-
-
-{- | Typechecking property tests for all PIR compiler passes. Currently we only typecheck the term
- after a pass.
-
- There were test failures when we infer the type before a pass and check that the
- type after a pass is the same. The failures are probably caused by the
- `PlutusIR.TypeCheck.AllowEscape` typechecker config.
--}
-module PlutusIR.Properties.Typecheck where
-
-import Control.Monad.Reader
-import PlutusCore.Default
-import PlutusCore.Generators.QuickCheck.Utils
-import PlutusCore.Quote
-import PlutusCore.Rename
-import PlutusCore.TypeCheck qualified as PLC
-import PlutusIR.Compiler
-import PlutusIR.Core
-import PlutusIR.Generators.QuickCheck.GenerateTerms
-import PlutusIR.TypeCheck
-import PlutusPrelude (($>))
-import Test.QuickCheck (Property, elements)
-import Test.QuickCheck.Arbitrary
-
-instance Arbitrary (BuiltinSemanticsVariant DefaultFun) where
-    arbitrary = elements [DefaultFunSemanticsVariant1, DefaultFunSemanticsVariant2]
-
--- Convert Either Error () to Either String () to match with the Testable (Either String ())
--- instance.
-convertToEitherString :: Either (Error DefaultUni DefaultFun ()) ()
-  -> Either String ()
-convertToEitherString = \case
-  Left err -> Left $ show err
-  Right () -> Right ()
-
--- | Check that a term typechecks after one of the pure passes.
-pureTypecheckProp ::
-  -- | The pure simplification pass.
-  (Term TyName Name DefaultUni DefaultFun ()
-  -> Term TyName Name DefaultUni DefaultFun ())
-  -> Property
-pureTypecheckProp pass =
-  forAllDoc "ty,tm" genTypeAndTerm_ (const []) $ \ (_ty, tm) ->
-    convertToEitherString $ do
-      config <- getDefTypeCheckConfig ()
-      _ <- runQuoteT $ do
-        -- the generated term may not have globally unique names
-        renamed <- rename tm
-        inferType config (pass renamed)
-      pure ()
-
--- | Check that a term typechecks after a non-pure pass.
-nonPureTypecheckProp :: (Term TyName Name DefaultUni DefaultFun (Provenance ())
-  -> QuoteT
-      (Either (Error DefaultUni DefaultFun ()))
-      (Term TyName Name DefaultUni DefaultFun a))
-  -> Property
-nonPureTypecheckProp pass =
-  forAllDoc "ty,tm" genTypeAndTerm_ (const []) $ \ (_ty, tm) ->
-    convertToEitherString $ do
-      config <- getDefTypeCheckConfig ()
-      _ <- runQuoteT $ do
-        -- the generated term may not have globally unique names
-        processed <- pass =<< rename (Original () <$ tm)
-        inferType config (processed $> ())
-      pure ()
-
--- | Check that a term typechecks after a non-pure pass that requires extra constraints.
-extraConstraintTypecheckProp ::
-  (Term TyName Name DefaultUni DefaultFun (Provenance ())
-  -> QuoteT
-      (ReaderT
-         (CompilationCtx DefaultUni DefaultFun c)
-         (Either (Error DefaultUni DefaultFun b)))
-      (Term TyName Name DefaultUni DefaultFun a))
-  -> Property
-extraConstraintTypecheckProp pass =
-  forAllDoc "ty,tm" genTypeAndTerm_ (const []) $ \ (_ty, tm) ->
-    convertToEitherString $ do
-      config <- getDefTypeCheckConfig ()
-      plcConfig <- PLC.getDefTypeCheckConfig ()
-      let processed =
-            flip runReaderT (toDefaultCompilationCtx plcConfig) $
-              runQuoteT $ pass =<< rename (Original () <$ tm)
-      case processed of
-        Left err -> Left $ err $> ()
-        Right processSuccess -> do
-          _ <- runQuoteT $ do
-            -- need to rename because some passes don't preserve global uniqueness
-            renamedProcessed <- rename processSuccess
-            inferType config (renamedProcessed $> ())
-          pure ()
diff --git a/plutus-tx-plugin/src/PlutusTx/Plugin.hs b/plutus-tx-plugin/src/PlutusTx/Plugin.hs
index bdae60a2558..07f34f65a8e 100644
--- a/plutus-tx-plugin/src/PlutusTx/Plugin.hs
+++ b/plutus-tx-plugin/src/PlutusTx/Plugin.hs
@@ -471,12 +471,11 @@ runCompiler moduleName opts expr = do
             _                                      ->
                 AlwaysInline `elem` fmap annInline (toList ann)
     -- Compilation configuration
-    let pirTcConfig = if _posDoTypecheck opts
-                      -- pir's tc-config is based on plc tcconfig
-                      then Just $ PIR.PirTCConfig plcTcConfig PIR.YesEscape
-                      else Nothing
+    -- pir's tc-config is based on plc tcconfig
+    let pirTcConfig = PIR.PirTCConfig plcTcConfig PIR.YesEscape
         pirCtx = PIR.toDefaultCompilationCtx plcTcConfig
                  & set (PIR.ccOpts . PIR.coOptimize) (opts ^. posOptimize)
+                 & set (PIR.ccOpts . PIR.coTypecheck) (opts ^. posDoTypecheck)
                  & set (PIR.ccOpts . PIR.coPedantic) (opts ^. posPedantic)
                  & set (PIR.ccOpts . PIR.coVerbose) (opts ^. posVerbosity == Verbose)
                  & set (PIR.ccOpts . PIR.coDebug) (opts ^. posVerbosity == Debug)
diff --git a/plutus-tx-plugin/test/AsData/Budget/9.6/patternMatching.uplc.golden b/plutus-tx-plugin/test/AsData/Budget/9.6/patternMatching.uplc.golden
index ff58b4029f7..0a8a089e09a 100644
--- a/plutus-tx-plugin/test/AsData/Budget/9.6/patternMatching.uplc.golden
+++ b/plutus-tx-plugin/test/AsData/Budget/9.6/patternMatching.uplc.golden
@@ -35,10 +35,10 @@ program
                                   (addInteger cse))
                                (addInteger cse))
                             (addInteger cse))
-                         (case cse [(\x y z w -> w)]))
-                      (case cse [(\x y z w -> y)]))
+                         (case cse [(\x y z w -> y)]))
+                      (case cse [(\x y z w -> x)]))
                    (case cse [(\x y z w -> z)]))
-                (case cse [(\x y z w -> x)]))
+                (case cse [(\x y z w -> w)]))
              (\x y -> addInteger x y))
           (\x y ->
              force ifThenElse