diff --git a/ouroboros-consensus/ouroboros-consensus.cabal b/ouroboros-consensus/ouroboros-consensus.cabal
index a0d3a83786..50def9146f 100644
--- a/ouroboros-consensus/ouroboros-consensus.cabal
+++ b/ouroboros-consensus/ouroboros-consensus.cabal
@@ -204,6 +204,7 @@ library
     Ouroboros.Consensus.Node.Serialisation
     Ouroboros.Consensus.NodeId
     Ouroboros.Consensus.Peras.SelectView
+    Ouroboros.Consensus.Peras.Voting
     Ouroboros.Consensus.Peras.Weight
     Ouroboros.Consensus.Protocol.Abstract
     Ouroboros.Consensus.Protocol.BFT
@@ -305,6 +306,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
@@ -671,8 +673,10 @@ test-suite consensus-test
     Test.Consensus.MiniProtocol.LocalStateQuery.Server
     Test.Consensus.MiniProtocol.ObjectDiffusion.PerasCert.Smoke
     Test.Consensus.MiniProtocol.ObjectDiffusion.Smoke
+    Test.Consensus.Peras.Voting
     Test.Consensus.Peras.WeightSnapshot
     Test.Consensus.Util.MonadSTM.NormalForm
+    Test.Consensus.Util.Pred
     Test.Consensus.Util.Versioned
 
   build-depends:
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..0f5bb03804
--- /dev/null
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/Voting.hs
@@ -0,0 +1,398 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE RankNTypes #-}
+{-# 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 Cardano.Slotting.Slot (WithOrigin)
+import Data.Bifunctor (bimap)
+import Data.Typeable (Typeable)
+import Ouroboros.Consensus.Block (WithOrigin (..))
+import Ouroboros.Consensus.Block.Abstract
+  ( GetHeader (..)
+  , Header
+  , SlotNo (..)
+  , StandardHash
+  , castPoint
+  , succWithOrigin
+  )
+import Ouroboros.Consensus.Block.SupportsPeras
+  ( HasPerasCertRound (..)
+  , PerasRoundNo (..)
+  , ValidatedPerasCert
+  , getPerasCertBoostedBlock
+  , getPerasCertRound
+  , onPerasRoundNo
+  )
+import Ouroboros.Consensus.BlockchainTime.WallClock.Types
+  ( WithArrivalTime (..)
+  )
+import Ouroboros.Consensus.HardFork.History.EraParams (fromPerasEnabled)
+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
+  { perasParams :: !PerasParams
+  -- ^ Peras protocol parameters.
+  , currRoundNo :: !PerasRoundNo
+  -- ^ The current Peras round number.
+  , latestCertSeen :: !(WithOrigin cert)
+  -- ^ The most recent certificate seen by the voter.
+  , latestCertOnChain :: !(WithOrigin cert)
+  -- ^ The most recent certificate present in some chain.
+  , certRoundStart :: cert -> SlotNo
+  -- ^ Get the slot number at the start of the Peras round of a certificate.
+  , arrivalSlot :: cert -> SlotNo
+  -- ^ Get the arrival slot number of a certificate
+  , candidateExtendsCert :: 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 ->
+  WithOrigin cert ->
+  WithOrigin cert ->
+  AnchoredFragment (Header blk) ->
+  HF.Summary blks ->
+  PerasVotingView cert
+mkPerasVotingView
+  perasParams
+  currRoundNo
+  latestCertSeen
+  latestCertOnChain
+  currChain
+  summary =
+    PerasVotingView
+      { perasParams = perasParams
+      , currRoundNo = currRoundNo
+      , latestCertSeen = latestCertSeen
+      , latestCertOnChain = latestCertOnChain
+      , certRoundStart = certRoundStart
+      , arrivalSlot = arrivalSlot
+      , candidateExtendsCert = candidateExtendsCert
+      }
+   where
+    -- Run a pure query with the given summary
+    pureQuery = flip HF.runQueryPure summary
+
+    -- The Peras block minium slots parameter (L).
+    _L = SlotNo (unPerasBlockMinSlots (perasBlockMinSlots perasParams))
+
+    -- Candidate block slot, i.e., that of the block that's at least
+    -- 'blockMinSlots' (L) old from the start of the current round.
+    --
+    -- NOTE: here we need make sure that the result doesn't underflow.
+    candidateSlot
+      | currRoundStart >= _L = currRoundStart - _L
+      | otherwise = SlotNo 0
+     where
+      currRoundStart = roundStart currRoundNo
+
+    -- 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 = slotNo
+     where
+      (slotNo, _) =
+        pureQuery (fromPerasEnabledOrFail <$> HF.perasRoundNoToSlot roundNo)
+
+      fromPerasEnabledOrFail =
+        fromPerasEnabled
+          (error "mkPerasVotingView: Peras is disabled in the current era")
+
+    -- A slightly safer version of 'roundStart' that works with certificates.
+    --
+    -- NOTE: Instead of using 'roundStart' directly, this makes it more
+    -- harder for the user of the voting interface to accidentally pass a
+    -- 'PerasRoundNo' that triggers the 'PastHorizonException', as the
+    -- existence of a certificate _should_ imply that Peras was enabled
+    -- at the time the certificate was issued.
+    certRoundStart = roundStart . getPerasCertRound
+
+    -- 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, _, _) =
+        pureQuery (HF.wallclockToSlot (getArrivalTime cert))
+
+    -- 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 sufficiently old"
+    VR2B ->
+      "the last certificate on chain is exactly one or more cooldown periods old"
+
+-- | 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
+  PerasVotingView
+    { perasParams
+    , currRoundNo
+    , latestCertSeen
+    , arrivalSlot
+    , certRoundStart
+    } =
+    VR1A := vr1a1 :/\: vr1a2
+   where
+    -- The latest certificate seen is from the previous round
+    --
+    -- NOTE: 'succWithOrigin' handles the 'Origin' case (i.e. when we have
+    -- never seen a certificate before) correctly by returning 0, as this is
+    -- the only round number that should satisfy this equality when we are
+    -- bootstrapping the voting process. In other words, we should be able to
+    -- start voting from round 0 even if we have never seen a certificate
+    -- before, but failing to do so should trigger a cooldown period
+    -- immediately after.
+    vr1a1 =
+      currRoundNo :==: succWithOrigin (getPerasCertRound <$> latestCertSeen)
+
+    -- The latest certificate seen was received within X slots from the start
+    -- of the round
+    vr1a2 =
+      case latestCertSeen of
+        -- We have seen a certificate ==> check its arrival time
+        NotOrigin cert -> arrivalSlot cert :<=: certRoundStart cert + _X
+        -- We have never seen a certificate ==> vacuously true
+        Origin -> Bool True
+
+    _X =
+      SlotNo $
+        unPerasCertArrivalThreshold $
+          perasCertArrivalThreshold perasParams
+
+-- | VR-1B: the block being voted upon extends the most recently certified one.
+perasVR1B ::
+  PerasVotingView cert ->
+  Pred PerasVotingRule
+perasVR1B
+  PerasVotingView
+    { latestCertSeen
+    , candidateExtendsCert
+    } =
+    VR1B := vr1b
+   where
+    -- The block being voted upon extends the most recently certified one
+    vr1b =
+      case latestCertSeen of
+        -- We have seen a certificate ==> check that it extends our chain
+        NotOrigin cert -> Bool (candidateExtendsCert cert)
+        -- We have never seen a certificate ==> vacuously true
+        Origin -> Bool True
+
+-- | 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
+  PerasVotingView
+    { perasParams
+    , currRoundNo
+    , latestCertSeen
+    } =
+    VR2A := vr2a
+   where
+    vr2a =
+      -- NOTE: we use 'succWithOrigin' and '-1' to handle the 'Origin' case
+      -- (i.e. when we have never seen a certificate before) correctly,
+      -- treating the 'Origin' certificate as being from round -1.
+      (succWithOrigin (getPerasCertRound <$> latestCertSeen) - 1 + _R)
+        :<=: currRoundNo
+
+    _R =
+      PerasRoundNo $
+        unPerasIgnoranceRounds $
+          perasIgnoranceRounds $
+            perasParams
+
+-- | 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
+  PerasVotingView
+    { perasParams
+    , currRoundNo
+    , latestCertOnChain
+    } =
+    VR2B := vr2b
+   where
+    vr2b =
+      case latestCertOnChain of
+        -- There is a certificate on chain ==> we must check its round number
+        NotOrigin cert ->
+          -- The certificate comes from a round older than the current one
+          (currRoundNo :>: getPerasCertRound cert)
+            -- The certificate round is c⋅K rounds away from the current one
+            :/\: (currRoundNo `rmod` _K :==: getPerasCertRound cert `rmod` _K)
+        -- There is no certificate on chain ==> check if we are recovering
+        -- from an initial cooldown after having initially failed to
+        -- reach a quorum during bootstrapping.
+        --
+        -- NOTE: '_K - 1' here is treating the 'Origin' certificate as being
+        -- from round -1.
+        Origin -> currRoundNo `rmod` _K :==: _K - 1
+
+    rmod = onPerasRoundNo mod
+
+    _K =
+      PerasRoundNo $
+        unPerasCooldownRounds $
+          perasCooldownRounds $
+            perasParams
+
+-- | 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/Util/Pred.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Util/Pred.hs
new file mode 100644
index 0000000000..8e4ab1dbc6
--- /dev/null
+++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Util/Pred.hs
@@ -0,0 +1,234 @@
+{-# 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 predicates 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 (C := 10 :>: 5))
+--
+-- >>> 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
+  deriving (Show, Eq)
+
+-- | 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 > 3) $
+        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/src/unstable-consensus-testlib/Test/Util/QuickCheck.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Util/QuickCheck.hs
index c22361a64d..723f4d6229 100644
--- a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Util/QuickCheck.hs
+++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Util/QuickCheck.hs
@@ -23,6 +23,9 @@ module Test.Util.QuickCheck
   , frequency'
   , oneof'
 
+    -- * Sampling from distributions
+  , geometric
+
     -- * Comparing maps
   , isSubmapOfBy
 
@@ -308,3 +311,19 @@ frequency' xs0 = lift (choose (1, tot)) >>= (`pick` xs0)
 oneof' :: (MonadTrans t, Monad (t Gen)) => [t Gen a] -> t Gen a
 oneof' [] = error "QuickCheck.oneof used with empty list"
 oneof' gs = lift (chooseInt (0, length gs - 1)) >>= (gs !!)
+
+{-------------------------------------------------------------------------------
+  Sampling from distributions
+-------------------------------------------------------------------------------}
+
+-- NOTE: if more advanced sampling is required, consider using 'mwc-random':
+-- https://hackage.haskell.org/package/mwc-random
+
+-- | Sample from a geometric distribution
+geometric :: Double -> Gen Int
+geometric p
+  | p <= 0 || p > 1 = error "p must be in (0,1]"
+  | otherwise = do
+      u <- choose (0.0, 1.0)
+      let k = floor (log u / log (1 - p))
+      return k
diff --git a/ouroboros-consensus/test/consensus-test/Main.hs b/ouroboros-consensus/test/consensus-test/Main.hs
index 79d681213a..2775745a44 100644
--- a/ouroboros-consensus/test/consensus-test/Main.hs
+++ b/ouroboros-consensus/test/consensus-test/Main.hs
@@ -18,8 +18,10 @@ import qualified Test.Consensus.MiniProtocol.ChainSync.Client (tests)
 import qualified Test.Consensus.MiniProtocol.LocalStateQuery.Server (tests)
 import qualified Test.Consensus.MiniProtocol.ObjectDiffusion.PerasCert.Smoke (tests)
 import qualified Test.Consensus.MiniProtocol.ObjectDiffusion.Smoke (tests)
+import qualified Test.Consensus.Peras.Voting (tests)
 import qualified Test.Consensus.Peras.WeightSnapshot (tests)
 import qualified Test.Consensus.Util.MonadSTM.NormalForm (tests)
+import qualified Test.Consensus.Util.Pred (tests)
 import qualified Test.Consensus.Util.Versioned (tests)
 import Test.Tasty
 import Test.Util.TestEnv
@@ -48,9 +50,14 @@ tests =
         , Test.Consensus.Mempool.Fairness.tests
         , Test.Consensus.Mempool.StateMachine.tests
         ]
