diff --git a/strict-checked-vars/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs b/strict-checked-vars/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
index 581dccabd..49929bf23 100644
--- a/strict-checked-vars/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
+++ b/strict-checked-vars/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
@@ -96,6 +96,10 @@ newEmptyMVarWithInvariant inv = StrictMVar inv <$> Strict.newEmptyMVar
 newMVar :: MonadMVar m => a -> m (StrictMVar m a)
 newMVar a = StrictMVar (const Nothing) <$> Strict.newMVar a
 
+-- | Create a 'StrictMVar' with an invariant.
+--
+-- Contrary to functions that modify a 'StrictMVar', this function checks the
+-- invariant /before/ putting the value in a new 'StrictMVar'.
 newMVarWithInvariant :: (HasCallStack, MonadMVar m)
                      => (a -> Maybe String)
                      -> a
diff --git a/strict-checked-vars/strict-checked-vars.cabal b/strict-checked-vars/strict-checked-vars.cabal
index 6334a0f9f..c3ee536dd 100644
--- a/strict-checked-vars/strict-checked-vars.cabal
+++ b/strict-checked-vars/strict-checked-vars.cabal
@@ -73,12 +73,16 @@ test-suite test
   main-is:          Main.hs
   other-modules:
     Test.Control.Concurrent.Class.MonadMVar.Strict.Checked
+    Test.Control.Concurrent.Class.MonadMVar.Strict.Checked.WHNF
+    Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked.WHNF
     Test.Utils
 
   default-language: Haskell2010
   build-depends:
     , base                 >=4.9 && <4.19
+    , io-classes
     , io-sim
+    , nothunks
     , QuickCheck
     , strict-checked-vars
     , tasty
diff --git a/strict-checked-vars/test/Main.hs b/strict-checked-vars/test/Main.hs
index 4b7213dbc..cc170dd78 100644
--- a/strict-checked-vars/test/Main.hs
+++ b/strict-checked-vars/test/Main.hs
@@ -1,9 +1,11 @@
 module Main where
 
-import qualified Test.Control.Concurrent.Class.MonadMVar.Strict.Checked as Checked
-import           Test.Tasty
+import qualified Test.Control.Concurrent.Class.MonadMVar.Strict.Checked as Test.StrictMVar.Checked
+import qualified Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked.WHNF as Test.StrictTVar.Checked
+import           Test.Tasty (defaultMain, testGroup)
 
 main :: IO ()
 main = defaultMain $ testGroup "strict-checked-vars" [
-      Checked.tests
+      Test.StrictMVar.Checked.tests
+    , Test.StrictTVar.Checked.tests
     ]
diff --git a/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs b/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
index bdedfa2d4..039746e62 100644
--- a/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
+++ b/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
@@ -3,6 +3,7 @@
 module Test.Control.Concurrent.Class.MonadMVar.Strict.Checked where
 
 import           Control.Concurrent.Class.MonadMVar.Strict.Checked
+import qualified Test.Control.Concurrent.Class.MonadMVar.Strict.Checked.WHNF as Test.WHNF
 import           Test.QuickCheck.Monadic
 import           Test.Tasty
 import           Test.Tasty.QuickCheck
@@ -23,6 +24,7 @@ tests = testGroup "Test.Control.Concurrent.Class.MonadMVar.Strict" [
             , testProperty "prop_invariantShouldNotFail" $
                 once                 $ monadicSim prop_invariantShouldNotFail
             ]
+        , Test.WHNF.tests
         ]
     ]
 
