diff --git a/changelog.d/5-internal/in-mem-specs b/changelog.d/5-internal/in-mem-specs
new file mode 100644
index 0000000000..57fd8d6b57
--- /dev/null
+++ b/changelog.d/5-internal/in-mem-specs
@@ -0,0 +1 @@
+Added laws for DefaultSsoCode, Now, IdP and ScimExternalIdStore
diff --git a/services/spar/package.yaml b/services/spar/package.yaml
index fc27e3fb8a..935e8cbfe0 100644
--- a/services/spar/package.yaml
+++ b/services/spar/package.yaml
@@ -99,7 +99,7 @@ tests:
       - QuickCheck
       - spar
       - uri-bytestring
-      - polysemy-check
+      - polysemy-check >= 0.9
 
 executables:
   spar:
diff --git a/services/spar/spar.cabal b/services/spar/spar.cabal
index a71562b0f4..cc6c8bb789 100644
--- a/services/spar/spar.cabal
+++ b/services/spar/spar.cabal
@@ -4,7 +4,7 @@ cabal-version: 1.12
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 34138a2c7fa249191ae03bc1581a7c95c94b12080f104da084a9bc37ac54c9ad
+-- hash: 4a323def34cfdc7673cea02e13fe518d53d7b04bae552bff2d0784dfb6964162
 
 name:           spar
 version:        0.1
@@ -514,8 +514,11 @@ test-suite spec
       Test.Spar.Intra.BrigSpec
       Test.Spar.Roundtrip.ByteString
       Test.Spar.ScimSpec
+      Test.Spar.Sem.DefaultSsoCodeSpec
       Test.Spar.Sem.IdPRawMetadataStoreSpec
       Test.Spar.Sem.IdPSpec
+      Test.Spar.Sem.NowSpec
+      Test.Spar.Sem.ScimExternalIdStoreSpec
       Test.Spar.TypesSpec
       Paths_spar
   hs-source-dirs:
@@ -564,7 +567,7 @@ test-suite spec
     , network-uri
     , optparse-applicative
     , polysemy
-    , polysemy-check
+    , polysemy-check >=0.9
     , polysemy-plugin
     , raw-strings-qq
     , retry
diff --git a/services/spar/src/Spar/Sem/DefaultSsoCode.hs b/services/spar/src/Spar/Sem/DefaultSsoCode.hs
index c18f0334b1..9f594c16b4 100644
--- a/services/spar/src/Spar/Sem/DefaultSsoCode.hs
+++ b/services/spar/src/Spar/Sem/DefaultSsoCode.hs
@@ -9,4 +9,6 @@ data DefaultSsoCode m a where
   Store :: SAML.IdPId -> DefaultSsoCode m ()
   Delete :: DefaultSsoCode m ()
 
+deriving instance Show (DefaultSsoCode m a)
+
 makeSem ''DefaultSsoCode
diff --git a/services/spar/src/Spar/Sem/Now.hs b/services/spar/src/Spar/Sem/Now.hs
index 63d8e740ad..f5a701b1a0 100644
--- a/services/spar/src/Spar/Sem/Now.hs
+++ b/services/spar/src/Spar/Sem/Now.hs
@@ -9,6 +9,8 @@ data Now m a where
 
 makeSem ''Now
 
+deriving instance Show (Now m a)
+
 -- | Check a time against 'Now', checking if it's still alive (hasn't occurred yet.)
 boolTTL ::
   Member Now r =>
diff --git a/services/spar/src/Spar/Sem/ScimExternalIdStore.hs b/services/spar/src/Spar/Sem/ScimExternalIdStore.hs
index b2a43f6b32..3978108770 100644
--- a/services/spar/src/Spar/Sem/ScimExternalIdStore.hs
+++ b/services/spar/src/Spar/Sem/ScimExternalIdStore.hs
@@ -10,4 +10,6 @@ data ScimExternalIdStore m a where
   Lookup :: TeamId -> Email -> ScimExternalIdStore m (Maybe UserId)
   Delete :: TeamId -> Email -> ScimExternalIdStore m ()
 
+deriving instance Show (ScimExternalIdStore m a)
+
 makeSem ''ScimExternalIdStore
diff --git a/services/spar/test/Arbitrary.hs b/services/spar/test/Arbitrary.hs
index bc7ca9fae4..a5536460c6 100644
--- a/services/spar/test/Arbitrary.hs
+++ b/services/spar/test/Arbitrary.hs
@@ -23,7 +23,7 @@
 module Arbitrary where
 
 import Data.Aeson
