diff --git a/docs/agda-spec/src/Ledger/Crypto.lagda b/docs/agda-spec/src/Ledger/Crypto.lagda
index 206f919e47..aa15512891 100644
--- a/docs/agda-spec/src/Ledger/Crypto.lagda
+++ b/docs/agda-spec/src/Ledger/Crypto.lagda
@@ -172,7 +172,9 @@ record KESScheme (srl : Serializer) : Type₁ where
 
 \begin{figure*}[h]
 \begin{code}[hide]
-record VRFScheme : Type₁ where
+record VRFScheme (srl : Serializer) : Type₁ where
+  open Serializer srl
+
   field
         pks : PKScheme
 
@@ -183,18 +185,18 @@ record VRFScheme : Type₁ where
 \emph{Types \& functions}
 \begin{code}
         Seed Proof : Type
-        verify     : {T : Type} → VKey → Seed → Proof × T → Type
-        evaluate   : {T : Type} → SKey → Seed → Proof × T
+        verify     : VKey → Seed → Proof × Ser → Type
+        evaluate   : SKey → Seed → Proof × Ser
         _XOR_      : Seed → Seed → Seed
 \end{code}
 \emph{Properties}
 \begin{code}[hide]
-  field ⦃ Dec-verify ⦄ : {T : Type} → verify {T} ⁇³
+  field ⦃ Dec-verify ⦄ : verify ⁇³
         verify-correct :
 \end{code}
 \begin{code}        
-          ∀ {T : Type} ((sk , vk , _) : KeyPair) (seed : Seed)
-            → verify {T = T} vk seed (evaluate sk seed)
+          ∀ ((sk , vk , _) : KeyPair) (seed : Seed)
+            → verify vk seed (evaluate sk seed)
 \end{code}
 \begin{code}[hide]         
         ⦃ DecEq-Seed  ⦄ : DecEq Seed
@@ -211,7 +213,7 @@ record Crypto : Type₁ where
   field srl  : Serializer
         dsig : DSigScheme srl
         kes  : KESScheme srl
-        vrf  : VRFScheme
+        vrf  : VRFScheme srl
 
   open Serializer srl public
   open DSigScheme dsig renaming (VKey to VKeyˢ; Sig to Sigˢ; isSigned to isSignedˢ) public
diff --git a/docs/agda-spec/src/Spec/BlockDefinitions.lagda b/docs/agda-spec/src/Spec/BlockDefinitions.lagda
index a238de9ae8..a25707d43c 100644
--- a/docs/agda-spec/src/Spec/BlockDefinitions.lagda
+++ b/docs/agda-spec/src/Spec/BlockDefinitions.lagda
@@ -27,18 +27,16 @@ record BlockStructure : Type₁ where
 \begin{code}
     HashHeader : Type -- hash of a block header
     HashBBody  : Type -- hash of a block body
-    VRFRes     : Type -- VRF result value
 \end{code}
 \begin{code}[hide]
     ⦃ DecEq-HashHeader ⦄ : DecEq HashHeader
     ⦃ DecEq-HashBBody  ⦄ : DecEq HashBBody
-    ⦃ DecEq-VRFRes     ⦄ : DecEq VRFRes
     ⦃ Show-HashHeader  ⦄ : Show HashHeader
     ⦃ Show-HashBBody   ⦄ : Show HashBBody
-    ⦃ Show-VRFRes      ⦄ : Show VRFRes
 \end{code}
 \emph{Concrete types}
 \begin{code}
+  VRFRes = Ser -- VRF result value
   BlockNo = ℕ -- block number
   Certifiedℕ = ∃[ n ] n < 2 ^ 512 -- [0, 2^512) (64-byte VRF output)
 \end{code}
diff --git a/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda b/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda
index ecafba9e84..f1375782f2 100644
--- a/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda
+++ b/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda
@@ -2,18 +2,27 @@ module Spec.Foreign.ExternalFunctions where -- TODO: Complete
 
 open import Ledger.Prelude
 import Spec.Foreign.HSTypes as F using (Rational)
+import Foreign.Haskell as F using (Pair; _,_)
 open import Spec.Foreign.HSConsensus.Core
 
 record ExternalFunctions : Type where
   field
+    extSignˢ     : ℕ → ℕ → ℕ
     extIsSignedˢ : ℕ → ℕ → ℕ → Bool
+    extSignᵏ     : (ℕ → ℕ) → ℕ → ℕ → ℕ
     extIsSignedᵏ : ℕ → ℕ → ℕ → ℕ → Bool