diff --git a/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked/WHNF.hs b/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked/WHNF.hs
new file mode 100644
index 000000000..d249e2821
--- /dev/null
+++ b/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked/WHNF.hs
@@ -0,0 +1,208 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Test.Control.Concurrent.Class.MonadMVar.Strict.Checked.WHNF where
+
+import           Control.Concurrent.Class.MonadMVar.Strict.Checked hiding
+                     (newEmptyMVar, newEmptyMVarWithInvariant, newMVar,
+                     newMVarWithInvariant)
+import qualified Control.Concurrent.Class.MonadMVar.Strict.Checked as Checked
+import           Control.Monad (void)
+import           Data.Typeable (Typeable)
+import           NoThunks.Class (OnlyCheckWhnf (OnlyCheckWhnf), unsafeNoThunks)
+import           Test.QuickCheck.Monadic (PropertyM, monadicIO, monitor, run)
+import           Test.Tasty (TestTree, testGroup)
+import           Test.Tasty.QuickCheck (Fun, applyFun, counterexample,
+                     testProperty)
+import           Test.Utils (Invariant (..), monadicSim, noInvariant,
+                     trivialInvariant, whnfInvariant, (.:))
+
+{-------------------------------------------------------------------------------
+  Main test tree
+-------------------------------------------------------------------------------}
+
+tests :: TestTree
+tests = testGroup "WHNF" [
+      testGroup "IO" [
+          testIO    "No invariant"      noInvariant
+        , testIO    "Trivial invariant" trivialInvariant
+        , testIO    "WHNF invariant"    whnfInvariant
+        ]
+    , testGroup "IOSim" [
+          testIOSim "No invariant"      noInvariant
+        , testIOSim "Trivial invariant" trivialInvariant
+        , testIOSim "WHNF invariant"    whnfInvariant
+        ]
+    ]
+  where
+    testIO name inv = testGroup name [
+          testProperty "prop_newMVarWithInvariant" $
+            monadicIO .: prop_newMVarWithInvariant inv
+        , testProperty "prop_putMVar" $
+            monadicIO .: prop_putMVar inv
+        , testProperty "prop_swapMVar" $
+            monadicIO .: prop_swapMVar inv
+        , testProperty "prop_tryPutMVarJust" $
+            monadicIO .: prop_tryPutMVarNothing inv
+        , testProperty "prop_tryPutMVarNothing" $
+            monadicIO .: prop_tryPutMVarNothing inv
+        , testProperty "prop_modifyMVar_" $
+            monadicIO .: prop_modifyMVar_ inv
+        , testProperty "prop_modifyMVar" $
+            monadicIO .: prop_modifyMVar inv
+        , testProperty "prop_modifyMVarMasked_" $
+            monadicIO .: prop_modifyMVarMasked_ inv
+        , testProperty "prop_modifyMVarMasked" $
+            monadicIO .: prop_modifyMVarMasked inv
+        ]
+
+    testIOSim name inv = testGroup name [
+          testProperty "prop_newMVarWithInvariant" $ \x f ->
+            monadicSim $ prop_newMVarWithInvariant inv x f
+        , testProperty "prop_putMVar" $ \x f ->
+            monadicSim $ prop_putMVar inv x f
+        , testProperty "prop_swapMVar" $ \x f ->
+            monadicSim $ prop_swapMVar inv x f
+        , testProperty "prop_tryPutMVarJust" $ \x f ->
+            monadicSim $ prop_tryPutMVarJust inv x f
+        , testProperty "prop_tryPutMVarNothing" $ \x f ->
+            monadicSim $ prop_tryPutMVarNothing inv x f
+        , testProperty "prop_modifyMVar_" $ \x f ->
+            monadicSim $ prop_modifyMVar_ inv x f
+        , testProperty "prop_modifyMVar" $ \x f ->
+            monadicSim $ prop_modifyMVar inv x f
+        , testProperty "prop_modifyMVarMasked_" $ \x f ->
+            monadicSim $ prop_modifyMVarMasked_ inv x f
+        , testProperty "prop_modifyMVarMasked" $ \x f ->
+            monadicSim $ prop_modifyMVarMasked inv x f
+        ]
+
+{-------------------------------------------------------------------------------
+  Utilities
+-------------------------------------------------------------------------------}
+
+isInWHNF :: (MonadMVar m, Typeable a) => StrictMVar m a -> PropertyM m Bool
+isInWHNF v = do
+    x <- run $ readMVar v
+    case unsafeNoThunks (OnlyCheckWhnf x) of
+      Nothing    -> pure True
+      Just tinfo -> monitor (counterexample $ "Not in WHNF: " ++ show tinfo)
+                 >> pure False
+
+-- | Wrapper around 'Checked.newMVar' and 'Checked.newMVarWithInvariant'.
+newMVarWithInvariant :: MonadMVar m => Invariant a -> a -> m (StrictMVar m a)
+newMVarWithInvariant = \case
+    NoInvariant   -> Checked.newMVar
+    Invariant inv -> Checked.newMVarWithInvariant inv
+
+-- | Wrapper around 'Checked.newEmptyMVar' and
+-- 'Checked.newEmptyMVarWithInvariant'.
+newEmptyMVarWithInvariant :: MonadMVar m => Invariant a -> m (StrictMVar m a)
+newEmptyMVarWithInvariant = \case
+    NoInvariant   -> Checked.newEmptyMVar
+    Invariant inv -> Checked.newEmptyMVarWithInvariant inv
+
+{-------------------------------------------------------------------------------
+  Properties
+-------------------------------------------------------------------------------}
+
+-- | Test 'newMVarWithInvariant', not to be confused with
+-- 'Checked.newMVarWithInvariant'.
+prop_newMVarWithInvariant ::
+     MonadMVar m
+  => Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_newMVarWithInvariant inv x f = do
+    v <- run $ newMVarWithInvariant inv (applyFun f x)
+    isInWHNF v
+
+prop_putMVar ::
+     MonadMVar m
+  => Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_putMVar inv x f = do
+    v <- run $ newEmptyMVarWithInvariant inv
+    run $ putMVar v (applyFun f x)
+    isInWHNF v
+
+prop_swapMVar ::
+     MonadMVar m
+  => Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_swapMVar inv x f = do
+    v <- run $ newMVarWithInvariant inv x
+    void $ run $ swapMVar v (applyFun f x)
+    isInWHNF v
+
+prop_tryPutMVarJust ::
+     MonadMVar m
+  => Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_tryPutMVarJust inv x f = do
+    v <- run $ newEmptyMVarWithInvariant inv
+    b <- run $ tryPutMVar v (applyFun f x)
+    b' <- isInWHNF v
+    pure (b && b')
+
+prop_tryPutMVarNothing ::
+     MonadMVar m
+  => Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_tryPutMVarNothing inv x f = do
+    v <- run $ newMVarWithInvariant inv x
+    b <- run $ tryPutMVar v (applyFun f x)
+    b' <- isInWHNF v
+    pure (not b && b')
+
+prop_modifyMVar_ ::
+     MonadMVar m
+  => Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_modifyMVar_ inv x f = do
+    v <-  run $ newMVarWithInvariant inv x
+    run $ modifyMVar_ v (pure . applyFun f)
+    isInWHNF v
+
+prop_modifyMVar ::
+     MonadMVar m
+  => Invariant Int
+  -> Int
+  -> Fun Int (Int, Char)
+  -> PropertyM m Bool
+prop_modifyMVar inv x f =do
+    v <-  run $ newMVarWithInvariant inv x
+    void $ run $ modifyMVar v (pure . applyFun f)
+    isInWHNF v
+
+prop_modifyMVarMasked_ ::
+     MonadMVar m
+  => Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_modifyMVarMasked_ inv x f =do
+    v <-  run $ newMVarWithInvariant inv x
+    void $ run $ modifyMVarMasked_ v (pure . applyFun f)
+    isInWHNF v
+
+prop_modifyMVarMasked ::
+     MonadMVar m
+  => Invariant Int
+  -> Int
+  -> Fun Int (Int, Char)
+  -> PropertyM m Bool
+prop_modifyMVarMasked inv x f =do
+    v <-  run $ newMVarWithInvariant inv x
+    void $ run $ modifyMVarMasked v (pure . applyFun f)
+    isInWHNF v
diff --git a/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked/WHNF.hs b/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked/WHNF.hs
new file mode 100644
index 000000000..b561a470a
--- /dev/null
+++ b/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked/WHNF.hs
@@ -0,0 +1,192 @@
+{-# LANGUAGE LambdaCase    #-}
+{-# LANGUAGE TupleSections #-}
+
+module Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked.WHNF where
+
+import           Control.Concurrent.Class.MonadSTM (MonadSTM, STM, atomically)
+import           Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked hiding
+                     (newTVar, newTVarIO, newTVarWithInvariant,
+                     newTVarWithInvariantIO)
+import qualified Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked as Checked
+import           Control.Monad (void)
+import           Data.Typeable (Typeable)
+import           NoThunks.Class (OnlyCheckWhnf (OnlyCheckWhnf), unsafeNoThunks)
+import           Test.QuickCheck.Monadic (PropertyM, monadicIO, monitor, run)
+import           Test.Tasty (TestTree, testGroup)
+import           Test.Tasty.QuickCheck (Fun, applyFun, counterexample,
+                     testProperty)
+import           Test.Utils (Invariant (..), monadicSim, noInvariant,
+                     trivialInvariant, whnfInvariant, (.:))
+
+{-------------------------------------------------------------------------------
+  Main test tree
+-------------------------------------------------------------------------------}
+
+tests :: TestTree
+tests = testGroup "Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked.WHNF" [
+      testGroup "IO" [
+          testIO    "No invariant"      sanityCheckWhnf   noInvariant
+        , testIO    "Trivial invariant" sanityCheckWhnf   trivialInvariant
+        , testIO    "WHNF invariant"    sanityCheckWhnf   whnfInvariant
+        ]
+      -- Sanity checks for WHNF fail in IOSim because IOSim runs in the lazy ST
+      -- monad, so we turn off sanity checks here.
+    , testGroup "IOSim" [
+          testIOSim "No invariant"      noSanityCheckWhnf noInvariant
+        , testIOSim "Trivial invariant" noSanityCheckWhnf trivialInvariant
+        , testIOSim "WHNF invariant"    noSanityCheckWhnf whnfInvariant
+        ]
+    ]
+  where
+    testIO name check inv = testGroup name [
+          testProperty "prop_newTVarWithInvariant" $
+            monadicIO .: prop_newTVarWithInvariant check inv
+        , testProperty "prop_newTVarWithInvariantIO" $
+            monadicIO .: prop_newTVarWithInvariantIO check inv
+        , testProperty "prop_writeTVar" $
+            monadicIO .: prop_writeTVar check inv
+        , testProperty "prop_modifyTVar" $
+            monadicIO .: prop_modifyTVar check inv
+        , testProperty "prop_stateTVar" $
+            monadicIO .: prop_stateTVar check inv
+        , testProperty "prop_swapTVar" $
+            monadicIO .: prop_swapTVar check inv
+        ]
+
+    testIOSim name check inv = testGroup name [
+          testProperty "prop_newTVarWithInvariant" $ \x f ->
+            monadicSim $ prop_newTVarWithInvariant check inv x f
+        , testProperty "prop_newTVarWithInvariantIO" $ \x f ->
+            monadicSim $ prop_newTVarWithInvariantIO check inv x f
+        , testProperty "prop_writeTVar" $ \x f ->
+            monadicSim $ prop_writeTVar check inv x f
+        , testProperty "prop_modifyTVar" $ \x f ->
+            monadicSim $ prop_modifyTVar check inv x f
+        , testProperty "prop_stateTVar" $ \x f ->
+            monadicSim $ prop_stateTVar check inv x f
+        , testProperty "prop_swapTVar" $ \x f ->
+            monadicSim $ prop_swapTVar check inv x f
+        ]
+
+{-------------------------------------------------------------------------------
+  Utilities
+-------------------------------------------------------------------------------}
+
+
+isInWHNF :: (MonadSTM m, Typeable a) => StrictTVar m a -> PropertyM m Bool
+isInWHNF v = do
+    x <- run $ readTVarIO v
+    case unsafeNoThunks (OnlyCheckWhnf x) of
+      Nothing    -> pure True
+      Just tinfo -> monitor (counterexample $ "Not in WHNF: " ++ show tinfo)
+                 >> pure False
+
+-- | Wrapper around 'Checked.newTVar' and 'Checked.newTVarWithInvariant'.
+newTVarWithInvariant :: MonadSTM m => Invariant a -> a -> STM m (StrictTVar m a)
+newTVarWithInvariant = \case
+    NoInvariant   -> Checked.newTVar
+    Invariant inv -> Checked.newTVarWithInvariant inv
+
+-- | Wrapper around 'Checked.newTVarIO' and 'Checked.newTVarWithInvariantIO'.
+newTVarWithInvariantIO :: MonadSTM m => Invariant a -> a -> m (StrictTVar m a)
+newTVarWithInvariantIO = \case
+    NoInvariant   -> Checked.newTVarIO
+    Invariant inv -> Checked.newTVarWithInvariantIO inv
+
+newtype SanityCheckWhnf = SanityCheckWhnf { getSanityCheckWhnf :: Bool }
+  deriving (Show, Eq)
+
+noSanityCheckWhnf :: SanityCheckWhnf
+noSanityCheckWhnf = SanityCheckWhnf False
+
+sanityCheckWhnf :: SanityCheckWhnf
+sanityCheckWhnf = SanityCheckWhnf True
+
+withSanityCheckWhnf ::
+     (MonadSTM m, Typeable a)
+  => SanityCheckWhnf
+  -> StrictTVar m a
+  -> PropertyM m Bool
+withSanityCheckWhnf check v =
+    if getSanityCheckWhnf check then
+      isInWHNF v
+    else
+      pure True
+
+{-------------------------------------------------------------------------------
+  Properties
+-------------------------------------------------------------------------------}
+
+-- | Test 'newTVarWithInvariant', not to be confused with
+-- 'Checked.newTVarWithInvariant'.
+prop_newTVarWithInvariant ::
+     MonadSTM m
+  => SanityCheckWhnf
+  -> Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_newTVarWithInvariant check inv x f = do
+    v <- run $ atomically $ newTVarWithInvariant inv (applyFun f x)
+    withSanityCheckWhnf check v
+
+-- | Test 'newTVarWithInvariantIO', not to be confused with
+-- 'Checked.newTVarWithInvariantIO'.
+prop_newTVarWithInvariantIO ::
+     MonadSTM m
+  => SanityCheckWhnf
+  -> Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_newTVarWithInvariantIO check inv x f = do
+    v <- run $ newTVarWithInvariantIO inv (applyFun f x)
+    withSanityCheckWhnf check v
+
+prop_writeTVar ::
+     MonadSTM m
+  => SanityCheckWhnf
+  -> Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_writeTVar check inv x f = do
+    v <- run $ newTVarWithInvariantIO inv x
+    run $ atomically $ writeTVar v (applyFun f x)
+    withSanityCheckWhnf check v
+
+prop_modifyTVar ::
+     MonadSTM m
+  => SanityCheckWhnf
+  -> Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_modifyTVar check inv x f = do
+    v <- run $ newTVarWithInvariantIO inv x
+    run $ atomically $ modifyTVar v (applyFun f)
+    withSanityCheckWhnf check v
+
+prop_stateTVar ::
+     MonadSTM m
+  => SanityCheckWhnf
+  -> Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_stateTVar check inv x f = do
+    v <- run $ newTVarWithInvariantIO inv x
+    run $ atomically $ stateTVar v (((),) . applyFun f)
+    withSanityCheckWhnf check v
+
+prop_swapTVar ::
+     MonadSTM m
+  => SanityCheckWhnf
+  -> Invariant Int
+  -> Int
+  -> Fun Int Int
+  -> PropertyM m Bool
+prop_swapTVar check inv x f = do
+    v <- run $ newTVarWithInvariantIO inv x
+    void $ run $ atomically $ swapTVar v (applyFun f x)
+    withSanityCheckWhnf check v
diff --git a/strict-checked-vars/test/Test/Utils.hs b/strict-checked-vars/test/Test/Utils.hs
index 8600a2c6d..2788b6b8c 100644
--- a/strict-checked-vars/test/Test/Utils.hs
+++ b/strict-checked-vars/test/Test/Utils.hs
@@ -1,11 +1,21 @@
 {-# LANGUAGE RankNTypes #-}
 
 module Test.Utils (
+    -- * Property runners
     monadicSim
   , runSimGen
+    -- * Function composition
+  , (.:)
+    -- * Invariants
+  , Invariant (..)
+  , noInvariant
+  , trivialInvariant
+  , whnfInvariant
   ) where
 
 import           Control.Monad.IOSim (IOSim, runSimOrThrow)
+import           Data.Typeable (Typeable)
+import           NoThunks.Class (OnlyCheckWhnf (..), unsafeNoThunks)
 import           Test.QuickCheck (Gen, Property, Testable (..))
 import           Test.QuickCheck.Gen.Unsafe (Capture (..), capture)
 import           Test.QuickCheck.Monadic (PropertyM, monadic')
@@ -21,3 +31,33 @@ runSimGen f = do
 
 monadicSim :: Testable a => (forall s. PropertyM (IOSim s) a) -> Property
 monadicSim m = property (runSimGen (monadic' m))
+
+{-------------------------------------------------------------------------------
+  Function composition
+-------------------------------------------------------------------------------}
+
+infixr 9 .:
+
+(.:) :: (y -> z) -> (x0 -> x1 -> y) -> (x0 -> x1 -> z)
+(.:) g f x0 x1 = g (f x0 x1)
+
+{-------------------------------------------------------------------------------
+  Invariants
+-------------------------------------------------------------------------------}
+
+-- | Invariants
+--
+-- Testing with @'Invariant' (const Nothing)'@ /should/ be the same as testing
+-- with 'NoInvariant'.
+data Invariant a =
+    NoInvariant
+  | Invariant (a -> Maybe String)
+
+noInvariant :: Invariant a
+noInvariant = NoInvariant
+
+whnfInvariant :: Typeable a => Invariant a
+whnfInvariant = Invariant $ fmap show . unsafeNoThunks . OnlyCheckWhnf
+
+trivialInvariant :: Invariant a
+trivialInvariant = Invariant $ const Nothing