diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,37 @@
+# Revision history of strict-checked-vars
+
+## 0.2.1.0 — 2025-05-15
+
+* Use `io-classes-1.8`.
+
+## 0.2.0.0
+
+* Remove 'Switch' modules. From now on, instead of switching _imports_, this
+  package switches the _representations_ of checked variables depending on the
+  `checkmvarinvariants` and `checktvarinvariants` flags. This solves a problem
+  where compiling projects that depend on `strict-checked-vars` might succeed
+  with a flag turned on but fail when it is turned off (and vice versa).
+
+* Add new `unsafeToUncheckedStrictMVar` and `unsafeToUncheckedStrictTVar`
+  functions.
+
+## 0.1.0.4
+
+* Propagate HasCallStack constraints in the `Switch` module for checked strict
+  MVars.
+
+## 0.1.0.3
+
+* Make `writeTVar` more strict.
+
+## 0.1.0.2
+
+* Make `newTVarWithInvariant`, `newTVarWithInvariantIO` and `newMVarWithInvariant` strict.
+
+## 0.1.0.1
+
+* Export `checkInvariant`.
+
+## 0.1.0.0
+
+* Initial version, not released on Hackage.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,177 @@
+
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
diff --git a/NOTICE b/NOTICE
new file mode 100644
--- /dev/null
+++ b/NOTICE
@@ -0,0 +1,14 @@
+Copyright 2019-2023 Input Output Global Inc (IOG).
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,63 @@
+# Strict `MVar`s and `TVar`s with invariant checking
+
+The `strict-checked-vars` package provides a strict interface to mutable
+variables (`MVar`) and `TVar`s with invariant checking. It builds on top of
+`strict-mvar`, `strict-stm` and `io-classes`, and thus it provides the interface
+for `MVar`/`TVar` implementations for both
+[IO](https://hackage.haskell.org/package/base-4.18.0.0/docs/Prelude.html#t:IO)
+and [io-sim](https://hackage.haskell.org/package/io-sim).
+
+## Checked and unchecked variants
+
+There are currently two variant implementations of `StrictTVar`s.
+* From `strict-stm`: `Control.Concurrent.Class.MonadSTM.Strict.TVar`
+* From `strict-checked-vars`: `Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked`
+
+Similarly, there are currently two variant implementations of `StrictMVar`s.
+* From `strict-mvar`: `Control.Concurrent.Class.MonadMVar.Strict`
+* From `strict-checked-vars`: `Control.Concurrent.Class.MonadMVar.Strict.Checked`
+
+
+The _unchecked_ modules provide the simplest implementation of strict variables:
+a light wrapper around lazy variables that forces values to WHNF before they are
+put inside the variable. The _checked_ module does the exact same thing, but it
+has the additional feature that the user can provide an invariant that is
+checked each time a new value is placed inside the variable. The checked modules
+are drop-in replacements for the unchecked modules, though invariants will be
+trivially true in that case. Non-trivial invariants can be set when creating a
+new variable.
+
+```haskell
+newMVarWithInvariant :: MonadMVar m
+                     => (a -> Maybe String)
+                     -> a
+                     -> m (StrictMVar m a)
+
+newEmptyMVarWithInvariant :: MonadMVar m
+                          => (a -> Maybe String)
+                          -> m (StrictMVar m a)
+
+newTVarWithInvariant :: (MonadSTM m, HasCallStack)
+                     => (a -> Maybe String)
+                     -> a
+                     -> STM m (StrictTVar m a)
+
+newTVarWithInvariantIO :: (MonadSTM m, HasCallStack)
+                       => (a -> Maybe String)
+                       -> a
+                       -> m (StrictTVar m a)
+```
+
+**Note:** though the checked modules are drop-in replacements for the unchecked
+modules, the `StrictMVar`/`StrictTVar` types are distinct. This means we can't
+make mixed use of the checked and unchecked modules.
+
+## Guarantees for invariant checking on `StrictMVar`s
+
+Although all functions that modify a checked `StrictMVar` will check the
+invariant, we do *not* guarantee that the value inside the `StrictMVar` always
+satisfies the invariant. Instead, we *do* guarantee that if the `StrictMVar` is
+updated with a value that does not satisfy the invariant, an exception is thrown
+*after* the new value is written to the `StrictMVar`. The reason for this weaker
+guarantee is that leaving an `MVar` empty can lead to very hard to debug
+"blocked indefinitely" problems.
diff --git a/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs b/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
@@ -0,0 +1,246 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | This module corresponds to "Control.Concurrent.MVar" in the @base@ package.
+--
+-- This module can be used as a drop-in replacement for
+-- "Control.Concurrent.Class.MonadMVar.Strict", but not the other way around.
+module Control.Concurrent.Class.MonadMVar.Strict.Checked
+  ( -- * StrictMVar
+    LazyMVar
+  , StrictMVar
+  , castStrictMVar
+  , fromLazyMVar
+  , isEmptyMVar
+  , modifyMVar
+  , modifyMVarMasked
+  , modifyMVarMasked_
+  , modifyMVar_
+  , newEmptyMVar
+  , newEmptyMVarWithInvariant
+  , newMVar
+  , newMVarWithInvariant
+  , putMVar
+  , readMVar
+  , swapMVar
+  , takeMVar
+  , toLazyMVar
+  , tryPutMVar
+  , tryReadMVar
+  , tryTakeMVar
+  , unsafeToUncheckedStrictMVar
+  , withMVar
+  , withMVarMasked
+
+    -- * Invariant
+  , checkInvariant
+
+    -- * Re-exports
+  , MonadMVar
+  ) where
+
+import Control.Concurrent.Class.MonadMVar.Strict (LazyMVar, MonadMVar)
+import Control.Concurrent.Class.MonadMVar.Strict qualified as Strict
+import Data.Kind (Type)
+import GHC.Stack (HasCallStack)
+
+{-------------------------------------------------------------------------------
+  StrictMVar
+-------------------------------------------------------------------------------}
+
+-- | A strict MVar with invariant checking.
+--
+-- There is a weaker invariant for a 'StrictMVar' than for a 'StrictTVar':
+-- although all functions that modify the 'StrictMVar' check the invariant, we
+-- do /not/ guarantee that the value inside the 'StrictMVar' always satisfies
+-- the invariant. Instead, we /do/ guarantee that if the 'StrictMVar' is updated
+-- with a value that does not satisfy the invariant, an exception is thrown. The
+-- reason for this weaker guarantee is that leaving an 'MVar' empty can lead to
+-- very hard to debug "blocked indefinitely" problems.
+type StrictMVar :: (Type -> Type) -> Type -> Type
+#if CHECK_MVAR_INVARIANTS
+data StrictMVar m a = StrictMVar {
+    -- | The invariant that is checked whenever the 'StrictMVar' is updated.
+    invariant :: !(a -> Maybe String)
+  , mvar      :: !(Strict.StrictMVar m a)
+  }
+#else
+newtype StrictMVar m a = StrictMVar {
+    mvar :: Strict.StrictMVar m a
+  }
+#endif
+
+castStrictMVar ::
+  LazyMVar m ~ LazyMVar n =>
+  StrictMVar m a -> StrictMVar n a
+castStrictMVar v = mkStrictMVar (getInvariant v) (Strict.castStrictMVar $ mvar v)
+
+-- | Get the underlying @MVar@
+--
+-- Since we obviously can not guarantee that updates to this 'LazyMVar' will be
+-- strict, this should be used with caution.
+--
+-- Similarly, we can not guarantee that updates to this 'LazyMVar' do not break
+-- the original invariant that the 'StrictMVar' held.
+toLazyMVar :: StrictMVar m a -> LazyMVar m a
+toLazyMVar = Strict.toLazyMVar . mvar
+
+-- | Create a 'StrictMVar' from a 'LazyMVar'
+--
+-- It is not guaranteed that the 'LazyMVar' contains a value that is in WHNF, so
+-- there is no guarantee that the resulting 'StrictMVar' contains a value that
+-- is in WHNF. This should be used with caution.
+--
+-- The resulting 'StrictMVar' has a trivial invariant.
+fromLazyMVar :: LazyMVar m a -> StrictMVar m a
+fromLazyMVar = mkStrictMVar (const Nothing) . Strict.fromLazyMVar
+
+-- | Create an unchecked reference to the given checked 'StrictMVar'.
+--
+-- Note that the invariant is only guaranteed when modifying the checked MVar.
+-- Any modification to the unchecked reference might break the invariants.
+unsafeToUncheckedStrictMVar :: StrictMVar m a -> Strict.StrictMVar m a
+unsafeToUncheckedStrictMVar = mvar
+
+newEmptyMVar :: MonadMVar m => m (StrictMVar m a)
+newEmptyMVar = mkStrictMVar (const Nothing) <$> Strict.newEmptyMVar
+
+newEmptyMVarWithInvariant ::
+  MonadMVar m =>
+  (a -> Maybe String) ->
+  m (StrictMVar m a)
+newEmptyMVarWithInvariant inv = mkStrictMVar inv <$> Strict.newEmptyMVar
+
+newMVar :: MonadMVar m => a -> m (StrictMVar m a)
+newMVar a = mkStrictMVar (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 ->
+  m (StrictMVar m a)
+newMVarWithInvariant inv !a =
+  checkInvariant (inv a) $
+    mkStrictMVar inv <$> Strict.newMVar a
+
+takeMVar :: MonadMVar m => StrictMVar m a -> m a
+takeMVar = Strict.takeMVar . mvar
+
+putMVar :: (HasCallStack, MonadMVar m) => StrictMVar m a -> a -> m ()
+putMVar v a = do
+  Strict.putMVar (mvar v) a
+  checkInvariant (getInvariant v a) $ pure ()
+
+readMVar :: MonadMVar m => StrictMVar m a -> m a
+readMVar v = Strict.readMVar (mvar v)
+
+swapMVar :: (HasCallStack, MonadMVar m) => StrictMVar m a -> a -> m a
+swapMVar v a = do
+  oldValue <- Strict.swapMVar (mvar v) a
+  checkInvariant (getInvariant v a) $ pure oldValue
+
+tryTakeMVar :: MonadMVar m => StrictMVar m a -> m (Maybe a)
+tryTakeMVar v = Strict.tryTakeMVar (mvar v)
+
+tryPutMVar :: (HasCallStack, MonadMVar m) => StrictMVar m a -> a -> m Bool
+tryPutMVar v a = do
+  didPut <- Strict.tryPutMVar (mvar v) a
+  checkInvariant (getInvariant v a) $ pure didPut
+
+isEmptyMVar :: MonadMVar m => StrictMVar m a -> m Bool
+isEmptyMVar v = Strict.isEmptyMVar (mvar v)
+
+withMVar :: MonadMVar m => StrictMVar m a -> (a -> m b) -> m b
+withMVar v = Strict.withMVar (mvar v)
+
+withMVarMasked :: MonadMVar m => StrictMVar m a -> (a -> m b) -> m b
+withMVarMasked v = Strict.withMVarMasked (mvar v)
+
+-- | 'modifyMVar_' is defined in terms of 'modifyMVar'.
+modifyMVar_ ::
+  (HasCallStack, MonadMVar m) =>
+  StrictMVar m a ->
+  (a -> m a) ->
+  m ()
+modifyMVar_ v io = modifyMVar v io'
+ where
+  io' a = (,()) <$> io a
+
+modifyMVar ::
+  (HasCallStack, MonadMVar m) =>
+  StrictMVar m a ->
+  (a -> m (a, b)) ->
+  m b
+modifyMVar v io = do
+  (a', b) <- Strict.modifyMVar (mvar v) io'
+  checkInvariant (getInvariant v a') $ pure b
+ where
+  io' a = do
+    (a', b) <- io a
+    -- Returning @a'@ along with @b@ allows us to check the invariant /after/
+    -- filling in the MVar.
+    pure (a', (a', b))
+
+-- | 'modifyMVarMasked_' is defined in terms of 'modifyMVarMasked'.
+modifyMVarMasked_ ::
+  (HasCallStack, MonadMVar m) =>
+  StrictMVar m a ->
+  (a -> m a) ->
+  m ()
+modifyMVarMasked_ v io = modifyMVarMasked v io'
+ where
+  io' a = (,()) <$> io a
+
+modifyMVarMasked ::
+  (HasCallStack, MonadMVar m) =>
+  StrictMVar m a ->
+  (a -> m (a, b)) ->
+  m b
+modifyMVarMasked v io = do
+  (a', b) <- Strict.modifyMVarMasked (mvar v) io'
+  checkInvariant (getInvariant v a') $ pure b
+ where
+  io' a = do
+    (a', b) <- io a
+    -- Returning @a'@ along with @b@ allows us to check the invariant /after/
+    -- filling in the MVar.
+    pure (a', (a', b))
+
+tryReadMVar :: MonadMVar m => StrictMVar m a -> m (Maybe a)
+tryReadMVar v = Strict.tryReadMVar (mvar v)
+
+--
+-- Dealing with invariants
+--
+
+-- | Check invariant (if enabled) before continuing
+--
+-- @checkInvariant mErr x@ is equal to @x@ if @mErr == Nothing@, and throws
+-- an error @err@ if @mErr == Just err@.
+--
+-- This is exported so that other code that wants to conditionally check
+-- invariants can reuse the same logic, rather than having to introduce new
+-- per-package flags.
+checkInvariant :: HasCallStack => Maybe String -> a -> a
+getInvariant :: StrictMVar m a -> a -> Maybe String
+mkStrictMVar :: (a -> Maybe String) -> Strict.StrictMVar m a -> StrictMVar m a
+
+#if CHECK_MVAR_INVARIANTS
+checkInvariant Nothing    k = k
+checkInvariant (Just err) _ = error $ "StrictMVar invariant violation: " ++ err
+getInvariant StrictMVar {invariant} = invariant
+mkStrictMVar invariant  mvar        = StrictMVar {invariant, mvar}
+#else
+checkInvariant _err       k  = k
+getInvariant _               = const Nothing
+mkStrictMVar _invariant mvar = StrictMVar {mvar}
+#endif
diff --git a/src/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs b/src/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs
@@ -0,0 +1,210 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | This module corresponds to "Control.Concurrent.STM.TVar" in the @stm@ package.
+--
+-- This module can be used as a drop-in replacement for
+-- "Control.Concurrent.Class.MonadSTM.Strict.TVar", but not the other way
+-- around.
+module Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked
+  ( -- * StrictTVar
+    LazyTVar
+  , StrictTVar
+  , castStrictTVar
+  , fromLazyTVar
+  , modifyTVar
+  , newTVar
+  , newTVarIO
+  , newTVarWithInvariant
+  , newTVarWithInvariantIO
+  , readTVar
+  , readTVarIO
+  , stateTVar
+  , swapTVar
+  , toLazyTVar
+  , unsafeToUncheckedStrictTVar
+  , writeTVar
+
+    -- * MonadLabelSTM
+  , labelTVar
+  , labelTVarIO
+
+    -- * MonadTraceSTM
+  , traceTVar
+  , traceTVarIO
+
+    -- * Invariant
+  , checkInvariant
+  ) where
+
+import Control.Concurrent.Class.MonadSTM
+  ( InspectMonadSTM
+  , MonadLabelledSTM
+  , MonadSTM
+  , MonadTraceSTM
+  , STM
+  , TraceValue
+  , atomically
+  )
+import Control.Concurrent.Class.MonadSTM.Strict.TVar qualified as Strict
+import GHC.Stack (HasCallStack)
+
+{-------------------------------------------------------------------------------
+  StrictTVar
+-------------------------------------------------------------------------------}
+
+type LazyTVar m = Strict.LazyTVar m
+
+#if CHECK_TVAR_INVARIANTS
+data StrictTVar m a = StrictTVar {
+    -- | Invariant checked whenever updating the 'StrictTVar'.
+    invariant :: !(a -> Maybe String)
+  , tvar      :: !(Strict.StrictTVar m a)
+  }
+#else
+newtype StrictTVar m a = StrictTVar {
+    tvar :: Strict.StrictTVar m a
+  }
+#endif
+
+castStrictTVar ::
+  LazyTVar m ~ LazyTVar n =>
+  StrictTVar m a -> StrictTVar n a
+castStrictTVar v = mkStrictTVar (getInvariant v) (Strict.castStrictTVar $ tvar v)
+
+-- | Get the underlying @TVar@
+--
+-- Since we obviously cannot guarantee that updates to this 'LazyTVar' will be
+-- strict, this should be used with caution.
+--
+-- Similarly, we can not guarantee that updates to this 'LazyTVar' do not break
+-- the original invariant that the 'StrictTVar' held.
+toLazyTVar :: StrictTVar m a -> LazyTVar m a
+toLazyTVar = Strict.toLazyTVar . tvar
+
+-- | Create a 'StrictMVar' from a 'LazyMVar'
+--
+-- It is not guaranteed that the 'LazyTVar' contains a value that is in WHNF, so
+-- there is no guarantee that the resulting 'StrictTVar' contains a value that
+-- is in WHNF. This should be used with caution.
+--
+-- The resulting 'StrictTVar' has a trivial invariant.
+fromLazyTVar :: LazyTVar m a -> StrictTVar m a
+fromLazyTVar = mkStrictTVar (const Nothing) . Strict.fromLazyTVar
+
+-- | Create an unchecked reference to the given checked 'StrictTVar'.
+--
+-- Note that the invariant is only guaranteed when modifying the checked TVar.
+-- Any modification to the unchecked reference might break the invariants.
+unsafeToUncheckedStrictTVar :: StrictTVar m a -> Strict.StrictTVar m a
+unsafeToUncheckedStrictTVar = tvar
+
+newTVar :: MonadSTM m => a -> STM m (StrictTVar m a)
+newTVar a = mkStrictTVar (const Nothing) <$> Strict.newTVar a
+
+newTVarIO :: MonadSTM m => a -> m (StrictTVar m a)
+newTVarIO = newTVarWithInvariantIO (const Nothing)
+
+newTVarWithInvariant ::
+  (MonadSTM m, HasCallStack) =>
+  (a -> Maybe String) ->
+  a ->
+  STM m (StrictTVar m a)
+newTVarWithInvariant inv !a =
+  checkInvariant (inv a) $
+    mkStrictTVar inv <$> Strict.newTVar a
+
+newTVarWithInvariantIO ::
+  (MonadSTM m, HasCallStack) =>
+  (a -> Maybe String) ->
+  a ->
+  m (StrictTVar m a)
+newTVarWithInvariantIO inv !a =
+  checkInvariant (inv a) $
+    mkStrictTVar inv <$> Strict.newTVarIO a
+
+readTVar :: MonadSTM m => StrictTVar m a -> STM m a
+readTVar = Strict.readTVar . tvar
+
+readTVarIO :: MonadSTM m => StrictTVar m a -> m a
+readTVarIO = Strict.readTVarIO . tvar
+
+writeTVar :: (MonadSTM m, HasCallStack) => StrictTVar m a -> a -> STM m ()
+writeTVar v !a =
+  checkInvariant (getInvariant v a) $
+    Strict.writeTVar (tvar v) a
+
+modifyTVar :: MonadSTM m => StrictTVar m a -> (a -> a) -> STM m ()
+modifyTVar v f = readTVar v >>= writeTVar v . f
+
+stateTVar :: MonadSTM m => StrictTVar m s -> (s -> (a, s)) -> STM m a
+stateTVar v f = do
+  a <- readTVar v
+  let (b, a') = f a
+  writeTVar v a'
+  return b
+
+swapTVar :: MonadSTM m => StrictTVar m a -> a -> STM m a
+swapTVar v a' = do
+  a <- readTVar v
+  writeTVar v a'
+  return a
+
+--
+-- Dealing with invariants
+--
+
+-- | Check invariant (if enabled) before continuing
+--
+-- @checkInvariant mErr x@ is equal to @x@ if @mErr == Nothing@, and throws
+-- an error @err@ if @mErr == Just err@.
+--
+-- This is exported so that other code that wants to conditionally check
+-- invariants can reuse the same logic, rather than having to introduce new
+-- per-package flags.
+checkInvariant :: HasCallStack => Maybe String -> a -> a
+getInvariant :: StrictTVar m a -> a -> Maybe String
+mkStrictTVar :: (a -> Maybe String) -> Strict.StrictTVar m a -> StrictTVar m a
+
+#if CHECK_TVAR_INVARIANTS
+checkInvariant Nothing    k = k
+checkInvariant (Just err) _ = error $ "StrictTVar invariant violation: " ++ err
+getInvariant StrictTVar {invariant} = invariant
+mkStrictTVar invariant  tvar        = StrictTVar {invariant, tvar}
+#else
+checkInvariant _err       k  = k
+getInvariant _               = const Nothing
+mkStrictTVar _invariant tvar = StrictTVar {tvar}
+#endif
+
+{-------------------------------------------------------------------------------
+  MonadLabelledSTM
+-------------------------------------------------------------------------------}
+
+labelTVar :: MonadLabelledSTM m => StrictTVar m a -> String -> STM m ()
+labelTVar = Strict.labelTVar . tvar
+
+labelTVarIO :: MonadLabelledSTM m => StrictTVar m a -> String -> m ()
+labelTVarIO v = atomically . labelTVar v
+
+{-------------------------------------------------------------------------------
+  MonadTraceSTM
+-------------------------------------------------------------------------------}
+
+traceTVar ::
+  MonadTraceSTM m =>
+  proxy m ->
+  StrictTVar m a ->
+  (Maybe a -> a -> InspectMonadSTM m TraceValue) ->
+  STM m ()
+traceTVar p = Strict.traceTVar p . tvar
+
+traceTVarIO ::
+  MonadTraceSTM m =>
+  StrictTVar m a ->
+  (Maybe a -> a -> InspectMonadSTM m TraceValue) ->
+  m ()
+traceTVarIO = Strict.traceTVarIO . tvar
diff --git a/strict-checked-vars.cabal b/strict-checked-vars.cabal
new file mode 100644
--- /dev/null
+++ b/strict-checked-vars.cabal
@@ -0,0 +1,114 @@
+cabal-version: 3.0
+name: strict-checked-vars
+version: 0.2.1.0
+synopsis:
+  Strict MVars and TVars with invariant checking for IO and IOSim
+
+description:
+  Strict @MVar@ and @TVar@ interfaces with invariant checking compatible with
+  [IO](https://hackage.haskell.org/package/base-4.18.0.0/docs/Prelude.html#t:IO)
+  & [io-sim](https://hackage.haskell.org/package/io-sim).
+
+license: Apache-2.0
+license-files:
+  LICENSE
+  NOTICE
+
+copyright: 2019-2023 Input Output Global Inc (IOG).
+author: IOG Engineering Team
+maintainer: operations@iohk.io, Joris Dral
+category: Concurrency
+build-type: Simple
+extra-doc-files:
+  CHANGELOG.md
+  README.md
+
+bug-reports: https://github.com/IntersectMBO/io-classes-extra/issues
+tested-with: ghc ==9.6 || ==9.8 || ==9.10 || ==9.12
+
+source-repository head
+  type: git
+  location: https://github.com/IntersectMBO/io-classes-extra
+  subdir: strict-checked-vars
+
+source-repository this
+  type: git
+  location: https://github.com/IntersectMBO/io-classes-extra
+  subdir: strict-checked-vars
+  tag: strict-checked-vars-0.2.1.0
+
+flag checkmvarinvariants
+  description: Enable runtime invariant checks on StrictMVars
+  manual: True
+  default: False
+
+flag checktvarinvariants
+  description: Enable runtime invariant checks on StrictTVars
+  manual: True
+  default: False
+
+library
+  hs-source-dirs: src
+  exposed-modules:
+    Control.Concurrent.Class.MonadMVar.Strict.Checked
+    Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked
+
+  default-language: Haskell2010
+  default-extensions: ImportQualifiedPost
+  build-depends:
+    base >=4.9 && <5,
+    io-classes:{io-classes, strict-mvar, strict-stm} ^>=1.8,
+
+  ghc-options:
+    -Wall
+    -Wcompat
+    -Wincomplete-uni-patterns
+    -Wincomplete-record-updates
+    -Wpartial-fields
+    -Widentities
+    -Wunused-packages
+
+  if flag(checkmvarinvariants)
+    cpp-options: -DCHECK_MVAR_INVARIANTS
+
+  if flag(checktvarinvariants)
+    cpp-options: -DCHECK_TVAR_INVARIANTS
+
+test-suite test
+  type: exitcode-stdio-1.0
+  hs-source-dirs: 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
+    Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked.WHNF
+    Test.Utils
+
+  default-language: Haskell2010
+  default-extensions: ImportQualifiedPost
+  build-depends:
+    QuickCheck,
+    base,
+    io-classes,
+    io-sim,
+    nothunks,
+    strict-checked-vars,
+    tasty,
+    tasty-quickcheck,
+
+  ghc-options:
+    -Wall
+    -Wcompat
+    -Wincomplete-uni-patterns
+    -Wincomplete-record-updates
+    -Wpartial-fields
+    -Widentities
+    -Wunused-packages
+    -fno-ignore-asserts
+
+  if flag(checkmvarinvariants)
+    cpp-options: -DCHECK_MVAR_INVARIANTS
+
+  if flag(checktvarinvariants)
+    cpp-options: -DCHECK_TVAR_INVARIANTS
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,18 @@
+module Main where
+
+import Test.Control.Concurrent.Class.MonadMVar.Strict.Checked qualified
+import Test.Control.Concurrent.Class.MonadMVar.Strict.Checked.WHNF qualified
+import Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked qualified
+import Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked.WHNF qualified
+import Test.Tasty (defaultMain, testGroup)
+
+main :: IO ()
+main =
+  defaultMain $
+    testGroup
+      "strict-checked-vars"
+      [ Test.Control.Concurrent.Class.MonadMVar.Strict.Checked.tests
+      , Test.Control.Concurrent.Class.MonadMVar.Strict.Checked.WHNF.tests
+      , Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked.tests
+      , Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked.WHNF.tests
+      ]
diff --git a/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs b/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Test.Control.Concurrent.Class.MonadMVar.Strict.Checked where
+
+import Control.Concurrent.Class.MonadMVar.Strict.Checked
+import Test.QuickCheck.Monadic
+import Test.Tasty
+import Test.Tasty.QuickCheck
+import Test.Utils
+
+tests :: TestTree
+tests =
+  testGroup
+    "Test.Control.Concurrent.Class.MonadMVar.Strict"
+    [ testGroup
+        "Checked"
+        [ testGroup
+            "IO"
+            [ testProperty "prop_invariantShouldFail" $
+                once $
+                  cppToggle $
+                    monadicIO prop_invariantShouldFail
+            , testProperty "prop_invariantShouldNotFail" $
+                once $
+                  monadicIO prop_invariantShouldNotFail
+            ]
+        , testGroup
+            "IOSim"
+            [ testProperty "prop_invariantShouldFail" $
+                once $
+                  cppToggle $
+                    monadicSim prop_invariantShouldFail
+            , testProperty "prop_invariantShouldNotFail" $
+                once $
+                  monadicSim prop_invariantShouldNotFail
+            ]
+        ]
+    ]
+
+-- | Invariant that checks whether an @Int@ is positive.
+invPositiveInt :: Int -> Maybe String
+invPositiveInt x
+  | x >= 0 = Nothing
+  | otherwise = Just $ "x<0 for x=" <> show x
+
+prop_invariantShouldNotFail :: MonadMVar m => PropertyM m ()
+prop_invariantShouldNotFail = run $ do
+  v <- newMVarWithInvariant invPositiveInt 0
+  modifyMVar_ v (\x -> pure $ x + 1)
+
+prop_invariantShouldFail :: MonadMVar m => PropertyM m ()
+prop_invariantShouldFail = run $ do
+  v <- newMVarWithInvariant invPositiveInt 0
+  modifyMVar_ v (\x -> pure $ x - 1)
+
+cppToggle :: Property -> Property
+#if CHECK_TVAR_INVARIANTS
+cppToggle = expectFailure
+#else
+cppToggle = id
+#endif
diff --git a/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked/WHNF.hs b/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked/WHNF.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked/WHNF.hs
@@ -0,0 +1,352 @@
+{-# 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 Control.Concurrent.Class.MonadMVar.Strict.Checked qualified as Checked
+import Control.Monad (void)
+import Control.Monad.IOSim (runSimOrThrow)
+import Data.Typeable (Typeable)
+import NoThunks.Class (OnlyCheckWhnf (..), unsafeNoThunks)
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.QuickCheck
+  ( Fun
+  , Property
+  , applyFun
+  , counterexample
+  , ioProperty
+  , property
+  , testProperty
+  , (.&&.)
+  )
+import Test.Utils (Invariant (..), (..:))
+
+{-------------------------------------------------------------------------------
+  Main test tree
+-------------------------------------------------------------------------------}
+
+tests :: TestTree
+tests =
+  testGroup
+    "WHNF"
+    [ testGroup "IO" testIO
+    , testGroup "IOSim" testIOSim
+    ]
+ where
+  testIO =
+    [ testProperty
+        "prop_IO_newMVarWithInvariant"
+        prop_IO_newMVarWithInvariant
+    , testProperty
+        "prop_IO_putMVar"
+        prop_IO_putMVar
+    , testProperty
+        "prop_IO_swapMVar"
+        prop_IO_swapMVar
+    , testProperty
+        "prop_IO_tryPutMVarJust"
+        prop_IO_tryPutMVarJust
+    , testProperty
+        "prop_IO_tryPutMVarNothing"
+        prop_IO_tryPutMVarNothing
+    , testProperty
+        "prop_IO_modifyMVar_"
+        prop_IO_modifyMVar_
+    , testProperty
+        "prop_IO_modifyMVar"
+        prop_IO_modifyMVar
+    , testProperty
+        "prop_IO_modifyMVarMasked_"
+        prop_IO_modifyMVarMasked_
+    , testProperty
+        "prop_IO_modifyMVarMasked"
+        prop_IO_modifyMVarMasked
+    ]
+
+  testIOSim =
+    [ testProperty
+        "prop_IOSim_newMVarWithInvariant"
+        prop_IOSim_newMVarWithInvariant
+    , testProperty
+        "prop_IOSim_putMVar"
+        prop_IOSim_putMVar
+    , testProperty
+        "prop_IOSim_swapMVar"
+        prop_IOSim_swapMVar
+    , testProperty
+        "prop_IOSim_tryPutMVarJust"
+        prop_IOSim_tryPutMVarJust
+    , testProperty
+        "prop_IOSim_tryPutMVarNothing"
+        prop_IOSim_tryPutMVarNothing
+    , testProperty
+        "prop_IOSim_modifyMVar_"
+        prop_IOSim_modifyMVar_
+    , testProperty
+        "prop_IOSim_modifyMVar"
+        prop_IOSim_modifyMVar
+    , testProperty
+        "prop_IOSim_modifyMVarMasked_"
+        prop_IOSim_modifyMVarMasked_
+    , testProperty
+        "prop_IOSim_modifyMVarMasked"
+        prop_IOSim_modifyMVarMasked
+    ]
+
+{-------------------------------------------------------------------------------
+  Utilities
+-------------------------------------------------------------------------------}
+
+isInWHNF :: (MonadMVar m, Typeable a) => StrictMVar m a -> m Property
+isInWHNF v = do
+  x <- readMVar v
+  pure $ case unsafeNoThunks (OnlyCheckWhnf x) of
+    Nothing -> property True
+    Just tinfo ->
+      counterexample ("Not in WHNF: " ++ show tinfo) $
+        property 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
+-------------------------------------------------------------------------------}
+
+--
+-- newMVarWithInvariant
+--
+
+-- | Test 'newMVarWithInvariant', not to be confused with
+-- 'Checked.newMVarWithInvariant'.
+prop_M_newMVarWithInvariant ::
+  MonadMVar m =>
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_M_newMVarWithInvariant inv x f = do
+  v <- newMVarWithInvariant inv (applyFun f x)
+  isInWHNF v
+
+prop_IO_newMVarWithInvariant :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IO_newMVarWithInvariant =
+  ioProperty
+    ..: prop_M_newMVarWithInvariant
+
+prop_IOSim_newMVarWithInvariant :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IOSim_newMVarWithInvariant inv x f =
+  runSimOrThrow $
+    prop_M_newMVarWithInvariant inv x f
+
+--
+-- putMVar
+--
+
+prop_M_putMVar ::
+  MonadMVar m =>
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_M_putMVar inv x f = do
+  v <- newEmptyMVarWithInvariant inv
+  putMVar v (applyFun f x)
+  isInWHNF v
+
+prop_IO_putMVar :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IO_putMVar =
+  ioProperty
+    ..: prop_M_putMVar
+
+prop_IOSim_putMVar :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IOSim_putMVar inv x f =
+  runSimOrThrow $
+    prop_M_putMVar inv x f
+
+--
+-- swapMVar
+--
+
+prop_M_swapMVar ::
+  MonadMVar m =>
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_M_swapMVar inv x f = do
+  v <- newMVarWithInvariant inv x
+  void $ swapMVar v (applyFun f x)
+  isInWHNF v
+
+prop_IO_swapMVar :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IO_swapMVar =
+  ioProperty
+    ..: prop_M_swapMVar
+
+prop_IOSim_swapMVar :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IOSim_swapMVar inv x f =
+  runSimOrThrow $
+    prop_M_swapMVar inv x f
+
+--
+-- tryPutMVar
+--
+
+prop_M_tryPutMVarJust ::
+  MonadMVar m =>
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_M_tryPutMVarJust inv x f = do
+  v <- newEmptyMVarWithInvariant inv
+  b <- tryPutMVar v (applyFun f x)
+  b' <- isInWHNF v
+  pure (property b .&&. b')
+
+prop_IO_tryPutMVarJust :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IO_tryPutMVarJust =
+  ioProperty
+    ..: prop_M_tryPutMVarJust
+
+prop_IOSim_tryPutMVarJust :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IOSim_tryPutMVarJust inv x f =
+  runSimOrThrow $
+    prop_M_tryPutMVarJust inv x f
+
+prop_M_tryPutMVarNothing ::
+  MonadMVar m =>
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_M_tryPutMVarNothing inv x f = do
+  v <- newMVarWithInvariant inv x
+  b <- tryPutMVar v (applyFun f x)
+  b' <- isInWHNF v
+  pure (property (not b) .&&. b')
+
+prop_IO_tryPutMVarNothing :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IO_tryPutMVarNothing =
+  ioProperty
+    ..: prop_M_tryPutMVarNothing
+prop_IOSim_tryPutMVarNothing :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IOSim_tryPutMVarNothing inv x f =
+  runSimOrThrow $
+    prop_M_tryPutMVarNothing inv x f
+
+--
+-- modifyMVar_
+--
+
+prop_M_modifyMVar_ ::
+  MonadMVar m =>
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_M_modifyMVar_ inv x f = do
+  v <- newMVarWithInvariant inv x
+  modifyMVar_ v (pure . applyFun f)
+  isInWHNF v
+
+prop_IO_modifyMVar_ :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IO_modifyMVar_ =
+  ioProperty
+    ..: prop_M_modifyMVar_
+
+prop_IOSim_modifyMVar_ :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IOSim_modifyMVar_ inv x f =
+  runSimOrThrow $
+    prop_M_modifyMVar_ inv x f
+
+--
+-- modifyMVar_
+--
+
+prop_M_modifyMVar ::
+  MonadMVar m =>
+  Invariant Int ->
+  Int ->
+  Fun Int (Int, Char) ->
+  m Property
+prop_M_modifyMVar inv x f = do
+  v <- newMVarWithInvariant inv x
+  void $ modifyMVar v (pure . applyFun f)
+  isInWHNF v
+
+prop_IO_modifyMVar :: Invariant Int -> Int -> Fun Int (Int, Char) -> Property
+prop_IO_modifyMVar =
+  ioProperty
+    ..: prop_M_modifyMVar
+
+prop_IOSim_modifyMVar :: Invariant Int -> Int -> Fun Int (Int, Char) -> Property
+prop_IOSim_modifyMVar inv x f =
+  runSimOrThrow $
+    prop_M_modifyMVar inv x f
+
+--
+-- modifyMVarMasked_
+--
+
+prop_M_modifyMVarMasked_ ::
+  MonadMVar m =>
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_M_modifyMVarMasked_ inv x f = do
+  v <- newMVarWithInvariant inv x
+  void $ modifyMVarMasked_ v (pure . applyFun f)
+  isInWHNF v
+
+prop_IO_modifyMVarMasked_ :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IO_modifyMVarMasked_ =
+  ioProperty
+    ..: prop_M_modifyMVarMasked_
+
+prop_IOSim_modifyMVarMasked_ :: Invariant Int -> Int -> Fun Int Int -> Property
+prop_IOSim_modifyMVarMasked_ inv x f =
+  runSimOrThrow $
+    prop_M_modifyMVarMasked_ inv x f
+
+--
+-- modifyMVarMasked
+--
+
+prop_M_modifyMVarMasked ::
+  MonadMVar m =>
+  Invariant Int ->
+  Int ->
+  Fun Int (Int, Char) ->
+  m Property
+prop_M_modifyMVarMasked inv x f = do
+  v <- newMVarWithInvariant inv x
+  void $ modifyMVarMasked v (pure . applyFun f)
+  isInWHNF v
+
+prop_IO_modifyMVarMasked :: Invariant Int -> Int -> Fun Int (Int, Char) -> Property
+prop_IO_modifyMVarMasked =
+  ioProperty
+    ..: prop_M_modifyMVarMasked
+
+prop_IOSim_modifyMVarMasked :: Invariant Int -> Int -> Fun Int (Int, Char) -> Property
+prop_IOSim_modifyMVarMasked inv x f =
+  runSimOrThrow $
+    prop_M_modifyMVarMasked inv x f
diff --git a/test/Test/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs b/test/Test/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked where
+
+import Control.Concurrent.Class.MonadSTM (MonadSTM, atomically)
+import Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked
+import Test.QuickCheck.Monadic
+import Test.Tasty
+import Test.Tasty.QuickCheck
+import Test.Utils
+
+tests :: TestTree
+tests =
+  testGroup
+    "Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked"
+    [ testGroup
+        "Checked"
+        [ testGroup
+            "IO"
+            [ testProperty "prop_invariantShouldFail" $
+                once $
+                  cppToggle $
+                    monadicIO prop_invariantShouldFail
+            , testProperty "prop_invariantShouldNotFail" $
+                once $
+                  monadicIO prop_invariantShouldNotFail
+            ]
+        , testGroup
+            "IOSim"
+            [ testProperty "prop_invariantShouldFail" $
+                once $
+                  cppToggle $
+                    monadicSim prop_invariantShouldFail
+            , testProperty "prop_invariantShouldNotFail" $
+                once $
+                  monadicSim prop_invariantShouldNotFail
+            ]
+        ]
+    ]
+
+-- | Invariant that checks whether an @Int@ is positive.
+invPositiveInt :: Int -> Maybe String
+invPositiveInt x
+  | x >= 0 = Nothing
+  | otherwise = Just $ "x<0 for x=" <> show x
+
+prop_invariantShouldNotFail :: MonadSTM m => PropertyM m ()
+prop_invariantShouldNotFail = run $ atomically $ do
+  v <- newTVarWithInvariant invPositiveInt 0
+  modifyTVar v (+ 1)
+
+prop_invariantShouldFail :: MonadSTM m => PropertyM m ()
+prop_invariantShouldFail = run $ atomically $ do
+  v <- newTVarWithInvariant invPositiveInt 0
+  modifyTVar v (subtract 1)
+
+cppToggle :: Property -> Property
+#if CHECK_TVAR_INVARIANTS
+cppToggle = expectFailure
+#else
+cppToggle = id
+#endif
diff --git a/test/Test/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked/WHNF.hs b/test/Test/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked/WHNF.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked/WHNF.hs
@@ -0,0 +1,332 @@
+{-# 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 Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked qualified as Checked
+import Control.Monad (void)
+import Control.Monad.IOSim (runSimOrThrow)
+import Data.Typeable (Typeable)
+import NoThunks.Class (OnlyCheckWhnf (..), unsafeNoThunks)
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.QuickCheck
+  ( Fun
+  , Property
+  , applyFun
+  , counterexample
+  , ioProperty
+  , property
+  , testProperty
+  )
+import Test.Utils (Invariant (..), (..:))
+
+{-------------------------------------------------------------------------------
+  Main test tree
+-------------------------------------------------------------------------------}
+
+tests :: TestTree
+tests =
+  testGroup
+    "Test.Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked.WHNF"
+    [ testGroup "IO" testIO
+    , testGroup "IOSim" testIOSim
+    ]
+ where
+  testIO =
+    [ testProperty
+        "prop_newTVarWithInvariant_IO"
+        prop_newTVarWithInvariant_IO
+    , testProperty
+        "prop_newTVarWithInvariantIO_IO"
+        prop_newTVarWithInvariantIO_IO
+    , testProperty
+        "prop_writeTVar_IO"
+        prop_writeTVar_IO
+    , testProperty
+        "prop_modifyTVar_IO"
+        prop_modifyTVar_IO
+    , testProperty
+        "prop_stateTVar_IO"
+        prop_stateTVar_IO
+    , testProperty
+        "prop_swapTVar_IO"
+        prop_swapTVar_IO
+    ]
+
+  testIOSim =
+    [ testProperty
+        "prop_newTVarWithInvariant_IOSim"
+        prop_newTVarWithInvariant_IOSim
+    , testProperty
+        "prop_newTVarWithInvariantIO_IOSim"
+        prop_newTVarWithInvariantIO_IOSim
+    , testProperty
+        "prop_writeTVar_IOSim"
+        prop_writeTVar_IOSim
+    , testProperty
+        "prop_modifyTVar_IOSim"
+        prop_modifyTVar_IOSim
+    , testProperty
+        "prop_stateTVar"
+        prop_stateTVar_IOSim
+    , testProperty
+        "prop_swapTVar"
+        prop_swapTVar_IOSim
+    ]
+
+{-------------------------------------------------------------------------------
+  Utilities
+-------------------------------------------------------------------------------}
+
+isInWHNF :: (MonadSTM m, Typeable a) => StrictTVar m a -> m Property
+isInWHNF v = do
+  x <- readTVarIO v
+  pure $ case unsafeNoThunks (OnlyCheckWhnf x) of
+    Nothing -> property True
+    Just tinfo ->
+      counterexample ("Not in WHNF: " ++ show tinfo) $
+        property 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
+
+-- | The 'isInWHNF' check fails when running tests in 'IOSim', since 'IOSim'
+-- runs in the lazy 'ST' monad. 'withSanityCheckWhnf' can be used to perform the
+-- test conditionally.
+withSanityCheckWhnf ::
+  (MonadSTM m, Typeable a) =>
+  Bool ->
+  StrictTVar m a ->
+  m Property
+withSanityCheckWhnf check v =
+  if check
+    then
+      isInWHNF v
+    else
+      pure $ property True
+
+{-------------------------------------------------------------------------------
+  Properties
+-------------------------------------------------------------------------------}
+
+--
+-- newTVarWithInvariant
+--
+
+-- | Test 'newTVarWithInvariant', not to be confused with
+-- 'Checked.newTVarWithInvariant'.
+prop_newTVarWithInvariant_M ::
+  MonadSTM m =>
+  Bool ->
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_newTVarWithInvariant_M check inv x f = do
+  v <- atomically $ newTVarWithInvariant inv (applyFun f x)
+  withSanityCheckWhnf check v
+
+prop_newTVarWithInvariant_IO ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_newTVarWithInvariant_IO =
+  ioProperty
+    ..: prop_newTVarWithInvariant_M True
+
+prop_newTVarWithInvariant_IOSim ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_newTVarWithInvariant_IOSim inv x f =
+  runSimOrThrow $
+    prop_newTVarWithInvariant_M False inv x f
+
+--
+-- newTVarWithInvariantIO
+--
+
+-- | Test 'newTVarWithInvariantIO', not to be confused with
+-- 'Checked.newTVarWithInvariantIO'.
+prop_newTVarWithInvariantIO_M ::
+  MonadSTM m =>
+  Bool ->
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_newTVarWithInvariantIO_M check inv x f = do
+  v <- newTVarWithInvariantIO inv (applyFun f x)
+  withSanityCheckWhnf check v
+
+prop_newTVarWithInvariantIO_IO ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_newTVarWithInvariantIO_IO =
+  ioProperty
+    ..: prop_newTVarWithInvariantIO_M True
+
+prop_newTVarWithInvariantIO_IOSim ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_newTVarWithInvariantIO_IOSim inv x f =
+  runSimOrThrow $
+    prop_newTVarWithInvariantIO_M False inv x f
+
+--
+-- writeTVar
+--
+
+prop_writeTVar_M ::
+  MonadSTM m =>
+  Bool ->
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_writeTVar_M check inv x f = do
+  v <- newTVarWithInvariantIO inv x
+  atomically $ writeTVar v (applyFun f x)
+  withSanityCheckWhnf check v
+
+prop_writeTVar_IO ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_writeTVar_IO =
+  ioProperty
+    ..: prop_writeTVar_M True
+
+prop_writeTVar_IOSim ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_writeTVar_IOSim inv x f =
+  runSimOrThrow $
+    prop_writeTVar_M False inv x f
+
+--
+-- modifyTVar
+--
+
+prop_modifyTVar_M ::
+  MonadSTM m =>
+  Bool ->
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_modifyTVar_M check inv x f = do
+  v <- newTVarWithInvariantIO inv x
+  atomically $ modifyTVar v (applyFun f)
+  withSanityCheckWhnf check v
+
+prop_modifyTVar_IO ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_modifyTVar_IO =
+  ioProperty
+    ..: prop_modifyTVar_M True
+
+prop_modifyTVar_IOSim ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_modifyTVar_IOSim inv x f =
+  runSimOrThrow $
+    prop_modifyTVar_M False inv x f
+
+--
+-- stateTVar
+--
+
+prop_stateTVar_M ::
+  MonadSTM m =>
+  Bool ->
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_stateTVar_M check inv x f = do
+  v <- newTVarWithInvariantIO inv x
+  atomically $ stateTVar v (((),) . applyFun f)
+  withSanityCheckWhnf check v
+
+prop_stateTVar_IO ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_stateTVar_IO =
+  ioProperty
+    ..: prop_stateTVar_M True
+
+prop_stateTVar_IOSim ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_stateTVar_IOSim inv x f =
+  runSimOrThrow $
+    prop_stateTVar_M False inv x f
+
+--
+-- swapTVar
+--
+
+prop_swapTVar_M ::
+  MonadSTM m =>
+  Bool ->
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  m Property
+prop_swapTVar_M check inv x f = do
+  v <- newTVarWithInvariantIO inv x
+  void $ atomically $ swapTVar v (applyFun f x)
+  withSanityCheckWhnf check v
+
+prop_swapTVar_IO ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_swapTVar_IO =
+  ioProperty
+    ..: prop_swapTVar_M True
+
+prop_swapTVar_IOSim ::
+  Invariant Int ->
+  Int ->
+  Fun Int Int ->
+  Property
+prop_swapTVar_IOSim inv x f =
+  runSimOrThrow $
+    prop_swapTVar_M False inv x f
diff --git a/test/Test/Utils.hs b/test/Test/Utils.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Utils.hs
@@ -0,0 +1,77 @@
+{-# 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 (Arbitrary (..), Gen, Property, Testable (..), elements)
+import Test.QuickCheck.Gen.Unsafe (Capture (..), capture)
+import Test.QuickCheck.Monadic (PropertyM, monadic')
+
+{-------------------------------------------------------------------------------
+  Property runners (copied from "Ouroboros.Network.Testing.QuickCheck")
+-------------------------------------------------------------------------------}
+
+runSimGen :: (forall s. Gen (IOSim s a)) -> Gen a
+runSimGen f = do
+  Capture eval <- capture
+  return $ runSimOrThrow (eval f)
+
+monadicSim :: Testable a => (forall s. PropertyM (IOSim s) a) -> Property
+monadicSim m = property (runSimGen (monadic' m))
+
+{-------------------------------------------------------------------------------
+  Function composition
+-------------------------------------------------------------------------------}
+
+infixr 9 ..:
+
+(..:) :: (y -> z) -> (x0 -> x1 -> x2 -> y) -> (x0 -> x1 -> x2 -> z)
+(..:) g f x0 x1 x2 = g (f x0 x1 x2)
+
+{-------------------------------------------------------------------------------
+  Invariants
+-------------------------------------------------------------------------------}
+
+-- | Invariants
+--
+-- Testing with @'Invariant' (const Nothing)'@ /should/ be the same as testing
+-- with 'NoInvariant'.
+data Invariant a
+  = NoInvariant
+  | Invariant String (a -> Maybe String)
+
+instance Show (Invariant a) where
+  show NoInvariant = "NoInvariant"
+  show (Invariant name _) = "Invariant " <> name
+
+instance Typeable a => Arbitrary (Invariant a) where
+  arbitrary =
+    elements
+      [ noInvariant
+      , whnfInvariant
+      , trivialInvariant
+      ]
+
+noInvariant :: Invariant a
+noInvariant = NoInvariant
+
+whnfInvariant :: Typeable a => Invariant a
+whnfInvariant = Invariant "WHNF" $ fmap show . unsafeNoThunks . OnlyCheckWhnf
+
+trivialInvariant :: Invariant a
+trivialInvariant = Invariant "Trivial" $ const Nothing