+    extEvaluate  : ℕ → ℕ → F.Pair ℕ ℕ
+    extVerify    : ℕ → ℕ → F.Pair ℕ ℕ → Bool
     extExp       : F.Rational → F.Rational
     extLn        : F.Rational → F.Rational
 {-# FOREIGN GHC
   data ExternalFunctions = MkExternalFunctions
-    { extIsSignedDSIG :: Integer -> Integer -> Integer -> Bool
+    { extSignDSIG     :: Integer -> Integer -> Integer
+    , extIsSignedDSIG :: Integer -> Integer -> Integer -> Bool
+    , extSignKES      :: (Integer -> Integer) -> Integer -> Integer -> Integer
     , extIsSignedKES  :: Integer -> Integer -> Integer -> Integer -> Bool
+    , extEvaluate     :: Integer -> Integer -> (Integer , Integer)
+    , extVerify       :: Integer -> Integer -> (Integer , Integer) -> Bool
     , extExp          :: Rational -> Rational
     , extLn           :: Rational -> Rational
     }
@@ -22,8 +31,12 @@ record ExternalFunctions : Type where
 
 dummyExternalFunctions : ExternalFunctions
 dummyExternalFunctions = record
-  { extIsSignedˢ = λ _ _ _ → true
+  { extSignˢ     = λ _ _ → 0
+  ; extIsSignedˢ = λ _ _ _ → true
+  ; extSignᵏ     = λ _ _ _ → 0
   ; extIsSignedᵏ = λ _ _ _ _ → true
+  ; extEvaluate  = λ _ _ → 0 F., 0
+  ; extVerify    = λ _ _ _ → true
   ; extExp       = λ p → to (rationalExtStructure≈ .exp (from p))
   ; extLn        = λ p → to (rationalExtStructure≈ .ln (from p) ⦃ if (from p) ℚ.> 0ℚ then (λ{p>0} → positive p>0) else error "Not a positive rational number" ⦄)
   }
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda
index cf56807788..0ac94306d4 100644
--- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda
@@ -5,6 +5,7 @@ module Spec.Foreign.HSConsensus.ExternalStructures (externalFunctions : External
 open import Ledger.Crypto
 open import Ledger.Types.Epoch
 open import Spec.Foreign.HSConsensus.Core
+open import Foreign.Haskell.Coerce
 
 HSGlobalConstants = GlobalConstants ∋ record {Implementation}
 instance
@@ -33,7 +34,7 @@ instance
     { pks              = HSPKScheme
     ; Sig              = ℕ
     ; isSigned         = λ vk d σ → extIsSignedˢ vk d σ ≡ true
-    ; sign             = λ _ _ → 0 -- NOTE: Dummy for now
+    ; sign             = extSignˢ
     ; isSigned-correct = error "isSigned-correct evaluated"
     ; Dec-isSigned     = ⁇ (_ ≟ _)
     }
@@ -45,25 +46,26 @@ instance
     { pks              = HSPKScheme
     ; Sig              = ℕ
     ; isSigned         = λ vk n d σ → extIsSignedᵏ vk n d σ ≡ true
-    ; sign             = λ _ _ _ → 0 -- NOTE: Dummy for now
+    ; sign             = extSignᵏ
     ; isSigned-correct = error "isSigned-correct evaluated"
     ; Dec-isSigned     = ⁇ (_ ≟ _)
     }
     where
       open ExternalFunctions externalFunctions
 
-  -- NOTE: Dummy for now.
-  HSVRFScheme : VRFScheme
+  HSVRFScheme : VRFScheme HSSerializer
   HSVRFScheme = record
     { Implementation
     ; pks            = HSPKScheme
     ; Proof          = ℕ
-    ; verify         = λ _ _ _ → ⊤
-    ; evaluate       = error "evaluate evaluated"
+    ; verify         = λ vk seed out → extVerify vk seed (coerce out) ≡ true
+    ; evaluate       = coerce ∘ extEvaluate
     ; _XOR_          = _+_
     ; verify-correct = error "verify-correct evaluated"
-    ; Dec-verify     = λ {T = _} {_} {_} {_} → ⁇ (true because ofʸ tt)
+    ; Dec-verify     = ⁇ (_ ≟ _)
     }
+    where
+      open ExternalFunctions externalFunctions
 
   HSCrypto : Crypto
   HSCrypto = record
@@ -92,7 +94,6 @@ instance
   HSBlockStructure = record
     { HashHeader       = ℕ
     ; HashBBody        = ℕ
-    ; VRFRes           = ℕ
     ; DecEq-HashHeader = DecEq-ℕ
     }
 
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Protocol.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Protocol.agda
index 6c4e279bdb..c836a395e3 100644
--- a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Protocol.agda
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Protocol.agda
@@ -85,7 +85,7 @@ module _ (ext : ExternalFunctions) where
                   ∷ ("slotToSeed slot                     \t: " +ˢ show stsslot)
                   ∷ ("nonceToSeed η₀                      \t: " +ˢ show ntsη₀)
                   ∷ ("seed                                \t: " +ˢ show seed)
-                  ∷ ("verify vrfVk seed (vrfPrf , vrfRes) \t: " +ˢ show (⌊ ¿ verify {T = VRFRes} ¿³ vrfVk seed (vrfPrf , vrfRes) ⌋))
+                  ∷ ("verify vrfVk seed (vrfPrf , vrfRes) \t: " +ˢ show (⌊ ¿ verify ¿³ vrfVk seed (vrfPrf , vrfRes) ⌋))
                   ∷ ("hBLeader bhb                        \t: " +ˢ Show-Certifiedℕ {DummyBlockStructure} .show t)
                   ∷ ("f                                   \t: " +ˢ show ActiveSlotCoeff)
                   ∷ ("checkLeaderVal? (hBLeader bhb) f σ  \t: " +ˢ show (⌊ checkLeaderVal? t ActiveSlotCoeff σ ⌋))
diff --git a/docs/agda-spec/src/Spec/Protocol/Properties.agda b/docs/agda-spec/src/Spec/Protocol/Properties.agda
index af668e377b..ba5e6e1c16 100644
--- a/docs/agda-spec/src/Spec/Protocol/Properties.agda
+++ b/docs/agda-spec/src/Spec/Protocol/Properties.agda
@@ -50,7 +50,7 @@ vrfChecks? η₀ pd f bhb
 ... | nothing          = no λ ()
 ... | just (σ , vrfHK) =
         vrfHK ≟ hash vrfVk
-        ×-dec ¿ verify {T = VRFRes} ¿³ vrfVk seed (vrfPrf , vrfRes)
+        ×-dec ¿ verify ¿³ vrfVk seed (vrfPrf , vrfRes)
         ×-dec checkLeaderVal? (hBLeader bhb) f σ
   where
     open BHBody bhb
diff --git a/docs/agda-spec/src/Spec/hs-src/cabal.project b/docs/agda-spec/src/Spec/hs-src/cabal.project
index dfb30afe59..7e2ff8378e 100644
--- a/docs/agda-spec/src/Spec/hs-src/cabal.project
+++ b/docs/agda-spec/src/Spec/hs-src/cabal.project
@@ -1,2 +1,23 @@
 -- TODO: Remove this file when code is properly integrated to the existing setup
+
+-- Custom repository for cardano haskell packages, see CONTRIBUTING for more
+repository cardano-haskell-packages
+  url: https://chap.intersectmbo.org/
+  secure: True
+  root-keys:
+    3e0cce471cf09815f930210f7827266fd09045445d65923e6d0238a6cd15126f
+    443abb7fb497a134c343faf52f0b659bd7999bc06b7f63fa76dc99d631f9bea1
+    a86a1f6ce86c449c46666bda44268677abf29b5b2d2eb5ec7af903ec2f117a82
+    bcec67e8e99cabfa7764d75ad9b158d72bfacf70ca1d0ec8bc6b4406d1bf8413
+    c00aae8461a256275598500ea0e187588c35a5d5d7454fb57eac18d9edb86a56
+    d4a35cd3121aa00d18544bb0ac01c3e1691d618f462c46129271bccf39f7e8ee
+
+-- See CONTRIBUTING for some Nix commands you will need to run if you
+-- update either of these.
+index-state:
+  -- Bump this if you need newer packages from Hackage
+  , hackage.haskell.org 2025-06-03T21:29:34Z
+  -- Bump this if you need newer packages from CHaP
+  , cardano-haskell-packages 2025-06-03T13:42:38Z
+
 packages: .
diff --git a/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal b/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal
index 5af036424a..01a3869f80 100644
--- a/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal
+++ b/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal
@@ -27,6 +27,8 @@ test-suite test
     hs-source-dirs: test
     main-is: Spec.hs
     other-modules:
+        Base
+        SpecHook
         TickNonceSpec
         UpdateNonceSpec
         OperationalCertificateSpec
@@ -35,9 +37,16 @@ test-suite test
         ChainHeadSpec
     build-depends:
         cardano-consensus-executable-spec,
+        cardano-crypto-class,
+        cardano-crypto-praos >= 2.2.1.0,
+        cardano-protocol-tpraos ^>=1.4,
+        cardano-ledger-core,
+        ouroboros-consensus-protocol,
         hspec,
         HUnit,
-        text
+        text,
+        bytestring,
+        io-classes >=1.4.0,
     build-tool-depends: hspec-discover:hspec-discover
     type: exitcode-stdio-1.0
     ghc-options:
diff --git a/docs/agda-spec/src/Spec/hs-src/test/Base.hs b/docs/agda-spec/src/Spec/hs-src/test/Base.hs
new file mode 100644
index 0000000000..b07a6d2bbf
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/test/Base.hs
@@ -0,0 +1,310 @@
+{-# LANGUAGE TypeApplications #-}
+
+module Base (
+  externalFunctions
+, sampleSKeyDSIGN
+, deriveVkeyDSIGFromSkeyDSIG
+, sampleSKeyKES
+, deriveVkeyKESFromSkeyKES
+, sampleSKeyVRF
+, deriveVkeyVRFFromSkeyVRF
+) where
+
+import Lib
+
+import Cardano.Ledger.Hashes (Hash, HASH, HashAlgorithm)
+import Cardano.Ledger.Keys (DSIGN, VKey (..))
+import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..), verifySignedDSIGN, signedDSIGN)
+import qualified Cardano.Crypto.KES as KES
+import qualified Cardano.Crypto.VRF as VRF
+import qualified Cardano.Crypto.VRF.Praos as VRF
+import Cardano.Crypto.Util (naturalToBytes, bytesToNatural)
+import Cardano.Crypto.Hash (hashFromBytes, sizeHash)
+import Cardano.Crypto.Seed (Seed, mkSeedFromBytes)
+import Data.Data (Proxy (..))
+import Data.ByteString (ByteString)
+import qualified Data.ByteString.Char8 as BC
+import Data.Either (isRight)
+import Data.Maybe (fromMaybe)
+
+-- NOTE:
+-- We allow the use of the "unsafe" APIs (e.g. `unsoundPureSignKES`) since the functions in
+-- this file are only for the purposes of conformance testing.
+
+
+-- Hashes
+
+integerToHash :: forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a)
+integerToHash = hashFromBytes . naturalToBytes (fromIntegral . sizeHash $ Proxy @h) . fromInteger
+
+-- DSIGN
+
+vkeyDSIGNFromInteger :: Integer -> Maybe (VKey kd)
+vkeyDSIGNFromInteger = fmap VKey . rawDeserialiseVerKeyDSIGN . naturalToBytes 32 . fromInteger
+
+vkeyDSIGNToInteger :: VKey kd -> Integer
+vkeyDSIGNToInteger = toInteger . bytesToNatural . rawSerialiseVerKeyDSIGN . unVKey
+
+skeyDSIGNFromInteger :: DSIGNAlgorithm v => Integer -> Maybe (SignKeyDSIGN v)
+skeyDSIGNFromInteger = rawDeserialiseSignKeyDSIGN . naturalToBytes 32 . fromInteger
+
+skeyDSIGNToInteger :: DSIGNAlgorithm v => SignKeyDSIGN v -> Integer
+skeyDSIGNToInteger = toInteger . bytesToNatural . rawSerialiseSignKeyDSIGN
+
+sigDSIGNFromInteger :: DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
+sigDSIGNFromInteger = rawDeserialiseSigDSIGN . naturalToBytes 64 . fromInteger
+
+sigDSIGNToInteger :: DSIGNAlgorithm v => SigDSIGN v -> Integer
+sigDSIGNToInteger = toInteger . bytesToNatural . rawSerialiseSigDSIGN
+
+signedDSIGNFromInteger :: forall v a. DSIGNAlgorithm v => Integer -> SignedDSIGN v a
+signedDSIGNFromInteger n =
+  SignedDSIGN
+    . fromMaybe
+      (error "Failed to decode the DSIGN signature")
+      $ sigDSIGNFromInteger n
+
+signedDSIGNToInteger :: DSIGNAlgorithm v => SignedDSIGN v a -> Integer
+signedDSIGNToInteger (SignedDSIGN x) = sigDSIGNToInteger x
+
+deriveVkeyDSIGFromSkeyDSIG :: Integer -> Integer
+deriveVkeyDSIGFromSkeyDSIG sk = vkeyDSIGNToInteger $ VKey $ deriveVerKeyDSIGN skey
+  where
+    skey =
+      fromMaybe
+        (error "Failed to convert an Agda DSIGN SKey to a Haskell DSIGN SKey")
+        $ skeyDSIGNFromInteger sk
+
+-- KES
+
+type KESAlg = KES.Sum6KES DSIGN HASH
+
+vkeyKESFromInteger :: KES.KESAlgorithm v => Integer -> Maybe (KES.VerKeyKES v)
+vkeyKESFromInteger = KES.rawDeserialiseVerKeyKES . naturalToBytes (fromIntegral $ KES.sizeVerKeyKES $ Proxy @KESAlg) . fromInteger
+
+vkeyKESToInteger :: KES.KESAlgorithm v => KES.VerKeyKES v -> Integer
+vkeyKESToInteger = toInteger . bytesToNatural . KES.rawSerialiseVerKeyKES
+
+skeyKESFromInteger :: KES.UnsoundPureKESAlgorithm v => Integer -> Maybe (KES.UnsoundPureSignKeyKES v)
+skeyKESFromInteger = KES.rawDeserialiseUnsoundPureSignKeyKES . naturalToBytes (fromIntegral $ KES.sizeSignKeyKES $ Proxy @KESAlg) . fromInteger
+
+skeyKESToInteger :: KES.UnsoundPureKESAlgorithm v => KES.UnsoundPureSignKeyKES v -> Integer
+skeyKESToInteger = toInteger . bytesToNatural . KES.rawSerialiseUnsoundPureSignKeyKES
+
+sigKESFromInteger :: KES.KESAlgorithm v => Integer -> Maybe (KES.SigKES v)
+sigKESFromInteger = KES.rawDeserialiseSigKES . naturalToBytes (fromIntegral $ KES.sizeSigKES $ Proxy @KESAlg) . fromInteger
+
+sigKESToInteger :: KES.KESAlgorithm v => KES.SigKES v -> Integer
+sigKESToInteger = toInteger . bytesToNatural . KES.rawSerialiseSigKES
+
+signedKESFromInteger :: forall v a. KES.KESAlgorithm v => Integer -> KES.SignedKES v a
+signedKESFromInteger n =
+  KES.SignedKES
+    . fromMaybe
+        (error "Failed to decode the KES signature")
+        $ sigKESFromInteger n
+
+signedKESToInteger :: KES.KESAlgorithm v => KES.SignedKES v a -> Integer
+signedKESToInteger (KES.SignedKES x) = sigKESToInteger x
+
+deriveVkeyKESFromSkeyKES :: Integer -> Integer
+deriveVkeyKESFromSkeyKES sk = vkeyKESToInteger @KESAlg $ KES.unsoundPureDeriveVerKeyKES skey
+  where
+    skey =
+      fromMaybe
+        (error "Failed to convert an Agda KES SKey to a Haskell KES SKey")
+        $ skeyKESFromInteger sk
+
+-- VRF
+
+type VRFAlg = VRF.PraosVRF
+
+vkeyVRFFromInteger :: VRF.VRFAlgorithm v => Integer -> Maybe (VRF.VerKeyVRF v)
+vkeyVRFFromInteger = VRF.rawDeserialiseVerKeyVRF . naturalToBytes (fromIntegral $ VRF.sizeVerKeyVRF $ Proxy @VRFAlg) . fromInteger
+
+vkeyVRFToInteger :: VRF.VRFAlgorithm v => VRF.VerKeyVRF v -> Integer
+vkeyVRFToInteger = toInteger . bytesToNatural . VRF.rawSerialiseVerKeyVRF
+
+skeyVRFFromInteger :: Integer -> VRF.SignKeyVRF VRFAlg
+skeyVRFFromInteger = fst . VRF.genKeyPairVRF . mkSeedFromBytes . naturalToBytes (fromIntegral $ VRF.sizeSignKeyVRF $ Proxy @VRFAlg) . fromInteger
+
+skeyVRFToInteger :: VRF.VRFAlgorithm v => VRF.SignKeyVRF v -> Integer
+skeyVRFToInteger = toInteger . bytesToNatural . VRF.rawSerialiseSignKeyVRF
+
+proofVRFFromInteger :: VRF.VRFAlgorithm v => Integer -> Maybe (VRF.CertVRF v)
+proofVRFFromInteger = VRF.rawDeserialiseCertVRF . naturalToBytes (fromIntegral $ VRF.sizeCertVRF $ Proxy @VRFAlg) . fromInteger
+
+proofVRFToInteger :: VRF.VRFAlgorithm v => VRF.CertVRF v -> Integer
+proofVRFToInteger = toInteger . bytesToNatural . VRF.rawSerialiseCertVRF
+
+deriveVkeyVRFFromSkeyVRF :: Integer -> Integer
+deriveVkeyVRFFromSkeyVRF = vkeyVRFToInteger @VRFAlg . VRF.deriveVerKeyVRF . skeyVRFFromInteger
+
+-- External functions
+
+externalFunctions :: ExternalFunctions
+externalFunctions = dummyExternalFunctions
+  { extSignDSIG     = extSignDSIG'
+  , extIsSignedDSIG = extIsSignedDSIG'
+  , extSignKES      = extSignKES'
+  , extIsSignedKES  = extIsSignedKES'
+  , extEvaluate     = extEvaluate'
+  , extVerify       = extVerify'
+  }
+  where
+    extSignDSIG' sk ser =
+      signedDSIGNToInteger $
+        signedDSIGN
+          @DSIGN
+          @(Hash HASH ByteString)
+          ()
+          hash
+          skey
+      where
+        skey =
+          fromMaybe
+            (error "Failed to convert an Agda SKey to a Haskell SKey")
+            $ skeyDSIGNFromInteger sk
+
+        hash =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show ser)
+            $ integerToHash ser
+
+    extIsSignedDSIG' vk ser sig =
+      isRight $
+        verifySignedDSIGN
+          @DSIGN
+          @(Hash HASH ByteString)
+          ()
+          vkey
+          hash
+          signature
+      where
+        vkey =
+          unVKey
+            . fromMaybe (error "Failed to convert an Agda VKey to a Haskell VKey")
+            $ vkeyDSIGNFromInteger vk
+
+        hash =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show ser)
+            $ integerToHash ser
+
+        signature =
+          signedDSIGNFromInteger sig
+
+    extSignKES' skf n ser =
+      sigKESToInteger $
+        KES.unsoundPureSignKES
+          @KESAlg
+          @(Hash HASH ByteString)
+          ()
+          kp
+          hash
+          skey
+      where
+        skey =
+          fromMaybe
+            (error "Failed to convert an Agda KES SKey to a Haskell KES SKey")
+            $ skeyKESFromInteger (skf n)
+
+        kp =
+          fromIntegral n
+
+        hash =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show ser)
+            $ integerToHash ser
+
+    extIsSignedKES' vk n ser sig =
+      isRight $
+        KES.verifySignedKES
+          @KESAlg
+          @(Hash HASH ByteString)
+          ()
+          vkey
+          kp
+          hash
+          signature
+      where
+        vkey =
+          fromMaybe
+            (error "Failed to convert an Agda KES VKey to a Haskell KES VKey")
+            $ vkeyKESFromInteger vk
+
+        kp =
+          fromIntegral n
+
+        hash =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show ser)
+            $ integerToHash ser
+
+        signature =
+          signedKESFromInteger sig
+
+    extEvaluate' sk seed = (proof, ser)
+      where
+        skey =
+          skeyVRFFromInteger sk
+
+        input =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show seed)
+            $ integerToHash seed
+
+        VRF.CertifiedVRF output cert =
+          VRF.evalCertified
+            @VRFAlg
+            @(Hash HASH ByteString)
+            ()
+            input
+            skey
+
+        proof =
+          proofVRFToInteger cert
+
+        ser =
+          (toInteger . bytesToNatural . VRF.getOutputVRFBytes) output
+
+    extVerify' vk seed (proof, ser) =
+      VRF.verifyCertified
+        @VRFAlg
+        @(Hash HASH ByteString)
+        ()
+        vkey
+        input
+        (VRF.CertifiedVRF output cert)
+      where
+        vkey =
+          fromMaybe
+            (error "Failed to convert an Agda VRF VKey to a Haskell VRF VKey")
+            $ vkeyVRFFromInteger vk
+
+        input =
+          fromMaybe
+            (error $ "Failed to get hash from integer:\n" <> show seed)
+            $ integerToHash seed
+
+        output =
+          VRF.mkTestOutputVRF $ fromIntegral ser
+
+        cert =
+          fromMaybe
+            (error "Failed to convert an Agda VRF proof to a Haskell VRF proof")
+            $ proofVRFFromInteger proof
+
+-- Utilities
+
+sampleSeed :: Seed
+sampleSeed = mkSeedFromBytes $ BC.pack $ replicate 32 '0'
+
+sampleSKeyDSIGN :: Integer
+sampleSKeyDSIGN = skeyDSIGNToInteger $ genKeyDSIGN @DSIGN sampleSeed
+
+sampleSKeyKES :: Integer
+sampleSKeyKES = skeyKESToInteger @KESAlg $ KES.unsoundPureGenKeyKES sampleSeed
+
+sampleSKeyVRF :: Integer
+sampleSKeyVRF = (skeyVRFToInteger @VRFAlg . fst . VRF.genKeyPairVRF) sampleSeed
diff --git a/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs
index 9fa3c8fc68..dfe14072b3 100644
--- a/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs
+++ b/docs/agda-spec/src/Spec/hs-src/test/OperationalCertificateSpec.hs
@@ -1,4 +1,11 @@
-module OperationalCertificateSpec (spec) where
+{-# LANGUAGE OverloadedRecordDot #-}
+
+module OperationalCertificateSpec (
+  spec
+, bh
+, bhb
+, hk
+) where
 
 import Data.Text
 
@@ -6,10 +13,37 @@ import Test.Hspec ( Spec, describe, it )
 import Test.HUnit ( (@?=) )
 
 import Lib
+import Base (
+    externalFunctions
+  , sampleSKeyDSIGN
+  , deriveVkeyDSIGFromSkeyDSIG
+  , sampleSKeyKES
+  , deriveVkeyKESFromSkeyKES)
 
 (.->) :: a -> b -> (a, b)
 (.->) = (,)
 
+coldSk :: Integer
+coldSk = sampleSKeyDSIGN
+
+coldVk :: Integer
+coldVk = deriveVkeyDSIGFromSkeyDSIG coldSk
+
+hotSk :: Integer
+hotSk = sampleSKeyKES
+
+hotVk :: Integer
+hotVk = deriveVkeyKESFromSkeyKES hotSk
+
+-- Since kp = kesPeriod bhbSlot = kesPeriod 0 = 0 / SlotsPerKESPeriodᶜ = 0 / 5 = 0,
+-- then period = kp -ᵏ ocC₀ = 0 - 0 = 0.
+period :: Integer
+period = 0
+
+skf :: Integer -> Integer
+skf 0 = hotSk -- for period 0
+skf _ = succ hotSk
+
 stpools :: OCertEnv
 stpools = MkHSSet []
 
@@ -27,16 +61,19 @@ cs' = MkHSMap
 
 oc :: OCert
 oc = MkOCert
-  { ocVkₕ = 123
+  { ocVkₕ = hotVk
   , ocN   = 234
   , ocC₀  = 0
-  , ocΣ   = 345
+  , ocΣ   = ocΣ'
   }
+  where
+    encodedOc = 0 -- since encode (ocVkₕ , ocN , ocC₀) = 0 due to mock serialization
+    ocΣ'      = externalFunctions.extSignDSIG coldSk encodedOc
 
 bhb :: BHBody
 bhb = MkBHBody
   { bhbPrevHeader = Nothing
-  , bhbIssuerVk   = 456
+  , bhbIssuerVk   = coldVk
   , bhbVrfVk      = 567
   , bhbBlockNo    = 1
   , bhbSlot       = 0
@@ -51,18 +88,18 @@ bhb = MkBHBody
 bh :: BHeader
 bh = MkBHeader
   { bhBody = bhb
-  , bhSig  = 901
+  , bhSig  = bhSig'
   }
+  where
+    encodedBhb = 0 -- since encode bhb = 0 due to mock serialization
+    bhSig'     = externalFunctions.extSignKES skf period encodedBhb
 
 hk :: KeyHashS
 hk = succ (bhbIssuerVk bhb) -- i.e., hash (bhbIssuerVk bhb)
 
-externalFunctions :: ExternalFunctions
-externalFunctions = dummyExternalFunctions { extIsSignedDSIG = \ _ _ sig -> sig > 0 }
-
 -- NOTE: Why should this test succeed? Here's the explanation:
 --
--- hk = hash bhbIssuerVk = hash 456 = 457
+-- hk = hash bhbIssuerVk = succ bhbIssuerVk (due to mock hashing)
 -- kp = kesPeriod bhbSlot = kesPeriod 0 = 0 / SlotsPerKESPeriodᶜ = 0 / 5 = 0
 -- t = kp -ᵏ ocC₀ = 0 - 0 = 0
 --
@@ -70,12 +107,12 @@ externalFunctions = dummyExternalFunctions { extIsSignedDSIG = \ _ _ sig -> sig
 -- ∙ kp < ocC₀ +ᵏ MaxKESEvo <=> 0 < 0 + 30 <=> 0 < 30 <=> true
 -- ∙ just 233 ≡ currentIssueNo stpools cs hk × (234 ≡ 233 ⊎ 234 ≡ suc 233))
 -- ∙ isSignedˢ bhbIssuerVk (encode (ocVkₕ , ocN , ocC₀)) ocΣ
---    <=> isSignedˢ 456 (encode (123 , 234 , 0)) 345
---    <=> isSignedˢ 456 0 345
+--    <=> isSignedˢ bhbIssuerVk (encode (ocVkₕ , 234 , 0)) ocΣ
+--    <=> isSignedˢ bhbIssuerVk 0 ocΣ
 --    <=> true
--- ∙ isSignedᵏ ocVkₕ t (encode bhb) 901
---    <=> isSignedᵏ 123 0 (encode bhb) 901
---    <=> isSignedᵏ 123 0 0 901
+-- ∙ isSignedᵏ ocVkₕ t (encode bhb) bhSig
+--    <=> isSignedᵏ ocVkₕ 0 (encode bhb) bhSig
+--    <=> isSignedᵏ ocVkₕ 0 0 bhSig
 --    <=> true
 
 spec :: Spec
@@ -84,5 +121,5 @@ spec = do
     it "ocertStep results in the expected state" $
       ocertStep externalFunctions stpools cs bh @?= Success cs'
 -- NOTE: Uncomment to run the debug version.
---  describe (unpack $ ocertDebug dummyExternalFunctions stpools cs bh) $ do
+--  describe (unpack $ ocertDebug externalFunctions stpools cs bh) $ do
 --    it "shows its argument" True
diff --git a/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs
index b8a46c1981..c9c8b02cd9 100644
--- a/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs
+++ b/docs/agda-spec/src/Spec/hs-src/test/ProtocolSpec.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE OverloadedRecordDot #-}
+
 module ProtocolSpec (spec) where
 
 import Data.Text
@@ -5,14 +7,32 @@ import Data.Text
 import Test.Hspec ( Spec, describe, it )
 import Test.HUnit ( (@?=) )
 
+import qualified OperationalCertificateSpec as OCS
 import Lib
+import Base (
+    externalFunctions
+  , sampleSKeyVRF
+  , deriveVkeyVRFFromSkeyVRF)
 
 (.->) :: a -> b -> (a, b)
 (.->) = (,)
 
+vrfSk :: Integer
+vrfSk = sampleSKeyVRF
+
+vrfVk :: Integer
+vrfVk = deriveVkeyVRFFromSkeyVRF vrfSk
+
+-- seed = slotToSeed 0 XOR nonceToSeed 2
+--      = id 0 XOR id 2
+--      = 0 + 2
+--      = 2
+seed :: Integer
+seed = 2
+
 pd :: PoolDistr
 pd = MkHSMap
-  [ hk .->  (1 / 3 , hkv) , 111 .-> (1 / 3 , 222) , 333 .-> (1 / 3 , 444) ]
+  [ OCS.hk .->  (1 / 3 , succ vrfVk) ]  -- i.e., hash vrfVk
 
 pe :: PrtclEnv
 pe = MkPrtclEnv
@@ -22,49 +42,26 @@ pe = MkPrtclEnv
 
 ps :: PrtclState
 ps = MkPrtclState
-  { psCs = MkHSMap [ hk  .-> 233 , 999 .-> 888 ]
+  { psCs = MkHSMap [ OCS.hk .-> 233 , 999 .-> 888 ]
   , psΗv = 3
   , psΗc = 5
   }
 
-oc :: OCert
-oc = MkOCert
-  { ocVkₕ = 123
-  , ocN   = 234
-  , ocC₀  = 0
-  , ocΣ   = 345
-  }
-
 bhb :: BHBody
-bhb = MkBHBody
-  { bhbPrevHeader = Nothing
-  , bhbIssuerVk   = 456
-  , bhbVrfVk      = 567
-  , bhbBlockNo    = 1
-  , bhbSlot       = 0
-  , bhbVrfRes     = 678
-  , bhbVrfPrf     = 789
-  , bhbBodySize   = 100
-  , bhbBodyHash   = 890
-  , bhbOc         = oc
-  , bhbPv         = (1, 0)
+bhb = OCS.bhb
+  { bhbVrfVk  = vrfVk
+  , bhbVrfRes = bhbVrfRes'
+  , bhbVrfPrf = bhbVrfPrf'
   }
+  where
+    (bhbVrfPrf', bhbVrfRes') = externalFunctions.extEvaluate vrfSk seed
 
 bh :: BHeader
-bh = MkBHeader
-  { bhBody = bhb
-  , bhSig  = 901
-  }
-
-hk :: KeyHashS
-hk = succ (bhbIssuerVk bhb) -- i.e., hash (bhbIssuerVk bhb)
-
-hkv :: KeyHashV
-hkv = 568
+bh = OCS.bh { bhBody = bhb }
 
 ps' :: PrtclState
 ps' = MkPrtclState
-  { psCs = MkHSMap [(hk, 234), (999, 888)],
+  { psCs = MkHSMap [ OCS.hk .-> 234, 999 .-> 888 ],
     psΗv = 4,
     psΗc = 4
   }
@@ -72,8 +69,7 @@ ps' = MkPrtclState
 {-
   NOTE: Why should this test succeed? Here's the explanation:
 
-  η = hBNonce bhb = serHashToNonce (hash (encode "N" ∥ encode vrfRes))
-                  = serHashToNonce (hash (encode "N" ∥ encode 678))
+  η = hBNonce bhb = serHashToNonce (hash (encode "N" ∥ encode bhbVrfRes))
                   = serHashToNonce (hash (0 ∥ 0))
                   = serHashToNonce (hash (0 + 0))
                   = serHashToNonce (hash 0)
@@ -90,20 +86,17 @@ ps' = MkPrtclState
     =
     vrfChecks 2 pd ½ bhb ???
 
-	∙ hk = hash issuerVk = hash 456 = succ 456 = 457
+	∙ hk = hash issuerVk = hash coldVk = succ coldVk
 
-  	∙ lookupPoolDistr pd 457 = just (1 / 3 , 568)
+  	∙ lookupPoolDistr pd (succ coldVk) = just (1 / 3 , succ vrfVk)
 
-  		∙ 568 ≡ hash 567 = succ 567 = 568 ===> True
+  		∙ succ vrfVk ≡ hash vrfVk = succ vrfVk ===> True
 
-  		∙ verify 567 2 (789 , 678) = True
+  		∙ verify vrfVk 2 (bhbVrfPrf , bhbVrfRes) = True
 
   		  since
 
-  		    seed = slotToSeed 0 XOR nonceToSeed 2
-  		         = id 0 XOR id 2
-  		         = 0 + 2
-  		         = 2
+  		    seed = 2
 
 	    ∙ checkLeaderVal (hBLeader bhb) f σ
   	      =
@@ -132,8 +125,7 @@ ps' = MkPrtclState
 		  since
 
             hBLeader bhb
-              = serHashToℕ (hash (encode "L" ∥ encode vrfRes))
-              = serHashToℕ (hash (encode "L" ∥ encode 678))
+              = serHashToℕ (hash (encode "L" ∥ encode bhbVrfRes))
               = serHashToℕ (hash (0 ∥ 0))
               = serHashToℕ (hash (0 + 0))
               = serHashToℕ (hash 0)
@@ -150,7 +142,7 @@ spec :: Spec
 spec = do
   describe "prtclStep" $ do
     it "prtclStep results in the expected state" $
-      prtclStep dummyExternalFunctions pe ps bh @?= Success ps'
+      prtclStep externalFunctions pe ps bh @?= Success ps'
 -- NOTE: Uncomment to run the debug version.
---  describe (unpack $ prtclDebug dummyExternalFunctions pe ps bh) $ do
+--  describe (unpack $ prtclDebug externalFunctions pe ps bh) $ do
 --    it "shows its argument" True
diff --git a/docs/agda-spec/src/Spec/hs-src/test/SpecHook.hs b/docs/agda-spec/src/Spec/hs-src/test/SpecHook.hs
new file mode 100644
index 0000000000..9b2acb9546
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/test/SpecHook.hs
@@ -0,0 +1,8 @@
+module SpecHook where
+
+import Test.Hspec
+import Cardano.Crypto.Init (cryptoInit)
+
+hook :: Spec -> Spec
+hook = before_ cryptoInit
+
diff --git a/nix/agda.nix b/nix/agda.nix
index 58870c5ce2..0d3ddea934 100644
--- a/nix/agda.nix
+++ b/nix/agda.nix
@@ -108,7 +108,17 @@ let
     hsExe = customAgda.haskell.lib.disableLibraryProfiling (customAgda.haskellPackages.callCabal2nixWithOptions "cardano-consensus-executable-spec" "${hsSrc}/haskell/Spec" "--no-haddock" { });
 
     shell = pkgs.mkShell {
-      packages = [ agda latex customAgda.ghc customAgda.cabal-install ];
+      packages = [
+        agda
+        latex
+        customAgda.ghc
+        customAgda.cabal-install
+        final.pkg-config
+        final.libsodium-vrf
+        final.blst
+        final.secp256k1
+        final.zlib
+      ];
     };
   };
 in