-    , Test.Consensus.Peras.WeightSnapshot.tests
+    , testGroup
+        "Peras"
+        [ Test.Consensus.Peras.Voting.tests
+        , Test.Consensus.Peras.WeightSnapshot.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/Peras/Voting.hs b/ouroboros-consensus/test/consensus-test/Test/Consensus/Peras/Voting.hs
new file mode 100644
index 0000000000..5fb5e4bb95
--- /dev/null
+++ b/ouroboros-consensus/test/consensus-test/Test/Consensus/Peras/Voting.hs
@@ -0,0 +1,318 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+-- | Test that the Peras voting rules can correctly decide when to vote.
+module Test.Consensus.Peras.Voting (tests) where
+
+import GHC.Generics (Generic)
+import GHC.Word (Word64)
+import Ouroboros.Consensus.Block.Abstract
+  ( SlotNo (..)
+  , WithOrigin (..)
+  , succWithOrigin
+  )
+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
+  , frequency
+  , tabulate
+  , testProperty
+  )
+import Test.Util.Orphans.Arbitrary (genNominalDiffTime50Years)
+import Test.Util.QuickCheck (geometric)
+import Test.Util.TestEnv (adjustQuickCheckTests)
+
+{-------------------------------------------------------------------------------
+  Tests
+-------------------------------------------------------------------------------}
+
+tests :: TestTree
+tests =
+  adjustQuickCheckTests (* 100) $
+    testGroup
+      "Peras voting rules"
+      [ testProperty "isPerasVotingAllowed" prop_isPerasVotingAllowed
+      ]
+
+{-------------------------------------------------------------------------------
+  Model conformance test property
+-------------------------------------------------------------------------------}
+
+-- | A simplified model of the Peras voting rules, used to compare against the
+-- real implementation. The main difference is that this model computes the
+-- result of the predicate directly over the inputs, rather than using the
+-- 'Pred' combinators to produce evidence in either direction.
+--
+-- NOTE: this predicate could be lifted directly from the agda specification.
+isPerasVotingAllowedModel ::
+  PerasVotingView TestCert ->
+  ( -- Should we vote according to the model?
+    Bool
+  , -- The individual voting rules that were applied
+    (Bool, Bool, Bool, Bool)
+  )
+isPerasVotingAllowedModel
+  PerasVotingView
+    { perasParams
+    , currRoundNo
+    , latestCertSeen
+    , latestCertOnChain
+    , certRoundStart
+    , arrivalSlot
+    , candidateExtendsCert
+    } =
+    ( vr1a && vr1b || vr2a && vr2b
+    , (vr1a, vr1b, vr2a, vr2b)
+    )
+   where
+    vr1a =
+      vr1a1 && vr1a2
+    vr1a1 =
+      currRoundNo == succWithOrigin (getPerasCertRound <$> latestCertSeen)
+    vr1a2 =
+      case latestCertSeen of
+        NotOrigin cert ->
+          arrivalSlot cert <= certRoundStart cert + _X
+        Origin -> True
+    vr1b =
+      case latestCertSeen of
+        NotOrigin cert -> candidateExtendsCert cert
+        Origin -> True
+    vr2a =
+      (succWithOrigin (getPerasCertRound <$> latestCertSeen) - 1 + _R)
+        <= currRoundNo
+
+    vr2b =
+      case latestCertOnChain of
+        NotOrigin cert ->
+          (currRoundNo > getPerasCertRound cert)
+            && (currRoundNo `rmod` _K == getPerasCertRound cert `rmod` _K)
+        Origin -> currRoundNo `rmod` _K == _K - 1
+
+    _X =
+      SlotNo $
+        unPerasCertArrivalThreshold $
+          perasCertArrivalThreshold $
+            perasParams
+    _R =
+      PerasRoundNo $
+        unPerasIgnoranceRounds $
+          perasIgnoranceRounds $
+            perasParams
+    _K =
+      PerasRoundNo $
+        unPerasCooldownRounds $
+          perasCooldownRounds $
+            perasParams
+
+    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
+  -- Some helper functions to report success/failure
+  let chain = flip (foldr ($)) . reverse
+  let ok desc =
+        chain
+          [ 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
+
+-- NOTE: we use a geometric distribution to bias towards smaller values.
+-- This increases the chance of covering all the voting rules more evenly,
+-- while still allowing for larger values to be generated occasionally.
+--
+-- Moreover, geometric(0.5) + 1 means that:
+--  - 50% chance of being 1
+--  - 25% chance of being 2
+--  - 12.5% chance of being 3
+--  ... and so on
+genPerasParams :: Gen PerasParams
+genPerasParams = do
+  _L <- fromIntegral . (+ 1) <$> geometric 0.5
+  _X <- fromIntegral . (+ 1) <$> geometric 0.5
+  _R <- fromIntegral . (+ 1) <$> geometric 0.5
+  _K <- fromIntegral . (+ 1) <$> geometric 0.5
+  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 @Integer (-3, 2)
+  -- NOTE: here we need to be careful not to underflow the round number or we
+  -- will get an exception later on when trying to evaluate 'succ maxBound'
+  let roundNo' =
+        PerasRoundNo $
+          fromIntegral $
+            max 0 $
+              toInteger (unPerasRoundNo roundNo) + offset
+  pure $
+    TestCert
+      { tcArrivalTime = arrivalTime
+      , tcRoundNo = roundNo'
+      }
+
+genWithOrigin :: Gen a -> Gen (WithOrigin a)
+genWithOrigin gen = frequency [(1, pure Origin), (9, NotOrigin <$> gen)]
+
+-- * Peras voting views
+
+-- | A version of 'PerasVotingView' with all functions lifted to 'Fun'
+data PerasVotingView' cert = PerasVotingView'
+  { perasParams' :: PerasParams
+  , currRoundNo' :: PerasRoundNo
+  , latestCertSeen' :: WithOrigin cert
+  , latestCertOnChain' :: WithOrigin cert
+  , arrivalSlot' :: Fun cert (Small Word64)
+  , certRoundStart' :: Fun cert (Small Word64)
+  , candidateExtendsCert' :: Fun cert Bool
+  }
+  deriving (Show, Generic) -- the whole reason to have this type
+
+instance Arbitrary (PerasVotingView' TestCert) where
+  arbitrary = do
+    roundNo <- genPerasRoundNo
+    PerasVotingView'
+      <$> genPerasParams
+      <*> pure roundNo
+      <*> genWithOrigin (genTestCert roundNo)
+      <*> genWithOrigin (genTestCert roundNo)
+      <*> arbitrary
+      <*> arbitrary
+      <*> arbitrary
+
+  -- NOTE: arbitrary functions can only be shown after shrinking them first
+  shrink pvv' =
+    [ pvv'
+        { arrivalSlot' = arrivalSlot'
+        , certRoundStart' = certRoundStart'
+        , candidateExtendsCert' = candidateExtendsCert'
+        }
+    | arrivalSlot' <- shrink (arrivalSlot' pvv')
+    , certRoundStart' <- shrink (certRoundStart' pvv')
+    , candidateExtendsCert' <- shrink (candidateExtendsCert' pvv')
+    ]
+
+toPerasVotingView :: PerasVotingView' TestCert -> PerasVotingView TestCert
+toPerasVotingView pvv' =
+  PerasVotingView
+    { perasParams = perasParams' pvv'
+    , currRoundNo = currRoundNo' pvv'
+    , latestCertSeen = latestCertSeen' pvv'
+    , latestCertOnChain = latestCertOnChain' pvv'
+    , arrivalSlot = SlotNo . getSmall <$> applyFun (arrivalSlot' pvv')
+    , certRoundStart = SlotNo . getSmall <$> applyFun (certRoundStart' pvv')
+    , candidateExtendsCert = applyFun (candidateExtendsCert' 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..62da378e28
--- /dev/null
+++ b/ouroboros-consensus/test/consensus-test/Test/Consensus/Util/Pred.hs
@@ -0,0 +1,123 @@
+{-# 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"
+    [ -- Basic tests ensuring that predicates produce the right evidence.
+      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)
+        ]
+    , -- Basic explanation rendering tests.
+      --
+      -- NOTE: we can't easily test equality/inequality of explanations without
+      -- turning these test into an annoying change detector (see [1]) but we
+      -- still _can_ test some specific case regarding operator precedence and
+      -- distributivity that should always hold regardless of implementation.
+      --
+      -- [1]: https://testing.googleblog.com/2015/01/testing-on-toilet-change-detector-tests.html
+      testGroup
+        "explain"
+        $ concat
+          [ [ eq_explain mode (p :/\: q :\/: r) ((p :/\: q) :\/: r)
+            , eq_explain mode (p :\/: q :/\: r) (p :\/: (q :/\: r))
+            , neq_explain mode (p :/\: q :\/: r) (p :/\: (q :\/: r))
+            , neq_explain mode (p :\/: q :/\: r) ((p :\/: q) :/\: r)
+            , neq_explain mode (Not (p :/\: q)) (Not p :/\: q)
+            , neq_explain mode (Not (p :\/: q)) (Not p :\/: q)
+            , neq_explain mode (P := Bool True :/\: Bool False) ((P := Bool True) :/\: Bool False)
+            , neq_explain mode (P := Bool True :\/: Bool False) ((P := Bool True) :\/: Bool False)
+            ]
+          | mode <- [Shallow, Deep]
+          ]
+    ]
+
+{-------------------------------------------------------------------------------
+  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`
+
+eq_explain :: (Show a, Explainable a) => ExplanationMode -> a -> a -> TestTree
+eq_explain mode x y =
+  testCase ("explain " <> show mode <> " " <> show x <> " == explain " <> show mode <> " " <> show y) $
+    assertEqual
+      "Expected equal explanations:"
+      (explain mode x)
+      (explain mode y)
+
+neq_explain :: (Show a, Explainable a) => ExplanationMode -> a -> a -> TestTree
+neq_explain mode x y =
+  testCase ("explain " <> show mode <> " " <> show x <> " /= explain " <> show mode <> " " <> show y) $
+    assertNotEqual
+      "Expected different explanations:"
+      (explain mode x)
+      (explain mode y)
+
+-- Surprising this is not already in 'tasty-hunit'
+assertNotEqual :: (Eq a, Show a) => String -> a -> a -> IO ()
+assertNotEqual preface expected actual
+  | actual /= expected = return ()
+  | otherwise = assertFailure msg
+ where
+  msg =
+    (if null preface then "" else preface <> "\n")
+      <> "\n but got: "
+      <> show actual
diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine.hs
index e3a787a6c6..3d7fbcef00 100644
--- a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine.hs
+++ b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine.hs
@@ -1607,6 +1607,14 @@ genBlk chunkInfo Model{..} =
         )
       ]
 
+genSecurityParam :: Gen SecurityParam
+genSecurityParam =
+  SecurityParam
+    . unsafeNonZero
+    . fromIntegral
+    . (+ 2) -- shift to the right to avoid degenerate cases
+    <$> geometric 0.5 -- range in [0, +inf); mean = 1/p = 2
+
 {-------------------------------------------------------------------------------
   Top-level tests
 -------------------------------------------------------------------------------}