-import Data.Id (TeamId)
+import Data.Id (TeamId, UserId)
 import Data.Proxy
 import Data.String.Conversions (cs)
 import Data.Swagger hiding (Header (..))
@@ -97,6 +97,8 @@ instance Arbitrary E.Replaced where
 
 instance CoArbitrary a => CoArbitrary (E.GetIdPResult a)
 
+-- TODO(sandy): IdPIds are unlikely to collide. Does the size parameter
+-- affect them?
 instance CoArbitrary IdPId
 
 instance CoArbitrary WireIdP
@@ -105,6 +107,10 @@ instance CoArbitrary WireIdPAPIVersion
 
 instance CoArbitrary TeamId
 
+instance CoArbitrary UserId
+
+instance CoArbitrary Time
+
 instance CoArbitrary Issuer where
   coarbitrary (Issuer ur) = coarbitrary $ show ur
 
diff --git a/services/spar/test/Test/Spar/Sem/DefaultSsoCodeSpec.hs b/services/spar/test/Test/Spar/Sem/DefaultSsoCodeSpec.hs
new file mode 100644
index 0000000000..9a638ba990
--- /dev/null
+++ b/services/spar/test/Test/Spar/Sem/DefaultSsoCodeSpec.hs
@@ -0,0 +1,173 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
+
+module Test.Spar.Sem.DefaultSsoCodeSpec where
+
+import Arbitrary ()
+import Imports
+import Polysemy
+import Polysemy.Check
+import SAML2.WebSSO.Types
+import qualified Spar.Sem.DefaultSsoCode as E
+import Spar.Sem.DefaultSsoCode.Mem
+import Test.Hspec
+import Test.Hspec.QuickCheck
+import Test.QuickCheck
+
+deriveGenericK ''E.DefaultSsoCode
+
+propsForInterpreter ::
+  PropConstraints r f =>
+  String ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Spec
+propsForInterpreter interpreter lower = do
+  describe interpreter $ do
+    prop "delete/delete" $ prop_deleteDelete Nothing lower
+    prop "delete/get" $ prop_deleteGet Nothing lower
+    prop "delete/store" $ prop_deleteStore Nothing lower
+    prop "get/store" $ prop_getStore Nothing lower
+    prop "store/delete" $ prop_storeStore Nothing lower
+    prop "store/get" $ prop_storeGet Nothing lower
+    prop "store/store" $ prop_storeStore Nothing lower
+
+spec :: Spec
+spec = modifyMaxSuccess (const 1000) $ do
+  propsForInterpreter "defaultSsoCodeToMem" $ pure . run . defaultSsoCodeToMem
+
+-- | All the constraints we need to generalize properties in this module.
+-- A regular type synonym doesn't work due to dreaded impredicative
+-- polymorphism.
+class
+  (Functor f, Member E.DefaultSsoCode r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+instance
+  (Functor f, Member E.DefaultSsoCode r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+prop_storeGet ::
+  PropConstraints r f =>
+  Maybe (f (Maybe IdPId) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_storeGet =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    s <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.store s
+            E.get
+        )
+        ( do
+            E.store s
+            pure (Just s)
+        )
+
+prop_getStore ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_getStore =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    pure $
+      simpleLaw
+        ( do
+            E.get >>= maybe (pure ()) E.store
+        )
+        ( do
+            pure ()
+        )
+
+prop_storeDelete ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_storeDelete =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    s <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.store s
+            E.delete
+        )
+        ( do
+            E.delete
+        )
+
+prop_deleteStore ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_deleteStore =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    s <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.delete
+            E.store s
+        )
+        ( do
+            E.store s
+        )
+
+prop_storeStore ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_storeStore =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    s <- arbitrary
+    s' <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.store s
+            E.store s'
+        )
+        ( do
+            E.store s'
+        )
+
+prop_deleteDelete ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_deleteDelete =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    pure $
+      simpleLaw
+        ( do
+            E.delete
+            E.delete
+        )
+        ( do
+            E.delete
+        )
+
+prop_deleteGet ::
+  PropConstraints r f =>
+  Maybe (f (Maybe IdPId) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_deleteGet =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    pure $
+      simpleLaw
+        ( do
+            E.delete
+            E.get
+        )
+        ( do
+            E.delete
+            pure Nothing
+        )
diff --git a/services/spar/test/Test/Spar/Sem/IdPRawMetadataStoreSpec.hs b/services/spar/test/Test/Spar/Sem/IdPRawMetadataStoreSpec.hs
index c1d5f6b9b8..28aa64122d 100644
--- a/services/spar/test/Test/Spar/Sem/IdPRawMetadataStoreSpec.hs
+++ b/services/spar/test/Test/Spar/Sem/IdPRawMetadataStoreSpec.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
 
@@ -15,97 +16,121 @@ import Test.QuickCheck
 
 deriveGenericK ''E.IdPRawMetadataStore
 
+class
+  (Functor f, Member E.IdPRawMetadataStore r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+instance
+  (Functor f, Member E.IdPRawMetadataStore r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
 prop_storeGetRaw ::
-  Member E.IdPRawMetadataStore r =>
-  (forall a. Sem r a -> IO (RawState, a)) ->
+  PropConstraints r f =>
+  Maybe (f (Maybe Text) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
   Property
-prop_storeGetRaw x =
+prop_storeGetRaw =
   prepropLaw @'[E.IdPRawMetadataStore]
     ( do
         idpid <- arbitrary
         t <- arbitrary
-        pure
-          ( do
-              E.store idpid t
-              E.get idpid,
-            do
-              E.store idpid t
-              pure (Just t)
-          )
+        pure $
+          simpleLaw
+            ( do
+                E.store idpid t
+                E.get idpid
+            )
+            ( do
+                E.store idpid t
+                pure (Just t)
+            )
     )
-    x
 
 prop_storeStoreRaw ::
-  Member E.IdPRawMetadataStore r =>
-  (forall a. Sem r a -> IO (RawState, a)) ->
+  PropConstraints r f =>
+  Maybe (f (Maybe Text) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
   Property
-prop_storeStoreRaw x =
+prop_storeStoreRaw =
   prepropLaw @'[E.IdPRawMetadataStore]
     ( do
         idpid <- arbitrary
         t1 <- arbitrary
         t2 <- arbitrary
-        pure
-          ( do
-              E.store idpid t1
-              E.store idpid t2,
-            do
-              E.store idpid t2
-          )
+        pure $
+          simpleLaw
+            ( do
+                E.store idpid t1
+                E.store idpid t2
+                E.get idpid
+            )
+            ( do
+                E.store idpid t2
+                E.get idpid
+            )
     )
-    x
 
 prop_storeDeleteRaw ::
-  Member E.IdPRawMetadataStore r =>
-  (forall a. Sem r a -> IO (RawState, a)) ->
+  PropConstraints r f =>
+  Maybe (f (Maybe Text) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
   Property
-prop_storeDeleteRaw x =
-  prepropLaw @'[E.IdPRawMetadataStore]
-    ( do
-        idpid <- arbitrary
-        t <- arbitrary
-        pure
+prop_storeDeleteRaw =
+  prepropLaw @'[E.IdPRawMetadataStore] $
+    do
+      idpid <- arbitrary
+      t <- arbitrary
+      pure $
+        simpleLaw
           ( do
               E.store idpid t
-              E.delete idpid,
-            do
               E.delete idpid
+              E.get idpid
+          )
+          ( do
+              E.delete idpid
+              E.get idpid
           )
-    )
-    x
 
 prop_deleteGetRaw ::
-  Member E.IdPRawMetadataStore r =>
-  (forall a. Sem r a -> IO (RawState, a)) ->
+  PropConstraints r f =>
+  Maybe (f (Maybe Text) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
   Property
-prop_deleteGetRaw x =
+prop_deleteGetRaw =
   prepropLaw @'[E.IdPRawMetadataStore]
     ( do
         idpid <- arbitrary
-        pure
-          ( do
-              E.delete idpid
-              E.get idpid,
-            do
-              E.delete idpid
-              pure Nothing
-          )
+        t <- arbitrary
+        pure $
+          Law
+            { lawLhs = do
+                E.delete idpid
+                E.get idpid,
+              lawRhs = do
+                E.delete idpid
+                pure Nothing,
+              lawPrelude =
+                [ E.store idpid t
+                ],
+              lawPostlude = [] @(Sem _ ())
+            }
     )
-    x
 
 testInterpreter :: Sem '[E.IdPRawMetadataStore] a -> IO (RawState, a)
 testInterpreter = pure . run . idpRawMetadataStoreToMem
 
 propsForInterpreter ::
-  Member E.IdPRawMetadataStore r =>
-  (forall a. Sem r a -> IO (RawState, a)) ->
+  PropConstraints r f =>
+  (forall x. f x -> x) ->
+  (forall a. Sem r a -> IO (f a)) ->
   Spec
-propsForInterpreter lower = do
-  prop "store/store" $ prop_storeStoreRaw lower
-  prop "store/get" $ prop_storeGetRaw lower
-  prop "store/deleteRawMetadata" $ prop_storeDeleteRaw lower
-  prop "deleteRawMetadata/get" $ prop_deleteGetRaw lower
+propsForInterpreter extract lower = do
+  prop "store/store" $ prop_storeStoreRaw (Just $ constructorLabel . extract) lower
+  prop "store/get" $ prop_storeGetRaw (Just $ constructorLabel . extract) lower
+  prop "store/delete" $ prop_storeDeleteRaw (Just $ constructorLabel . extract) lower
+  prop "delete/get" $ prop_deleteGetRaw (Just $ constructorLabel . extract) lower
 
 spec :: Spec
 spec = modifyMaxSuccess (const 1000) $ do
-  propsForInterpreter testInterpreter
+  propsForInterpreter snd testInterpreter
diff --git a/services/spar/test/Test/Spar/Sem/IdPSpec.hs b/services/spar/test/Test/Spar/Sem/IdPSpec.hs
index 162f5b1625..ef1eba1f47 100644
--- a/services/spar/test/Test/Spar/Sem/IdPSpec.hs
+++ b/services/spar/test/Test/Spar/Sem/IdPSpec.hs
@@ -1,72 +1,322 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE StandaloneDeriving #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
 
 module Test.Spar.Sem.IdPSpec where
 
 import Arbitrary ()
+import Control.Arrow
 import Control.Lens
+import Data.Data (Data)
 import Imports
 import Polysemy
 import Polysemy.Check
 import SAML2.WebSSO.Types
+import qualified SAML2.WebSSO.Types as SAML
 import qualified Spar.Sem.IdP as E
 import Spar.Sem.IdP.Mem
 import Test.Hspec
 import Test.Hspec.QuickCheck
 import Test.QuickCheck
+import qualified Wire.API.User.IdentityProvider as IP
 
 deriveGenericK ''E.IdP
 
+deriving instance Data (E.GetIdPResult IdPId)
+
+deriving instance Data (IdPId)
+
+propsForInterpreter ::
+  (Member E.IdP r, PropConstraints r f) =>
+  String ->
+  (forall x. f x -> x) ->
+  (forall x. Show x => Maybe (f x -> String)) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Spec
+propsForInterpreter interpreter extract labeler lower = do
+  describe interpreter $ do
+    prop "deleteConfig/deleteConfig" $ prop_deleteDelete Nothing lower
+    prop "deleteConfig/getConfig" $ prop_deleteGet labeler lower
+    prop "getConfig/storeConfig" $ prop_getStore (Just $ show . (() <$) . extract) lower
+    prop "getConfig/getConfig" $ prop_getGet (Just $ show . ((() <$) *** (() <$)) . extract) lower
+    prop "setReplacedBy/clearReplacedBy" $ prop_setClear labeler lower
+    prop "setReplacedBy/getReplacedBy" $ prop_setGet (Just $ show . (fmap (() <$)) . extract) lower
+    prop "setReplacedBy/setReplacedBy" $ prop_setSet (Just $ show . (fmap (() <$)) . extract) lower
+    prop "storeConfig/getConfig" $ prop_storeGet (Just $ show . (() <$) . extract) lower
+    prop "storeConfig/getIdByIssuerWithoutTeam" $ prop_storeGetByIssuer (Just $ constructorLabel . extract) lower
+    prop "storeConfig/storeConfig (different keys)" $ prop_storeStoreInterleave Nothing lower
+    prop "storeConfig/storeConfig (same keys)" $ prop_storeStore Nothing lower
+
+spec :: Spec
+spec = modifyMaxSuccess (const 1000) $ do
+  propsForInterpreter "idPToMem" snd (Just $ show . snd) $ pure . run . idPToMem
+
+getReplacedBy :: Member E.IdP r => SAML.IdPId -> Sem r (Maybe (Maybe SAML.IdPId))
+getReplacedBy idpid = fmap (view $ SAML.idpExtraInfo . IP.wiReplacedBy) <$> E.getConfig idpid
+
+-- | All the constraints we need to generalize properties in this module.
+-- A regular type synonym doesn't work due to dreaded impredicative
+-- polymorphism.
+class
+  (Functor f, Member E.IdP r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+instance
+  (Functor f, Member E.IdP r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+prop_storeStore ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Property
+prop_storeStore =
+  prepropLaw @'[E.IdP] $ do
+    s <- arbitrary
+    s' <- arbitrary
+    pure $
+      Law
+        { lawLhs = do
+            E.storeConfig $ s & SAML.idpId .~ s' ^. SAML.idpId
+            E.storeConfig s',
+          lawRhs = do
+            E.storeConfig s',
+          lawPrelude = [],
+          lawPostlude = [E.getConfig $ s' ^. SAML.idpId]
+        }
+
+prop_storeStoreInterleave ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Property
+prop_storeStoreInterleave =
+  prepropLaw @'[E.IdP] $ do
+    s <- arbitrary
+    s' <- arbitrary
+    !_ <-
+      when (s ^. SAML.idpId == s' ^. SAML.idpId) discard
+    pure $
+      Law
+        { lawLhs = do
+            E.storeConfig s
+            E.storeConfig s',
+          lawRhs = do
+            E.storeConfig s'
+            E.storeConfig s,
+          lawPrelude = [],
+          lawPostlude = [E.getConfig $ s ^. SAML.idpId, E.getConfig $ s' ^. SAML.idpId]
+        }
+
 prop_storeGet ::
-  Member E.IdP r =>
-  (forall a. Sem r a -> IO (TypedState, a)) ->
+  PropConstraints r f =>
+  Maybe (f (Maybe IP.IdP) -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
   Property
-prop_storeGet x =
-  prepropLaw @'[E.IdP]
-    ( do
-        s <- arbitrary
-        pure
+prop_storeGet =
+  prepropLaw @'[E.IdP] $
+    do
+      s <- arbitrary
+      pure $
+        simpleLaw
           ( do
               E.storeConfig s
-              E.getConfig $ s ^. idpId,
-            do
+              E.getConfig $ s ^. idpId
+          )
+          ( do
               E.storeConfig s
               pure (Just s)
           )
-    )
-    x
+
+prop_deleteGet ::
+  PropConstraints r f =>
+  Maybe (f (Maybe IP.IdP) -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Property
+prop_deleteGet =
+  prepropLaw @'[E.IdP] $ do
+    s <- arbitrary
+    pure $
+      Law
+        { lawLhs = do
+            E.deleteConfig s
+            E.getConfig $ s ^. SAML.idpId,
+          lawRhs = do
+            E.deleteConfig s
+            pure Nothing,
+          lawPrelude =
+            [ E.storeConfig s
+            ],
+          lawPostlude = [] :: [Sem r ()]
+        }
+
+prop_deleteDelete ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Property
+prop_deleteDelete =
+  prepropLaw @'[E.IdP] $ do
+    s <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.deleteConfig s
+            E.deleteConfig s
+        )
+        ( do
+            E.deleteConfig s
+        )
 
 prop_storeGetByIssuer ::
-  Member E.IdP r =>
-  (forall a. Sem r a -> IO (TypedState, a)) ->
+  PropConstraints r f =>
+  Maybe (f (E.GetIdPResult IdPId) -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
   Property
-prop_storeGetByIssuer x =
-  prepropLaw @'[E.IdP]
-    ( do
-        s <- arbitrary
-        pure
+prop_storeGetByIssuer =
+  prepropLaw @'[E.IdP] $
+    do
+      s <- arbitrary
+      pure $
+        simpleLaw
           ( do
               E.storeConfig s
-              E.getIdByIssuerWithoutTeam $ s ^. idpMetadata . edIssuer,
-            do
+              E.getIdByIssuerWithoutTeam $ s ^. idpMetadata . edIssuer
+          )
+          ( do
               E.storeConfig s
               pure $ E.GetIdPFound $ s ^. idpId
           )
-    )
-    x
 
-testInterpreter :: Sem '[E.IdP] a -> IO (TypedState, a)
-testInterpreter = pure . run . idPToMem
+prop_setClear ::
+  PropConstraints r f =>
+  Maybe (f (Maybe (Maybe IdPId)) -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Property
+prop_setClear =
+  prepropLaw @'[E.IdP] $
+    do
+      idp <- arbitrary
+      replaced_id <- arbitrary
+      let replaced = E.Replaced replaced_id
+      replacing <- arbitrary
+      pure $
+        Law
+          { lawLhs = do
+              E.setReplacedBy replaced replacing
+              E.clearReplacedBy replaced
+              getReplacedBy replaced_id,
+            lawRhs = do
+              E.clearReplacedBy replaced
+              getReplacedBy replaced_id,
+            lawPrelude =
+              [ E.storeConfig $ idp & SAML.idpId .~ replaced_id
+              ],
+            lawPostlude = [] @(Sem _ ())
+          }
 
-propsForInterpreter ::
-  Member E.IdP r =>
-  (forall a. Sem r a -> IO (TypedState, a)) ->
-  Spec
-propsForInterpreter lower = do
-  describe "Config Actions" $ do
-    prop "storeConfig/getConfig" $ prop_storeGet lower
-    prop "storeConfig/getIdByIssuerWithoutTeam" $ prop_storeGetByIssuer lower
+prop_getGet ::
+  forall r f.
+  PropConstraints r f =>
+  Maybe (f (Maybe IP.IdP, Maybe IP.IdP) -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Property
+prop_getGet =
+  prepropLaw @'[E.IdP] $
+    do
+      idpid <- arbitrary
+      idp <- arbitrary
+      pure $
+        Law
+          { lawLhs = do
+              liftA2 (,) (E.getConfig idpid) (E.getConfig idpid),
+            lawRhs = do
+              cfg <- E.getConfig idpid
+              pure (cfg, cfg),
+            lawPrelude =
+              [ E.storeConfig $ idp & SAML.idpId .~ idpid
+              ],
+            lawPostlude = [] :: [Sem r ()]
+          }
 
-spec :: Spec
-spec = modifyMaxSuccess (const 1000) $ do
-  propsForInterpreter testInterpreter
+prop_getStore ::
+  PropConstraints r f =>
+  Maybe (f (Maybe IP.IdP) -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Property
+prop_getStore =
+  prepropLaw @'[E.IdP] $
+    do
+      idpid <- arbitrary
+      s <- arbitrary
+      let s' = s & SAML.idpId .~ idpid
+      pure $
+        Law
+          { lawLhs = do
+              r <- E.getConfig idpid
+              maybe (pure ()) E.storeConfig r
+              pure r,
+            lawRhs = do
+              E.getConfig idpid,
+            lawPrelude =
+              [E.storeConfig s'],
+            lawPostlude =
+              [E.getConfig idpid]
+          }
+
+prop_setSet ::
+  PropConstraints r f =>
+  Maybe (f (Maybe (Maybe IdPId)) -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Property
+prop_setSet =
+  prepropLaw @'[E.IdP] $
+    do
+      replaced_id <- arbitrary
+      s <- arbitrary
+      let s' = s & SAML.idpId .~ replaced_id
+      let replaced = E.Replaced replaced_id
+      replacing <- arbitrary
+      replacing' <- arbitrary
+      pure $
+        Law
+          { lawLhs = do
+              E.setReplacedBy replaced replacing
+              E.setReplacedBy replaced replacing'
+              getReplacedBy replaced_id,
+            lawRhs = do
+              E.setReplacedBy replaced replacing'
+              getReplacedBy replaced_id,
+            lawPrelude =
+              [E.storeConfig s'],
+            lawPostlude = [] @(Sem _ ())
+          }
+
+prop_setGet ::
+  PropConstraints r f =>
+  Maybe (f (Maybe (Maybe IdPId)) -> String) ->
+  (forall x. Sem r x -> IO (f x)) ->
+  Property
+prop_setGet =
+  prepropLaw @'[E.IdP] $
+    do
+      idp <- arbitrary
+      replaced_id <- arbitrary
+      let replaced = E.Replaced replaced_id
+      replacing_id <- arbitrary
+      let replacing = E.Replacing replacing_id
+      pure $
+        Law
+          { lawLhs = do
+              E.setReplacedBy replaced replacing
+              getReplacedBy replaced_id,
+            lawRhs = do
+              E.setReplacedBy replaced replacing
+              (Just replacing_id <$) <$> E.getConfig replaced_id,
+            lawPrelude =
+              [ E.storeConfig $ idp & SAML.idpId .~ replaced_id
+              ],
+            lawPostlude = [] :: [Sem r ()]
+          }
diff --git a/services/spar/test/Test/Spar/Sem/NowSpec.hs b/services/spar/test/Test/Spar/Sem/NowSpec.hs
new file mode 100644
index 0000000000..0c9fdacadf
--- /dev/null
+++ b/services/spar/test/Test/Spar/Sem/NowSpec.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
+
+module Test.Spar.Sem.NowSpec where
+
+import Arbitrary ()
+import Data.Time
+import Data.Time.Calendar.Julian
+import Imports
+import Polysemy
+import Polysemy.Check
+import Polysemy.Input
+import SAML2.WebSSO.Types
+import qualified Spar.Sem.Now as E
+import Spar.Sem.Now.IO
+import Spar.Sem.Now.Input
+import Test.Hspec
+import Test.Hspec.QuickCheck
+import Test.QuickCheck
+
+deriveGenericK ''E.Now
+
+propsForInterpreter ::
+  PropConstraints r f =>
+  String ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Spec
+propsForInterpreter interpreter lower = do
+  describe interpreter $ do
+    prop "now/now" $ prop_nowNow Nothing lower
+
+someTime :: Time
+someTime = Time (UTCTime (fromJulianYearAndDay 1990 209) (secondsToDiffTime 0))
+
+spec :: Spec
+spec = do
+  modifyMaxSuccess (const 1000) $ do
+    propsForInterpreter "nowToIO" $ fmap Identity . runM . nowToIO . runInputConst ()
+    propsForInterpreter "nowToInput" $ pure . Identity . run . runInputConst someTime . nowToInput . runInputConst ()
+
+-- | All the constraints we need to generalize properties in this module.
+-- A regular type synonym doesn't work due to dreaded impredicative
+-- polymorphism.
+class
+  (Functor f, Member E.Now r, Member (Input ()) r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+instance
+  (Functor f, Member E.Now r, Member (Input ()) r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+prop_nowNow ::
+  PropConstraints r f =>
+  Maybe (f Bool -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_nowNow =
+  -- NOTE: This @Input ()@ effect is a workaround to an oversight in
+  -- @polysemy-check@. 'prepropLaw' wants to synthesize some actions to run
+  -- before and after its generators, and check their results for equality. We
+  -- can't use 'Now' as this effect, because 'E.get' won't return equivalent
+  -- results! And we can't keep it empty, because that triggers a crash in
+  -- @polysemy-check@. Thus @Input ()@, which isn't beautiful, but works fine.
+  prepropLaw @'[Input ()] $ do
+    pure $
+      simpleLaw
+        (liftA2 (<=) E.get E.get)
+        ( pure True
+        )
diff --git a/services/spar/test/Test/Spar/Sem/ScimExternalIdStoreSpec.hs b/services/spar/test/Test/Spar/Sem/ScimExternalIdStoreSpec.hs
new file mode 100644
index 0000000000..e6ccad58a4
--- /dev/null
+++ b/services/spar/test/Test/Spar/Sem/ScimExternalIdStoreSpec.hs
@@ -0,0 +1,192 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
+
+module Test.Spar.Sem.ScimExternalIdStoreSpec where
+
+import Arbitrary ()
+import Data.Id
+import Imports
+import Polysemy
+import Polysemy.Check
+import qualified Spar.Sem.ScimExternalIdStore as E
+import Spar.Sem.ScimExternalIdStore.Mem
+import Test.Hspec
+import Test.Hspec.QuickCheck
+import Test.QuickCheck
+
+deriveGenericK ''E.ScimExternalIdStore
+
+propsForInterpreter ::
+  PropConstraints r f =>
+  String ->
+  (forall a. f a -> a) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Spec
+propsForInterpreter interpreter extract lower = do
+  describe interpreter $ do
+    prop "delete/delete" $ prop_deleteDelete Nothing lower
+    prop "delete/lookup" $ prop_deleteLookup (Just $ show . (() <$) . extract) lower
+    prop "delete/insert" $ prop_deleteInsert Nothing lower
+    prop "lookup/insert" $ prop_lookupInsert Nothing lower
+    prop "insert/delete" $ prop_insertDelete Nothing lower
+    prop "insert/lookup" $ prop_insertLookup (Just $ show . (() <$) . extract) lower
+    prop "insert/insert" $ prop_insertInsert (Just $ show . (() <$) . extract) lower
+
+spec :: Spec
+spec = modifyMaxSuccess (const 1000) $ do
+  propsForInterpreter "scimExternalIdStoreToMem" snd $ pure . run . scimExternalIdStoreToMem
+
+-- | All the constraints we need to generalize properties in this module.
+-- A regular type synonym doesn't work due to dreaded impredicative
+-- polymorphism.
+class
+  (Functor f, Member E.ScimExternalIdStore r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+instance
+  (Functor f, Member E.ScimExternalIdStore r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+prop_insertLookup ::
+  PropConstraints r f =>
+  Maybe (f (Maybe UserId) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_insertLookup =
+  prepropLaw @'[E.ScimExternalIdStore] $ do
+    tid <- arbitrary
+    email <- arbitrary
+    uid <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.insert tid email uid
+            E.lookup tid email
+        )
+        ( do
+            E.insert tid email uid
+            pure (Just uid)
+        )
+
+prop_lookupInsert ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_lookupInsert =
+  prepropLaw @'[E.ScimExternalIdStore] $ do
+    tid <- arbitrary
+    email <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.lookup tid email >>= maybe (pure ()) (E.insert tid email)
+        )
+        ( do
+            pure ()
+        )
+
+prop_insertDelete ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_insertDelete =
+  prepropLaw @'[E.ScimExternalIdStore] $ do
+    tid <- arbitrary
+    email <- arbitrary
+    uid <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.insert tid email uid
+            E.delete tid email
+        )
+        ( do
+            E.delete tid email
+        )
+
+prop_deleteInsert ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_deleteInsert =
+  prepropLaw @'[E.ScimExternalIdStore] $ do
+    tid <- arbitrary
+    email <- arbitrary
+    uid <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.delete tid email
+            E.insert tid email uid
+        )
+        ( do
+            E.insert tid email uid
+        )
+
+prop_insertInsert ::
+  PropConstraints r f =>
+  Maybe (f (Maybe UserId) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_insertInsert =
+  prepropLaw @'[E.ScimExternalIdStore] $ do
+    tid <- arbitrary
+    email <- arbitrary
+    uid <- arbitrary
+    uid' <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.insert tid email uid
+            E.insert tid email uid'
+            E.lookup tid email
+        )
+        ( do
+            E.insert tid email uid'
+            E.lookup tid email
+        )
+
+prop_deleteDelete ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_deleteDelete =
+  prepropLaw @'[E.ScimExternalIdStore] $ do
+    tid <- arbitrary
+    email <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.delete tid email
+            E.delete tid email
+        )
+        ( do
+            E.delete tid email
+        )
+
+prop_deleteLookup ::
+  PropConstraints r f =>
+  Maybe (f (Maybe UserId) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_deleteLookup =
+  prepropLaw @'[E.ScimExternalIdStore] $ do
+    tid <- arbitrary
+    email <- arbitrary
+    uid <- arbitrary
+    pure $
+      Law
+        { lawLhs = do
+            E.delete tid email
+            E.lookup tid email,
+          lawRhs = do
+            E.delete tid email
+            pure Nothing,
+          lawPrelude = [E.insert tid email uid],
+          lawPostlude = [] @(Sem _ ())
+        }
diff --git a/stack.yaml b/stack.yaml
index 12671354d5..582b4745f2 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -226,7 +226,7 @@ extra-deps:
 # Not on stackage yet
 - polysemy-1.7.0.0
 - polysemy-plugin-0.4.2.0
-- polysemy-check-0.8.1.0
+- polysemy-check-0.9.0.0
 
 ############################################################
 # Development tools
diff --git a/stack.yaml.lock b/stack.yaml.lock
index 6da7fa2060..009c4b13f7 100644
--- a/stack.yaml.lock
+++ b/stack.yaml.lock
@@ -690,12 +690,12 @@ packages:
   original:
     hackage: polysemy-plugin-0.4.2.0
 - completed:
-    hackage: polysemy-check-0.8.1.0@sha256:5cce3ae162d2f8d8f629397daa28ec5e425f72d357afeb4fe994e102425f2383,2648
+    hackage: polysemy-check-0.9.0.0@sha256:f28c23c5cbae246a049d11e06c51ee85212a2b13a069e93598cf8cdd13ad5a18,2665
     pantry-tree:
-      size: 1027
-      sha256: bc880fb3405307ed251c02358d604979d8014040b78c2ffe6319076431f93509
+      size: 1086
+      sha256: a473605eda27f36717e3f0cbd66651563789107daa9b8d9db59b80cc07ff60d1
   original:
-    hackage: polysemy-check-0.8.1.0
+    hackage: polysemy-check-0.9.0.0
 - completed:
     hackage: ormolu-0.1.4.1@sha256:ed404eac6e4eb64da1ca5fb749e0f99907431a9633e6ba34e44d260e7d7728ba,6499
     pantry-tree: