diff --git a/ouroboros-consensus/ouroboros-consensus.cabal b/ouroboros-consensus/ouroboros-consensus.cabal
index acbca582c1..4a0ac254c4 100644
--- a/ouroboros-consensus/ouroboros-consensus.cabal
+++ b/ouroboros-consensus/ouroboros-consensus.cabal
@@ -208,6 +208,8 @@ library
     Ouroboros.Consensus.NodeId
     Ouroboros.Consensus.Peras.SelectView
     Ouroboros.Consensus.Peras.Weight
+    Ouroboros.Consensus.Peras.Voting
+    Ouroboros.Consensus.Peras.Params
     Ouroboros.Consensus.Protocol.Abstract
     Ouroboros.Consensus.Protocol.BFT
     Ouroboros.Consensus.Protocol.LeaderSchedule
@@ -310,6 +312,7 @@ library
     Ouroboros.Consensus.Util.NormalForm.StrictMVar
     Ouroboros.Consensus.Util.NormalForm.StrictTVar
     Ouroboros.Consensus.Util.Orphans
+    Ouroboros.Consensus.Util.Pred
     Ouroboros.Consensus.Util.RedundantConstraints
     Ouroboros.Consensus.Util.STM
     Ouroboros.Consensus.Util.Time
@@ -613,8 +616,10 @@ test-suite consensus-test
     Test.Consensus.MiniProtocol.ObjectDiffusion.PerasCert.Smoke
     Test.Consensus.MiniProtocol.ObjectDiffusion.Smoke
     Test.Consensus.Peras.WeightSnapshot
+    Test.Consensus.Peras.Voting
     Test.Consensus.Util.MonadSTM.NormalForm
     Test.Consensus.Util.Versioned
+    Test.Consensus.Util.Pred
 
   build-depends:
     QuickCheck,
diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Block/SupportsPeras.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Block/SupportsPeras.hs
index 41adcb03fa..1e2d27e34a 100644
--- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Block/SupportsPeras.hs
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Block/SupportsPeras.hs
@@ -13,16 +13,16 @@
 
 module Ouroboros.Consensus.Block.SupportsPeras
   ( PerasRoundNo (..)
+  , onPerasRoundNo
   , PerasWeight (..)
   , BlockSupportsPeras (..)
   , PerasCert (..)
   , PerasCfg (..)
   , ValidatedPerasCert (..)
   , makePerasCfg
-  , HasPerasCert (..)
-  , getPerasCertRound
-  , getPerasCertBoostedBlock
-  , getPerasCertBoost
+  , HasPerasCertRound (..)
+  , HasPerasCertBoostedBlock (..)
+  , HasPerasCertBoost (..)
 
     -- * Ouroboros Peras round length
   , PerasRoundLength (..)
@@ -45,6 +45,7 @@ import Quiet (Quiet (..))
 
 newtype PerasRoundNo = PerasRoundNo {unPerasRoundNo :: Word64}
   deriving Show via Quiet PerasRoundNo
+  deriving Semigroup via Sum Word64
   deriving stock Generic
   deriving newtype (Enum, Eq, Ord, NoThunks, Serialise)
 
@@ -54,6 +55,10 @@ instance Condense PerasRoundNo where
 instance ShowProxy PerasRoundNo where
   showProxy _ = "PerasRoundNo"
 
+-- | Lift a binary operation on 'Word64' to 'PerasRoundNo'
+onPerasRoundNo :: (Word64 -> Word64 -> Word64) -> PerasRoundNo -> PerasRoundNo -> PerasRoundNo
+onPerasRoundNo f a b = PerasRoundNo $ (unPerasRoundNo a `f` unPerasRoundNo b)
+
 newtype PerasWeight = PerasWeight {unPerasWeight :: Word64}
   deriving Show via Quiet PerasWeight
   deriving stock Generic
@@ -158,29 +163,51 @@ makePerasCfg _ =
     { perasCfgWeightBoost = boostPerCert
     }
 
-class StandardHash blk => HasPerasCert cert blk | cert -> blk where
-  getPerasCert :: cert -> PerasCert blk
+-- | Extract the certificate round from a Peras certificate container
+class HasPerasCertRound cert where
+  getPerasCertRound :: cert -> PerasRoundNo
+
+instance HasPerasCertRound (PerasCert blk) where
+  getPerasCertRound = pcCertRound
+
+instance HasPerasCertRound (ValidatedPerasCert blk) where
+  getPerasCertRound = getPerasCertRound . vpcCert
 
-getPerasCertRound :: HasPerasCert cert blk => cert -> PerasRoundNo
-getPerasCertRound = pcCertRound . getPerasCert
+instance
+  HasPerasCertRound cert =>
+  HasPerasCertRound (WithArrivalTime cert)
+  where
+  getPerasCertRound = getPerasCertRound . forgetArrivalTime
 
-getPerasCertBoostedBlock :: HasPerasCert cert blk => cert -> Point blk
-getPerasCertBoostedBlock = pcCertBoostedBlock . getPerasCert
+-- | Extract the boosted block point from a Peras certificate container
+class HasPerasCertBoostedBlock cert where
+  type BoostedBlock cert
+  getPerasCertBoostedBlock :: cert -> BoostedBlock cert
 
-instance StandardHash blk => HasPerasCert (PerasCert blk) blk where
-  getPerasCert = id
+instance HasPerasCertBoostedBlock (PerasCert blk) where
+  type BoostedBlock (PerasCert blk) = Point blk
+  getPerasCertBoostedBlock = pcCertBoostedBlock
 
-instance StandardHash blk => HasPerasCert (ValidatedPerasCert blk) blk where
-  getPerasCert = vpcCert
+instance HasPerasCertBoostedBlock (ValidatedPerasCert blk) where
+  type BoostedBlock (ValidatedPerasCert blk) = Point blk
+  getPerasCertBoostedBlock = getPerasCertBoostedBlock . vpcCert
 
-instance HasPerasCert cert blk => HasPerasCert (WithArrivalTime cert) blk where
-  getPerasCert = getPerasCert . forgetArrivalTime
+instance
+  HasPerasCertBoostedBlock cert =>
+  HasPerasCertBoostedBlock (WithArrivalTime cert)
+  where
+  type BoostedBlock (WithArrivalTime cert) = BoostedBlock cert
+  getPerasCertBoostedBlock = getPerasCertBoostedBlock . forgetArrivalTime
 
-class HasPerasCertBoost cert blk | cert -> blk where
+-- | Extract the certificate boost from a Peras certificate container
+class HasPerasCertBoost cert where
   getPerasCertBoost :: cert -> PerasWeight
 
-instance HasPerasCertBoost (ValidatedPerasCert blk) blk where
+instance HasPerasCertBoost (ValidatedPerasCert blk) where
   getPerasCertBoost = vpcCertBoost
 
-instance HasPerasCertBoost cert blk => HasPerasCertBoost (WithArrivalTime cert) blk where
+instance
+  HasPerasCertBoost cert =>
+  HasPerasCertBoost (WithArrivalTime cert)
+  where
   getPerasCertBoost = getPerasCertBoost . forgetArrivalTime
diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/MiniProtocol/ObjectDiffusion/ObjectPool/PerasCert.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/MiniProtocol/ObjectDiffusion/ObjectPool/PerasCert.hs
index f4f0cb5562..68b923218b 100644
--- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/MiniProtocol/ObjectDiffusion/ObjectPool/PerasCert.hs
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/MiniProtocol/ObjectDiffusion/ObjectPool/PerasCert.hs
@@ -15,7 +15,7 @@ import Control.Monad ((>=>))
 import GHC.Exception (throw)
 import Ouroboros.Consensus.Block
 import Ouroboros.Consensus.BlockchainTime (WithArrivalTime)
-import Ouroboros.Consensus.BlockchainTime.WallClock.Types (SystemTime (..), addArrivalTime)
+import Ouroboros.Consensus.BlockchainTime.WallClock.Types (SystemTime (..), addArrivalTime, WithArrivalTime (..))
 import Ouroboros.Consensus.MiniProtocol.ObjectDiffusion.ObjectPool.API
 import Ouroboros.Consensus.Storage.ChainDB.API (ChainDB)
 import qualified Ouroboros.Consensus.Storage.ChainDB.API as ChainDB
@@ -28,7 +28,7 @@ import qualified Ouroboros.Consensus.Storage.PerasCertDB.API as PerasCertDB
 import Ouroboros.Consensus.Util.IOLike
 
 makePerasCertPoolReaderFromSnapshot ::
-  (IOLike m, StandardHash blk) =>
+  IOLike m =>
   STM m (PerasCertSnapshot blk) ->
   ObjectPoolReader PerasRoundNo (PerasCert blk) PerasCertTicketNo m
 makePerasCertPoolReaderFromSnapshot getCertSnapshot =
@@ -39,13 +39,13 @@ makePerasCertPoolReaderFromSnapshot getCertSnapshot =
         certSnapshot <- getCertSnapshot
         pure $
           take (fromIntegral limit) $
-            [ (ticketNo, getPerasCertRound cert, pure (getPerasCert cert))
+            [ (ticketNo, getPerasCertRound cert, pure (vpcCert (forgetArrivalTime cert)))
             | (cert, ticketNo) <- PerasCertDB.getCertsAfter certSnapshot lastKnown
             ]
     }
 
 makePerasCertPoolReaderFromCertDB ::
-  (IOLike m, StandardHash blk) =>
+  IOLike m =>
   PerasCertDB m blk -> ObjectPoolReader PerasRoundNo (PerasCert blk) PerasCertTicketNo m
 makePerasCertPoolReaderFromCertDB perasCertDB =
   makePerasCertPoolReaderFromSnapshot (PerasCertDB.getCertSnapshot perasCertDB)
@@ -65,7 +65,7 @@ makePerasCertPoolWriterFromCertDB systemTime perasCertDB =
     }
 
 makePerasCertPoolReaderFromChainDB ::
-  (IOLike m, StandardHash blk) =>
+  IOLike m =>
   ChainDB m blk -> ObjectPoolReader PerasRoundNo (PerasCert blk) PerasCertTicketNo m
 makePerasCertPoolReaderFromChainDB chainDB =
   makePerasCertPoolReaderFromSnapshot (ChainDB.getPerasCertSnapshot chainDB)
diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/Params.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/Params.hs
new file mode 100644
index 0000000000..a5b172ef44
--- /dev/null
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/Params.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+-- | Peras protocol parameters
+module Ouroboros.Consensus.Peras.Params
+  ( PerasIgnoranceRounds (..)
+  , PerasCooldownRounds (..)
+  , PerasBlockMinSlots (..)
+  , PerasCertArrivalThreshold (..)
+  , PerasParams (..)
+  )
+where
+
+import Data.Word (Word64)
+import GHC.Generics (Generic)
+import Ouroboros.Consensus.Util.IOLike (NoThunks)
+import Quiet (Quiet (..))
+
+{-------------------------------------------------------------------------------
+  Protocol parameters
+-------------------------------------------------------------------------------}
+
+-- | Number of rounds for which to ignore certificates after entering a cool-down period.
+newtype PerasIgnoranceRounds = PerasIgnoranceRounds {unPerasIgnoranceRounds :: Word64}
+  deriving Show via Quiet PerasIgnoranceRounds
+  deriving stock Generic
+  deriving newtype (Enum, Eq, Ord, NoThunks)
+
+-- | Minimum number of rounds to wait before voting again after a cool-down period starts.
+newtype PerasCooldownRounds = PerasCooldownRounds {unPerasCooldownRounds :: Word64}
+  deriving Show via Quiet PerasCooldownRounds
+  deriving stock Generic
+  deriving newtype (Enum, Eq, Ord, NoThunks)
+
+-- | Minimum age (in slots) of a block to be voted on at the beginning of a Peras round.
+newtype PerasBlockMinSlots = PerasBlockMinSlots {unPerasBlockMinSlots :: Word64}
+  deriving Show via Quiet PerasBlockMinSlots
+  deriving stock Generic
+  deriving newtype (Enum, Eq, Ord, NoThunks)
+
+-- | Maximum number of slots to after the start of a round to consider a certificate for voting.
+newtype PerasCertArrivalThreshold = PerasCertArrivalThreshold {unPerasCertArrivalThreshold :: Word64}
+  deriving Show via Quiet PerasCertArrivalThreshold
+  deriving stock Generic
+  deriving newtype (Enum, Eq, Ord, NoThunks)
+
+{-------------------------------------------------------------------------------
+  Protocol parameters bundle
+-------------------------------------------------------------------------------}
+
+data PerasParams = PerasParams
+  { perasIgnoranceRounds :: PerasIgnoranceRounds
+  , perasCooldownRounds :: PerasCooldownRounds
+  , perasBlockMinSlots :: PerasBlockMinSlots
+  , perasCertArrivalThreshold :: PerasCertArrivalThreshold
+  }
+  deriving (Show, Generic, NoThunks)
diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/Voting.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/Voting.hs
new file mode 100644
index 0000000000..790a44fd42
--- /dev/null
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/Voting.hs
@@ -0,0 +1,299 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | Pure Peras voting rules
+--
+-- This module implements the Peras voting rules in a pure fasion, along with
+-- the necessary inpure machinery to retrieve their inputs. These rules are
+-- translated as verbatim as possible from:
+--
+-- https://github.com/cardano-foundation/CIPs/blob/master/CIP-0140/README.md#rules-for-voting-in-a-round
+module Ouroboros.Consensus.Peras.Voting
+  ( PerasVotingView (..)
+  , mkPerasVotingView
+  , isPerasVotingAllowed
+  , PerasVotingRule (..)
+  , VoteReason (..)
+  , NoVoteReason (..)
+  , perasVR1A
+  , perasVR1B
+  , perasVR2A
+  , perasVR2B
+  , perasVR1
+  , perasVR2
+  , perasVotingRules
+  )
+where
+
+import Data.Bifunctor (bimap)
+import Data.Coerce (coerce)
+import Data.Typeable (Typeable)
+import GHC.Word (Word64)
+import Ouroboros.Consensus.Block.Abstract
+  ( GetHeader (..)
+  , Header
+  , SlotNo (..)
+  , StandardHash
+  , castPoint
+  )
+import Ouroboros.Consensus.Block.SupportsPeras
+  ( HasPerasCertRound
+  , PerasRoundNo (..)
+  , ValidatedPerasCert
+  , getPerasCertBoostedBlock
+  , getPerasCertRound
+  , onPerasRoundNo
+  )
+import Ouroboros.Consensus.BlockchainTime.WallClock.Types
+  ( WithArrivalTime (..)
+  )
+import Ouroboros.Consensus.HardFork.History.EraParams
+import qualified Ouroboros.Consensus.HardFork.History.Qry as HF
+import qualified Ouroboros.Consensus.HardFork.History.Summary as HF
+import Ouroboros.Consensus.Peras.Params
+  ( PerasBlockMinSlots (..)
+  , PerasCertArrivalThreshold (..)
+  , PerasCooldownRounds (..)
+  , PerasIgnoranceRounds (..)
+  , PerasParams (..)
+  )
+import Ouroboros.Consensus.Util.Pred
+  ( Evidence
+  , Explainable (..)
+  , ExplanationMode (..)
+  , Pred (..)
+  , evalPred
+  )
+import Ouroboros.Network.AnchoredFragment (AnchoredFragment)
+import qualified Ouroboros.Network.AnchoredFragment as AF
+
+{-------------------------------------------------------------------------------
+  Voting interface
+-------------------------------------------------------------------------------}
+
+-- | Interface needed to evaluate the Peras voting rules
+data PerasVotingView cert = PerasVotingView
+  { pvvPerasParams :: !PerasParams
+  -- ^ Peras protocol parameters.
+  , pvvCurrRoundNo :: !PerasRoundNo
+  -- ^ The current Peras round number.
+  , pvvLatestCertSeen :: !cert
+  -- ^ The most recent certificate seen by the voter.
+  , pvvLatestCertOnChain :: !cert
+  -- ^ The most recent certificate present in some chain.
+  , pvvRoundStart :: PerasRoundNo -> SlotNo
+  -- ^ Get the slot number at the start of a Peras round.
+  , pvvArrivalSlot :: cert -> SlotNo
+  -- ^ Get the arrival slot number of a certificate
+  , pvvCandidateExtendsCert :: cert -> Bool
+  -- ^ Does the candidate block extend the one boosted by a certificate?
+  }
+
+-- | Construct a 'PerasVotingView'.
+--
+-- NOTE: this assumes that the client code computes all the needed inputs
+-- within the same STM transaction, or the results may be inconsistent.
+mkPerasVotingView ::
+  ( cert ~ WithArrivalTime (ValidatedPerasCert blk)
+  , StandardHash blk
+  , Typeable blk
+  , GetHeader blk
+  ) =>
+  PerasParams ->
+  PerasRoundNo ->
+  cert ->
+  cert ->
+  AnchoredFragment (Header blk) ->
+  HF.Summary blks ->
+  PerasVotingView cert
+mkPerasVotingView
+  perasParams
+  currRoundNo
+  latestCertSeen
+  latestCertOnChain
+  currChain
+  summary =
+    PerasVotingView
+      { pvvPerasParams = perasParams
+      , pvvCurrRoundNo = currRoundNo
+      , pvvLatestCertSeen = latestCertSeen
+      , pvvLatestCertOnChain = latestCertOnChain
+      , pvvRoundStart = roundStart
+      , pvvArrivalSlot = arrivalSlot
+      , pvvCandidateExtendsCert = candidateExtendsCert
+      }
+   where
+    -- The Peras block minium slots parameter (L).
+    blockMinSlots = coerce (perasBlockMinSlots perasParams)
+
+    -- Candidate block slot, i.e., that of the block that's at least
+    -- 'blockMinSlots' old from the start of the current round.
+    candidateSlot = roundStart currRoundNo - blockMinSlots
+
+    -- The prefix of our current chain leading to the candidate block.
+    chainAtCandidate = fst (AF.splitAtSlot candidateSlot currChain)
+
+    -- The slot number at the start of a Peras round.
+    --
+    -- NOTE: this might throw a 'PastHorizonException' if the caller is not
+    -- is not prepared to start voting.
+    roundStart roundNo =
+      fst $
+        fromPerasEnabled
+          (error "mkPerasVotingView: Peras is disabled in the current era")
+          (HF.runQueryPure (HF.perasRoundNoToSlot roundNo) summary)
+
+    -- The arrival slot number of a certificate.
+    --
+    -- NOTE: this might throw a 'PastHorizonException' if the caller does not
+    -- ensure that the arrival time is within the current realizable horizon.
+    arrivalSlot cert = slotNo
+     where
+      (slotNo, _, _) =
+        HF.runQueryPure (HF.wallclockToSlot (getArrivalTime cert)) summary
+
+    -- Does the candidate block extend the one boosted by a certificate?
+    --
+    -- This can be trivially tested by checking whether the certificate is
+    -- within the bounds of the chain prefix leading to the candidate block.
+    --
+    -- NOTE: in the case of an extremely old certificate boosting a block
+    -- beyond the immutable prefix, this could incorrectly return false even
+    -- if the voting candidate technically extends the certificate point.
+    -- However, this a boring case that we can safely ignore. Conversely,
+    -- the case of a certificate that's too new to be voted for is covered
+    -- by using the approriate prefix of our current chain.
+    candidateExtendsCert cert =
+      AF.withinFragmentBounds certBoostedBlockHeader chainAtCandidate
+     where
+      certBoostedBlockHeader = castPoint (getPerasCertBoostedBlock cert)
+
+-- | Reason for voting being disallowed
+newtype NoVoteReason = NoVoteReason (Evidence PerasVotingRule)
+  deriving (Show, Explainable)
+
+-- | Reason for voting being allowed
+newtype VoteReason = VoteReason (Evidence PerasVotingRule)
+  deriving (Show, Explainable)
+
+-- | Evaluate whether voting is allowed or not according to the voting rules
+isPerasVotingAllowed ::
+  HasPerasCertRound cert =>
+  PerasVotingView cert ->
+  Either NoVoteReason VoteReason
+isPerasVotingAllowed pvv =
+  bimap NoVoteReason VoteReason $
+    evalPred (perasVotingRules pvv)
+
+{-------------------------------------------------------------------------------
+  Voting rules
+-------------------------------------------------------------------------------}
+
+-- | Voting rules
+--
+-- Each constructor corresponds to a voting rule as per CIP-0140.
+--
+-- * VR1x correspond to the "happy" path, i.e., when nodes proceed to vote
+-- normally, whereas
+-- * VR2x correspond to the "cool-down" path, i.e., when nodes are exiting a
+-- cool-down period.
+data PerasVotingRule = VR1A | VR1B | VR2A | VR2B
+  deriving (Show, Eq)
+
+instance Explainable PerasVotingRule where
+  explain Shallow = \case
+    VR1A -> "VR-1A"
+    VR1B -> "VR-1B"
+    VR2A -> "VR-2A"
+    VR2B -> "VR-2B"
+  explain Deep = \case
+    VR1A ->
+      "voter has seen the certificate for the previous round in time"
+    VR1B ->
+      "the block being voted upon extends the most recently certified block"
+    VR2A ->
+      "the last certificate seen is from at least R rounds ago"
+    VR2B ->
+      "the last certificate on chain is from exactly c⋅K rounds ago"
+
+-- | VR-1A: the voter has seen the certificate for the previous round, and the
+-- certificate was received in the first X slots after the start of the round.
+perasVR1A ::
+  HasPerasCertRound cert =>
+  PerasVotingView cert -> Pred PerasVotingRule
+perasVR1A pvv =
+  VR1A
+    := (pvvCurrRoundNo pvv :==: latestCertSeenRoundNo <> _1)
+    :/\: (latestCertSeenArrivalSlot :<=: latestCertSeenRoundStart + _X)
+ where
+  _1 = coerce @Word64 1
+  _X = coerce (perasCertArrivalThreshold (pvvPerasParams pvv))
+  latestCertSeenRoundNo = getPerasCertRound (pvvLatestCertSeen pvv)
+  latestCertSeenRoundStart = pvvRoundStart pvv latestCertSeenRoundNo
+  latestCertSeenArrivalSlot = pvvArrivalSlot pvv (pvvLatestCertSeen pvv)
+
+-- | VR-1B: the block being voted upon extends the most recently certified one.
+perasVR1B :: PerasVotingView cert -> Pred PerasVotingRule
+perasVR1B pvv =
+  VR1B := Bool (pvvCandidateExtendsCert pvv (pvvLatestCertSeen pvv))
+
+-- | VR-2A: the last certificate a party has seen is from a round at least R
+-- rounds previously. This enforces the chain-healing period that must occur
+-- before leaving a cool-down period.
+perasVR2A ::
+  HasPerasCertRound cert =>
+  PerasVotingView cert ->
+  Pred PerasVotingRule
+perasVR2A pvv =
+  VR2A := latestCertSeenRoundNo <> _R :<=: currRoundNo
+ where
+  _R = coerce (perasIgnoranceRounds (pvvPerasParams pvv))
+  currRoundNo = pvvCurrRoundNo pvv
+  latestCertSeenRoundNo = getPerasCertRound (pvvLatestCertSeen pvv)
+
+-- | VR-2B: the last certificate included in a party's current chain is from a
+-- round exactly c⋅K rounds ago for some c ∈ ℕ with c ≥ 0. This enforces chain
+-- quality and common prefix before leaving a cool-down period.
+perasVR2B ::
+  HasPerasCertRound cert =>
+  PerasVotingView cert ->
+  Pred PerasVotingRule
+perasVR2B pvv =
+  VR2B
+    := (currRoundNo :>: latestCertOnChainRoundNo)
+    :/\: (currRoundNo `rmod` _K :==: latestCertOnChainRoundNo `rmod` _K)
+ where
+  _K = coerce (perasCooldownRounds (pvvPerasParams pvv))
+  currRoundNo = pvvCurrRoundNo pvv
+  latestCertOnChainRoundNo = getPerasCertRound (pvvLatestCertOnChain pvv)
+  rmod = onPerasRoundNo mod
+
+-- | Both VR-1A and VR-1B hold, which is the situation typically occurring when
+-- the voting has regularly occurred in preceding rounds.
+perasVR1 ::
+  HasPerasCertRound cert =>
+  PerasVotingView cert ->
+  Pred PerasVotingRule
+perasVR1 pvv =
+  perasVR1A pvv :/\: perasVR1B pvv
+
+-- | Both VR-2A and VR-2B hold, which is the situation typically occurring when
+-- the chain is about to exit a cool-down period.
+perasVR2 ::
+  HasPerasCertRound cert =>
+  PerasVotingView cert ->
+  Pred PerasVotingRule
+perasVR2 pvv =
+  perasVR2A pvv :/\: perasVR2B pvv
+
+-- | Voting is allowed if either VR-1A and VR-1B hold, or VR-2A and VR-2B hold.
+perasVotingRules ::
+  HasPerasCertRound cert =>
+  PerasVotingView cert ->
+  Pred PerasVotingRule
+perasVotingRules pvv =
+  perasVR1 pvv :\/: perasVR2 pvv
diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/ChainDB/Impl/ChainSel.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/ChainDB/Impl/ChainSel.hs
index 9babf8a400..0b6ef598e6 100644
--- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/ChainDB/Impl/ChainSel.hs
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/ChainDB/Impl/ChainSel.hs
@@ -327,7 +327,7 @@ addBlockAsync CDB{cdbTracer, cdbChainSelQueue} =
 
 addPerasCertAsync ::
   forall m blk.
