diff --git a/.github/workflows/integrate.yaml b/.github/workflows/integrate.yaml
index 662e290..42b0d14 100644
--- a/.github/workflows/integrate.yaml
+++ b/.github/workflows/integrate.yaml
@@ -89,4 +89,4 @@ jobs:
           key: ${{ runner.os }}-cabal
 
       - name: Build the project
-        run: nix build
+        run: nix build .#check.x86_64-linux
diff --git a/Makefile b/Makefile
index feb2a3d..a2a17e7 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,5 @@
-SHELL := /usr/bin/env bash
+# This really ought to be `/usr/bin/env bash`, but nix flakes don't like that.
+SHELL := /bin/sh
 
 .PHONY: hoogle format haddock usage
 
@@ -10,7 +11,7 @@ usage:
 	@echo "  format -- Format the project"
 	@echo "  haddock -- Generate Haddock docs for project"
 
-hoogle: 
+hoogle:
 	hoogle generate --local=haddock --database=hoo/local.hoo
 	hoogle server --local -p 8081 >> /dev/null &
 	hoogle server --local --database=hoo/local.hoo -p 8082 >> /dev/null &
@@ -21,5 +22,11 @@ format:
 	git ls-tree -r HEAD --full-tree --name-only | grep -E '.*\.nix' | xargs nixfmt
 	git ls-tree -r HEAD --full-tree --name-only | grep -E '.*\.cabal' | xargs cabal-fmt -i
 
+format_check:
+	find -name '*.hs' \
+	     -not -path './dist*/*' \
+	     -not -path './haddock/*' \
+	  | xargs fourmolu $(FORMAT_EXTENSIONS) -m check
+
 haddock:
 	cabal haddock --haddock-html --haddock-hoogle --builddir=haddock
diff --git a/agora-test/Spec.hs b/agora-test/Spec.hs
index 37def06..502cb27 100644
--- a/agora-test/Spec.hs
+++ b/agora-test/Spec.hs
@@ -8,22 +8,24 @@ import Test.Tasty (defaultMain, testGroup)
 
 --------------------------------------------------------------------------------
 
-import Spec.Int
+import Spec.Model.MultiSig qualified as MultiSig
 import Spec.Stake qualified as Stake
 
+-- | The Agora test suite
 main :: IO ()
 main =
   defaultMain $
     testGroup
       "test suite"
       [ testGroup
-          "sample-tests"
+          "Stake tests"
           Stake.tests
       , testGroup
-          "apropos-tx"
+          "Multisig tests"
           [ testGroup
-              "Int"
-              [ intPlutarchTests
+              "MultiSig"
+              [ MultiSig.plutarchTests
+              , MultiSig.genTests
               ]
           ]
       ]
diff --git a/agora-test/Spec/Int.hs b/agora-test/Spec/Int.hs
deleted file mode 100644
index 8063784..0000000
--- a/agora-test/Spec/Int.hs
+++ /dev/null
@@ -1,88 +0,0 @@
-module Spec.Int (HasLogicalModel (..), IntProp (..), intGenTests, intPureTests, intPlutarchTests) where
-
-import Apropos
-import Apropos.Script
-import Test.Tasty (TestTree, testGroup)
-import Test.Tasty.Hedgehog (fromGroup)
-
-import Plutarch (compile)
-
-data IntProp
-  = IsNegative
-  | IsPositive
-  | IsZero
-  | IsLarge
-  | IsSmall
-  | IsMaxBound
-  | IsMinBound
-  deriving stock (Eq, Ord, Enum, Show, Bounded)
-
-instance Enumerable IntProp where
-  enumerated = [minBound .. maxBound]
-
-instance LogicalModel IntProp where
-  logic =
-    ExactlyOne [Var IsNegative, Var IsPositive, Var IsZero]
-      :&&: ExactlyOne [Var IsLarge, Var IsSmall]
-      :&&: (Var IsZero :->: Var IsSmall)
-      :&&: (Var IsMaxBound :->: (Var IsLarge :&&: Var IsPositive))
-      :&&: (Var IsMinBound :->: (Var IsLarge :&&: Var IsNegative))
-
-instance HasLogicalModel IntProp Int where
-  satisfiesProperty IsNegative i = i < 0
-  satisfiesProperty IsPositive i = i > 0
-  satisfiesProperty IsMaxBound i = i == maxBound
-  satisfiesProperty IsMinBound i = i == minBound
-  satisfiesProperty IsZero i = i == 0
-  satisfiesProperty IsLarge i = i > 10 || i < -10
-  satisfiesProperty IsSmall i = i <= 10 && i >= -10
-
-instance HasParameterisedGenerator IntProp Int where
-  parameterisedGenerator s = do
-    i <-
-      if IsZero `elem` s
-        then pure 0
-        else
-          if IsSmall `elem` s
-            then int (linear 1 10)
-            else
-              if IsMaxBound `elem` s
-                then pure maxBound
-                else int (linear 11 (maxBound - 1))
-    if IsNegative `elem` s
-      then
-        if IsMinBound `elem` s
-          then pure minBound
-          else pure (-i)
-      else pure i
-
-intGenTests :: TestTree
-intGenTests =
-  testGroup "intGenTests" $
-    fromGroup
-      <$> [ runGeneratorTestsWhere (Apropos :: Int :+ IntProp) "Int Generator" Yes
-          ]
-
-instance HasPureRunner IntProp Int where
-  expect _ = Var IsSmall :&&: Var IsNegative
-  script _ i = i < 0 && i >= -10
-
-intPureTests :: TestTree
-intPureTests =
-  testGroup "intPureTests" $
-    fromGroup
-      <$> [ runPureTestsWhere (Apropos :: Int :+ IntProp) "AcceptsSmallNegativeInts" Yes
-          ]
-
-instance HasScriptRunner IntProp Int where
-  expect _ = Var IsSmall :&&: Var IsNegative
-  script _ i =
-    let ii = fromIntegral i :: Integer
-     in compile (pif ((fromInteger ii #< (0 :: Term s PInteger)) #&& ((fromInteger (-10) :: Term s PInteger) #<= fromInteger ii)) (pcon PUnit) perror)
-
-intPlutarchTests :: TestTree
-intPlutarchTests =
-  testGroup "intPlutarchTests" $
-    fromGroup
-      <$> [ runScriptTestsWhere (Apropos :: Int :+ IntProp) "AcceptsSmallNegativeInts" Yes
-          ]
diff --git a/agora-test/Spec/Model/MultiSig.hs b/agora-test/Spec/Model/MultiSig.hs
new file mode 100644
index 0000000..15dcfae
--- /dev/null
+++ b/agora-test/Spec/Model/MultiSig.hs
@@ -0,0 +1,194 @@
+{- |
+Module     : Spec.Model.MultiSig
+Maintainer : emi@haskell.fyi
+Description: apropos-tx model and tests for 'MultiSig' functions
+
+apropos-tx model and tests for 'MultiSig' functions
+-}
+module Spec.Model.MultiSig (
+  plutarchTests,
+  genTests,
+) where
+
+import Data.List (intersect)
+
+--------------------------------------------------------------------------------
+
+import Plutus.V1.Ledger.Api (
+  Script,
+  ScriptContext (scriptContextPurpose),
+  ScriptPurpose (Spending),
+  TxInfo (
+    txInfoDCert,
+    txInfoData,
+    txInfoFee,
+    txInfoId,
+    txInfoInputs,
+    txInfoMint,
+    txInfoOutputs,
+    txInfoValidRange,
+    txInfoWdrl
+  ),
+  TxOutRef (TxOutRef),
+  scriptContextTxInfo,
+  txInfoSignatories,
+ )
+import Plutus.V1.Ledger.Contexts (ScriptContext (ScriptContext), TxInfo (TxInfo))
+import Plutus.V1.Ledger.Crypto (PubKeyHash)
+import Plutus.V1.Ledger.Interval qualified as Interval
+import Plutus.V1.Ledger.Value qualified as Value
+
+--------------------------------------------------------------------------------
+
+import Apropos (
+  Apropos (Apropos),
+  Formula (ExactlyOne, Var, Yes),
+  HasLogicalModel (..),
+  HasParameterisedGenerator,
+  LogicalModel (logic),
+  parameterisedGenerator,
+  runGeneratorTestsWhere,
+  (:+),
+ )
+import Apropos.Gen (Gen, choice, int, linear, list)
+import Apropos.LogicalModel (Enumerable)
+import Apropos.LogicalModel.Enumerable (Enumerable (enumerated))
+import Apropos.Script (HasScriptRunner (expect, runScriptTestsWhere, script))
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.Hedgehog (fromGroup)
+
+--------------------------------------------------------------------------------
+
+import Agora.MultiSig (MultiSig (..), validatedByMultisig)
+
+--------------------------------------------------------------------------------
+
+-- | apropos model for testing multisigs.
+data MultiSigModel = MultiSigModel
+  { ms :: MultiSig
+  -- ^ `MultiSig` value to be tested.
+  , ctx :: ScriptContext
+  -- ^ The `ScriptContext` of the transaction.
+  }
+  deriving stock (Eq, Show)
+
+-- | Propositions that may hold true of a `MultiSigModel`.
+data MultiSigProp
+  = -- | Sufficient number of signatories in the script context.
+    MeetsMinSigs
+  | -- | Insufficient number of signatories in the script context.
+    DoesNotMeetMinSigs
+  deriving stock (Eq, Show, Ord)
+
+instance Enumerable MultiSigProp where
+  enumerated = [MeetsMinSigs, DoesNotMeetMinSigs]
+
+instance LogicalModel MultiSigProp where
+  -- Only logical relationship between the two propositions is
+  -- that exactly one of them holds for a given model.
+  logic = ExactlyOne [Var MeetsMinSigs, Var DoesNotMeetMinSigs]
+
+instance HasLogicalModel MultiSigProp MultiSigModel where
+  satisfiesProperty :: MultiSigProp -> MultiSigModel -> Bool
+  satisfiesProperty p m =
+    let minSigs = m.ms.minSigs
+        signatories = txInfoSignatories $ scriptContextTxInfo $ m.ctx
+        matchingSigs = intersect m.ms.keys signatories
+     in case p of
+          MeetsMinSigs -> length matchingSigs >= fromInteger minSigs
+          DoesNotMeetMinSigs -> length matchingSigs < fromInteger minSigs
+
+{- | Given a list of key hashes, returns a dummy `ScriptContext`,
+     with those hashes as signatories.
+-}
+contextWithSignatures :: [PubKeyHash] -> ScriptContext
+contextWithSignatures sigs =
+  ScriptContext
+    { scriptContextTxInfo =
+        TxInfo
+          { txInfoInputs = []
+          , txInfoOutputs = []
+          , txInfoFee = Value.singleton "" "" 2
+          , txInfoMint = mempty
+          , txInfoDCert = []
+          , txInfoWdrl = []
+          , txInfoValidRange = Interval.always
+          , txInfoSignatories = sigs
+          , txInfoData = []
+          , txInfoId = "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
+          }
+    , scriptContextPurpose = Spending (TxOutRef "" 0)
+    }
+
+-- | Generator returning one of four dummy public key hashes.
+genPK :: Gen PubKeyHash
+genPK =
+  choice
+    [ pure "8a30896c4fd5e79843e4ca1bd2cdbaa36f8c0bc3be7401214142019c"
+    , pure "0b12051dd2da4b3629cebb92e2be111e0e99c63c04727ed55b74a296"
+    , pure "87f5f31e4d7437463cd901c4c9edb7a51903ac858661503e9d72f492"
+    , pure "f74ccaee8244264b3c73fce3b66bd2337de3db70efff4261d6ff145b"
+    ]
+
+instance HasParameterisedGenerator MultiSigProp MultiSigModel where
+  parameterisedGenerator s = do
+    -- Gen between one and four signatures for the `MultiSig`.
+    expectedSignatures <- list (linear 1 4) genPK
+
+    -- Gen the value of `MultiSig.minSigs`.
+    minSigs <- toInteger <$> int (linear 1 (length expectedSignatures))
+
+    -- Assign values to msig.
+    let msig = MultiSig expectedSignatures minSigs
+
+    actualSignaturesLength <-
+      -- If we would like to generate a MultiSig model which passes...
+      if MeetsMinSigs `elem` s
+        then -- ... have a sufficient number of signatories.
+          int (linear (fromInteger minSigs) (length expectedSignatures))
+        else -- ... have zero signatories.
+          pure 0
+
+    -- Get a list of signatories for the script context.
+    let actualSignatures = take actualSignaturesLength expectedSignatures
+
+    let ctx = contextWithSignatures actualSignatures
+
+    -- Return the generated model.
+    pure (MultiSigModel msig ctx)
+
+instance HasScriptRunner MultiSigProp MultiSigModel where
+  -- When the script runs, we want the model to meet the minimum signatures.
+  expect :: (MultiSigModel :+ MultiSigProp) -> Formula MultiSigProp
+  expect Apropos = Var MeetsMinSigs
+
+  -- Function making a valid script from the model and propositions.
+  script :: (MultiSigModel :+ MultiSigProp) -> MultiSigModel -> Script
+  script Apropos msm =
+    compile $
+      pif
+        (validatedByMultisig msm.ms # pconstant msm.ctx.scriptContextTxInfo)
+        (pcon PUnit)
+        perror
+
+-- | Consistency tests for the 'HasParameterisedGenerator' instance of 'MultiSigModel'
+genTests :: TestTree
+genTests =
+  testGroup "genTests" $
+    fromGroup
+      <$> [ runGeneratorTestsWhere
+              (Apropos :: MultiSigModel :+ MultiSigProp)
+              "Generator"
+              Yes
+          ]
+
+-- | Tests for the 'HasScriptRunner' instance of 'MultiSigModel'
+plutarchTests :: TestTree
+plutarchTests =
+  testGroup "plutarchTests" $
+    fromGroup
+      <$> [ runScriptTestsWhere
+              (Apropos :: MultiSigModel :+ MultiSigProp)
+              "ScriptValid"
+              Yes
+          ]
diff --git a/agora-test/Spec/Sample/Stake.hs b/agora-test/Spec/Sample/Stake.hs
index 96a54ad..4bb0073 100644
--- a/agora-test/Spec/Sample/Stake.hs
+++ b/agora-test/Spec/Sample/Stake.hs
@@ -10,11 +10,14 @@ module Spec.Sample.Stake (
   policy,
   policySymbol,
   validatorHashTN,
+  signer,
 
   -- * Script contexts
   stakeCreation,
   stakeCreationWrongDatum,
   stakeCreationUnsigned,
+  stakeDepositWithdraw,
+  DepositWithdrawExample (..),
 ) where
 
 --------------------------------------------------------------------------------
@@ -36,11 +39,12 @@ import Plutus.V1.Ledger.Api (
   ScriptContext (..),
   ScriptPurpose (..),
   ToData (toBuiltinData),
+  TxInInfo (TxInInfo),
   TxInfo (..),
   TxOut (txOutAddress, txOutDatumHash, txOutValue),
   ValidatorHash (ValidatorHash),
  )
-import Plutus.V1.Ledger.Contexts (TxOut (TxOut))
+import Plutus.V1.Ledger.Contexts (TxOut (TxOut), TxOutRef (TxOutRef))
 import Plutus.V1.Ledger.Interval qualified as Interval
 import Plutus.V1.Ledger.Scripts (Validator)
 import Plutus.V1.Ledger.Value (TokenName (TokenName))
@@ -50,28 +54,34 @@ import Plutus.V1.Ledger.Value qualified as Value
 
 import Agora.SafeMoney
 import Agora.Stake
+import Spec.Util (datumPair, toDatumHash)
 
 --------------------------------------------------------------------------------
 
+-- | 'Stake' parameters for 'LQ'.
 stake :: Stake LQ
 stake = Stake
 
+-- | 'Stake' policy instance.
 policy :: MintingPolicy
 policy = mkMintingPolicy (stakePolicy stake)
 
 policySymbol :: CurrencySymbol
 policySymbol = mintingPolicySymbol policy
 
+-- | A sample 'PubKeyHash'.
 signer :: PubKeyHash
 signer = "8a30896c4fd5e79843e4ca1bd2cdbaa36f8c0bc3be7401214142019c"
 
+-- | 'Stake' validator instance.
 validator :: Validator
 validator = mkValidator (stakeValidator stake)
 
+-- | 'TokenName' that represents the hash of the 'Stake' validator.
 validatorHashTN :: TokenName
 validatorHashTN = let ValidatorHash vh = validatorHash validator in TokenName vh
 
--- | This script context should be a valid transaction
+-- | This script context should be a valid transaction.
 stakeCreation :: ScriptContext
 stakeCreation =
   let st = Value.singleton policySymbol validatorHashTN 1 -- Stake ST
@@ -100,7 +110,7 @@ stakeCreation =
         , scriptContextPurpose = Minting policySymbol
         }
 
--- | This ScriptContext should fail because the datum has too much GT
+-- | This ScriptContext should fail because the datum has too much GT.
 stakeCreationWrongDatum :: ScriptContext
 stakeCreationWrongDatum =
   let datum :: Datum
@@ -110,7 +120,7 @@ stakeCreationWrongDatum =
         , scriptContextPurpose = Minting policySymbol
         }
 
--- | This ScriptContext should fail because the datum has too much GT
+-- | This ScriptContext should fail because the datum has too much GT.
 stakeCreationUnsigned :: ScriptContext
 stakeCreationUnsigned =
   ScriptContext
@@ -120,3 +130,63 @@ stakeCreationUnsigned =
           }
     , scriptContextPurpose = Minting policySymbol
     }
+
+--------------------------------------------------------------------------------
+
+-- | Config for creating a ScriptContext that deposits or withdraws.
+data DepositWithdrawExample = DepositWithdrawExample
+  { startAmount :: Integer
+  -- ^ The amount of GT stored before the transaction.
+  , delta :: Integer
+  -- ^ The amount of GT deposited or withdrawn from the Stake.
+  }
+
+-- | Create a ScriptContext that deposits or withdraws, given the config for it.
+stakeDepositWithdraw :: DepositWithdrawExample -> ScriptContext
+stakeDepositWithdraw config =
+  let st = Value.singleton policySymbol validatorHashTN 1 -- Stake ST
+      stakeBefore :: StakeDatum
+      stakeBefore = StakeDatum config.startAmount signer
+
+      stakeAfter :: StakeDatum
+      stakeAfter = stakeBefore {stakedAmount = stakeBefore.stakedAmount + config.delta}
+   in ScriptContext
+        { scriptContextTxInfo =
+            TxInfo
+              { txInfoInputs =
+                  [ TxInInfo
+                      (TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1)
+                      TxOut
+                        { txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
+                        , txOutValue =
+                            st
+                              <> Value.singleton
+                                "da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
+                                "LQ"
+                                stakeBefore.stakedAmount
+                        , txOutDatumHash = Just (toDatumHash stakeAfter)
+                        }
+                  ]
+              , txInfoOutputs =
+                  [ TxOut
+                      { txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
+                      , txOutValue =
+                          st
+                            <> Value.singleton
+                              "da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
+                              "LQ"
+                              stakeAfter.stakedAmount
+                      , txOutDatumHash = Just (toDatumHash stakeAfter)
+                      }
+                  ]
+              , txInfoFee = Value.singleton "" "" 2
+              , txInfoMint = st
+              , txInfoDCert = []
+              , txInfoWdrl = []
+              , txInfoValidRange = Interval.always
+              , txInfoSignatories = [signer]
+              , txInfoData = [datumPair stakeAfter]
+              , txInfoId = "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
+              }
+        , scriptContextPurpose = Spending (TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1)
+        }
diff --git a/agora-test/Spec/Stake.hs b/agora-test/Spec/Stake.hs
index dd51749..8064ddf 100644
--- a/agora-test/Spec/Stake.hs
+++ b/agora-test/Spec/Stake.hs
@@ -1,3 +1,10 @@
+{- |
+Module     : Spec.Stake
+Maintainer : emi@haskell.fyi
+Description: Tests for Stake policy and validator
+
+Tests for Stake policy and validator
+-}
 module Spec.Stake (tests) where
 
 --------------------------------------------------------------------------------
@@ -10,19 +17,17 @@ import Test.Tasty (TestTree, testGroup)
 
 --------------------------------------------------------------------------------
 
-import Plutarch.Builtin (pforgetData)
-
---------------------------------------------------------------------------------
-
-import Agora.Stake (stakePolicy)
+import Agora.Stake (StakeDatum (StakeDatum), StakeRedeemer (DepositWithdraw), stakePolicy, stakeValidator)
 
 --------------------------------------------------------------------------------
 
+import Spec.Sample.Stake (DepositWithdrawExample (DepositWithdrawExample, delta, startAmount), signer)
 import Spec.Sample.Stake qualified as Stake
-import Spec.Util (policyFailsWith, policySucceedsWith)
+import Spec.Util (policyFailsWith, policySucceedsWith, toDatum, validatorFailsWith, validatorSucceedsWith)
 
 --------------------------------------------------------------------------------
 
+-- | Stake tests
 tests :: [TestTree]
 tests =
   [ testGroup
@@ -30,17 +35,35 @@ tests =
       [ policySucceedsWith
           "stakeCreation"
           (stakePolicy Stake.stake)
-          (pforgetData (pconstantData ()))
+          ()
           Stake.stakeCreation
       , policyFailsWith
           "stakeCreationWrongDatum"
           (stakePolicy Stake.stake)
-          (pforgetData (pconstantData ()))
+          ()
           Stake.stakeCreationWrongDatum
       , policyFailsWith
           "stakeCreationUnsigned"
           (stakePolicy Stake.stake)
-          (pforgetData (pconstantData ()))
+          ()
           Stake.stakeCreationUnsigned
+      , validatorSucceedsWith
+          "stakeDepositWithdraw deposit"
+          (stakeValidator Stake.stake)
+          (toDatum $ StakeDatum 100_000 signer)
+          (toDatum $ DepositWithdraw 100_000)
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = 100_000})
+      , validatorSucceedsWith
+          "stakeDepositWithdraw withdraw"
+          (stakeValidator Stake.stake)
+          (toDatum $ StakeDatum 100_000 signer)
+          (toDatum $ DepositWithdraw (negate 100_000))
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 100_000})
+      , validatorFailsWith
+          "stakeDepositWithdraw negative GT"
+          (stakeValidator Stake.stake)
+          (toDatum $ StakeDatum 100_000 signer)
+          (toDatum $ DepositWithdraw (negate 1_000_000))
+          (Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 1_000_000})
       ]
   ]
diff --git a/agora-test/Spec/Util.hs b/agora-test/Spec/Util.hs
index 3db7f53..4350e45 100644
--- a/agora-test/Spec/Util.hs
+++ b/agora-test/Spec/Util.hs
@@ -1,8 +1,24 @@
+{- |
+Module     : Spec.Util
+Maintainer : emi@haskell.fyi
+Description: Utility functions for testing Plutarch scripts with ScriptContext
+
+Utility functions for testing Plutarch scripts with ScriptContext
+-}
 module Spec.Util (
+  -- * Testing utils
   scriptSucceeds,
   scriptFails,
   policySucceedsWith,
   policyFailsWith,
+  validatorSucceedsWith,
+  validatorFailsWith,
+
+  -- * Plutus-land utils
+  datumHash,
+  toDatum,
+  toDatumHash,
+  datumPair,
 ) where
 
 --------------------------------------------------------------------------------
@@ -11,27 +27,109 @@ import Prelude
 
 --------------------------------------------------------------------------------
 
+import Codec.Serialise (serialise)
+import Data.ByteString.Lazy qualified as ByteString.Lazy
+
+--------------------------------------------------------------------------------
+
 import Test.Tasty (TestTree)
 import Test.Tasty.HUnit (assertFailure, testCase)
 
 --------------------------------------------------------------------------------
 
