diff --git a/docs/agda-spec/src/Foreign/Convertible.agda b/docs/agda-spec/src/Foreign/Convertible.agda
new file mode 100644
index 0000000000..3cc064528d
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/Convertible.agda
@@ -0,0 +1,82 @@
+module Foreign.Convertible where
+
+open import Ledger.Prelude
+open import Foreign.HaskellTypes
+
+record Convertible (A B : Type) : Type where
+  field to   : A → B
+        from : B → A
+open Convertible ⦃...⦄ public
+
+HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
+HsConvertible A = Convertible A (HsType A)
+
+Convertible-Refl : ∀ {A} → Convertible A A
+Convertible-Refl = λ where .to → id; .from → id
+
+Convertible₁ : (Type → Type) → (Type → Type) → Type₁
+Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)
+
+Convertible₂ : (Type → Type → Type) → (Type → Type → Type) → Type₁
+Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)
+
+Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F
+Functor⇒Convertible = λ where
+  .to   → map to
+  .from → map from
+
+Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F
+Bifunctor⇒Convertible = λ where
+  .to   → bimap to to
+  .from → bimap from from
+
+_⨾_ : ∀ {A B C} → Convertible A B → Convertible B C → Convertible A C
+(c ⨾ c') .to   = c' .to   ∘ c  .to
+(c ⨾ c') .from = c  .from ∘ c' .from
+
+-- ** instances
+
+open import Foreign.Haskell
+open import Foreign.Haskell.Coerce using (coerce)
+
+instance
+  Convertible-Maybe : Convertible₁ Maybe Maybe
+  Convertible-Maybe = Functor⇒Convertible
+
+  Convertible-× : Convertible₂ _×_ _×_
+  Convertible-× = Bifunctor⇒Convertible
+
+  Convertible-Pair : Convertible₂ _×_ Pair
+  Convertible-Pair = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-⊎ : Convertible₂ _⊎_ _⊎_
+  Convertible-⊎ = Bifunctor⇒Convertible
+
+  Convertible-Either : Convertible₂ _⊎_ Either
+  Convertible-Either = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-FinSet : Convertible₁ ℙ_ List
+  Convertible-FinSet = λ where
+    .to   → map to   ∘ setToList
+    .from → fromList ∘ map from
+
+  Convertible-Map : ∀ {K K' V V'} → ⦃ DecEq K ⦄
+    → ⦃ Convertible K K' ⦄ → ⦃ Convertible V V' ⦄
+    → Convertible (K ⇀ V) (List $ Pair K' V')
+  Convertible-Map = λ where
+    .to   → to        ∘ proj₁
+    .from → fromListᵐ ∘ map from
+
+  Convertible-List : Convertible₁ List List
+  Convertible-List = λ where
+    .to   → map to
+    .from → map from
+
+  Convertible-Fun : ∀ {A A' B B'} → ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄ → Convertible (A → B) (A' → B')
+  Convertible-Fun = λ where
+    .to   → λ f → to   ∘ f ∘ from
+    .from → λ f → from ∘ f ∘ to
diff --git a/docs/agda-spec/src/Foreign/Convertible/Deriving.agda b/docs/agda-spec/src/Foreign/Convertible/Deriving.agda
new file mode 100644
index 0000000000..dc85fc206c
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/Convertible/Deriving.agda
@@ -0,0 +1,172 @@
+module Foreign.Convertible.Deriving where
+
+open import Level
+open import MetaPrelude
+open import Meta
+
+import Data.List as L
+import Data.List.NonEmpty as NE
+import Data.String as S
+import Data.Product as P
+
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+open import Reflection.Tactic
+open import Reflection.AST.Term
+open import Reflection.AST.DeBruijn
+import Reflection.TCM as R
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+import Function.Identity.Effectful as Identity
+
+open import Class.DecEq
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadTC.Instances
+open import Class.Traversable
+open import Class.Show
+open import Class.MonadReader
+
+open import Tactic.Substitute
+open import Foreign.Convertible
+open import Foreign.HaskellTypes
+open import Foreign.HaskellTypes.Deriving
+
+private instance
+  _ = Functor-M {TC}
+
+-- TODO: move to agda-stdlib-meta
+liftTC : ∀ {a} {A : Set a} → R.TC A → TC A
+liftTC m _ = m
+
+private
+
+  open MonadReader ⦃...⦄
+
+  variable
+    A B C : Set
+
+  TyViewTel = List (Abs (Arg Type))
+
+  substTel : Subst TyViewTel
+  substTel x s [] = []
+  substTel x s (abs z t ∷ tel) = abs z (substArg x s t) ∷ (substTel (ℕ.suc x) s tel)
+    -- Note: `abs` is abused in TyViewTel and doesn't actually scope over the `t`
+
+  -- Substitute leading level parameters with lzero
+  smashLevels : TyViewTel → ℕ × TyViewTel
+  smashLevels (abs s (arg i (def (quote Level) [])) ∷ tel) =
+    P.map ℕ.suc (substTel 0 (quote 0ℓ ∙)) $ smashLevels tel
+  smashLevels tel = (0 , tel)
+
+  tyViewToTel : TyViewTel → Telescope
+  tyViewToTel = L.map λ where (abs s a) → s , a
+
+  hideTyView : Abs (Arg A) → Abs (Arg A)
+  hideTyView (abs s (arg (arg-info _ m) x)) = abs s (arg (arg-info hidden m) x)
+
+  -- The type of a Convertible instance. For parameterised types adds the appropriate instance
+  -- arguments and instantiates level arguments to lzero. For instance,
+  -- instanceType _⊎_ Hs.Either = {A B : Set} {a b : Set} → ⦃ Convertible A a ⦄ → ⦃ Convertible B b ⦄
+  --                              Convertible (A ⊎ B) (Hs.Either a b)
+  instanceType : (agdaName hsName : Name) → TC TypeView
+  instanceType agdaName hsName = do
+    aLvls , agdaParams ← smashLevels <$> getParamsAndIndices agdaName
+    hLvls , hsParams   ← smashLevels <$> getParamsAndIndices hsName
+    true ← return (length agdaParams == length hsParams)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of parameters" agdaName hsName
+    let n = length agdaParams
+        l₀ = quote 0ℓ ∙
+    agdaTy ← applyWithVisibility agdaName $ L.replicate aLvls l₀ ++ L.map ♯ (take n (downFrom (n + n)))
+    hsTy   ← applyWithVisibility hsName   $ L.replicate hLvls l₀ ++ L.map ♯ (downFrom n)
+    let instHead = weaken n $ quote Convertible ∙⟦ agdaTy ∣ hsTy ⟧
+        tel      = L.map hideTyView (agdaParams ++ hsParams) ++
+                   L.replicate n (abs "_" (iArg (quote Convertible ∙⟦ ♯ (n + n ∸ 1) ∣ ♯ (n ∸ 1) ⟧)))
+    return $ tel , instHead
+
+  -- Compute one clause of the Convertible instance. For instance,
+  -- conversionClause Convertible.to to ((c₁ , _) , (c₂ , _)) generates
+  -- .to (c₁ x₁ .. xn) = c₂ (to x₁) .. (to xn)
+  -- where the xi are the visible constructor arguments.
+  conversionClause : Name → Name → (Name × Type) × (Name × Type) → TC Clause
+  conversionClause prjP prjE ((fromC , fromTy) , (toC , toTy)) = do
+    let isVis   = λ { (abs _ (arg (arg-info visible _) _)) → true; _ → false }
+        fromTel = L.filterᵇ isVis (proj₁ (viewTy fromTy))
+        toTel   = L.filterᵇ isVis (proj₁ (viewTy toTy))
+        n       = length fromTel
+        mkCon  c mkArg = Term.con c    $ L.map (vArg ∘ mkArg ∘ ♯)  (downFrom n)
+        mkConP c mkArg = Pattern.con c $ L.map (vArg ∘ mkArg ∘ `_) (downFrom n)
+    true ← return (n == length toTel)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of arguments" fromC toC
+    return $ clause (tyViewToTel $ L.map (λ where (abs x (arg i _)) → abs x (arg i unknown)) fromTel)
+                    (vArg (proj prjP) ∷ vArg (mkConP fromC id) ∷ [])
+                    (mkCon toC (prjE ∙⟦_⟧))
+
+  -- Compute the clauses of a convertible instance.
+  instanceClauses : (agdaName hsName : Name) → TC (List Clause)
+  instanceClauses agdaName hsName = do
+    agdaCons ← getConstrs agdaName
+    hsCons   ← getConstrs hsName
+    agdaPars ← length <$> getParamsAndIndices agdaName
+    hsPars   ← length <$> getParamsAndIndices hsName
+    true ← return (length agdaCons == length hsCons)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of constructors" agdaName hsName
+    toClauses   ← mapM (conversionClause (quote Convertible.to)   (quote to)  ) (L.zip agdaCons hsCons)
+    fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
+    return $ toClauses ++ fromClauses
+
+  absurdClause : Name → Clause
+  absurdClause prj = absurd-clause (("x" , vArg unknown) ∷ []) (vArg (proj prj) ∷ vArg (absurd 0) ∷ [])
+
+  -- Compute conversion clauses for the current goal and wrap them in a pattern lambda.
+  patternLambda : TC Term
+  patternLambda = do
+    quote Convertible ∙⟦ `A ∣ `B ⟧ ← reduce =<< goalTy
+      where t → liftTC $ R.typeErrorFmt "Expected Convertible A B, got %t" t
+    agdaCons ← getConstrsForType `A
+    hsCons   ← getConstrsForType `B
+    toClauses   ← mapM (conversionClause (quote Convertible.to)   (quote to)  ) (L.zip agdaCons hsCons)
+    fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
+    case toClauses ++ fromClauses of λ where
+      []  → return $ pat-lam (absurdClause (quote Convertible.to) ∷ absurdClause (quote Convertible.from) ∷ []) []
+      cls → return $ pat-lam cls []
+
+doPatternLambda : Term → R.TC Term
+doPatternLambda hole = patternLambda =<< initTCEnvWithGoal hole
+
+-- Deriving a Convertible instance. Usage
+--   unquoteDecl iName = deriveConvertible iName (quote AgdaTy) (quote HsTy)
+deriveConvertible : Name → Name → Name → R.TC ⊤
+deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (agda-sort (lit 0)) do
+  agdaDef ← getDefinition agdaName
+  hsDef   ← getDefinition hsName
+  -- instName ← freshName $ "Convertible" S.++ show hsName
+  instTel , instTy ← instanceType agdaName hsName
+  inst    ← declareDef (iArg instName) (tyView (instTel , instTy))
+  clauses ← instanceClauses agdaName hsName
+  defineFun instName clauses
+  return _
+
+-- Macros providing an alternative interface. Usage
+--   iName : ConvertibleType AgdaTy HsTy
+--   iName = autoConvertible
+-- or
+--   iName = autoConvert AgdaTy
+macro
+  ConvertibleType : Name → Name → Tactic
+  ConvertibleType agdaName hsName = initTac ⦃ defaultTCOptions ⦄ $
+    unifyWithGoal ∘ tyView =<< instanceType agdaName hsName
+
+  autoConvertible : Tactic
+  autoConvertible = initTac ⦃ defaultTCOptions ⦄ $
+    unifyWithGoal =<< patternLambda
+
+  autoConvert : Name → Tactic
+  autoConvert d hole = do
+    hsTyMeta ← R.newMeta `Set
+    R.checkType hole $ quote Convertible ∙⟦ d ∙ ∣ hsTyMeta ⟧
+    hsTy ← solveHsType (d ∙)
+    R.unify hsTyMeta hsTy
+    R.unify hole =<< doPatternLambda hole
diff --git a/docs/agda-spec/src/Foreign/Convertible/DerivingTest.agda b/docs/agda-spec/src/Foreign/Convertible/DerivingTest.agda
new file mode 100644
index 0000000000..43f1ecc23d
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/Convertible/DerivingTest.agda
@@ -0,0 +1,86 @@
+
+module Foreign.Convertible.DerivingTest where
+
+open import Level
+open import MetaPrelude
+open import Meta
+
+import Data.List as L
+import Data.List.NonEmpty as NE
+import Data.String as S
+import Data.Product as P
+
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+open import Reflection.Tactic
+open import Reflection.AST.Term
+open import Reflection.AST.DeBruijn
+import Reflection.TCM as R
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+import Function.Identity.Effectful as Identity
+
+open import Class.DecEq
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadTC.Instances
+open import Class.Traversable
+open import Class.Show
+open import Class.MonadReader
+
+open import Foreign.Convertible
+open import Foreign.Convertible.Deriving
+
+-- Tests
+
+open import Data.Maybe.Base
+open import Data.Sum.Base
+
+data HsMaybe (a : Set) : Set where
+  just    : (x : a) → HsMaybe a
+  nothing : HsMaybe a
+
+data HsEither (a b : Set) : Set where
+  left : a → HsEither a b
+  right : b → HsEither a b
+
+-- We should be able to generate this
+ConvertibleMaybe : ∀ {a a'} → ⦃ Convertible a a' ⦄ → Convertible (Maybe a) (HsMaybe a')
+ConvertibleMaybe .to (just x)   = just (to x)
+ConvertibleMaybe .to nothing    = nothing
+ConvertibleMaybe .from (just x) = just (from x)
+ConvertibleMaybe .from nothing  = nothing
+
+-- With deriveConvertible
+unquoteDecl iConvertMaybe  = deriveConvertible iConvertMaybe (quote Maybe) (quote HsMaybe)
+
+-- or with ConvertibleType and autoConvertible
+instance
+  iConvertEither : ConvertibleType _⊎_ HsEither
+  iConvertEither = autoConvertible
+
+instance
+  ConvertibleNat = Convertible-Refl {ℕ}
+
+test : ℕ ⊎ Maybe ℕ → HsEither ℕ (HsMaybe ℕ)
+test = to
+
+_ : test (inj₂ (just 5)) ≡ right (just 5)
+_ = refl
+
+-- There was a problem due to Agda#7182 with record types in parameterised modules.
+
+module Param (A : Set) where
+  record AgdaThing : Set where
+    field theThing : A
+
+record HsThing : Set where
+  field theThing : ℕ
+
+open Param ℕ
+unquoteDecl iConvertThing = deriveConvertible iConvertThing (quote AgdaThing) (quote HsThing)
+
+convThing : Convertible AgdaThing HsThing
+convThing = autoConvertible
diff --git a/docs/agda-spec/src/Foreign/HaskellTypes.agda b/docs/agda-spec/src/Foreign/HaskellTypes.agda
new file mode 100644
index 0000000000..04ce72a1cf
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/HaskellTypes.agda
@@ -0,0 +1,52 @@
+
+module Foreign.HaskellTypes where
+
+open import Level using (Level)
+open import Data.Bool.Base using (Bool)
+open import Data.Nat.Base using (ℕ)
+open import Data.String.Base using (String)
+open import Data.List.Base using (List)
+open import Data.Maybe.Base using (Maybe)
+open import Data.Sum.Base using (_⊎_)
+open import Data.Product.Base using (_×_)
+open import Data.Unit using (⊤)
+
+open import Foreign.Haskell.Pair using (Pair)
+open import Foreign.Haskell.Either using (Either)
+
+private variable
+  l : Level
+  A B : Set l
+
+record HasHsType (A : Set l) : Set₁ where
+  field
+    HsType : Set
+
+HsType : (A : Set l) → ⦃ HasHsType A ⦄ → Set
+HsType _ ⦃ i ⦄ = i .HasHsType.HsType
+
+MkHsType : (A : Set l) (Hs : Set) → HasHsType A
+MkHsType A Hs .HasHsType.HsType = Hs
+
+instance
+
+  iHsTy-ℕ      = MkHsType ℕ ℕ
+  iHsTy-Bool   = MkHsType Bool Bool
+  iHsTy-⊤      = MkHsType ⊤ ⊤
+  iHsTy-String = MkHsType String String
+
+  -- Could make a macro for these kind of congruence instances.
+  iHsTy-List : ⦃ HasHsType A ⦄ → HasHsType (List A)
+  iHsTy-List {A = A} .HasHsType.HsType = List (HsType A)
+
+  iHsTy-Maybe : ⦃ HasHsType A ⦄ → HasHsType (Maybe A)
+  iHsTy-Maybe {A = A} .HasHsType.HsType = Maybe (HsType A)
+
+  iHsTy-Fun : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A → B)
+  iHsTy-Fun {A = A} {B = B} .HasHsType.HsType = HsType A → HsType B
+
+  iHsTy-Sum : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⊎ B)
+  iHsTy-Sum {A = A} {B = B} .HasHsType.HsType = Either (HsType A) (HsType B)
+
+  iHsTy-Pair : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A × B)
+  iHsTy-Pair {A = A} {B = B} .HasHsType.HsType = Pair (HsType A) (HsType B)
diff --git a/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda b/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda
new file mode 100644
index 0000000000..98149a3766
--- /dev/null
+++ b/docs/agda-spec/src/Foreign/HaskellTypes/Deriving.agda
@@ -0,0 +1,366 @@
+
+module Foreign.HaskellTypes.Deriving where
+
+open import Meta hiding (TC; Monad-TC; MonadError-TC)
+
+open import Level using (Level; 0ℓ)
+open import Agda.Builtin.Reflection using (declareData; defineData; pragmaForeign; pragmaCompile;
+                                           solveInstanceConstraints)
+open import Reflection as R hiding (showName; _>>=_; _>>_)
+open import Reflection.AST hiding (showName)
+open import Reflection.AST.DeBruijn
+open import Data.Maybe using (Maybe; nothing; just; fromMaybe; maybe′; _<∣>_)
+open import Data.Unit using (⊤; tt)
+open import Data.Integer.Base using (ℤ)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.String using (String) renaming (_++_ to _&_)
+open import Data.Product hiding (map; zip; zipWith)
+import Data.String as String
+open import Data.Bool
+open import Data.Nat
+open import Data.List hiding (lookup; fromMaybe)
+open import Data.Char using (toUpper; toLower)
+open import Foreign.Haskell
+open import Function
+open import Text.Printf
+
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadError
+open import Class.MonadReader
+open import Class.Show
+open import Class.Show.Instances
+open import Class.MonadTC using (TCEnv; dontReduce; defaultTCOptions)
+open import Tactic.Derive.Show using (showName)
+
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+open import Foreign.HaskellTypes
+open import Foreign.Haskell.Pair using (Pair)
+
+{-
+Need to generate:
+  - a data type that can be compiled to a Haskell data type
+  - the corresponding Haskell type (in a FOREIGN pragma)
+  - the COMPILE pragma binding them together
+-}
+
+private variable
+  l : Level
+  A B : Set l
+
+-- TODO: somewhere else
+`Set = agda-sort (Sort.set (quote 0ℓ ∙))
+
+-- * Controlling the names of the generated types
+
+record NameEnv : Set where
+  field
+    customNames : List (Name × String)
+    tName       : Name → Maybe String
+    cName       : Name → Maybe String
+    fName       : Name → Maybe String
+
+private
+  mapHead : (A → A) → List A → List A
+  mapHead f []       = []
+  mapHead f (x ∷ xs) = f x ∷ xs
+
+capitalize : String → String
+capitalize = String.fromList ∘ mapHead toUpper ∘ String.toList
+
+uncapitalize : String → String
+uncapitalize = String.fromList ∘ mapHead toLower ∘ String.toList
+
+private
+  lookup : ⦃ DecEq A ⦄ → A → List (A × B) → Maybe B
+  lookup x xs = proj₂ <$> findᵇ ((x ==_) ∘ proj₁) xs
+
+  lookupEnv : (NameEnv → Name → Maybe String) → NameEnv → Name → Maybe String
+  lookupEnv fn env x = lookup x (NameEnv.customNames env) <∣> fn env x
+
+  lookupTypeName  = lookupEnv NameEnv.tName
+  lookupConName   = lookupEnv NameEnv.cName
+  lookupFieldName = lookupEnv NameEnv.fName
+
+  emptyEnv : NameEnv
+  emptyEnv = record{ customNames = []
+                   ; tName = const nothing
+                   ; cName = const nothing
+                   ; fName = const nothing }
+
+  customName : Name → String → NameEnv
+  customName x s = record emptyEnv { customNames = (x , s) ∷ [] }
+
+onTypes : (String → String) → NameEnv
+onTypes f = record emptyEnv { tName = just ∘ f ∘ showName }
+
+onConstructors : (String → String) → NameEnv
+onConstructors f = record emptyEnv { cName = just ∘ f ∘ showName }
+
+withName : String → NameEnv
+withName t = onTypes (const t)
+
+-- Only use for single constructor types obviously
+withConstructor : String → NameEnv
+withConstructor c = onConstructors (const c)
+
+onFields : (String → String) → NameEnv
+onFields f = record emptyEnv { fName = just ∘ f ∘ showName }
+
+fieldPrefix : String → NameEnv
+fieldPrefix pre = onFields $ (pre String.++_) ∘ capitalize
+
+infixr 5 _•_
+_•_ : NameEnv → NameEnv → NameEnv
+env • env₁ = record
+  { customNames = env.customNames ++ env₁.customNames
+  ; tName       = λ x → env.tName x <∣> env₁.tName x
+  ; cName       = λ x → env.cName x <∣> env₁.cName x
+  ; fName       = λ x → env.fName x <∣> env₁.fName x
+  }
+  where
+    module env  = NameEnv env
+    module env₁ = NameEnv env₁
+
+
+-- * The inner workings
+
+solveHsType : Term → TC Term
+solveHsType tm = do
+  hsTy ← checkType (quote HsType ∙⟦ tm ⟧) `Set
+  solveInstanceConstraints
+  normalise hsTy >>= λ where
+    (def (quote HsType) _) → typeErrorFmt "Failed to solve HsType %t" tm
+    hsTy                   → return hsTy
+
+private
+  debug = debugPrintFmt "tactic.hs-types"
+
+  _‼_ : List A → ℕ → Maybe A
+  []       ‼ i     = nothing
+  (x ∷ xs) ‼ zero  = just x
+  (x ∷ xs) ‼ suc i = xs ‼ i
+
+  specialHsTypes : List (Name × String)
+  specialHsTypes = (quote ⊤      , "()")
+                 ∷ (quote ℕ      , "Integer")
+                 ∷ (quote ℤ      , "Integer")
+                 ∷ (quote Bool   , "Bool")
+                 ∷ (quote List   , "[]")
+                 ∷ (quote Pair   , "(,)")
+                 ∷ (quote Maybe  , "Maybe")
+                 ∷ (quote Either , "Either")
+                 ∷ (quote String , "Data.Text.Text")
+                 ∷ []
+
+  hsTypeName : NameEnv → Name → String
+  hsTypeName env d = fromMaybe (capitalize $ showName d) (lookupTypeName env d)
+
+  freshHsTypeName : NameEnv → Name → TC Name
+  freshHsTypeName env d = freshName (hsTypeName env d)
+
+  hsConName : NameEnv → Name → String
+  hsConName env c = fromMaybe (capitalize $ showName c) (lookupConName env c)
+
+  hsFieldName : NameEnv → Name → String
+  hsFieldName env f = fromMaybe (uncapitalize $ showName f) (lookupFieldName env f)
+
+  freshHsConName : NameEnv → Name → Name → TC Name
+  freshHsConName env tyName c =
+    if showName c == "constructor"
+    then freshName (hsConName env tyName) -- Unnamed record constructor: use type name
+    else freshName (hsConName env c)
+
+  isThis : Name → Term → Bool
+  isThis f (def g _) = f == g
+  isThis _ _ = false
+
+  computeHsType : Name → Name → Term → TC Term
+  computeHsType aThis hThis tm with isThis aThis tm
+  ... | true = pure (hThis ∙)
+  computeHsType aThis hThis (Π[ x ∶ arg (arg-info visible _) a ] b) | false = do
+    dom ← computeHsType aThis hThis a
+    rng ← extendContext x (vArg a) $ computeHsType aThis hThis b
+    pure (vΠ[ x ∶ dom ] rng)
+  computeHsType aThis hThis (Π[ x ∶ a ] b) | false = do
+    ty ← extendContext x a $ computeHsType aThis hThis b
+    just ty′ ← pure (strengthen ty)
+      where nothing → extendContext x a $ typeErrorFmt "%s free in computed HsType %t" x ty
+    pure ty′
+  -- Hack to get recursive occurrences under lists to work
+  computeHsType aThis hThis (def (quote List) (_ ∷ vArg a ∷ [])) | false = do
+    ty ← computeHsType aThis hThis a
+    pure (quote List ∙⟦ ty ⟧)
+  computeHsType _ _ tm | false = do
+    debug 10 "solving HsType %t" tm
+    ty ← solveHsType tm
+    debug 10 "HsType %t = %t" tm ty
+    pure ty
+
+  makeHsCon : NameEnv → Name → Name → Name → TC (Name × Agda.Builtin.Reflection.Quantity × Type)
+  makeHsCon env agdaName hsName c = do
+    debug 10 "Making constructor %q : %q" c agdaName
+    def agdaName' _ ← normalise (def agdaName [])
+      where _ → typeErrorFmt "Failed to compute source type for %q" agdaName
+    hsC  ← freshHsConName env hsName c
+    cTy  ← getType c
+    debug 10 "cTy = %t" cTy
+    hsTy ← computeHsType agdaName' hsName cTy
+    debug 10 "hsTy = %t" hsTy
+    pure (hsC , quantity-ω , hsTy)
+
+  makeHsData : NameEnv → Name → ℕ → List Name → TC Name
+  makeHsData env agdaName nPars constrs = do
+    hsName ← freshHsTypeName env agdaName
+    declareData hsName 0 `Set
+    hsCons ← mapM (makeHsCon env agdaName hsName) constrs
+    defineData hsName hsCons
+    pure hsName
+
+  makeHsType : NameEnv → Name → TC Name
+  makeHsType env d = getDefinition d >>= λ where
+      (data-type pars cs) → makeHsData env d pars cs
+      (record-type c fs)  → makeHsData env d 0 (c ∷ [])
+      _                   → typeErrorFmt "%q is not a data or record type" d
+
+  joinStrings : String → List String → String
+  joinStrings sep ss = foldr _&_ "" $ intersperse sep ss
+
+  compilePragma : Name → List Name → String
+  compilePragma d cs = printf "= data %s (%s)" (showName d) (joinStrings " | " (map showName cs))
+
+  renderHsTypeName : Name → String
+  renderHsTypeName d = fromMaybe ("MAlonzo.Code." String.++ R.showName d) (lookup d specialHsTypes)
+
+  renderHsType : Term → String
+  renderHsArgs : List (Arg Term) → List String
+
+  renderHsType (def (quote List) (_ ∷ vArg a ∷ [])) = printf "[%s]" (renderHsType a)
+  renderHsType (def (quote Pair) (_ ∷ _ ∷ vArg a ∷ vArg b ∷ [])) = printf "(%s, %s)" (renderHsType a) (renderHsType b)
+  renderHsType (def d []) = renderHsTypeName d
+  renderHsType (def d vs) = printf "(%s %s)" (renderHsTypeName d) (joinStrings " " (renderHsArgs vs))
+  renderHsType (Π[ s ∶ arg _ a ] b) = printf "%s -> %s" (renderHsType a) (renderHsType b)
+  renderHsType t = printf "(TODO: renderHsType %s)" (show t)
+
+  renderHsArgs [] = []
+  renderHsArgs (vArg a ∷ as) = renderHsType a ∷ renderHsArgs as
+  renderHsArgs (_ ∷ as) = renderHsArgs as
+
+  foreignPragma : Name → List Name → TC String
+  foreignPragma d cs = do
+    cons ← forM cs λ c → do
+            tel , _ ← viewTy <$> getType c
+            let args = map unAbs tel
+            pure $ printf "%s %s" (showName c) (joinStrings " " $ renderHsArgs args)
+    pure $ printf "data %s = %s\n  deriving (Show, Eq, Generic)"
+                  (showName d) (joinStrings " | " cons)
+
+  -- Record types
+  foreignPragmaRec : NameEnv → Name → List Name → List Name → TC String
+  foreignPragmaRec _ d [] _ = typeErrorFmt "impossible: %q is a record type with no constructors" d
+  foreignPragmaRec env d (c ∷ _) fs = do
+    tel , _ ← viewTy <$> withNormalisation true (getType c)
+    let fNames = map (hsFieldName env) fs
+    let args = map unAbs tel
+        renderField f ty = printf "%s :: %s" f (renderHsType $ unArg ty)
+        con = printf "%s {%s}" (showName c) (joinStrings ", " $ zipWith renderField fNames args)
+    pure $ printf "data %s = %s\n  deriving (Show, Eq, Generic)"
+                  (showName d) con
+
+  hsImports : String
+  hsImports = "import GHC.Generics (Generic)\nimport Text.Show.Functions\n"
+
+  hsInstances : String
+  hsInstances = "instance Eq (a -> b) where _ == _ = False\n" -- functions are never equal
+
+  -- Take the name of a simple data type and generate the COMPILE and
+  -- FOREIGN pragmas to bind to Haskell.
+  bindHsType : NameEnv → Name → Name → TC ⊤
+  bindHsType env agdaName hsName = getDefinition hsName >>= λ where
+    (data-type pars cs) → do
+      pragmaForeign "GHC" (hsImports & "\n" & hsInstances)
+      pragmaCompile "GHC" hsName $ compilePragma hsName cs
+      getDefinition agdaName >>= λ where
+        (data-type _ _)    → pragmaForeign "GHC" =<< foreignPragma hsName cs
+        (record-type _ fs) → pragmaForeign "GHC" =<< foreignPragmaRec env hsName cs (map unArg fs)
+        _ → typeErrorFmt "%q is not a data or record type" agdaName
+    _ → typeErrorFmt "%q is not a data type (impossible)" hsName
+
+  computeProjections : ℕ → Name → TC (List Term)
+  computeProjections npars c = do
+    argTys , _ ← viewTy <$> getType c
+    let is  = downFrom (length argTys)
+        tel = map (λ where (abs x ty) → x , ty) argTys
+        lhs = vArg (con c (map (λ where (i , abs x (arg info _)) → arg info (var i))
+                               (drop npars (zip is argTys)))) ∷ []
+    return $ map (λ i → pat-lam (clause tel lhs (var i []) ∷ []) []) (drop npars is)
+
+  makeTypeAlias : Name → NameEnv → Term → TC ⊤
+  makeTypeAlias agdaName env hole = do
+    hsTy ← solveHsType (def agdaName [])
+    pragmaForeign "GHC" $ printf "type %s = %s" (hsTypeName env agdaName) (renderHsType hsTy)
+    unify hole (quote return ∙⟦ con (quote tt) [] ⟧)
+
+-- * Exported macros
+
+doAutoHsType : NameEnv → Name → Term → TC Term
+doAutoHsType env d hole = do
+  checkType hole (quote HasHsType ∙⟦ d ∙ ⟧)
+  hs ← makeHsType env d
+  debug 50 "  HsType %q = %q" d hs
+  bindHsType env d hs
+  unify hole (`λ⟦ proj (quote HasHsType.HsType) ⇒ hs ∙ ⟧)
+  pure (hs ∙)
+
+macro
+  autoHsType : Name → Term → TC ⊤
+  autoHsType d hole = _ <$ doAutoHsType emptyEnv d hole
+
+  infix 0 autoHsType_⊣_
+  autoHsType_⊣_ : Name → NameEnv → Term → TC ⊤
+  autoHsType_⊣_ d env hole = _ <$ doAutoHsType env d hole
+
+  infix 9 _↦_
+  _↦_ : Name → String → Term → TC ⊤
+  x ↦ s = unify (quote customName ∙⟦ lit (name x) ∣ lit (string s) ⟧)
+
+  -- Generate a Haskell type synonym for the HsType of the given type
+  -- Usage `unquoteDecl = do hsTypeSynonym Foo; hsTypeSynonym Bar`
+  hsTypeAlias : Name → Term → TC ⊤
+  hsTypeAlias agdaName = makeTypeAlias agdaName emptyEnv
+
+  -- The only NameEnv that's useful here is `withName`.
+  hsTypeAlias_⊣_ : Name → NameEnv → Term → TC ⊤
+  hsTypeAlias agdaName ⊣ env = makeTypeAlias agdaName env
+
+  -- * Macros for constructing and deconstructing generated types
+
+  hsCon : Term → ℕ → Term → TC ⊤
+  hsCon agdaTy i hole = do
+    hsTy@(def hsName _) ← solveHsType agdaTy
+      where _ → typeErrorFmt "Failed to compute HsType of %t" agdaTy
+    cs ← getDefinition hsName >>= λ where
+      (data-type _ cs)  → return cs
+      _ → typeErrorFmt "Expected HsType %t to be a data type, but got %t" agdaTy hsTy
+    c ← maybe′ return  (typeErrorFmt "%q has only %u constructors" hsName (length cs)) (cs ‼ i)
+    unify hole (con c [])
+
+  hsProj : Term → ℕ → Term → TC ⊤
+  hsProj agdaTy i hole = do
+    hsTy@(def hsName _) ← solveHsType agdaTy
+      where _ → typeErrorFmt "Failed to compute HsType of %t" agdaTy
+    prjs ← getDefinition hsName >>= λ where
+      (data-type npars (c ∷ [])) → computeProjections npars c
+      _ → typeErrorFmt "Expected HsType %t to be a single constructor data type, but got %t" agdaTy hsTy
+    prj ← maybe′ return (typeErrorFmt "%q has only %u fields" hsName (length prjs)) (prjs ‼ i)
+    target ← newMeta `Set
+    checkType hole (pi (vArg hsTy) (abs "_" target))
+    unify hole prj
+
+  hsTyName : Term → Term → TC ⊤
+  hsTyName agdaTy hole = do
+    hsTy@(def hsName _) ← solveHsType agdaTy
+      where _ → typeErrorFmt "Failed to compute HsType of %t" agdaTy
+    unify hole (lit (name hsName))
diff --git a/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda b/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda
index d3cdb1b358..4b8622f60e 100644
--- a/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda
+++ b/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda
@@ -4,16 +4,14 @@
 -- TODO: The following should be likely located in Common.
 open import Ledger.Prelude
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 
 module InterfaceLibrary.Ledger
   (crypto : Crypto)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
   where
 
-open import Ledger.PParams crypto es ss using (PParams)
+open import Ledger.PParams using (PParams)
 open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr)
 
 \end{code}
diff --git a/docs/agda-spec/src/Ledger/PParams.lagda b/docs/agda-spec/src/Ledger/PParams.lagda
index 0667fb3b83..39cd3acd6b 100644
--- a/docs/agda-spec/src/Ledger/PParams.lagda
+++ b/docs/agda-spec/src/Ledger/PParams.lagda
@@ -1,59 +1,37 @@
 \section{Protocol Parameters}
 \label{sec:protocol-parameters}
-This section defines the adjustable protocol parameters of the Cardano ledger.
-These parameters are used in block validation and can affect various features of the system,
-such as minimum fees, maximum and minimum sizes of certain components, and more.
+This section defines the adjustable protocol parameters of the Cardano consensus.
+These parameters are used in block header validation and can affect various features
+of the system, such as maximum and minimum sizes of certain components, and more.
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
 
 open import Data.Product.Properties
 open import Data.Nat.Properties using (m+1+n≢m)
-open import Data.Rational using (ℚ)
-open import Relation.Nullary.Decidable
-open import Data.List.Relation.Unary.Any using (Any; here; there)
 
 open import Tactic.Derive.DecEq
 open import Tactic.Derive.Show
 
 open import Ledger.Prelude
-open import Ledger.Crypto
-open import Ledger.Script
-open import Ledger.Types.Epoch
 
-module Ledger.PParams
-  (crypto : Crypto )
-  (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  where
+module Ledger.PParams where
 
 private variable
   m n : ℕ
 \end{code}
 
-\begin{NoConway}
-The \AgdaRecord{Acnt} record has two fields, \AgdaField{treasury} and \AgdaField{reserves}, so
-the \AgdaBound{acnt} field in \AgdaRecord{NewEpochState} keeps track of the total assets that
-remain in treasury and reserves.
-
 \begin{figure*}[ht]
 \begin{AgdaMultiCode}
 \begin{code}
-record Acnt : Type where
-\end{code}
-\begin{code}[hide]
-  constructor ⟦_,_⟧ᵃ
-  field
-\end{code}
-\begin{code}
-    treasury reserves : Coin
-
 ProtVer : Type
 ProtVer = ℕ × ℕ
-
+\end{code}
+\begin{code}[hide]
 instance
   Show-ProtVer : Show ProtVer
   Show-ProtVer = Show-×
-
+\end{code}
+\begin{code}
 data pvCanFollow : ProtVer → ProtVer → Type where
   canFollowMajor : pvCanFollow (m , n) (m + 1 , 0)
   canFollowMinor : pvCanFollow (m , n) (m , n + 1)
@@ -62,34 +40,12 @@ data pvCanFollow : ProtVer → ProtVer → Type where
 \caption{Definitions related to protocol parameters}
 \label{fig:protocol-parameter-defs}
 \end{figure*}
-\end{NoConway}
 
 \begin{figure*}[ht]
 \begin{AgdaMultiCode}
 \begin{code}
 data PParamGroup : Type where
-  NetworkGroup     : PParamGroup
-  EconomicGroup    : PParamGroup
-  TechnicalGroup   : PParamGroup
-  GovernanceGroup  : PParamGroup
-  SecurityGroup    : PParamGroup
-
-record DrepThresholds : Type where
-\end{code}
-\begin{code}[hide]
-  field
-\end{code}
-\begin{code}
-    P1 P2a P2b P3 P4 P5a P5b P5c P5d P6 : ℚ
-
-record PoolThresholds : Type where
-\end{code}
-\begin{code}[hide]
-  field
-\end{code}
-\begin{code}
-    Q1 Q2a Q2b Q4 Q5e : ℚ
-
+  NetworkGroup : PParamGroup
 record PParams : Type where
 \end{code}
 \begin{code}[hide]
@@ -97,57 +53,9 @@ record PParams : Type where
 \end{code}
 \emph{Network group}
 \begin{code}
-        maxBlockSize                  : ℕ
-        maxTxSize                     : ℕ
-        maxHeaderSize                 : ℕ
-        maxTxExUnits                  : ExUnits
-        maxBlockExUnits               : ExUnits
-        maxValSize                    : ℕ
-        maxCollateralInputs           : ℕ
-\end{code}
-\begin{code}[hide]
-        pv                            : ProtVer -- retired, keep for now
-\end{code}
-\emph{Economic group}
-\begin{code}
-        a                             : ℕ
-        b                             : ℕ
-        keyDeposit                    : Coin
-        poolDeposit                   : Coin
-        coinsPerUTxOByte              : Coin
-        prices                        : Prices
-        minFeeRefScriptCoinsPerByte   : ℚ
-        maxRefScriptSizePerTx         : ℕ
-        maxRefScriptSizePerBlock      : ℕ
-        refScriptCostStride           : ℕ
-        refScriptCostMultiplier       : ℚ
-\end{code}
-\begin{code}[hide]
-        minUTxOValue                  : Coin -- retired, keep for now
-\end{code}
-\emph{Technical group}
-\begin{code}
-        Emax                          : Epoch
-        nopt                          : ℕ
-        a0                            : ℚ
-        collateralPercentage          : ℕ
-\end{code}
-\begin{code}[hide]
-        -- costmdls                   : Language →/⇀ CostModel (Does not work with DecEq)
-\end{code}
-\begin{code}
-        costmdls                      : CostModel
-\end{code}
-\emph{Governance group}
-\begin{code}
-        poolThresholds                : PoolThresholds
-        drepThresholds                : DrepThresholds
-        ccMinSize                     : ℕ
-        ccMaxTermLength               : ℕ
-        govActionLifetime             : ℕ
-        govActionDeposit              : Coin
-        drepDeposit                   : Coin
-        drepActivity                  : Epoch
+    maxHeaderSize : ℕ
+    maxBlockSize  : ℕ
+    pv            : ProtVer
 \end{code}
 \end{AgdaMultiCode}
 \caption{Protocol parameter definitions}
@@ -157,9 +65,7 @@ record PParams : Type where
 \begin{AgdaMultiCode}
 \begin{code}
 positivePParams : PParams → List ℕ
-positivePParams pp =  ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize ∷ refScriptCostStride
-                      ∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
-                      ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
+positivePParams pp = maxHeaderSize ∷ maxBlockSize ∷ []
 \end{code}
 \begin{code}[hide]
   where open PParams pp
@@ -174,9 +80,6 @@ paramsWF-elim : (pp : PParams) → paramsWellFormed pp → (n : ℕ) → n ∈ˡ
 paramsWF-elim pp pwf (suc n) x = z<s
 paramsWF-elim pp pwf 0 0∈ = ⊥-elim (pwf (to ∈-fromList 0∈))
   where open Equivalence
-
-refScriptCostStride>0 : (pp : PParams) → paramsWellFormed pp → (PParams.refScriptCostStride pp) > 0
-refScriptCostStride>0 pp pwf = paramsWF-elim pp pwf (PParams.refScriptCostStride pp) (there (there (there (there (here refl)))))
 \end{code}
 \end{AgdaMultiCode}
 \caption{Protocol parameter well-formedness}
@@ -186,229 +89,17 @@ refScriptCostStride>0 pp pwf = paramsWF-elim pp pwf (PParams.refScriptCostStride
 instance
   Show-ℚ = Show _ ∋ record {M}
     where import Data.Rational.Show as M
-  unquoteDecl DecEq-DrepThresholds = derive-DecEq
-    ((quote DrepThresholds , DecEq-DrepThresholds) ∷ [])
-  unquoteDecl DecEq-PoolThresholds = derive-DecEq
-    ((quote PoolThresholds , DecEq-PoolThresholds) ∷ [])
   unquoteDecl DecEq-PParams        = derive-DecEq
     ((quote PParams , DecEq-PParams) ∷ [])
-  unquoteDecl DecEq-PParamGroup    = derive-DecEq
-    ((quote PParamGroup , DecEq-PParamGroup) ∷ [])
-  unquoteDecl Show-DrepThresholds = derive-Show
-    ((quote DrepThresholds , Show-DrepThresholds) ∷ [])
-  unquoteDecl Show-PoolThresholds = derive-Show
-    ((quote PoolThresholds , Show-PoolThresholds) ∷ [])
   unquoteDecl Show-PParams        = derive-Show
     ((quote PParams , Show-PParams) ∷ [])
-
-module PParamsUpdate where
-  record PParamsUpdate : Type where
-    field
-          maxBlockSize maxTxSize        : Maybe ℕ
-          maxHeaderSize maxValSize      : Maybe ℕ
-          maxCollateralInputs           : Maybe ℕ
-          maxTxExUnits maxBlockExUnits  : Maybe ExUnits
-          pv                            : Maybe ProtVer -- retired, keep for now
-          a b                           : Maybe ℕ
-          keyDeposit                    : Maybe Coin
-          poolDeposit                   : Maybe Coin
-          coinsPerUTxOByte              : Maybe Coin
-          prices                        : Maybe Prices
-          minFeeRefScriptCoinsPerByte   : Maybe ℚ
-          maxRefScriptSizePerTx         : Maybe ℕ
-          maxRefScriptSizePerBlock      : Maybe ℕ
-          refScriptCostStride           : Maybe ℕ
-          refScriptCostMultiplier       : Maybe ℚ
-          minUTxOValue                  : Maybe Coin -- retired, keep for now
-          a0                            : Maybe ℚ
-          Emax                          : Maybe Epoch
-          nopt                          : Maybe ℕ
-          collateralPercentage          : Maybe ℕ
-          costmdls                      : Maybe CostModel
-          drepThresholds                : Maybe DrepThresholds
-          poolThresholds                : Maybe PoolThresholds
-          govActionLifetime             : Maybe ℕ
-          govActionDeposit drepDeposit  : Maybe Coin
-          drepActivity                  : Maybe Epoch
-          ccMinSize ccMaxTermLength     : Maybe ℕ
-  
-  paramsUpdateWellFormed : PParamsUpdate → Type
-  paramsUpdateWellFormed ppu =
-       just 0 ∉ fromList ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize
-                         ∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
-                         ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
-    where open PParamsUpdate ppu
-  
-  paramsUpdateWellFormed? : ( u : PParamsUpdate ) → Dec (paramsUpdateWellFormed u)
-  paramsUpdateWellFormed? u = ¿ paramsUpdateWellFormed u ¿
-  
-  modifiesNetworkGroup : PParamsUpdate → Bool
-  modifiesNetworkGroup ppu = let open PParamsUpdate ppu in
-    or
-      ( is-just maxBlockSize
-      ∷ is-just maxTxSize
-      ∷ is-just maxHeaderSize
-      ∷ is-just maxValSize
-      ∷ is-just maxCollateralInputs
-      ∷ is-just maxTxExUnits
-      ∷ is-just maxBlockExUnits
-      ∷ is-just pv
-      ∷ [])
-  
-  modifiesEconomicGroup : PParamsUpdate → Bool
-  modifiesEconomicGroup ppu = let open PParamsUpdate ppu in
-    or
-      ( is-just a
-      ∷ is-just b
-      ∷ is-just keyDeposit
-      ∷ is-just poolDeposit
-      ∷ is-just coinsPerUTxOByte
-      ∷ is-just minFeeRefScriptCoinsPerByte
-      ∷ is-just maxRefScriptSizePerTx
-      ∷ is-just maxRefScriptSizePerBlock
-      ∷ is-just refScriptCostStride
-      ∷ is-just refScriptCostMultiplier
-      ∷ is-just prices
-      ∷ is-just minUTxOValue
-      ∷ [])
-  
-  modifiesTechnicalGroup : PParamsUpdate → Bool
-  modifiesTechnicalGroup ppu = let open PParamsUpdate ppu in
-    or
-      ( is-just a0
-      ∷ is-just Emax
-      ∷ is-just nopt
-      ∷ is-just collateralPercentage
-      ∷ is-just costmdls
-      ∷ [])
-  
-  modifiesGovernanceGroup : PParamsUpdate → Bool
-  modifiesGovernanceGroup ppu = let open PParamsUpdate ppu in
-    or
-      ( is-just drepThresholds
-      ∷ is-just poolThresholds
-      ∷ is-just govActionLifetime
-      ∷ is-just govActionDeposit
-      ∷ is-just drepDeposit
-      ∷ is-just drepActivity
-      ∷ is-just ccMinSize
-      ∷ is-just ccMaxTermLength
-      ∷ [])
-  
-  modifiedUpdateGroups : PParamsUpdate → ℙ PParamGroup
-  modifiedUpdateGroups ppu =
-    ( modifiesNetworkGroup    ?═⇒ NetworkGroup
-    ∪ modifiesEconomicGroup   ?═⇒ EconomicGroup
-    ∪ modifiesTechnicalGroup  ?═⇒ TechnicalGroup
-    ∪ modifiesGovernanceGroup ?═⇒ GovernanceGroup
-    )
-    where
-      _?═⇒_ : (PParamsUpdate → Bool) → PParamGroup → ℙ PParamGroup
-      pred ?═⇒ grp = if pred ppu then ❴ grp ❵ else ∅
-  
-  _?↗_ : ∀ {A : Type} → Maybe A → A → A
-  just x ?↗ _ = x
-  nothing ?↗ x = x
-  
-  ≡-update : ∀ {A : Type} {u : Maybe A} {p : A} {x : A} → u ?↗ p ≡ x ⇔ (u ≡ just x ⊎ (p ≡ x × u ≡ nothing))
-  ≡-update {u} {p} {x} = mk⇔ to from
-    where
-      to : ∀ {A} {u : Maybe A} {p : A} {x : A} → u ?↗ p ≡ x → (u ≡ just x ⊎ (p ≡ x × u ≡ nothing))
-      to {u = just x} refl = inj₁ refl
-      to {u = nothing} refl = inj₂ (refl , refl)
-  
-      from : ∀ {A} {u : Maybe A} {p : A} {x : A} → u ≡ just x ⊎ (p ≡ x × u ≡ nothing) → u ?↗ p ≡ x
-      from (inj₁ refl) = refl
-      from (inj₂ (refl , refl)) = refl
-  
-  applyPParamsUpdate : PParams → PParamsUpdate → PParams
-  applyPParamsUpdate pp ppu =
-    record
-      { maxBlockSize                = U.maxBlockSize ?↗ P.maxBlockSize
-      ; maxTxSize                   = U.maxTxSize ?↗ P.maxTxSize
-      ; maxHeaderSize               = U.maxHeaderSize ?↗ P.maxHeaderSize
-      ; maxValSize                  = U.maxValSize ?↗ P.maxValSize
-      ; maxCollateralInputs         = U.maxCollateralInputs ?↗ P.maxCollateralInputs
-      ; maxTxExUnits                = U.maxTxExUnits ?↗ P.maxTxExUnits
-      ; maxBlockExUnits             = U.maxBlockExUnits ?↗ P.maxBlockExUnits
-      ; pv                          = U.pv ?↗ P.pv
-      ; a                           = U.a ?↗ P.a
-      ; b                           = U.b ?↗ P.b
-      ; keyDeposit                  = U.keyDeposit ?↗ P.keyDeposit
-      ; poolDeposit                 = U.poolDeposit ?↗ P.poolDeposit
-      ; coinsPerUTxOByte            = U.coinsPerUTxOByte ?↗ P.coinsPerUTxOByte
-      ; minFeeRefScriptCoinsPerByte = U.minFeeRefScriptCoinsPerByte ?↗ P.minFeeRefScriptCoinsPerByte
-      ; maxRefScriptSizePerTx       = U.maxRefScriptSizePerTx ?↗ P.maxRefScriptSizePerTx
-      ; maxRefScriptSizePerBlock    = U.maxRefScriptSizePerBlock ?↗ P.maxRefScriptSizePerBlock
-      ; refScriptCostStride         = U.refScriptCostStride ?↗ P.refScriptCostStride
-      ; refScriptCostMultiplier     = U.refScriptCostMultiplier ?↗ P.refScriptCostMultiplier
-      ; prices                      = U.prices ?↗ P.prices
-      ; minUTxOValue                = U.minUTxOValue ?↗ P.minUTxOValue
-      ; a0                          = U.a0 ?↗ P.a0
-      ; Emax                        = U.Emax ?↗ P.Emax
-      ; nopt                        = U.nopt ?↗ P.nopt
-      ; collateralPercentage        = U.collateralPercentage ?↗ P.collateralPercentage
-      ; costmdls                    = U.costmdls ?↗ P.costmdls
-      ; drepThresholds              = U.drepThresholds ?↗ P.drepThresholds
-      ; poolThresholds              = U.poolThresholds ?↗ P.poolThresholds
-      ; govActionLifetime           = U.govActionLifetime ?↗ P.govActionLifetime
-      ; govActionDeposit            = U.govActionDeposit ?↗ P.govActionDeposit
-      ; drepDeposit                 = U.drepDeposit ?↗ P.drepDeposit
-      ; drepActivity                = U.drepActivity ?↗ P.drepActivity
-      ; ccMinSize                   = U.ccMinSize ?↗ P.ccMinSize
-      ; ccMaxTermLength             = U.ccMaxTermLength ?↗ P.ccMaxTermLength
-      }
-    where
-      open module P = PParams pp
-      open module U = PParamsUpdate ppu
-
-  instance
-    unquoteDecl DecEq-PParamsUpdate  = derive-DecEq
-      ((quote PParamsUpdate , DecEq-PParamsUpdate) ∷ [])
 \end{code}
-% Retiring ProtVer's documentation since ProtVer is retired.
-% \ProtVer represents the protocol version used in the Cardano ledger.
-% It is a pair of natural numbers, representing the major and minor version,
-% respectively.
 
-\PParams contains parameters used in the Cardano ledger, which we group according
+\PParams contains parameters used in the Cardano consensus, which we group according
 to the general purpose that each parameter serves.
-\begin{itemize}
-  \item \NetworkGroup: parameters related to the network settings;
-  \item \EconomicGroup: parameters related to the economic aspects of the ledger;
-  \item \TechnicalGroup: parameters related to technical settings;
-  \item \GovernanceGroup: parameters related to governance settings;
-  \item \SecurityGroup: parameters that can impact the security of the system.
-\end{itemize}
-
-The first four groups have the property that every protocol parameter
-is associated to precisely one of these groups. The \SecurityGroup is
-special: a protocol parameter may or may not be in the
-\SecurityGroup. So, each protocol parameter belongs to at least one
-and at most two groups. Note that in \cite{cip1694} there is no
-\SecurityGroup, but there is the concept of security-relevant protocol
-parameters. The difference between these notions is only social, so we
-implement security-relevant protocol parameters as a group.
-
-The purpose of the groups is to determine voting thresholds for
-proposals aiming to change parameters. The thresholds depend on the
-groups of the parameters contained in such a proposal.
-
-These new parameters are declared in
-Figure~\ref{fig:protocol-parameter-declarations} and denote the
-following concepts.
 
 \begin{itemize}
-  \item \drepThresholds: governance thresholds for \DReps; these are rational numbers
-  named \Pone, \Ptwoa, \Ptwob, \Pthree, \Pfour, \Pfivea, \Pfiveb, \Pfivec, \Pfived, and \Psix;
-  \item \poolThresholds: pool-related governance thresholds; these are rational numbers named \Qone, \Qtwoa, \Qtwob, \Qfour and \Qfivee;
-  \item \ccMinSize: minimum constitutional committee size;
-  \item \ccMaxTermLength: maximum term limit (in epochs) of constitutional committee members;
-  \item \govActionLifetime: governance action expiration;
-  \item \govActionDeposit: governance action deposit;
-  \item \drepDeposit: \DRep deposit amount;
-  \item \drepActivity: \DRep activity period;
-  \item \minimumAVS: the minimum active voting threshold.
+  \item \NetworkGroup: parameters related to the network settings;
 \end{itemize}
 
 Figure~\ref{fig:protocol-parameter-declarations} also defines the
@@ -425,45 +116,3 @@ instance
   ... | yes refl | no ¬p    = yes canFollowMajor
   ... | yes refl | yes p    = ⊥-elim $ m+1+n≢m m $ ×-≡,≡←≡ p .proj₁
 \end{code}
-
-Finally, to update parameters we introduce an abstract type. An update
-can be applied and it has a set of groups associated with it. An
-update is well formed if it has at least one group (i.e. if it updates
-something) and if it preserves well-formedness.
-
-\begin{figure*}[ht]
-\begin{AgdaMultiCode}
-\begin{code}[hide]
-record PParamsDiff : Type₁ where
-  field
-\end{code}
-\emph{Abstract types \& functions}
-\begin{code}
-    UpdateT : Type
-    applyUpdate : PParams → UpdateT → PParams
-    updateGroups : UpdateT → ℙ PParamGroup
-
-\end{code}
-\begin{code}[hide]
-    ⦃ ppWF? ⦄ : ∀ {u} → (∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)) ⁇
-\end{code}
-\emph{Well-formedness condition}
-\begin{code}
-
-  ppdWellFormed : UpdateT → Type
-  ppdWellFormed u = updateGroups u ≢ ∅
-    × ∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)
-\end{code}
-\end{AgdaMultiCode}
-\caption{Abstract type for parameter updates}
-\label{fig:pp-update-type}
-\end{figure*}
-\begin{code}[hide]
-record GovParams : Type₁ where
-  field ppUpd : PParamsDiff
-  open PParamsDiff ppUpd renaming (UpdateT to PParamsUpdate) public
-  field ppHashingScheme : isHashableSet PParams
-  open isHashableSet ppHashingScheme renaming (THash to PPHash) public
-  field ⦃ DecEq-UpdT ⦄ : DecEq PParamsUpdate
---         ⦃ Show-UpdT ⦄ : Show PParamsUpdate
-\end{code}
diff --git a/docs/agda-spec/src/Ledger/Script.lagda b/docs/agda-spec/src/Ledger/Script.lagda
deleted file mode 100644
index b82be2f127..0000000000
--- a/docs/agda-spec/src/Ledger/Script.lagda
+++ /dev/null
@@ -1,184 +0,0 @@
-\section{Scripts}
-\begin{code}[hide]
-{-# OPTIONS --safe #-}
-
-open import Algebra using (CommutativeMonoid)
-open import Algebra.Morphism
-open import Data.List.Relation.Unary.All using (All; []; _∷_; all?; uncons)
-open import Data.List.Relation.Unary.Any
-open import Data.Nat.Properties using (+-0-commutativeMonoid; suc-injective)
-
-open import Data.List.Relation.Unary.MOf
-
-open import Tactic.Derive.DecEq
-open import Tactic.Inline
-
-open import Ledger.Prelude hiding (All; Any; all?; any?; _∷ʳ_; uncons; _⊆_)
-open import Ledger.Crypto
-open import Ledger.Types.Epoch
-
-module Ledger.Script
-  (crypto : _) (open Crypto crypto)
-  (es     : _) (open EpochStructure es)
-  where
-
-record P1ScriptStructure : Type₁ where
-  field P1Script : Type
-        validP1Script : ℙ KeyHashˢ → Maybe Slot × Maybe Slot → P1Script → Type
-        ⦃ Dec-validP1Script ⦄ : validP1Script ⁇³
-        ⦃ Hashable-P1Script ⦄ : Hashable P1Script ScriptHash
-        ⦃ DecEq-P1Script    ⦄ : DecEq P1Script
-
-record PlutusStructure : Type₁ where
-  field Dataʰ : HashableSet
-        Language PlutusScript CostModel Prices LangDepView ExUnits : Type
-        PlutusV1 PlutusV2 PlutusV3   : Language
-        ⦃ ExUnit-CommutativeMonoid ⦄ : IsCommutativeMonoid' 0ℓ 0ℓ ExUnits
-        ⦃ Hashable-PlutusScript    ⦄ : Hashable PlutusScript ScriptHash
-        ⦃ DecEq-Language           ⦄ : DecEq Language
-        ⦃ DecEq-CostModel          ⦄ : DecEq CostModel
-        ⦃ DecEq-LangDepView        ⦄ : DecEq LangDepView
-        ⦃ Show-CostModel           ⦄ : Show CostModel
-
-  field  _≥ᵉ_              : ExUnits → ExUnits → Type
-         ⦃ DecEq-ExUnits ⦄ : DecEq ExUnits
-         ⦃ DecEQ-Prices  ⦄ : DecEq Prices
-         ⦃ Show-ExUnits  ⦄ : Show ExUnits
-         ⦃ Show-Prices   ⦄ : Show Prices
-
-  open HashableSet Dataʰ renaming (T to Data; THash to DataHash) public
-
-  -- Type aliases for Data
-  Datum    = Data
-  Redeemer = Data
-
-  field validPlutusScript : CostModel → List Data → ExUnits → PlutusScript → Type
-        ⦃ Dec-validPlutusScript ⦄ : ∀ {x} → (validPlutusScript x ⁇³)
-        language : PlutusScript → Language
-        toData : ∀ {A : Type} → A → Data
-\end{code}
-We define \Timelock scripts here. They can verify the presence of keys and whether a transaction happens in a certain slot interval. These scripts are executed as part of the regular witnessing.
-\begin{figure*}[h]
-\begin{code}
-data Timelock : Type where
-  RequireAllOf       : List Timelock      → Timelock
-  RequireAnyOf       : List Timelock      → Timelock
-  RequireMOf         : ℕ → List Timelock  → Timelock
-  RequireSig         : KeyHashˢ           → Timelock
-  RequireTimeStart   : Slot               → Timelock
-  RequireTimeExpire  : Slot               → Timelock
-\end{code}
-\begin{code}[hide]
-unquoteDecl DecEq-Timelock = derive-DecEq ((quote Timelock , DecEq-Timelock) ∷ [])
-
-private variable
-  s : Timelock
-  ss ss' : List Timelock
-  m : ℕ
-  x : KeyHashˢ
-  a l r : Slot
-
-open import Data.List.Relation.Binary.Sublist.Ext
-open import Data.List.Relation.Binary.Sublist.Propositional as S
-import Data.Maybe.Relation.Unary.Any as M
-\end{code}
-\begin{code}[hide]
-data
-\end{code}
-\begin{code}
-  evalTimelock (khs : ℙ KeyHashˢ) (I : Maybe Slot × Maybe Slot) : Timelock → Type where
-  evalAll  : All (evalTimelock khs I) ss
-           → (evalTimelock khs I) (RequireAllOf ss)
-  evalAny  : Any (evalTimelock khs I) ss
-           → (evalTimelock khs I) (RequireAnyOf ss)
-  evalMOf  : MOf m (evalTimelock khs I) ss
-           → (evalTimelock khs I) (RequireMOf m ss)
-  evalSig  : x ∈ khs
-           → (evalTimelock khs I) (RequireSig x)
-  evalTSt  : M.Any (a ≤_) (I .proj₁)
-           → (evalTimelock khs I) (RequireTimeStart a)
-  evalTEx  : M.Any (_≤ a) (I .proj₂)
-           → (evalTimelock khs I) (RequireTimeExpire a)
-\end{code}
-\caption{Timelock scripts and their evaluation}
-\label{fig:defs:timelock}
-\end{figure*}
-
-\begin{code}[hide]
-instance
-  Dec-evalTimelock : evalTimelock ⁇³
-  Dec-evalTimelock {khs} {I} {tl} .dec = go? tl
-    where mutual
-      go = evalTimelock khs I
-
-      -- ** inversion principles for `evalTimelock`
-      evalAll˘ : ∀ {ss} → go (RequireAllOf ss) → All go ss
-      evalAll˘ (evalAll p) = p
-
-      evalAny˘ : ∀ {ss} → go (RequireAnyOf ss) → Any go ss
-      evalAny˘ (evalAny p) = p
-
-      evalTSt˘ : go (RequireTimeStart a) → M.Any (a ≤_) (I .proj₁)
-      evalTSt˘ (evalTSt p) = p
-
-      evalTEx˘ : go (RequireTimeExpire a) → M.Any (_≤ a) (I .proj₂)
-      evalTEx˘ (evalTEx p) = p
-
-      evalSig˘ : go (RequireSig x) → x ∈ khs
-      evalSig˘ (evalSig p) = p
-
-      evalMOf˘ : ∀ {m xs}
-        → go (RequireMOf m xs)
-        → MOf m go xs
-      evalMOf˘ (evalMOf p) = p
-
-      -- ** inlining recursive decision procedures to please the termination checker
-      MOf-go? : ∀ m xs → Dec (MOf m go xs)
-      unquoteDef MOf-go? = inline MOf-go? (quoteTerm (MOf? go?))
-
-      all-go? : Decidable¹ (All go)
-      unquoteDef all-go? = inline all-go? (quoteTerm (all? go?))
-
-      any-go? : Decidable¹ (Any go)
-      unquoteDef any-go? = inline any-go? (quoteTerm (any? go?))
-
-      -- ** the actual decision procedure
-      go? : Decidable¹ go
-      go? = λ where
-        (RequireAllOf ss)     → mapDec evalAll evalAll˘ (all-go? ss)
-        (RequireAnyOf ss)     → mapDec evalAny evalAny˘ (any-go? ss)
-        (RequireSig x)        → mapDec evalSig evalSig˘ dec
-        (RequireTimeStart a)  → mapDec evalTSt evalTSt˘ dec
-        (RequireTimeExpire a) → mapDec evalTEx evalTEx˘ dec
-        (RequireMOf m xs)     → mapDec evalMOf evalMOf˘ (MOf-go? m xs)
-
-P1ScriptStructure-TL : ⦃ Hashable Timelock ScriptHash ⦄ → P1ScriptStructure
-P1ScriptStructure-TL = record
-  { P1Script = Timelock
-  ; validP1Script = evalTimelock }
-
-record ScriptStructure : Type₁ where
-  field hashRespectsUnion :
-          {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash
-        ⦃ Hash-Timelock ⦄ : Hashable Timelock ScriptHash
-
-  p1s : P1ScriptStructure
-  p1s = P1ScriptStructure-TL
-  open P1ScriptStructure p1s public
-
-  field ps : PlutusStructure
-  open PlutusStructure ps public
-    renaming ( PlutusScript       to P2Script
-             ; validPlutusScript  to validP2Script
-             )
-
-  Script = P1Script ⊎ P2Script
-
-  open import Data.Empty
-  open import Agda.Builtin.Equality
-  open import Relation.Binary.PropositionalEquality
-
-  instance
-    Hashable-Script : Hashable Script ScriptHash
-    Hashable-Script = hashRespectsUnion Hashable-P1Script Hashable-PlutusScript
-\end{code}
diff --git a/docs/agda-spec/src/Makefile b/docs/agda-spec/src/Makefile
index 2de9935429..d2fe72f313 100644
--- a/docs/agda-spec/src/Makefile
+++ b/docs/agda-spec/src/Makefile
@@ -1,3 +1,4 @@
+# Constants
 PDF_NAME=consensus-spec
 AGDA?=agda
 AGDA_RUN=$(AGDA) --transliterate
@@ -9,14 +10,18 @@ PRE=$(addprefix $(LATEX_DIR)/,\
 PDF_DIR=$(OUT_DIR)/pdfs
 LIB_NAME=Ledger
 INTERFACE_LIB_NAME=InterfaceLibrary
+HS_DIR=$(OUT_DIR)/haskell
+MALONZO_DIR=MAlonzo/Code
+CABAL_TEST=cabal run test
 
 # Agda -> LaTeX -> PDF
 latexFiles=$(patsubst %.lagda, $(LATEX_DIR)/%.tex,\
              $(shell find . -name '*.lagda' | sed 's|\.\/||g'))
 $(latexFiles): $(LATEX_DIR)/%.tex: %.lagda
 	@echo "Compiling $<"
-	$(AGDA_RUN) --latex --latex-dir=$(LATEX_DIR) $< # --only-scope-checking
-define latexToPdf =
+	$(AGDA_RUN) --latex --latex-dir=$(LATEX_DIR) $<
+
+define latexToPdf
     @echo "Generating $@"
     $(eval PDF=$(notdir $@))
     mkdir -p $(dir $@)
@@ -27,8 +32,34 @@ endef
 $(PDF_DIR)/$(PDF_NAME).pdf: $(LATEX_DIR)/Spec/PDF.tex $(latexFiles) $(PRE)
 	$(latexToPdf)
 
+# Agda -> Haskell
+define agdaToHs
+    @echo "Generating $@"
+    $(eval CABAL_FILE=$(1).cabal)
+    $(eval HS_DIST=$(HS_DIR)/Spec)
+    mkdir -p $(HS_DIST)
+    cp -r Spec/hs-src/* $(HS_DIST)/
+    cp Spec/hs-src/$(CABAL_FILE) $(HS_DIST)/
+    $(AGDA_RUN) -c --ghc-dont-call-ghc --compile-dir $(HS_DIST) $<
+    find $(HS_DIST)/MAlonzo -name "*.hs" -print\
+      | sed "s#^$(HS_DIST)/#        #;s#\.hs##;s#/#.#g"\
+      >> $(HS_DIST)/$(CABAL_FILE)
+endef
+HS_CONSENSUS=$(HS_DIR)/Consensus/$(MALONZO_DIR)/Spec/Foreign/HSConsensus.hs
+$(HS_CONSENSUS): Spec/Foreign/HSConsensus.agda
+	$(call agdaToHs,cardano-consensus-executable-spec)
+
 # User commands
-.PHONY: default clean docs
+.PHONY: default clean docs hs hsTest
+
+consensus.hs: $(HS_CONSENSUS)
+
+hs: consensus.hs
+
+consensus.hsTest: $(HS_CONSENSUS)
+	cd $(HS_DIR)/Spec && $(CABAL_TEST)
+
+hsTest: consensus.hsTest
 
 docs: $(PDF_DIR)/$(PDF_NAME).pdf
 
diff --git a/docs/agda-spec/src/Spec/BaseTypes.lagda b/docs/agda-spec/src/Spec/BaseTypes.lagda
index 5049a61c8e..38e5c06045 100644
--- a/docs/agda-spec/src/Spec/BaseTypes.lagda
+++ b/docs/agda-spec/src/Spec/BaseTypes.lagda
@@ -22,4 +22,7 @@ open import Data.Nat using (ℕ)
 OCertCounters : Type
 OCertCounters = KeyHashˢ ⇀ ℕ
 
+Slot   = ℕ
+Epoch  = ℕ
+
 \end{code}
diff --git a/docs/agda-spec/src/Spec/BlockDefinitions.lagda b/docs/agda-spec/src/Spec/BlockDefinitions.lagda
index 0a728a4830..b94acc3a0b 100644
--- a/docs/agda-spec/src/Spec/BlockDefinitions.lagda
+++ b/docs/agda-spec/src/Spec/BlockDefinitions.lagda
@@ -7,17 +7,15 @@
 open import Spec.BaseTypes using (Nonces)
 open import Ledger.Prelude
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 
 module Spec.BlockDefinitions
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)  
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)  
   where
 
-open import Ledger.PParams crypto es ss using (ProtVer)
+open import Ledger.PParams using (ProtVer)
 
 record BlockStructure : Type₁ where
   field
diff --git a/docs/agda-spec/src/Spec/ChainHead.lagda b/docs/agda-spec/src/Spec/ChainHead.lagda
index f1adba653a..18c8d18887 100644
--- a/docs/agda-spec/src/Spec/ChainHead.lagda
+++ b/docs/agda-spec/src/Spec/ChainHead.lagda
@@ -27,7 +27,6 @@ open import InterfaceLibrary.Ledger
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Data.Rational.Ext
 
@@ -35,18 +34,17 @@ module Spec.ChainHead
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)  
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
-  (li     : LedgerInterface crypto es ss) (let open LedgerInterface li)
+  (li     : LedgerInterface crypto es) (let open LedgerInterface li)
   (rs     : _) (open RationalExtStructure rs)  
   where
 
 open import Spec.BaseTypes crypto using (OCertCounters)
-open import Spec.TickForecast crypto es ss li
+open import Spec.TickForecast crypto es li
 open import Spec.TickNonce crypto es nonces
-open import Spec.Protocol crypto nonces es ss bs af rs
-open import Ledger.PParams crypto es ss using (PParams; ProtVer)
+open import Spec.Protocol crypto nonces es bs af rs
+open import Ledger.PParams using (PParams; ProtVer)
 open import Ledger.Prelude
 
 \end{code}
diff --git a/docs/agda-spec/src/Spec/ChainHead/Properties.agda b/docs/agda-spec/src/Spec/ChainHead/Properties.agda
index af6b1d58cb..13fe48fad7 100644
--- a/docs/agda-spec/src/Spec/ChainHead/Properties.agda
+++ b/docs/agda-spec/src/Spec/ChainHead/Properties.agda
@@ -4,7 +4,6 @@ open import InterfaceLibrary.Ledger
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Data.Rational.Ext
 
@@ -12,23 +11,22 @@ module Spec.ChainHead.Properties
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
-  (li     : LedgerInterface crypto es ss) (let open LedgerInterface li)
+  (li     : LedgerInterface crypto es) (let open LedgerInterface li)
   (rs     : _) (open RationalExtStructure rs)
   where
 
 open import Tactic.GenError
 open import Ledger.Prelude
-open import Ledger.PParams crypto es ss using (PParams; ProtVer)
-open import Spec.TickForecast crypto es ss li
-open import Spec.TickForecast.Properties crypto es ss li
+open import Ledger.PParams using (PParams; ProtVer)
+open import Spec.TickForecast crypto es li
+open import Spec.TickForecast.Properties crypto es li
 open import Spec.TickNonce crypto es nonces
 open import Spec.TickNonce.Properties crypto es nonces
-open import Spec.Protocol crypto nonces es ss bs af rs
-open import Spec.Protocol.Properties crypto nonces es ss bs af rs
-open import Spec.ChainHead crypto nonces es ss bs af li rs
+open import Spec.Protocol crypto nonces es bs af rs
+open import Spec.Protocol.Properties crypto nonces es bs af rs
+open import Spec.ChainHead crypto nonces es bs af li rs
 
 instance
 
diff --git a/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda b/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda
new file mode 100644
index 0000000000..542d2ee5c9
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/ExternalFunctions.agda
@@ -0,0 +1,15 @@
+module Spec.Foreign.ExternalFunctions where -- TODO: Complete
+
+open import Ledger.Prelude
+open import Foreign.HaskellTypes.Deriving
+
+record ExternalFunctions : Set where
+  field extDummy : ℕ → Bool
+{-# FOREIGN GHC
+  data ExternalFunctions = MkExternalFunctions { extDummy :: Integer -> Bool }
+#-}
+{-# COMPILE GHC ExternalFunctions = data ExternalFunctions (MkExternalFunctions) #-}
+
+dummyExternalFunctions : ExternalFunctions
+dummyExternalFunctions = record { extDummy = λ x → true }
+{-# COMPILE GHC dummyExternalFunctions as dummyExternalFunctions #-}
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus.agda
new file mode 100644
index 0000000000..a5fa43ee47
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus.agda
@@ -0,0 +1,4 @@
+module Spec.Foreign.HSConsensus where
+
+open import Spec.Foreign.HSConsensus.TickNonce public
+open import Spec.Foreign.HSConsensus.UpdateNonce public
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda
new file mode 100644
index 0000000000..ee74196cbe
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/BaseTypes.agda
@@ -0,0 +1,77 @@
+module Spec.Foreign.HSConsensus.BaseTypes where
+
+open import Data.Rational
+
+open import Spec.Foreign.ExternalFunctions
+open import Spec.Foreign.HSConsensus.Core public
+import Spec.Foreign.HSTypes as F
+
+instance
+  iConvTop    = Convertible-Refl {⊤}
+  iConvNat    = Convertible-Refl {ℕ}
+  iConvString = Convertible-Refl {String}
+  iConvBool   = Convertible-Refl {Bool}
+
+instance -- TODO: Complete
+
+  -- * Unit and empty
+
+  HsTy-⊥ = MkHsType ⊥ F.Empty
+  Conv-⊥ = autoConvert ⊥
+
+  HsTy-⊤ = MkHsType ⊤ ⊤
+
+  -- * Rational numbers
+
+  HsTy-Rational = MkHsType ℚ F.Rational
+  Conv-Rational : HsConvertible ℚ
+  Conv-Rational = λ where
+    .to (mkℚ n d _)       → n F., suc d
+    .from (n F., zero)    → 0ℚ -- TODO is there a safer way to do this?
+    .from (n F., (suc d)) → n Data.Rational./ suc d
+
+  -- * Maps and Sets
+
+  HsTy-HSSet : ∀ {A} → ⦃ HasHsType A ⦄ → HasHsType (ℙ A)
+  HsTy-HSSet {A} = MkHsType _ (F.HSSet (HsType A))
+
+  Conv-HSSet : ∀ {A} ⦃ _ : HasHsType A ⦄
+             → ⦃ HsConvertible A ⦄
+             → HsConvertible (ℙ A)
+  Conv-HSSet = λ where
+    .to → F.MkHSSet ∘ to ∘ setToList
+    .from → fromListˢ ∘ from ∘ F.HSSet.elems
+
+  HsTy-Map : ∀ {A B} → ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⇀ B)
+  HsTy-Map {A} {B} = MkHsType _ (F.HSMap (HsType A) (HsType B))
+
+  Conv-HSMap : ∀ {A B} ⦃ _ : HasHsType A ⦄ ⦃ _ : HasHsType B ⦄
+    → ⦃ DecEq A ⦄
+    → ⦃ HsConvertible A ⦄
+    → ⦃ HsConvertible B ⦄
+    → HsConvertible (A ⇀ B)
+  Conv-HSMap = λ where
+    .to → F.MkHSMap ∘ to
+    .from → from ∘ F.HSMap.assocList
+
+  -- * ComputationResult
+
+  HsTy-ComputationResult : ∀ {l} {Err} {A : Type l}
+                           → ⦃ HasHsType Err ⦄ → ⦃ HasHsType A ⦄
+                           → HasHsType (ComputationResult Err A)
+  HsTy-ComputationResult {Err = Err} {A} = MkHsType _ (F.ComputationResult (HsType Err) (HsType A))
+
+  Conv-ComputationResult : ConvertibleType ComputationResult F.ComputationResult
+  Conv-ComputationResult = autoConvertible
+
+open import Spec.Foreign.HSConsensus.ExternalStructures dummyExternalFunctions
+  renaming
+    ( HSEpochStructure to DummyEpochStructure
+    ; HSCrypto to DummyCrypto
+    ; HSNonces to DummyNonces
+    )
+  public
+
+unquoteDecl = do
+  hsTypeAlias Slot
+  hsTypeAlias Epoch
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda
new file mode 100644
index 0000000000..5ba0e6a3f2
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/Core.agda
@@ -0,0 +1,55 @@
+open import Spec.Foreign.ExternalFunctions
+
+module Spec.Foreign.HSConsensus.Core where
+
+open import Ledger.Prelude hiding (ε) renaming (fromList to fromListˢ) public
+open Computational public
+
+open import Foreign.Convertible           public
+open import Foreign.Convertible.Deriving  public
+open import Foreign.HaskellTypes          public
+open import Foreign.HaskellTypes.Deriving public
+
+open import Ledger.Crypto
+
+open import Spec.Foreign.Util public
+
+open import Data.Rational using (1ℚ; ½; Positive; positive; _<_) renaming (_≤_ to _≤ℚ_)
+open import Data.Rational.Ext using (PosUnitInterval)
+open import Data.Integer using (_≤_; _<_)
+
+½-positive : Positive ½
+½-positive = positive {½} (_<_.*<* (_<_.+<+ (s≤s z≤n)))
+
+½≤1 : ½ ≤ℚ 1ℚ
+½≤1 = _≤ℚ_.*≤* (_≤_.+≤+ (s≤s z≤n))
+
+module _ {A : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance
+  ∀Hashable : Hashable A A
+  ∀Hashable = λ where .hash → id
+
+  ∀isHashableSet : isHashableSet A
+  ∀isHashableSet = mkIsHashableSet A
+
+instance
+  Hashable-⊤ : Hashable ⊤ ℕ
+  Hashable-⊤ = λ where .hash tt → 0
+
+module Implementation where
+  -- Global constants
+  Network                        = ℕ
+  SlotsPerEpochᶜ                 = 100
+  StabilityWindowᶜ               = 10
+  RandomnessStabilisationWindowᶜ = 20
+  Quorum                         = 1
+  NetworkId                      = 0
+  SlotsPerKESPeriodᶜ             = 5
+  MaxKESEvoᶜ                     = 30
+  ActiveSlotCoeffᶜ : PosUnitInterval
+  ActiveSlotCoeffᶜ               = ½ , ½-positive , ½≤1
+  MaxMajorPVᶜ                    = 1
+
+  -- VRFs and nonces
+  Seed = ℕ
+
+module ExternalStructures (externalFunctions : ExternalFunctions) where
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda
new file mode 100644
index 0000000000..2811f2b63e
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/ExternalStructures.agda
@@ -0,0 +1,88 @@
+open import Spec.Foreign.ExternalFunctions
+
+module Spec.Foreign.HSConsensus.ExternalStructures (externalFunctions : ExternalFunctions) where
+
+open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length)
+open import Ledger.Crypto
+open import Ledger.Types.Epoch
+open import Spec.Foreign.HSConsensus.Core
+
+HSGlobalConstants = GlobalConstants ∋ record {Implementation}
+instance
+  HSEpochStructure = EpochStructure ∋ ℕEpochStructure HSGlobalConstants
+
+  -- NOTE: Dummy for now.
+  HSSerializer : Serializer
+  HSSerializer = record
+    { Ser             = String
+    ; encode          = const ""
+    ; decode          = const nothing
+    ; _∥_             = _+ˢ_
+    ; enc-dec-correct = error "enc-dec-correct evaluated"
+    }
+
+  -- NOTE: Dummy for now.
+  HSPKScheme : PKScheme
+  HSPKScheme = record
+    { SKey      = ℕ
+    ; VKey      = ℕ
+    ; isKeyPair = _≡_
+    }
+
+  -- Note: Dummy for now.
+  HSDSigScheme : DSigScheme HSSerializer
+  HSDSigScheme = record
+    { pks              = HSPKScheme
+    ; isSigned         = λ _ _ _ → ⊤
+    ; sign             = λ _ _ → 0
+    ; isSigned-correct = error "isSigned-correct evaluated"
+    ; Dec-isSigned     = λ {_} {_} {_} → ⁇ (true because ofʸ tt)
+    }
+
+  -- NOTE: Dummy for now.
+  HSKESScheme : KESScheme HSSerializer
+  HSKESScheme = record
+    { pks              = HSPKScheme
+    ; Sig              = ℕ
+    ; isSigned         = λ _ _ _ _ → ⊤
+    ; sign             = λ _ _ _ → 0
+    ; isSigned-correct = error "isSigned-correct evaluated"
+    ; Dec-isSigned     = λ {_} {_} {_} {_} → ⁇ (true because ofʸ tt)
+    }
+
+  -- NOTE: Dummy for now.
+  HSVRFScheme : VRFScheme
+  HSVRFScheme = record
+    { Implementation
+    ; pks            = HSPKScheme
+    ; Proof          = ℕ
+    ; verify         = λ _ _ _ → ⊤
+    ; evaluate       = error "evaluate evaluated"
+    ; _XOR_          = _+_
+    ; verify-correct = error "verify-correct evaluated"
+    ; Dec-verify     = λ {T = _} {_} {_} {_} → ⁇ (true because ofʸ tt)
+    }
+
+  HSCrypto : Crypto
+  HSCrypto = record
+    { srl        = HSSerializer
+    ; dsig       = HSDSigScheme
+    ; kes        = HSKESScheme
+    ; vrf        = HSVRFScheme
+    ; ScriptHash = ℕ
+    }
+
+  open import Spec.BaseTypes HSCrypto
+
+  -- NOTE: Dummy for now.
+  HSNonces : Nonces
+  HSNonces = record
+    { Implementation
+    ; Nonce       = ℕ
+    ; _⋆_         = _+_
+    ; nonceToSeed = id
+    }
+
+  open EpochStructure HSEpochStructure public
+  open Crypto HSCrypto public
+  open Nonces HSNonces public
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/TickNonce.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/TickNonce.agda
new file mode 100644
index 0000000000..03b349283b
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/TickNonce.agda
@@ -0,0 +1,19 @@
+module Spec.Foreign.HSConsensus.TickNonce where
+
+open import Spec.Foreign.HSConsensus.BaseTypes
+open import Spec.TickNonce it it it
+
+open import Spec.TickNonce.Properties it it it using (Computational-TICKN)
+
+instance
+
+  HsTy-TickNonceEnv = autoHsType TickNonceEnv ⊣ withConstructor "MkTickNonceEnv"
+  Conv-TickNonceEnv = autoConvert TickNonceEnv
+
+  HsTy-TickNonceState = autoHsType TickNonceState ⊣ withConstructor "MkTickNonceState"
+  Conv-TickNonceState = autoConvert TickNonceState
+
+tickn-step : HsType (TickNonceEnv → TickNonceState → Bool → ComputationResult String TickNonceState)
+tickn-step = to (compute Computational-TICKN)
+
+{-# COMPILE GHC tickn-step as ticknStep #-}
diff --git a/docs/agda-spec/src/Spec/Foreign/HSConsensus/UpdateNonce.agda b/docs/agda-spec/src/Spec/Foreign/HSConsensus/UpdateNonce.agda
new file mode 100644
index 0000000000..1dfafb494c
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSConsensus/UpdateNonce.agda
@@ -0,0 +1,27 @@
+module Spec.Foreign.HSConsensus.UpdateNonce where
+
+open import Spec.Foreign.ExternalFunctions
+
+open import Foreign.Haskell.Coerce
+
+open import Spec.Foreign.HSConsensus.BaseTypes
+open import Spec.UpdateNonce DummyCrypto DummyNonces DummyEpochStructure
+
+instance
+
+  HsTy-UpdateNonceEnv = autoHsType UpdateNonceEnv ⊣ withConstructor "MkUpdateNonceEnv"
+                                                  • fieldPrefix "ue"
+  Conv-UpdateNonceEnv = autoConvert UpdateNonceEnv
+
+  HsTy-UpdateNonceState = autoHsType UpdateNonceState ⊣ withConstructor "MkUpdateNonceState"
+                                                      • fieldPrefix "us"
+  Conv-UpdateNonceState = autoConvert UpdateNonceState
+
+module _ (ext : ExternalFunctions) where
+  open import Spec.Foreign.HSConsensus.ExternalStructures ext hiding (Slot)
+  open import Spec.UpdateNonce.Properties HSCrypto HSNonces HSEpochStructure
+
+  updn-step : HsType (UpdateNonceEnv → UpdateNonceState → Slot → ComputationResult String UpdateNonceState)
+  updn-step = to (coerce ⦃ TrustMe ⦄ $ compute Computational-UPDN)
+
+  {-# COMPILE GHC updn-step as updnStep #-}
diff --git a/docs/agda-spec/src/Spec/Foreign/HSTypes.agda b/docs/agda-spec/src/Spec/Foreign/HSTypes.agda
new file mode 100644
index 0000000000..7c6d168ab7
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/HSTypes.agda
@@ -0,0 +1,76 @@
+module Spec.Foreign.HSTypes where
+
+{-# FOREIGN GHC
+  {-# LANGUAGE DeriveGeneric #-}
+  {-# LANGUAGE DeriveFunctor #-}
+#-}
+
+open import Prelude
+
+open import Foreign.Haskell
+open import Foreign.Haskell.Coerce
+open import Foreign.Haskell.Either
+open import Data.Rational.Base
+
+{-# FOREIGN GHC
+  import GHC.Generics (Generic)
+  import Data.Void (Void)
+  import Prelude hiding (Rational)
+  import GHC.Real (Ratio(..))
+#-}
+
+-- * The empty type
+
+data Empty : Type where
+{-# COMPILE GHC Empty = data Void () #-}
+
+-- * Rational
+
+data Rational : Type where
+  _,_ : ℤ → ℕ → Rational
+{-# COMPILE GHC Rational = data Rational ((:%)) #-}
+
+-- We'll generate code with qualified references to Rational in this
+-- module, so make sure to define it.
+{-# FOREIGN GHC type Rational = Ratio Integer #-}
+
+-- * Maps and Sets
+
+record HSMap K V : Type where
+  constructor MkHSMap
+  field assocList : List (Pair K V)
+
+record HSSet A : Type where
+  constructor MkHSSet
+  field elems : List A
+
+{-# FOREIGN GHC
+  newtype HSMap k v = MkHSMap [(k, v)]
+    deriving (Generic, Show, Eq, Ord)
+  newtype HSSet a = MkHSSet [a]
+    deriving (Generic, Show, Eq, Ord)
+#-}
+{-# COMPILE GHC HSMap = data HSMap (MkHSMap) #-}
+{-# COMPILE GHC HSSet = data HSSet (MkHSSet) #-}
+
+-- * ComputationResult
+
+data ComputationResult E A : Type where
+  Success : A → ComputationResult E A
+  Failure : E → ComputationResult E A
+
+{-# FOREIGN GHC
+  data ComputationResult e a = Success a | Failure e
+    deriving (Functor, Eq, Show, Generic)
+
+  instance Applicative (ComputationResult e) where
+    pure = Success
+    (Success f) <*> x = f <$> x
+    (Failure e) <*> _ = Failure e
+
+  instance Monad (ComputationResult e) where
+    return = pure
+    (Success a) >>= m = m a
+    (Failure e) >>= _ = Failure e
+#-}
+{-# COMPILE GHC ComputationResult = data ComputationResult (Success | Failure) #-}
diff --git a/docs/agda-spec/src/Spec/Foreign/Util.agda b/docs/agda-spec/src/Spec/Foreign/Util.agda
new file mode 100644
index 0000000000..32136269ce
--- /dev/null
+++ b/docs/agda-spec/src/Spec/Foreign/Util.agda
@@ -0,0 +1,8 @@
+module Spec.Foreign.Util where
+
+open import Ledger.Prelude
+
+postulate
+  error : {A : Set} → String → A
+{-# FOREIGN GHC import Data.Text #-}
+{-# COMPILE GHC error = \ _ s -> error (unpack s) #-}
diff --git a/docs/agda-spec/src/Spec/OperationalCertificate.lagda b/docs/agda-spec/src/Spec/OperationalCertificate.lagda
index ea8f02ece7..c1a4661ffa 100644
--- a/docs/agda-spec/src/Spec/OperationalCertificate.lagda
+++ b/docs/agda-spec/src/Spec/OperationalCertificate.lagda
@@ -10,7 +10,6 @@ and consists of the mapping of operation certificate issue numbers. Its signal i
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
@@ -19,8 +18,7 @@ module Spec.OperationalCertificate
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)  
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
   where
 
diff --git a/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda
index 53cce7cd4e..5373f3b03d 100644
--- a/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda
+++ b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
@@ -10,14 +9,13 @@ module Spec.OperationalCertificate.Properties
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
   where
 
 open import Ledger.Prelude
 open import Data.Maybe.Relation.Unary.Any as M
-open import Spec.OperationalCertificate crypto nonces es ss bs af
+open import Spec.OperationalCertificate crypto nonces es bs af
 
 instance
 
diff --git a/docs/agda-spec/src/Spec/Protocol.lagda b/docs/agda-spec/src/Spec/Protocol.lagda
index c145fbaf2d..e472fef9bd 100644
--- a/docs/agda-spec/src/Spec/Protocol.lagda
+++ b/docs/agda-spec/src/Spec/Protocol.lagda
@@ -23,7 +23,6 @@ Its state is shown in Figure~\ref{fig:ts-types:prtcl} and consists of
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Data.Rational.Ext
 
@@ -31,14 +30,13 @@ module Spec.Protocol
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)  
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
   (rs     : _) (open RationalExtStructure rs)
   where
 
 open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr; lookupPoolDistr)
-open import Spec.OperationalCertificate crypto nonces es ss bs af
+open import Spec.OperationalCertificate crypto nonces es bs af
 open import Spec.UpdateNonce crypto nonces es
 open import Spec.BaseTypes crypto using (OCertCounters)
 open import Data.Rational as ℚ using (ℚ; 0ℚ; 1ℚ)
diff --git a/docs/agda-spec/src/Spec/Protocol/Properties.agda b/docs/agda-spec/src/Spec/Protocol/Properties.agda
index b682a7f83d..624bc64424 100644
--- a/docs/agda-spec/src/Spec/Protocol/Properties.agda
+++ b/docs/agda-spec/src/Spec/Protocol/Properties.agda
@@ -3,7 +3,6 @@
 open import Spec.BaseTypes using (Nonces)
 open import Spec.BlockDefinitions
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Data.Rational.Ext
 
@@ -11,8 +10,7 @@ module Spec.Protocol.Properties
   (crypto : _) (open Crypto crypto)
   (nonces : Nonces crypto) (open Nonces nonces)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (bs     : BlockStructure crypto nonces es ss) (open BlockStructure bs)
+  (bs     : BlockStructure crypto nonces es) (open BlockStructure bs)
   (af     : _) (open AbstractFunctions af)
   (rs     : _) (open RationalExtStructure rs)
   where
@@ -20,12 +18,12 @@ module Spec.Protocol.Properties
 open import Data.Rational as ℚ using (1ℚ)
 open import Ledger.Prelude
 open import Tactic.GenError
-open import Spec.Protocol crypto nonces es ss bs af rs
+open import Spec.Protocol crypto nonces es bs af rs
 open import Spec.BaseTypes crypto using (OCertCounters)
 open import Spec.UpdateNonce crypto nonces es
 open import Spec.UpdateNonce.Properties crypto nonces es
-open import Spec.OperationalCertificate crypto nonces es ss bs af
-open import Spec.OperationalCertificate.Properties crypto nonces es ss bs af
+open import Spec.OperationalCertificate crypto nonces es bs af
+open import Spec.OperationalCertificate.Properties crypto nonces es bs af
 open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr; lookupPoolDistr)
 
 private
diff --git a/docs/agda-spec/src/Spec/TickForecast.lagda b/docs/agda-spec/src/Spec/TickForecast.lagda
index 53c648e112..c4350e4bca 100644
--- a/docs/agda-spec/src/Spec/TickForecast.lagda
+++ b/docs/agda-spec/src/Spec/TickForecast.lagda
@@ -9,15 +9,13 @@ and its signal is the current slot.
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import InterfaceLibrary.Ledger
 
 module Spec.TickForecast
   (crypto : Crypto)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (li     : LedgerInterface crypto es ss) (let open LedgerInterface li)
+  (li     : LedgerInterface crypto es) (let open LedgerInterface li)
   where
 
 open import Ledger.Prelude
diff --git a/docs/agda-spec/src/Spec/TickForecast/Properties.agda b/docs/agda-spec/src/Spec/TickForecast/Properties.agda
index 8eea212058..7e890d1055 100644
--- a/docs/agda-spec/src/Spec/TickForecast/Properties.agda
+++ b/docs/agda-spec/src/Spec/TickForecast/Properties.agda
@@ -1,19 +1,17 @@
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import InterfaceLibrary.Ledger
 
 module Spec.TickForecast.Properties
   (crypto : Crypto)
   (es     : _) (open EpochStructure es)
-  (ss     : ScriptStructure crypto es) (open ScriptStructure ss)
-  (li     : LedgerInterface crypto es ss) (let open LedgerInterface li)
+  (li     : LedgerInterface crypto es) (let open LedgerInterface li)
   where
 
 open import Ledger.Prelude
-open import Spec.TickForecast crypto es ss li
+open import Spec.TickForecast crypto es li
 
 instance
 
diff --git a/docs/agda-spec/src/Spec/TickNonce.lagda b/docs/agda-spec/src/Spec/TickNonce.lagda
index 663a09e12b..c3da798baf 100644
--- a/docs/agda-spec/src/Spec/TickNonce.lagda
+++ b/docs/agda-spec/src/Spec/TickNonce.lagda
@@ -11,7 +11,6 @@ Its state consists of the epoch nonce \afld{η₀} and the previous epoch's last
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Spec.BaseTypes using (Nonces)
 
diff --git a/docs/agda-spec/src/Spec/TickNonce/Properties.agda b/docs/agda-spec/src/Spec/TickNonce/Properties.agda
index 52d49cbcaf..46ccfc7edb 100644
--- a/docs/agda-spec/src/Spec/TickNonce/Properties.agda
+++ b/docs/agda-spec/src/Spec/TickNonce/Properties.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --safe #-}
 
 open import Ledger.Crypto
-open import Ledger.Script
 open import Ledger.Types.Epoch
 open import Spec.BaseTypes using (Nonces)
 
diff --git a/docs/agda-spec/src/Spec/hs-src/LICENSE b/docs/agda-spec/src/Spec/hs-src/LICENSE
new file mode 100644
index 0000000000..261eeb9e9f
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/LICENSE
@@ -0,0 +1,201 @@
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
diff --git a/docs/agda-spec/src/Spec/hs-src/Lib.hs b/docs/agda-spec/src/Spec/hs-src/Lib.hs
new file mode 100644
index 0000000000..45b343a4cf
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/Lib.hs
@@ -0,0 +1,15 @@
+module Lib
+  ( module X
+  , module Lib
+  ) where
+
+import MAlonzo.Code.Spec.Foreign.HSTypes                 as X
+  (ComputationResult(..)) -- TODO: Complete
+import MAlonzo.Code.Spec.Foreign.HSConsensus.TickNonce   as X
+  (TickNonceEnv(..), TickNonceState(..), ticknStep)
+import MAlonzo.Code.Spec.Foreign.HSConsensus.UpdateNonce as X
+  (UpdateNonceEnv(..), UpdateNonceState(..), updnStep)
+import MAlonzo.Code.Spec.Foreign.HSConsensus.BaseTypes   as X
+  (Slot, Epoch)
+import MAlonzo.Code.Spec.Foreign.ExternalFunctions       as X
+  (ExternalFunctions(..), dummyExternalFunctions)
diff --git a/docs/agda-spec/src/Spec/hs-src/NOTICE b/docs/agda-spec/src/Spec/hs-src/NOTICE
new file mode 100644
index 0000000000..cd9fe00ebb
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/NOTICE
@@ -0,0 +1,14 @@
+Copyright 2019-2023 Input Output Global Inc (IOG), INTERSECT 2023-2024.
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+
diff --git a/docs/agda-spec/src/Spec/hs-src/cabal.project b/docs/agda-spec/src/Spec/hs-src/cabal.project
new file mode 100644
index 0000000000..dfb30afe59
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/cabal.project
@@ -0,0 +1,2 @@
+-- TODO: Remove this file when code is properly integrated to the existing setup
+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
new file mode 100644
index 0000000000..ed4a3dcbd7
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/cardano-consensus-executable-spec.cabal
@@ -0,0 +1,54 @@
+cabal-version:      3.0
+name:               cardano-consensus-executable-spec
+version:            0.1.0.0
+synopsis: Executable Formal Specification of Ouroboros Consensus
+description: The Haskell code generated from the Agda executable formal specification of the consensus layer for the Ouroboros blockchain protocol
+license: Apache-2.0
+license-files:
+  LICENSE
+  NOTICE
+homepage:
+author:             Javier Díaz
+maintainer:         javier.diaz@iohk.io
+category: Formal Specification
+
+common globalOptions
+    default-language: Haskell2010
+    build-depends: base
+    default-extensions:
+        PolyKinds EmptyDataDecls EmptyCase ExistentialQuantification
+        ScopedTypeVariables NoMonomorphismRestriction RankNTypes
+        PatternSynonyms DeriveGeneric
+    ghc-options:
+        -Wno-overlapping-patterns
+
+test-suite test
+    import: globalOptions
+    hs-source-dirs: test
+    main-is: Spec.hs
+    other-modules:
+        TickNonceSpec
+        UpdateNonceSpec
+    build-depends:
+        cardano-consensus-executable-spec,
+        hspec,
+        HUnit,
+        text
+    build-tool-depends: hspec-discover:hspec-discover
+    type: exitcode-stdio-1.0
+    ghc-options:
+        -Wall
+        -threaded -rtsopts -with-rtsopts=-N
+        -fno-warn-type-defaults
+
+library
+    import: globalOptions
+    hs-source-dirs: .
+    exposed-modules:
+        Lib
+    build-depends:
+        base >=4.14 && <4.21,
+        text,
+        ieee
+-- This will be generated automatically when building with nix
+    other-modules:
diff --git a/docs/agda-spec/src/Spec/hs-src/test/Spec.hs b/docs/agda-spec/src/Spec/hs-src/test/Spec.hs
new file mode 100644
index 0000000000..a824f8c30c
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/test/Spec.hs
@@ -0,0 +1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
diff --git a/docs/agda-spec/src/Spec/hs-src/test/TickNonceSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/TickNonceSpec.hs
new file mode 100644
index 0000000000..34ac7c50a4
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/test/TickNonceSpec.hs
@@ -0,0 +1,29 @@
+{-# OPTIONS -Wno-orphans #-}
+module TickNonceSpec (spec) where
+
+import Data.Text
+
+import Test.Hspec ( Spec, describe, it )
+import Test.HUnit ( (@?=) )
+
+import Lib
+
+initEnv :: TickNonceEnv
+initEnv = MkTickNonceEnv { ηc = 2, ηph = 5 }
+
+initState :: TickNonceState
+initState = MkTickNonceState { η₀ = 3, ηh = 4 }
+
+testTickNonceStepFalse :: ComputationResult Text TickNonceState
+testTickNonceStepFalse = ticknStep initEnv initState False
+
+testTickNonceStepTrue :: ComputationResult Text TickNonceState
+testTickNonceStepTrue = ticknStep initEnv initState True
+
+spec :: Spec
+spec = do
+  describe "ticknStep" $ do
+    it "ticknStep results in the expected state with signal False" $
+      testTickNonceStepFalse @?= Success (MkTickNonceState { η₀ = 3, ηh = 4 })
+    it "ticknStep results in the expected state with signal True" $
+      testTickNonceStepTrue @?= Success (MkTickNonceState { η₀ = 6, ηh = 5 })
diff --git a/docs/agda-spec/src/Spec/hs-src/test/UpdateNonceSpec.hs b/docs/agda-spec/src/Spec/hs-src/test/UpdateNonceSpec.hs
new file mode 100644
index 0000000000..2ca18e3b2c
--- /dev/null
+++ b/docs/agda-spec/src/Spec/hs-src/test/UpdateNonceSpec.hs
@@ -0,0 +1,45 @@
+{-# OPTIONS -Wno-orphans #-}
+module UpdateNonceSpec (spec) where
+
+import Data.Text
+
+import Test.Hspec ( Spec, describe, it )
+import Test.HUnit ( (@?=) )
+
+import Lib
+
+initEnv :: UpdateNonceEnv
+initEnv = MkUpdateNonceEnv { ueΗ = 2 }
+
+initState :: UpdateNonceState
+initState = MkUpdateNonceState { usΗv = 3, usΗc = 4 }
+
+slotBeforeWindow :: Slot
+slotBeforeWindow = 1
+
+testUpdateNonceStepWithSlotBeforeWindow :: ComputationResult Text UpdateNonceState
+testUpdateNonceStepWithSlotBeforeWindow = updnStep dummyExternalFunctions initEnv initState slotBeforeWindow
+
+{-                      window = 20
+                      ______________
+                     /              \
+                     s
+ +---+---+---+---+---+---+---+---+---+---+---+---+
+ 0  1  2 ...         99  100         119 ... 199 200
+ \___________________/   \___________________/
+        epoch 0                 epoch 1
+-}
+
+slotAfterWindow :: Slot
+slotAfterWindow = 99
+
+testUpdateNonceStepWithSlotAfterWindow :: ComputationResult Text UpdateNonceState
+testUpdateNonceStepWithSlotAfterWindow = updnStep dummyExternalFunctions initEnv initState slotAfterWindow
+
+spec :: Spec
+spec = do
+  describe "updnStep" $ do
+    it "updnStep results in the expected state with slot before window" $
+      testUpdateNonceStepWithSlotBeforeWindow @?= Success (MkUpdateNonceState { usΗv = 3 + 2, usΗc = 3 + 2 })
+    it "updnStep results in the expected state with slot after window" $
+      testUpdateNonceStepWithSlotAfterWindow @?= Success (MkUpdateNonceState { usΗv = 3 + 2, usΗc = 4 })
diff --git a/docs/agda-spec/src/Tactic/Substitute.agda b/docs/agda-spec/src/Tactic/Substitute.agda
new file mode 100644
index 0000000000..f54efdd92d
--- /dev/null
+++ b/docs/agda-spec/src/Tactic/Substitute.agda
@@ -0,0 +1,47 @@
+
+module Tactic.Substitute where
+
+open import MetaPrelude
+open import Meta
+
+-- There aren't any nice substitution functions (that I can find) in the standard library or
+-- stdlib-meta. This one is cheating and only works for closed terms at either never gets
+-- applied, or where we can safely throw away the arguments (e.g. `unknown`).
+
+Subst : Set → Set
+Subst A = ℕ → Term → A → A
+
+substTerm : Subst Term
+substArgs : Subst (Args Term)
+substArg  : Subst (Arg Term)
+substAbs  : Subst (Abs Term)
+substSort : Subst Sort
+
+substTerm x s (var y args) =
+  case compare x y of λ where
+    (less _ _)    → var (y ∸ 1) (substArgs x s args)
+    (equal _)     → s  -- cheating and dropping the args!
+    (greater _ _) → var y (substArgs x s args)
+substTerm x s (con c args) = con c (substArgs x s args)
+substTerm x s (def f args) = def f (substArgs x s args)
+substTerm x s (lam v t) = lam v (substAbs x s t)
+substTerm x s (pat-lam cs args₁) = unknown  -- ignoring for now
+substTerm x s (pi a b) = pi (substArg x s a) (substAbs x s b)
+substTerm x s (agda-sort s₁) = agda-sort (substSort x s s₁)
+substTerm x s (lit l) = lit l
+substTerm x s (meta m args) = meta m (substArgs x s args)
+substTerm x s unknown = unknown
+
+substArgs x s [] = []
+substArgs x s (a ∷ as) = substArg x s a ∷ substArgs x s as
+
+substArg x s (arg i t) = arg i (substTerm x s t)
+
+substAbs x s (abs z t) = abs z (substTerm (ℕ.suc x) s t)
+
+substSort x s (set t) = set (substTerm x s t)
+substSort x s (lit n) = lit n
+substSort x s (prop t) = prop (substTerm x s t)
+substSort x s (propLit n) = propLit n
+substSort x s (inf n) = inf n
+substSort x s unknown = unknown
diff --git a/docs/agda-spec/src/formal-ledger.agda-lib b/docs/agda-spec/src/formal-consensus.agda-lib
similarity index 69%
rename from docs/agda-spec/src/formal-ledger.agda-lib
rename to docs/agda-spec/src/formal-consensus.agda-lib
index 0176be2b09..2ec75a2da4 100644
--- a/docs/agda-spec/src/formal-ledger.agda-lib
+++ b/docs/agda-spec/src/formal-consensus.agda-lib
@@ -1,6 +1,6 @@
-name: formal-ledger
+name: formal-consensus
 depend:
   standard-library
   standard-library-classes
   standard-library-meta
-include: .
\ No newline at end of file
+include: .
diff --git a/nix/agda.nix b/nix/agda.nix
index 03f91165c9..9cfd55e58a 100644
--- a/nix/agda.nix
+++ b/nix/agda.nix
@@ -49,7 +49,7 @@ let
   };
 
   deps = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta ];
-  agdaWithPkgs = p: customAgda.agda.withPackages { pkgs = p; ghc = pkgs.ghc; };
+  agdaWithPkgs = p: customAgda.agda.withPackages { pkgs = p; };
 
   attrs = pkgs.recurseIntoAttrs rec {
     agda = agdaWithPkgs deps;
@@ -82,8 +82,33 @@ let
       dontInstall = true;
     };
 
+    # this derivation generates the Haskell code from the Agda spec, but does
+    # not build or test it.
+    # TODO(georgy.lukyanov): share agda typechecking with the docs derivation
+    hsSrc = pkgs.stdenv.mkDerivation {
+      inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
+      pname = "agda-spec-hs-src";
+      version = "0.1";
+      src = ../docs/agda-spec;
+      meta = { };
+      buildInputs = [ agda customAgda.ghc customAgda.cabal-install ];
+      buildPhase = ''
+        OUT_DIR=$out make hs
+      '';
+      doCheck = true;
+      checkPhase = ''
+        test -n "$(find $out/haskell/ -type f -name '*.hs')"
+      '';
+      dontInstall = true;
+    };
+
+    # this derivation picks up the Haskell project generated by hsSrc and
+    # builds and tests it. Note that the profiled build is intentionally disabled
+    # as is causes some GHC versions to panic.
+    hsExe = customAgda.haskell.lib.disableLibraryProfiling (customAgda.haskellPackages.callCabal2nixWithOptions "cardano-consensus-executable-spec" "${hsSrc}/haskell/Spec" "--no-haddock" { });
+
     shell = pkgs.mkShell {
-      packages = [ agda latex ];
+      packages = [ agda latex customAgda.ghc customAgda.cabal-install ];
     };
   };
 in