-  (IOLike m, HasHeader blk) =>
+  (IOLike m) =>
   ChainDbEnv m blk ->
   WithArrivalTime (ValidatedPerasCert blk) ->
   m (AddPerasCertPromise m)
diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/ChainDB/Impl/Types.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/ChainDB/Impl/Types.hs
index 17a6e941cb..dbc003b7b5 100644
--- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/ChainDB/Impl/Types.hs
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/ChainDB/Impl/Types.hs
@@ -607,7 +607,7 @@ addBlockToAdd tracer (ChainSelQueue{varChainSelQueue, varChainSelPoints}) punish
 
 -- | Add a Peras certificate to the background queue.
 addPerasCertToQueue ::
-  (IOLike m, StandardHash blk) =>
+  (IOLike m) =>
   Tracer m (TraceAddPerasCertEvent blk) ->
   ChainSelQueue m blk ->
   WithArrivalTime (ValidatedPerasCert blk) ->
diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/Impl.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/Impl.hs
index 3428ce5f64..c6e32a8585 100644
--- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/Impl.hs
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Storage/PerasCertDB/Impl.hs
@@ -215,7 +215,7 @@ implGetCertSnapshot PerasCertDbEnv{pcdbVolatileState} =
 
 implGarbageCollect ::
   forall m blk.
-  (IOLike m, StandardHash blk) =>
+  (IOLike m) =>
   PerasCertDbEnv m blk -> SlotNo -> m ()
 implGarbageCollect PerasCertDbEnv{pcdbVolatileState} slot =
   -- No need to update the 'Fingerprint' as we only remove certificates that do
diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Util/Pred.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Util/Pred.hs
new file mode 100644
index 0000000000..b4e022c404
--- /dev/null
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Util/Pred.hs
@@ -0,0 +1,233 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+-- | Self-explaining boolean predicates
+--
+-- These can be used to provide detailed counterexamples or witnesses for
+-- boolean predicate that evaluate to 'False' or 'True', respectively.
+--
+-- NOTE: to keep this as simple as possible, we do not perform any boolean
+-- simplifications (e.g., double negations, or De Morgan's laws) on the
+-- predicates while evauating them. This can be added later if needed.
+module Ouroboros.Consensus.Util.Pred
+  ( Pred (..)
+  , Evidence
+  , evalPred
+  , Explainable (..)
+  , ExplanationMode (..)
+  , ShowExplain (..)
+  , explainShallow
+  , explainDeep
+  )
+where
+
+import Data.Bifunctor (bimap)
+import Data.Typeable (Typeable, cast)
+
+{-------------------------------------------------------------------------------
+  Self-explaining boolean predicates
+-------------------------------------------------------------------------------}
+
+data Pred tag where
+  -- | Tag a predicate with some metadata
+  (:=) :: !tag -> !(Pred tag) -> Pred tag
+  -- | A concrete boolean value
+  Bool :: !Bool -> Pred tag
+  -- | Boolean negation
+  Not :: !(Pred tag) -> Pred tag
+  -- | Greater-than comparison
+  (:>:) :: (Typeable a, Ord a, Show a) => !a -> !a -> Pred tag
+  -- | Less-than-or-equal comparison
+  (:<=:) :: (Typeable a, Ord a, Show a) => !a -> !a -> Pred tag
+  -- | Equality comparison
+  (:==:) :: (Typeable a, Eq a, Show a) => !a -> !a -> Pred tag
+  -- | Conjunction
+  (:/\:) :: !(Pred tag) -> !(Pred tag) -> Pred tag
+  -- | Disjunction
+  (:\/:) :: !(Pred tag) -> !(Pred tag) -> Pred tag
+
+deriving instance Show tag => Show (Pred tag)
+
+instance Eq tag => Eq (Pred tag) where
+  (t1 := p1) == (t2 := p2) =
+    t1 == t2 && p1 == p2
+  Bool b1 == Bool b2 =
+    b1 == b2
+  Not p1 == Not p2 =
+    p1 == p2
+  (a1 :>: b1) == (a2 :>: b2)
+    | Just (a2', b2') <- cast (a2, b2) =
+        a1 == a2' && b1 == b2'
+  (a1 :<=: b1) == (a2 :<=: b2)
+    | Just (a2', b2') <- cast (a2, b2) =
+        a1 == a2' && b1 == b2'
+  (a1 :==: b1) == (a2 :==: b2)
+    | Just (a2', b2') <- cast (a2, b2) =
+        a1 == a2' && b1 == b2'
+  (a1 :/\: b1) == (a2 :/\: b2) =
+    a1 == a2 && b1 == b2
+  (a1 :\/: b1) == (a2 :\/: b2) =
+    a1 == a2 && b1 == b2
+  _ == _ =
+    False
+
+infixr 2 :=
+
+infixr 3 :\/:
+
+infixr 4 :/\:
+
+infixr 5 `Not`
+
+infix 5 :>:
+
+infix 5 :<=:
+
+infix 5 :==:
+
+-- | Sufficient evidence to show that a predicate is either true or false
+type Evidence a = Pred a
+
+-- | Evaluate a predicate, yielding either a counterexample or a witness.
+--
+-- The returned value contains the minimum (modulo conjunction/disjunction
+-- short circuiting) evidence needed to explain the outcome.
+--
+-- Some examples:
+--
+-- >>> data P = A | B | C  deriving Show
+-- >>> a = A := Bool True   -- a ~ True
+-- >>> b = B := 2+2 :==: 5  -- b ~ False
+-- >>> c = C := 10 :>: 5    -- c ~ True
+--
+-- >>> evalPred $ a :/\: c  -- success because both a~True and c~True
+-- Right ((A := Bool True) :/\: (C := 10 :>: 5))
+--
+-- >>> evalPred $ a :\/: b -- success because a~True, short-circuits
+-- Right (A := Bool True)
+--
+-- >>> evalPred $ a :/\: b :/\: c -- failure because b~False, short-circuits
+-- Left (B := 4 :==: 5)
+--
+-- >>> evalPred $ (b :\/: a) :/\: (b :\/: c) -- success because of a~True and c~True
+-- Right ((A := Bool True) :/\: (C := 10 :>: 5))
+--
+-- >>> evalPred $ b :\/: (Not c) -- failure because both b~False and c~True
+-- Left ((B := 4 :==: 5) :\/: Not (A := Bool True))
+--
+-- >>> evalPred $ Not (a :/\: b) -- success because b~False
+-- Right (Not (B := 4 :==: 5))
+--
+-- >>> evalPred $ Not (a :/\: c) -- failure because both a~True and c~True
+-- Left (Not ((A := Bool True) :/\: (C := 10 :>: 5)))
+evalPred :: Pred tag -> Either (Evidence tag) (Evidence tag)
+evalPred = \case
+  tag := p' ->
+    lift (tag :=) id p'
+  p@(Bool b) ->
+    boolean b p
+  Not p' ->
+    lift Not negation p'
+  p@(a :>: b) ->
+    boolean (a > b) p
+  p@(a :<=: b) ->
+    boolean (a <= b) p
+  p@(a :==: b) ->
+    boolean (a == b) p
+  a :/\: b ->
+    case evalPred a of
+      Left a' -> Left a' -- short-circuit
+      Right a' ->
+        case evalPred b of
+          Right b' -> Right (a' :/\: b')
+          Left b' -> Left b'
+  a :\/: b ->
+    case evalPred a of
+      Right a' -> Right a' -- short-circuit
+      Left a' ->
+        case evalPred b of
+          Right b' -> Right b'
+          Left b' -> Left (a' :\/: b')
+ where
+  boolean b p
+    | b = Right p
+    | otherwise = Left p
+
+  lift f g p = bimap f f (g (evalPred p))
+
+  negation = either Right Left
+
+{-------------------------------------------------------------------------------
+  Explainable type class
+-------------------------------------------------------------------------------}
+
+-- | Explanation mode
+--
+-- Used to control whether we want to continue explaining terms beyond tags
+-- * Shallow: only explain tags
+-- * Deep: explain full predicates
+data ExplanationMode = Shallow | Deep
+
+-- | Provides a human-readable explanation for a value
+class Explainable a where
+  explain :: ExplanationMode -> a -> String
+  explain = explainPrec 0
+
+  explainPrec :: Int -> ExplanationMode -> a -> String
+  explainPrec _ = explain
+
+  {-# MINIMAL (explain | explainPrec) #-}
+
+-- | Shallow explanation
+explainShallow :: Explainable a => a -> String
+explainShallow = explain Shallow
+
+-- | Deep explanation
+explainDeep :: Explainable a => a -> String
+explainDeep = explain Deep
+
+-- | Default 'Explainable' instance via 'Show' to be used with 'deriving via'
+newtype ShowExplain a = ShowExplain a
+  deriving stock Show
+
+instance Show a => Explainable (ShowExplain a) where
+  explain _ (ShowExplain a) = show a
+
+deriving via ShowExplain Bool instance Explainable Bool
+
+instance Explainable a => Explainable (Pred a) where
+  explainPrec prec mode = \case
+    tag := p ->
+      case mode of
+        Shallow ->
+          explainShallow tag
+        Deep ->
+          parensIf (prec > 1) $
+            explainShallow tag <> " := " <> explainPrec 2 mode p
+    Bool b ->
+      explain mode b
+    Not p ->
+      parensIf (prec > 4) $
+        "not " <> explainPrec 5 mode p
+    a :>: b ->
+      parensIf (prec > 4) $
+        show a <> " > " <> show b
+    a :<=: b ->
+      parensIf (prec > 4) $
+        show a <> " <= " <> show b
+    a :==: b ->
+      parensIf (prec > 4) $
+        show a <> " == " <> show b
+    a :/\: b ->
+      parensIf (prec > 4) $
+        explainPrec 4 mode a <> " and " <> explainPrec 3 mode b
+    a :\/: b ->
+      parensIf (prec > 2) $
+        explainPrec 3 mode a <> " or " <> explainPrec 2 mode b
+   where
+    parensIf :: Bool -> String -> String
+    parensIf True s = "(" <> s <> ")"
+    parensIf False s = s
diff --git a/ouroboros-consensus/test/consensus-test/Main.hs b/ouroboros-consensus/test/consensus-test/Main.hs
index 79d681213a..26c36e3cd8 100644
--- a/ouroboros-consensus/test/consensus-test/Main.hs
+++ b/ouroboros-consensus/test/consensus-test/Main.hs
@@ -21,11 +21,13 @@ import qualified Test.Consensus.MiniProtocol.ObjectDiffusion.Smoke (tests)
 import qualified Test.Consensus.Peras.WeightSnapshot (tests)
 import qualified Test.Consensus.Util.MonadSTM.NormalForm (tests)
 import qualified Test.Consensus.Util.Versioned (tests)
+import qualified Test.Consensus.Util.Pred (tests)
 import Test.Tasty
 import Test.Util.TestEnv
   ( defaultMainWithTestEnv
   , defaultTestEnvConfig
   )
+import qualified Test.Consensus.Peras.Voting
 
 main :: IO ()
 main = defaultMainWithTestEnv defaultTestEnvConfig tests
@@ -49,8 +51,10 @@ tests =
         , Test.Consensus.Mempool.StateMachine.tests
         ]
     , Test.Consensus.Peras.WeightSnapshot.tests
+    , Test.Consensus.Peras.Voting.tests
     , Test.Consensus.Util.MonadSTM.NormalForm.tests
     , Test.Consensus.Util.Versioned.tests
+    , Test.Consensus.Util.Pred.tests
     , testGroup
         "HardFork"
         [ testGroup
diff --git a/ouroboros-consensus/test/consensus-test/Test/Consensus/MiniProtocol/ObjectDiffusion/PerasCert/Smoke.hs b/ouroboros-consensus/test/consensus-test/Test/Consensus/MiniProtocol/ObjectDiffusion/PerasCert/Smoke.hs
index c0db35ff1a..aae01c253f 100644
--- a/ouroboros-consensus/test/consensus-test/Test/Consensus/MiniProtocol/ObjectDiffusion/PerasCert/Smoke.hs
+++ b/ouroboros-consensus/test/consensus-test/Test/Consensus/MiniProtocol/ObjectDiffusion/PerasCert/Smoke.hs
@@ -48,6 +48,7 @@ import Test.QuickCheck
 import Test.Tasty
 import Test.Tasty.QuickCheck (testProperty)
 import Test.Util.TestBlock
+import Ouroboros.Consensus.BlockchainTime.WallClock.Types (WithArrivalTime(..))
 
 tests :: TestTree
 tests =
@@ -152,6 +153,6 @@ prop_smoke protocolConstants (ListWithUniqueIds certs) =
         getAllInboundPoolContent = do
           snap <- atomically $ PerasCertDB.getCertSnapshot inboundPool
           let rawContent = PerasCertDB.getCertsAfter snap (PerasCertDB.zeroPerasCertTicketNo)
-          pure $ getPerasCert . fst <$> rawContent
+          pure $ vpcCert . forgetArrivalTime . fst <$> rawContent
 
     return (outboundPoolReader, inboundPoolWriter, getAllInboundPoolContent)
diff --git a/ouroboros-consensus/test/consensus-test/Test/Consensus/Peras/Voting.hs b/ouroboros-consensus/test/consensus-test/Test/Consensus/Peras/Voting.hs
new file mode 100644
index 0000000000..dd52ab713b
--- /dev/null
+++ b/ouroboros-consensus/test/consensus-test/Test/Consensus/Peras/Voting.hs
@@ -0,0 +1,249 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- | Test that the Peras voting rules can correctly decide when to vote.
+module Test.Consensus.Peras.Voting (tests) where
+
+import Data.Coerce (coerce)
+import GHC.Generics (Generic)
+import GHC.Word (Word64)
+import Ouroboros.Consensus.Block.Abstract (SlotNo (..))
+import Ouroboros.Consensus.Block.SupportsPeras
+  ( HasPerasCertRound (..)
+  , PerasRoundNo (..)
+  , getPerasCertRound
+  , onPerasRoundNo
+  )
+import Ouroboros.Consensus.BlockchainTime
+  ( RelativeTime (..)
+  )
+import Ouroboros.Consensus.Peras.Params
+  ( PerasBlockMinSlots (..)
+  , PerasCertArrivalThreshold (..)
+  , PerasCooldownRounds (..)
+  , PerasIgnoranceRounds (..)
+  , PerasParams (..)
+  )
+import Ouroboros.Consensus.Peras.Voting (PerasVotingView (..), isPerasVotingAllowed)
+import Ouroboros.Consensus.Util.Pred (explainShallow)
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.QuickCheck
+  ( Arbitrary (..)
+  , CoArbitrary
+  , Fun (..)
+  , Function
+  , Gen
+  , Positive (..)
+  , Property
+  , Small (..)
+  , Testable (..)
+  , applyFun
+  , choose
+  , counterexample
+  , tabulate
+  , testProperty
+  )
+import Test.Util.Orphans.Arbitrary (genNominalDiffTime50Years)
+
+{-------------------------------------------------------------------------------
+  Tests
+-------------------------------------------------------------------------------}
+
+tests :: TestTree
+tests =
+  testGroup
+    "Peras voting rules"
+    [ testProperty "isPerasVotingAllowed" prop_isPerasVotingAllowed
+    ]
+
+{-------------------------------------------------------------------------------
+  Model conformance test property
+-------------------------------------------------------------------------------}
+
+isPerasVotingAllowedModel ::
+  PerasVotingView TestCert ->
+  (Bool, (Bool, Bool, Bool, Bool))
+isPerasVotingAllowedModel pvv =
+  ( vr1a && vr1b || vr2a && vr2b
+  , (vr1a, vr1b, vr2a, vr2b)
+  )
+ where
+  vr1a =
+    pvvCurrRoundNo pvv == latestCertSeenRoundNo <> _1
+      && latestCertSeenArrivalSlot <= latestCertSeenRoundStart + _X
+  vr1b =
+    pvvCandidateExtendsCert pvv (pvvLatestCertSeen pvv)
+  vr2a =
+    latestCertSeenRoundNo <> _R <= currRoundNo
+  vr2b =
+    currRoundNo > latestCertOnChainRoundNo
+      && (currRoundNo `rmod` _K == latestCertOnChainRoundNo `rmod` _K)
+
+  _1 = coerce @Word64 1
+  _X = coerce (perasCertArrivalThreshold (pvvPerasParams pvv))
+  _R = coerce (perasIgnoranceRounds (pvvPerasParams pvv))
+  _K = coerce (perasCooldownRounds (pvvPerasParams pvv))
+
+  currRoundNo = pvvCurrRoundNo pvv
+  latestCertSeenRoundNo = getPerasCertRound (pvvLatestCertSeen pvv)
+  latestCertSeenRoundStart = pvvRoundStart pvv latestCertSeenRoundNo
+  latestCertSeenArrivalSlot = pvvArrivalSlot pvv (pvvLatestCertSeen pvv)
+  latestCertOnChainRoundNo = getPerasCertRound (pvvLatestCertOnChain pvv)
+
+  rmod = onPerasRoundNo mod
+
+-- | Test that the Peras voting rules can correctly decide when to vote based
+-- on a simplified model that doesn't use anything fancy to evaluate the rules.
+prop_isPerasVotingAllowed :: PerasVotingView' TestCert -> Property
+prop_isPerasVotingAllowed pvv' = do
+  -- Unpack the generated Peras voting view
+  let pvv = toPerasVotingView pvv'
+  -- Determine whether we should vote according to the model
+  let (shouldVote, votingRules@(vr1a, vr1b, vr2a, vr2b)) =
+        isPerasVotingAllowedModel pvv
+  -- Prepare helper functions to report success/failure
+  let compose = flip (foldr ($)) . reverse
+  let ok desc =
+        compose
+          [ tabulate "VR-1A" [show vr1a]
+          , tabulate "VR-1B" [show vr1b]
+          , tabulate "VR-2A" [show vr2a]
+          , tabulate "VR-2B" [show vr2b]
+          , tabulate "VR-(1A|1B|2A|2B)" [show votingRules]
+          , tabulate "Should vote according to model" [show shouldVote]
+          , tabulate "Actual result" [desc]
+          ]
+          $ property True
+  let failure desc =
+        counterexample desc $
+          property False
+  -- Now check that the real implementation agrees with the model
+  case isPerasVotingAllowed pvv of
+    Right voteReason
+      | shouldVote ->
+          ok $ "VoteReason(" <> explainShallow voteReason <> ")"
+      | otherwise ->
+          failure $ "Expected not to vote, but got: " <> show voteReason
+    Left noVoteReason
+      | not shouldVote ->
+          ok $ "NoVoteReason(" <> explainShallow noVoteReason <> ")"
+      | otherwise ->
+          failure $ "Expected to vote, but got: " <> show noVoteReason
+
+{-------------------------------------------------------------------------------
+  Arbitrary helpers
+-------------------------------------------------------------------------------}
+
+-- * Peras round numbers
+
+genPerasRoundNo :: Gen PerasRoundNo
+genPerasRoundNo = do
+  Positive (Small n) <- arbitrary
+  pure (PerasRoundNo n)
+
+-- * Peras parameters
+
+genPerasParams :: Gen PerasParams
+genPerasParams = do
+  Positive (Small _L) <- arbitrary
+  Positive (Small _X) <- arbitrary
+  Positive (Small _R) <- arbitrary
+  Positive (Small _K) <- arbitrary
+  pure
+    PerasParams
+      { perasBlockMinSlots = PerasBlockMinSlots _L
+      , perasCertArrivalThreshold = PerasCertArrivalThreshold _X
+      , perasIgnoranceRounds = PerasIgnoranceRounds _R
+      , perasCooldownRounds = PerasCooldownRounds _K
+      }
+
+-- * Mocked certificate type
+
+-- NOTE: we could also use the real 'WithArrivalTime (ValidatedPerasCert blk)'
+-- here. However, this one is much easier to derive a 'Function' instance for,
+-- so we can actually generate the methods needed by 'PerasVotingView'.
+
+data TestCert
+  = TestCert
+  { tcArrivalTime :: RelativeTime
+  , tcRoundNo :: PerasRoundNo
+  }
+  deriving (Show, Eq, Generic)
+
+instance HasPerasCertRound TestCert where
+  getPerasCertRound = tcRoundNo
+
+-- | Generate a test certificate
+--
+-- NOTE: to improve the probabilities of covering all the paths in the code,
+-- we generate certificates relative to a given Peras round (the current one).
+genTestCert :: PerasRoundNo -> Gen TestCert
+genTestCert roundNo = do
+  arrivalTime <- RelativeTime <$> genNominalDiffTime50Years
+  offset <- choose @Int (-5, 2)
+  let roundNo' = PerasRoundNo (unPerasRoundNo roundNo + fromIntegral offset)
+  pure $
+    TestCert
+      { tcArrivalTime = arrivalTime
+      , tcRoundNo = roundNo'
+      }
+
+-- * Peras voting views
+
+-- | A version of 'PerasVotingView' with all functions lifted to 'Fun'
+data PerasVotingView' cert = PerasVotingView'
+  { pvvPerasParams' :: PerasParams
+  , pvvCurrRoundNo' :: PerasRoundNo
+  , pvvLatestCertSeen' :: cert
+  , pvvLatestCertOnChain' :: cert
+  , pvvArrivalSlot' :: Fun cert (Small Word64)
+  , pvvRoundStart' :: Fun PerasRoundNo (Small Word64)
+  , pvvCandidateExtendsCert' :: Fun cert Bool
+  }
+  deriving Show -- the whole reason to have this type
+
+instance Arbitrary (PerasVotingView' TestCert) where
+  arbitrary = do
+    perasParams <- genPerasParams
+    currRoundNo <- genPerasRoundNo
+    latestCertSeen <- genTestCert currRoundNo
+    latestCertOnChain <- genTestCert currRoundNo
+    arrivalSlot <- arbitrary
+    roundStart <- arbitrary
+    candidateExtendsCert <- arbitrary
+    pure
+      PerasVotingView'
+        { pvvPerasParams' = perasParams
+        , pvvCurrRoundNo' = currRoundNo
+        , pvvLatestCertSeen' = latestCertSeen
+        , pvvLatestCertOnChain' = latestCertOnChain
+        , pvvArrivalSlot' = arrivalSlot
+        , pvvRoundStart' = roundStart
+        , pvvCandidateExtendsCert' = candidateExtendsCert
+        }
+
+toPerasVotingView :: PerasVotingView' TestCert -> PerasVotingView TestCert
+toPerasVotingView pvv' =
+  PerasVotingView
+    { pvvPerasParams = pvvPerasParams' pvv'
+    , pvvCurrRoundNo = pvvCurrRoundNo' pvv'
+    , pvvLatestCertSeen = pvvLatestCertSeen' pvv'
+    , pvvLatestCertOnChain = pvvLatestCertOnChain' pvv'
+    , pvvArrivalSlot = SlotNo . getSmall <$> applyFun (pvvArrivalSlot' pvv')
+    , pvvRoundStart = SlotNo . getSmall <$> applyFun (pvvRoundStart' pvv')
+    , pvvCandidateExtendsCert = applyFun (pvvCandidateExtendsCert' pvv')
+    }
+
+-- * Orphan instances needed for 'Function' constraints
+
+instance Function RelativeTime
+instance Function PerasRoundNo
+instance Function TestCert
+
+instance CoArbitrary RelativeTime
+instance CoArbitrary PerasRoundNo
+instance CoArbitrary TestCert
diff --git a/ouroboros-consensus/test/consensus-test/Test/Consensus/Util/Pred.hs b/ouroboros-consensus/test/consensus-test/Test/Consensus/Util/Pred.hs
new file mode 100644
index 0000000000..99859a7f0c
--- /dev/null
+++ b/ouroboros-consensus/test/consensus-test/Test/Consensus/Util/Pred.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE RankNTypes #-}
+
+-- | Tests for self-explaning boolean predcates
+module Test.Consensus.Util.Pred (tests) where
+
+import Ouroboros.Consensus.Util.Pred
+import Test.Tasty
+import Test.Tasty.HUnit
+
+tests :: TestTree
+tests =
+  testGroup
+    "Pred"
+    [ testGroup
+        "evalPred"
+        [ p `proves` p
+        , q `refutes` q
+        , r `proves` r
+        , Not p `refutes` Not p
+        , Not q `proves` Not q
+        , Not r `refutes` Not r
+        , p :/\: r `proves` p :/\: r
+        , q `refutes` p :/\: q
+        , q `refutes` p :/\: q :/\: r
+        , p `proves` p :\/: q
+        , p `proves` q :\/: p
+        , p :/\: r `proves` (p :\/: q) :/\: (q :\/: r)
+        ]
+    ]
+
+{-------------------------------------------------------------------------------
+  Setup
+-------------------------------------------------------------------------------}
+
+data Prop = P | Q | R
+  deriving stock (Show, Eq)
+  deriving Explainable via ShowExplain Prop
+
+p :: Pred Prop -- ~ True
+p = P := Bool True
+
+q :: Pred Prop -- ~ False
+q = Q := (5 :<=: (3 :: Int))
+
+r :: Pred Prop -- ~ True
+r = R := Not (4 :<=: (2 :: Int))
+
+test_evalPred :: String -> Pred Prop -> Either (Evidence Prop) (Evidence Prop) -> TestTree
+test_evalPred name predicate expected =
+  testCase name $
+    case evalPred predicate of
+      Left ce -> Left ce @?= expected
+      Right w -> Right w @?= expected
+
+proves :: Pred Prop -> Evidence Prop -> TestTree
+evidence `proves` predicate =
+  test_evalPred
+    (explainDeep evidence <> " ⊢ " <> explainShallow predicate <> " => ⊤")
+    predicate
+    (Right evidence)
+
+infix 1 `proves`
+
+refutes :: Pred Prop -> Evidence Prop -> TestTree
+evidence `refutes` predicate =
+  test_evalPred
+    (explainDeep evidence <> " ⊢ " <> explainShallow predicate <> " => ⊥")
+    predicate
+    (Left evidence)
+
+infix 1 `refutes`
diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/Model.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/Model.hs
index 812e031c78..71c37a668e 100644
--- a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/Model.hs
+++ b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/Model.hs
@@ -56,7 +56,7 @@ getWeightSnapshot Model{certs} =
     | cert <- Set.toList certs
     ]
 
-garbageCollect :: StandardHash blk => SlotNo -> Model blk -> Model blk
+garbageCollect :: SlotNo -> Model blk -> Model blk
 garbageCollect slot model@Model{certs} =
   model{certs = Set.filter keepCert certs}
  where