-import Plutarch
-import Plutarch.Api.V1 (PMintingPolicy)
+import Plutarch.Api.V1 (PMintingPolicy, PValidator)
+import Plutarch.Builtin (pforgetData)
+import Plutarch.Crypto (pblake2b_256)
 import Plutarch.Evaluate (evalScript)
-import Plutarch.Prelude ()
-import Plutus.V1.Ledger.Scripts (Script)
+import Plutarch.Lift (PUnsafeLiftDecl (PLifted))
+import Plutus.V1.Ledger.Contexts (ScriptContext)
+import Plutus.V1.Ledger.Scripts (Datum (Datum), DatumHash (DatumHash), Script)
+import PlutusTx.Builtins qualified as PlutusTx
+import PlutusTx.IsData qualified as PlutusTx
 
 --------------------------------------------------------------------------------
 
-policySucceedsWith :: String -> ClosedTerm PMintingPolicy -> ClosedTerm PData -> _ -> TestTree
+-- | Check that a policy script succeeds, given a name and arguments.
+policySucceedsWith ::
+  ( PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PMintingPolicy ->
+  PLifted redeemer ->
+  ScriptContext ->
+  TestTree
 policySucceedsWith tag policy redeemer scriptContext =
-  scriptSucceeds tag $ compile (policy # redeemer # pconstant scriptContext)
+  scriptSucceeds tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
 
-policyFailsWith :: String -> ClosedTerm PMintingPolicy -> ClosedTerm PData -> _ -> TestTree
+-- | Check that a policy script fails, given a name and arguments.
+policyFailsWith ::
+  ( PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PMintingPolicy ->
+  PLifted redeemer ->
+  ScriptContext ->
+  TestTree
 policyFailsWith tag policy redeemer scriptContext =
-  scriptFails tag $ compile (policy # redeemer # pconstant scriptContext)
+  scriptFails tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
 
+-- | Check that a validator script succeeds, given a name and arguments.
+validatorSucceedsWith ::
+  ( PLift datum
+  , PlutusTx.ToData (PLifted datum)
+  , PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PValidator ->
+  PLifted datum ->
+  PLifted redeemer ->
+  ScriptContext ->
+  TestTree
+validatorSucceedsWith tag policy datum redeemer scriptContext =
+  scriptSucceeds tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData datum)
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
+
+-- | Check that a validator script fails, given a name and arguments.
+validatorFailsWith ::
+  ( PLift datum
+  , PlutusTx.ToData (PLifted datum)
+  , PLift redeemer
+  , PlutusTx.ToData (PLifted redeemer)
+  ) =>
+  String ->
+  ClosedTerm PValidator ->
+  PLifted datum ->
+  PLifted redeemer ->
+  ScriptContext ->
+  TestTree
+validatorFailsWith tag policy datum redeemer scriptContext =
+  scriptFails tag $
+    compile
+      ( policy
+          # pforgetData (pconstantData datum)
+          # pforgetData (pconstantData redeemer)
+          # pconstant scriptContext
+      )
+
+-- | Check that an arbitrary script doesn't error when evaluated, given a name.
 scriptSucceeds :: String -> Script -> TestTree
 scriptSucceeds name script = testCase name $ do
   let (res, _budget, traces) = evalScript script
@@ -42,6 +140,7 @@ scriptSucceeds name script = testCase name $ do
     Right _v ->
       pure ()
 
+-- | Check that an arbitrary script **does** error when evaluated, given a name.
 scriptFails :: String -> Script -> TestTree
 scriptFails name script = testCase name $ do
   let (res, _budget, traces) = evalScript script
@@ -51,3 +150,35 @@ scriptFails name script = testCase name $ do
     Right v ->
       assertFailure $
         "Expected failure, but succeeded. " <> show v <> " Traces: " <> show traces
+
+--------------------------------------------------------------------------------
+
+{- | Create a pair from data for use in 'txInfoData'.
+
+   Example:
+   @
+     myTxInfo { 'txInfoData' = ['datumPair' myDatum] }
+   @
+-}
+datumPair :: PlutusTx.ToData a => a -> (DatumHash, Datum)
+datumPair = (,) <$> toDatumHash <*> toDatum
+
+-- | Calculate the blake2b-256 hash of a Datum.
+datumHash :: Datum -> DatumHash
+datumHash (Datum data') = toDatumHash data'
+
+-- | Convenience function to create a Datum from any type that implements ToData.
+toDatum :: PlutusTx.ToData a => a -> Datum
+toDatum = Datum . PlutusTx.toBuiltinData
+
+{- | Calculate the blake2b-256 hash of any type that implements ToData
+
+     Shamelessly go through plutus.
+-}
+toDatumHash :: PlutusTx.ToData a => a -> DatumHash
+toDatumHash datum =
+  DatumHash $
+    PlutusTx.toBuiltin $
+      plift $
+        pblake2b_256
+          # pconstant (ByteString.Lazy.toStrict $ serialise $ PlutusTx.toData datum)
diff --git a/agora.cabal b/agora.cabal
index 65039ad..b50a55b 100644
--- a/agora.cabal
+++ b/agora.cabal
@@ -108,12 +108,12 @@ common deps
 
 common test-deps
   build-depends:
+    , apropos-tx
     , QuickCheck
     , quickcheck-instances
     , tasty
     , tasty-hedgehog
     , tasty-hunit
-    , apropos-tx
 
 library
   import:          lang, deps
@@ -147,19 +147,16 @@ test-suite agora-test
   main-is:        Spec.hs
   hs-source-dirs: agora-test
   other-modules:
-    Spec.Int
+    Spec.Model.MultiSig
     Spec.Sample.Stake
     Spec.Stake
-
     Spec.Util
 
-  build-depends:
-    , agora
+  build-depends:  agora
 
 benchmark agora-bench
   import:         lang, deps
   hs-source-dirs: agora-bench
   main-is:        Main.hs
   type:           exitcode-stdio-1.0
-  build-depends:
-    , agora
+  build-depends:  agora
diff --git a/agora/Agora/MultiSig.hs b/agora/Agora/MultiSig.hs
index 2014c02..6e8270d 100644
--- a/agora/Agora/MultiSig.hs
+++ b/agora/Agora/MultiSig.hs
@@ -10,6 +10,7 @@ A basic N of M multisignature validation function.
 module Agora.MultiSig (
   validatedByMultisig,
   pvalidatedByMultisig,
+  PMultiSig (..),
   MultiSig (..),
 ) where
 
@@ -47,7 +48,7 @@ data MultiSig = MultiSig
   -- ^ List of PubKeyHashes that must be present in the list of signatories.
   , minSigs :: Integer
   }
-  deriving stock (GHC.Generic)
+  deriving stock (GHC.Generic, Eq, Show)
   deriving anyclass (Generic)
 
 PlutusTx.makeLift ''MultiSig
diff --git a/agora/Agora/SafeMoney.hs b/agora/Agora/SafeMoney.hs
index d40d99d..bec07c5 100644
--- a/agora/Agora/SafeMoney.hs
+++ b/agora/Agora/SafeMoney.hs
@@ -9,10 +9,11 @@ module Agora.SafeMoney (
   -- * Types
   MoneyClass,
   PDiscrete,
-  Discrete,
 
   -- * Utility functions
   paddDiscrete,
+  pgeqDiscrete,
+  pzeroDiscrete,
 
   -- * Conversions
   pdiscreteValue,
@@ -42,11 +43,11 @@ import Plutarch.Monadic qualified as P
 
 --------------------------------------------------------------------------------
 
-import Agora.Utils
+import Agora.Utils (passetClassValueOf, psingletonValue)
 
 --------------------------------------------------------------------------------
 
--- | Type-level unique identifier for an `AssetClass`
+-- | Type-level unique identifier for an 'Plutus.V1.Ledger.Value.AssetClass'
 type MoneyClass =
   ( -- AssetClass
     Symbol
@@ -56,16 +57,24 @@ type MoneyClass =
     Nat
   )
 
--- | A `PDiscrete` amount of currency tagged on the type level with the `MoneyClass` it belong sto
+-- | A 'PDiscrete' amount of currency tagged on the type level with the 'MoneyClass' it belongs to
 newtype PDiscrete (mc :: MoneyClass) (s :: S)
   = PDiscrete (Term s PInteger)
   deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (PDiscrete mc) PInteger)
 
-newtype Discrete (mc :: MoneyClass)
-  = Discrete Integer
-  deriving stock (Show)
+-- | Check if one 'PDiscrete' is greater than another.
+pgeqDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc :--> PDiscrete mc :--> PBool)
+pgeqDiscrete = phoistAcyclic $
+  plam $ \x y -> P.do
+    PDiscrete x' <- pmatch x
+    PDiscrete y' <- pmatch y
+    y' #<= x'
 
--- | Add two `PDiscrete` values of the same `MoneyClass`.
+-- | Returns a zero-value 'PDiscrete' unit for any 'MoneyClass'.
+pzeroDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc)
+pzeroDiscrete = phoistAcyclic $ pcon (PDiscrete 0)
+
+-- | Add two 'PDiscrete' values of the same 'MoneyClass'.
 paddDiscrete :: Term s (PDiscrete mc :--> PDiscrete mc :--> PDiscrete mc)
 paddDiscrete = phoistAcyclic $
   -- In the future, this should use plutarch-numeric
@@ -100,7 +109,8 @@ pvalueDiscrete = phoistAcyclic $
         # f
 
 {- | Get a `PValue` from a `PDiscrete`.
-     __NOTE__: `pdiscreteValue` after `pvalueDiscrete` is loses information
+     __NOTE__: `pdiscreteValue` after `pvalueDiscrete` is not a round-trip.
+     It filters for a particular 'MoneyClass'.
 -}
 pdiscreteValue ::
   forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
diff --git a/agora/Agora/SafeMoney/QQ.hs b/agora/Agora/SafeMoney/QQ.hs
index 96ec4c7..3fdf161 100644
--- a/agora/Agora/SafeMoney/QQ.hs
+++ b/agora/Agora/SafeMoney/QQ.hs
@@ -40,7 +40,7 @@ import Agora.SafeMoney (MoneyClass, PDiscrete)
 {- | Generate 'PDiscrete' values tagged by a particular MoneyClass
 
 @
-  [discrete| 123.456 ADA |] :: 'Term' s ('PDiscrete' 'ADA')
+  [discrete| 123.456 'Agora.SafeMoney.ADA' |] :: 'Term' s ('PDiscrete' 'Agora.SafeMoney.ADA')
 @
 -}
 discrete :: QuasiQuoter
diff --git a/agora/Agora/Stake.hs b/agora/Agora/Stake.hs
index 44199a6..3929449 100644
--- a/agora/Agora/Stake.hs
+++ b/agora/Agora/Stake.hs
@@ -9,8 +9,9 @@ Vote-lockable stake UTXOs holding GT.
 -}
 module Agora.Stake (
   PStakeDatum (..),
-  PStakeAction (..),
+  PStakeRedeemer (..),
   StakeDatum (..),
+  StakeRedeemer (..),
   Stake (..),
   stakePolicy,
   stakeValidator,
@@ -19,9 +20,12 @@ module Agora.Stake (
 
 --------------------------------------------------------------------------------
 
+import Data.Proxy (Proxy (Proxy))
+import Data.String (IsString (fromString))
 import GHC.Generics qualified as GHC
 import GHC.TypeLits (
   KnownSymbol,
+  symbolVal,
  )
 import Generics.SOP (Generic, I (I))
 import Prelude
@@ -50,6 +54,7 @@ import Plutarch.DataRepr (
  )
 import Plutarch.Internal (punsafeCoerce)
 import Plutarch.Monadic qualified as P
+import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
 
 --------------------------------------------------------------------------------
 
@@ -58,6 +63,8 @@ import Agora.SafeMoney (
   PDiscrete,
   paddDiscrete,
   pdiscreteValue,
+  pgeqDiscrete,
+  pzeroDiscrete,
  )
 import Agora.Utils (
   anyInput,
@@ -65,6 +72,9 @@ import Agora.Utils (
   paddValue,
   passert,
   pfindTxInByTxOutRef,
+  pgeqByClass,
+  pgeqByClass',
+  pgeqBySymbol,
   psingletonValue,
   psymbolValueOf,
   ptxSignedBy,
@@ -77,7 +87,7 @@ import Agora.Utils (
 data Stake (gt :: MoneyClass) = Stake
 
 -- | Plutarch-level redeemer for Stake scripts.
-data PStakeAction (gt :: MoneyClass) (s :: S)
+data PStakeRedeemer (gt :: MoneyClass) (s :: S)
   = -- | Deposit or withdraw a discrete amount of the staked governance token.
     PDepositWithdraw (Term s (PDataRecord '["delta" ':= PDiscrete gt]))
   | -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
@@ -87,7 +97,23 @@ data PStakeAction (gt :: MoneyClass) (s :: S)
   deriving anyclass (PIsDataRepr)
   deriving
     (PlutusType, PIsData)
-    via PIsDataReprInstances (PStakeAction gt)
+    via PIsDataReprInstances (PStakeRedeemer gt)
+
+-- FIXME: 'StakeRedeemer' and 'StakeDatum' are stripped of their
+-- typesafe `PDiscrete` equivalent due to issues with `makeIsDataIndexed`
+-- when using the kind @gt :: MoneyClass@. This ought to be fixed with
+-- a future patch in Plutarch upstream. For now, we will deal with lower
+-- type safety off-chain.
+
+-- | Haskell-level redeemer for Stake scripts.
+data StakeRedeemer
+  = -- | Deposit or withdraw a discrete amount of the staked governance token.
+    DepositWithdraw Integer
+  | -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
+    Destroy
+  deriving stock (Show, GHC.Generic)
+
+PlutusTx.makeIsDataIndexed ''StakeRedeemer [('DepositWithdraw, 0), ('Destroy, 1)]
 
 -- | Plutarch-level datum for Stake scripts.
 newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum
@@ -103,7 +129,8 @@ newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum
 
 -- | Haskell-level datum for Stake scripts.
 data StakeDatum = StakeDatum
-  { stakedAmount :: Integer
+  { -- FIXME: This needs to be gt
+  stakedAmount :: Integer
   , owner :: PubKeyHash
   }
   deriving stock (Show, GHC.Generic)
@@ -200,8 +227,28 @@ stakePolicy _stake =
                             # ctx.txInfo
                             # stakeDatum.owner
 
-                    -- TODO: Needs to be >=, rather than ==
-                    let valueCorrect = pdata value #== pdata expectedValue
+                    -- TODO: This is quite inefficient now, as it does two lookups
+                    -- instead of a more efficient single pass,
+                    -- but it doesn't really matter for this. At least it's correct.
+                    let valueCorrect =
+                          foldr1
+                            (#&&)
+                            [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
+                            , pgeqByClass'
+                                ( AssetClass
+                                    ( fromString . symbolVal $ Proxy @ac
+                                    , fromString . symbolVal $ Proxy @n
+                                    )
+                                )
+                                # value
+                                # expectedValue
+                            , pgeqByClass
+                                # ownSymbol
+                                # tn
+                                # value
+                                # expectedValue
+                            ]
+
                     ownerSignsTransaction
                       #&& valueCorrect
           popaque (pconstant ())
@@ -226,8 +273,8 @@ stakeValidator stake =
     txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
 
     -- Coercion is safe in that if coercion fails we crash hard.
-    let stakeAction :: Term _ (PStakeAction gt)
-        stakeAction = pfromData $ punsafeCoerce redeemer
+    let stakeRedeemer :: Term _ (PStakeRedeemer gt)
+        stakeRedeemer = pfromData $ punsafeCoerce redeemer
         stakeDatum' :: Term _ (PStakeDatum gt)
         stakeDatum' = pfromData $ punsafeCoerce datum
     stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
@@ -242,7 +289,7 @@ stakeValidator stake =
     mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfo.mint
     spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfo'
 
-    pmatch stakeAction $ \case
+    pmatch stakeRedeemer $ \case
       PDestroy _ -> P.do
         passert "ST at inputs must be 1" $
           spentST #== 1
@@ -270,13 +317,43 @@ stakeValidator stake =
               delta <- plet $ pfield @"delta" # r
               let isScriptAddress = pdata address #== ownAddress
               let correctOutputDatum =
-                    stakeDatum.owner #== newStakeDatum.owner
-                      #&& (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
+                    foldr1
+                      (#&&)
+                      [ stakeDatum.owner #== newStakeDatum.owner
+                      , (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
+                      , -- We can't magically conjure GT anyway (no input to spend!)
+                        -- do we need to check this, really?
+                        pgeqDiscrete # (pfromData newStakeDatum.stakedAmount) # pzeroDiscrete
+                      ]
               let expectedValue = paddValue # continuingValue # (pdiscreteValue # delta)
 
-              -- TODO: As above, needs to be >=, rather than ==
-              let correctValue = pdata value #== pdata expectedValue
-              isScriptAddress #&& correctOutputDatum #&& correctValue
+              -- TODO: Same as above. This is quite inefficient now, as it does two lookups
+              -- instead of a more efficient single pass,
+              -- but it doesn't really matter for this. At least it's correct.
+              let valueCorrect =
+                    foldr1
+                      (#&&)
+                      [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
+                      , pgeqByClass'
+                          ( AssetClass
+                              ( fromString . symbolVal $ Proxy @ac
+                              , fromString . symbolVal $ Proxy @n
+                              )
+                          )
+                          # value
+                          # expectedValue
+                      , pgeqBySymbol
+                          # stCurrencySymbol
+                          # value
+                          # expectedValue
+                      ]
+
+              foldr1
+                (#&&)
+                [ ptraceIfFalse "isScriptAddress" isScriptAddress
+                , ptraceIfFalse "correctOutputDatum" correctOutputDatum
+                , ptraceIfFalse "valueCorrect" valueCorrect
+                ]
 
         popaque (pconstant ())
 
diff --git a/agora/Agora/Utils.hs b/agora/Agora/Utils.hs
index 7cb9825..9c5224a 100644
--- a/agora/Agora/Utils.hs
+++ b/agora/Agora/Utils.hs
@@ -19,6 +19,9 @@ module Agora.Utils (
   psymbolValueOf,
   passetClassValueOf,
   passetClassValueOf',
+  pgeqByClass,
+  pgeqBySymbol,
+  pgeqByClass',
   pfindTxInByTxOutRef,
   psingletonValue,
   pfindMap,
@@ -180,6 +183,27 @@ passetClassValueOf' :: AssetClass -> Term s (PValue :--> PInteger)
 passetClassValueOf' (AssetClass (sym, token)) =
   passetClassValueOf # pconstant sym # pconstant token
 
+-- | Return '>=' on two values comparing by only a particular AssetClass
+pgeqByClass :: Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PValue :--> PBool)
+pgeqByClass =
+  phoistAcyclic $
+    plam $ \cs tn a b ->
+      passetClassValueOf # cs # tn # b #<= passetClassValueOf # cs # tn # a
+
+-- | Return '>=' on two values comparing by only a particular CurrencySymbol
+pgeqBySymbol :: Term s (PCurrencySymbol :--> PValue :--> PValue :--> PBool)
+pgeqBySymbol =
+  phoistAcyclic $
+    plam $ \cs a b ->
+      psymbolValueOf # cs # b #<= psymbolValueOf # cs # a
+
+-- | Return '>=' on two values comparing by only a particular Haskell-level AssetClass
+pgeqByClass' :: AssetClass -> Term s (PValue :--> PValue :--> PBool)
+pgeqByClass' ac =
+  phoistAcyclic $
+    plam $ \a b ->
+      passetClassValueOf' ac # b #<= passetClassValueOf' ac # a
+
 -- | Union two maps using a merge function on collisions.
 pmapUnionWith :: forall k v s. PIsData v => Term s ((v :--> v :--> v) :--> PMap k v :--> PMap k v :--> PMap k v)
 pmapUnionWith = phoistAcyclic $
diff --git a/agora/PPrelude.hs b/agora/PPrelude.hs
index 3a8025b..8fba4be 100644
--- a/agora/PPrelude.hs
+++ b/agora/PPrelude.hs
@@ -1,7 +1,17 @@
+{- |
+Module     : PPrelude
+Maintainer : emi@haskell.fyi
+Description: Prelude imported throughout this project
+
+Prelude imported throughout this project
+-}
 module PPrelude (
   module Prelude,
   module Plutarch.Prelude,
+  module Plutarch,
 ) where
 
+-- These are not exported by Plutarch.Prelude, for some reason. Maybe we can 'fix' this upstream?
+import Plutarch (ClosedTerm, compile)
 import Plutarch.Prelude
 import Prelude
diff --git a/flake.nix b/flake.nix
index 87be54c..e49426e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -8,7 +8,8 @@
   inputs.nixpkgs-2111 = { url = "github:NixOS/nixpkgs/nixpkgs-21.11-darwin"; };
 
   inputs.plutarch.url = "github:peter-mlabs/plutarch/liqwid/extra";
-  inputs.plutarch.inputs.nixpkgs.follows = "plutarch/haskell-nix/nixpkgs-unstable";
+  inputs.plutarch.inputs.nixpkgs.follows =
+    "plutarch/haskell-nix/nixpkgs-unstable";
 
   # https://github.com/mlabs-haskell/apropos-tx/pull/28
   inputs.apropos-tx.url =
@@ -18,31 +19,37 @@
 
   outputs = inputs@{ self, nixpkgs, haskell-nix, plutarch, ... }:
     let
-      supportedSystems = with nixpkgs.lib.systems.supported; tier1 ++ tier2 ++ tier3;
+      supportedSystems = with nixpkgs.lib.systems.supported;
+        tier1 ++ tier2 ++ tier3;
 
       perSystem = nixpkgs.lib.genAttrs supportedSystems;
 
-      nixpkgsFor = system: import nixpkgs { inherit system; overlays = [ haskell-nix.overlay ]; inherit (haskell-nix) config; };
-      nixpkgsFor' = system: import nixpkgs { inherit system; inherit (haskell-nix) config; };
+      nixpkgsFor = system:
+        import nixpkgs {
+          inherit system;
+          overlays = [ haskell-nix.overlay ];
+          inherit (haskell-nix) config;
+        };
+      nixpkgsFor' = system:
+        import nixpkgs {
+          inherit system;
+          inherit (haskell-nix) config;
+        };
 
       ghcVersion = "ghc921";
 
       projectFor = system:
-        let pkgs = nixpkgsFor system; in
-        let pkgs' = nixpkgsFor' system; in
-        (nixpkgsFor system).haskell-nix.cabalProject' {
+        let pkgs = nixpkgsFor system;
+        in let pkgs' = nixpkgsFor' system;
+        in (nixpkgsFor system).haskell-nix.cabalProject' {
           src = ./.;
           compiler-nix-name = ghcVersion;
           inherit (plutarch) cabalProjectLocal;
           extraSources = plutarch.extraSources ++ [
             {
               src = inputs.plutarch;
-              subdirs = [
-                "."
-                "plutarch-test"
-                "plutarch-extra"
-                "plutarch-numeric"
-              ];
+              subdirs =
+                [ "." "plutarch-test" "plutarch-extra" "plutarch-numeric" ];
             }
             {
               src = inputs.apropos-tx;
@@ -57,18 +64,17 @@
 
             # We use the ones from Nixpkgs, since they are cached reliably.
             # Eventually we will probably want to build these with haskell.nix.
-            nativeBuildInputs = with pkgs';
-              [
-                entr
-                haskellPackages.apply-refact
-                git
-                fd
-                cabal-install
-                hlint
-                haskellPackages.cabal-fmt
-                nixpkgs-fmt
-                graphviz
-              ];
+            nativeBuildInputs = with pkgs'; [
+              entr
+              haskellPackages.apply-refact
+              git
+              fd
+              cabal-install
+              haskell.packages."${ghcVersion}".hlint
+              haskellPackages.cabal-fmt
+              nixpkgs-fmt
+              graphviz
+            ];
 
             inherit (plutarch) tools;
 
@@ -87,42 +93,44 @@
         let
           pkgs = nixpkgsFor system;
           pkgs' = nixpkgsFor' system;
-        in
-        pkgs.runCommand "format-check"
-          {
-            nativeBuildInputs = [ pkgs'.git pkgs'.fd pkgs'.haskellPackages.cabal-fmt pkgs'.nixpkgs-fmt (pkgs.haskell-nix.tools ghcVersion { inherit (plutarch.tools) fourmolu; }).fourmolu ];
-          } ''
+        in pkgs.runCommand "format-check" {
+          nativeBuildInputs = [
+            pkgs'.git
+            pkgs'.fd
+            pkgs'.haskellPackages.cabal-fmt
+            pkgs'.nixpkgs-fmt
+            (pkgs.haskell-nix.tools ghcVersion {
+              inherit (plutarch.tools) fourmolu;
+            }).fourmolu
+          ];
+        } ''
           export LC_CTYPE=C.UTF-8
           export LC_ALL=C.UTF-8
           export LANG=C.UTF-8
           cd ${self}
-          make format_check
+          make format_check || (echo "    Please run 'make format'" ; exit 1)
           mkdir $out
-        ''
-      ;
-    in
-    {
+        '';
+    in {
       project = perSystem projectFor;
       flake = perSystem (system: (projectFor system).flake { });
 
       packages = perSystem (system: self.flake.${system}.packages);
+
+      # Define what we want to test
       checks = perSystem (system:
-        self.flake.${system}.checks
-        // {
+        self.flake.${system}.checks // {
           formatCheck = formatCheckFor system;
-        }
-      );
+          agora = self.flake.${system}.packages."agora:lib:agora";
+          agora-test = self.flake.${system}.packages."agora:test:agora-test";
+        });
       check = perSystem (system:
-        (nixpkgsFor system).runCommand "combined-test"
-          {
-            checksss = builtins.attrValues self.checks.${system};
-          } ''
+        (nixpkgsFor system).runCommand "combined-test" {
+          checksss = builtins.attrValues self.checks.${system};
+        } ''
           echo $checksss
           touch $out
-        ''
-      );
+        '');
       devShell = perSystem (system: self.flake.${system}.devShell);
     };
 }
-
-