diff --git a/lib/unit/test/unit/Cardano/Wallet/DB/Store/Delegations/StoreSpec.hs b/lib/unit/test/unit/Cardano/Wallet/DB/Store/Delegations/StoreSpec.hs
index 31d90493707..d85e418abe7 100644
--- a/lib/unit/test/unit/Cardano/Wallet/DB/Store/Delegations/StoreSpec.hs
+++ b/lib/unit/test/unit/Cardano/Wallet/DB/Store/Delegations/StoreSpec.hs
@@ -40,8 +40,16 @@ import Cardano.Wallet.DB.Store.Delegations.Store
     ( mkStoreDelegations
     )
 import Cardano.Wallet.Delegation.Model
-    ( Operation (..)
-    , Status (..)
+    ( Status (Inactive)
+    , pattern Delegate
+    , pattern DelegateAndVote
+    , pattern Delegating
+    , pattern DelegatingAndVoting
+    , pattern Deregister'
+    , pattern Register
+    , pattern Registered
+    , pattern Vote
+    , pattern Voting
     , status
     )
 import Cardano.Wallet.Delegation.ModelSpec
@@ -111,30 +119,6 @@ conf =
         , genNewDRep = \xs -> arbitrary `suchThat` (not . (`elem` xs))
         }
 
-pattern Register :: slot -> Operation slot drep pool
-pattern Register i = VoteAndDelegate Nothing Nothing i
-
-pattern Delegate :: pool -> slot -> Operation slot drep pool
-pattern Delegate p i = VoteAndDelegate Nothing (Just p) i
-
-pattern Vote :: drep -> slot -> Operation slot drep pool
-pattern Vote v i = VoteAndDelegate (Just v) Nothing i
-
-pattern DelegateAndVote :: pool -> drep -> slot -> Operation slot drep pool
-pattern DelegateAndVote p v i = VoteAndDelegate (Just v) (Just p) i
-
-pattern Registered :: Status drep pool
-pattern Registered = Active Nothing Nothing
-
-pattern Delegating :: pool -> Status drep pool
-pattern Delegating p = Active Nothing (Just p)
-
-pattern Voting :: drep -> Status drep pool
-pattern Voting v = Active (Just v) Nothing
-
-pattern DelegatingAndVoting :: pool -> drep -> Status drep pool
-pattern DelegatingAndVoting p v = Active (Just v) (Just p)
-
 units :: WalletProperty
 units = withInitializedWalletProp $ \_ runQ -> do
     [p0 :: PoolId, p1, _p2] <-
@@ -151,20 +135,20 @@ units = withInitializedWalletProp $ \_ runQ -> do
     runQ $ unitTestStore mempty mkStoreDelegations $ do
         unit "reg-dereg" $ do
             applyS $ Register 0
-            applyS $ Deregister 0
+            applyS $ Deregister' 0
             observeStatus 0 Inactive
         unit "reg-dereg, different time" $ do
             applyS $ Register 0
             observeStatus 0 Registered
-            applyS $ Deregister 1
+            applyS $ Deregister' 1
             observeStatus 0 Registered
             observeStatus 1 Inactive
         unit "dereg-reg" $ do
-            applyS $ Deregister 0
+            applyS $ Deregister' 0
             applyS $ Register 0
             observeStatus 0 Registered
         unit "dereg-reg different time" $ do
-            applyS $ Deregister 0
+            applyS $ Deregister' 0
             applyS $ Register 1
             observeStatus 1 Registered
         unit "reg-deleg" $ do
@@ -184,7 +168,7 @@ units = withInitializedWalletProp $ \_ runQ -> do
         unit "reg-deleg-dereg" $ do
             applyS $ Register 0
             applyS $ Delegate p0 0
-            applyS $ Deregister 1
+            applyS $ Deregister' 1
             observeStatus 2 Inactive
         unit "reg-vote" $ do
             applyS $ Register 0
@@ -203,7 +187,7 @@ units = withInitializedWalletProp $ \_ runQ -> do
         unit "reg-vote-dereg" $ do
             applyS $ Register 0
             applyS $ Vote v0 0
-            applyS $ Deregister 1
+            applyS $ Deregister' 1
             observeStatus 2 Inactive
         unit "reg-deleg-and-vote" $ do
             applyS $ Register 0
@@ -222,7 +206,7 @@ units = withInitializedWalletProp $ \_ runQ -> do
         unit "reg-deleg-and-vote-dereg" $ do
             applyS $ Register 0
             applyS $ DelegateAndVote p0 v0 0
-            applyS $ Deregister 1
+            applyS $ Deregister' 1
             observeStatus 2 Inactive
         unit "reg-deleg-then-vote" $ do
             applyS $ Register 0
diff --git a/lib/unit/test/unit/Cardano/Wallet/Delegation/ModelSpec.hs b/lib/unit/test/unit/Cardano/Wallet/Delegation/ModelSpec.hs
index 2e44854b07f..4ca1057f227 100644
--- a/lib/unit/test/unit/Cardano/Wallet/Delegation/ModelSpec.hs
+++ b/lib/unit/test/unit/Cardano/Wallet/Delegation/ModelSpec.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
@@ -22,6 +23,10 @@ import Cardano.Wallet.Delegation.Model
     ( History
     , Operation (..)
     , Status (Active)
+    , pattern Delegate
+    , pattern DelegateAndVote
+    , pattern Deregister'
+    , pattern Vote
     )
 import Cardano.Wallet.Delegation.Properties
     ( Step (Step)
@@ -89,9 +94,10 @@ genDelta c h = do
     pool <- genPool c h
     drep <- genRep c h
     elements
-        [ VoteAndDelegate (Just drep) (Just pool) slot
-        , VoteAndDelegate Nothing (Just pool) slot
-        , VoteAndDelegate (Just drep) Nothing slot
+        [ DelegateAndVote pool drep slot
+        , Delegate pool slot
+        , Vote drep slot
+        , Deregister' slot
         , Rollback slot
         ]
 
diff --git a/lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Layer.hs b/lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Layer.hs
index a953cb5346a..3896987d0cb 100644
--- a/lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Layer.hs
+++ b/lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Layer.hs
@@ -25,6 +25,7 @@ import Cardano.Wallet.DB.Store.Delegations.Model
 import Cardano.Wallet.Delegation.Model
     ( Operation (..)
     , Status (..)
+    , Transition (..)
     )
 import Cardano.Wallet.Primitive.Slotting
     ( TimeInterpreter
@@ -87,8 +88,9 @@ putDelegationCertificate
     -> SlotNo
     -> DeltaDelegations
 putDelegationCertificate cert sl = case cert of
-    CertDelegateNone _ -> Deregister sl
-    CertVoteAndDelegate _ pool drep -> VoteAndDelegate drep pool sl
+    CertDelegateNone _ -> ApplyTransition Deregister sl
+    CertVoteAndDelegate _ pool drep -> ApplyTransition
+        (VoteAndDelegate drep pool) sl
 
 -- | Arguments to 'readDelegation'.
 data CurrentEpochSlotting = CurrentEpochSlotting
diff --git a/lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Model.hs b/lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Model.hs
index f1303e43df3..2d796ecbe9e 100644
--- a/lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Model.hs
+++ b/lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Model.hs
@@ -15,6 +15,7 @@ import Cardano.Pool.Types
 import Cardano.Wallet.Delegation.Model
     ( History
     , Operation (..)
+    , Transition (..)
     )
 import Cardano.Wallet.Primitive.Types
     ( SlotNo
@@ -35,8 +36,8 @@ type DeltaDelegations = Operation SlotNo DRep PoolId
 
 instance Buildable DeltaDelegations where
     build = \case
-            Deregister slot -> "Deregister " <> build slot
-            VoteAndDelegate vote pool slot ->
+            ApplyTransition Deregister slot -> "Deregister " <> build slot
+            ApplyTransition (VoteAndDelegate vote pool) slot ->
                     "Delegate " <> build pool
                         <> " and vote "<> build vote <> " " <> build slot
             Rollback slot -> "Rollback " <> build slot
diff --git a/lib/wallet/src/Cardano/Wallet/Delegation/Model.hs b/lib/wallet/src/Cardano/Wallet/Delegation/Model.hs
index c0cad1cdb0b..4b4fb32a0d2 100644
--- a/lib/wallet/src/Cardano/Wallet/Delegation/Model.hs
+++ b/lib/wallet/src/Cardano/Wallet/Delegation/Model.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeFamilies #-}
 
 -- |
@@ -8,9 +9,24 @@
 module Cardano.Wallet.Delegation.Model
     ( Operation (..)
     , slotOf
+
+    , Transition (..)
+    , applyTransition
+
     , Status (..)
+
     , History
     , status
+
+    , pattern Register
+    , pattern Delegate
+    , pattern Vote
+    , pattern Deregister'
+    , pattern DelegateAndVote
+    , pattern Registered
+    , pattern Delegating
+    , pattern Voting
+    , pattern DelegatingAndVoting
     ) where
 
 import Prelude
@@ -27,18 +43,21 @@ import Data.Map.Strict
 
 import qualified Data.Map.Strict as Map
 
+data Transition drep pool
+    = VoteAndDelegate (Maybe drep) (Maybe pool)
+    | Deregister
+    deriving (Eq, Show)
+
 -- | Delta type for the delegation 'History'.
 data Operation slot drep pool
-    = VoteAndDelegate (Maybe drep) (Maybe pool) slot
-    | Deregister slot
+    = ApplyTransition (Transition drep pool) slot
     | Rollback slot
-    deriving (Show)
+    deriving (Eq, Show)
 
 -- | Target slot of each 'Operation'.
 slotOf :: Operation slot drep pool -> slot
-slotOf (Deregister x) = x
 slotOf (Rollback x) = x
-slotOf (VoteAndDelegate _ _ x) = x
+slotOf (ApplyTransition _ x) = x
 
 -- | Valid state for the delegations, independent of time.
 data Status drep pool
@@ -56,16 +75,17 @@ instance (Ord slot, Eq pool, Eq drep) => Delta (Operation slot drep pool) where
         slot = slotOf r
         hist' = cut (< slot) hist
         miss = status slot hist'
-        wanted = transition r $ status slot hist
+        wanted = case r of
+            ApplyTransition t _ -> applyTransition t $ status slot hist
+            Rollback _ -> status slot hist
 
-transition :: Operation slot drep pool -> Status drep pool -> Status drep pool
-transition (Deregister _) _ = Inactive
-transition (VoteAndDelegate d p _) (Active d' p') = Active d'' p''
+applyTransition :: Transition drep pool -> Status drep pool -> Status drep pool
+applyTransition Deregister _ = Inactive
+applyTransition (VoteAndDelegate d p) (Active d' p') = Active d'' p''
     where
         d'' = insertIfJust d d'
         p'' = insertIfJust p p'
-transition (VoteAndDelegate d p _) _ = Active d p
-transition _ s = s
+applyTransition (VoteAndDelegate d p) _ = Active d p
 
 insertIfJust :: Maybe a -> Maybe a -> Maybe a
 insertIfJust (Just y) _ = Just y
@@ -79,3 +99,31 @@ cut op = fst . Map.spanAntitone op
 -- | Status of the delegation at a given slot.
 status :: Ord slot => slot -> Map slot (Status drep pool) -> Status drep pool
 status x = maybe Inactive snd . Map.lookupMax . cut (<= x)
+
+pattern Register :: slot -> Operation slot drep pool
+pattern Register i = ApplyTransition (VoteAndDelegate Nothing Nothing) i
+
+pattern Delegate :: pool -> slot -> Operation slot drep pool
+pattern Delegate p i = ApplyTransition (VoteAndDelegate Nothing (Just p)) i
+
+pattern Vote :: drep -> slot -> Operation slot drep pool
+pattern Vote v i = ApplyTransition (VoteAndDelegate (Just v) Nothing) i
+
+pattern Deregister' :: slot -> Operation slot drep pool
+pattern Deregister' i = ApplyTransition Deregister i
+
+pattern DelegateAndVote :: pool -> drep -> slot -> Operation slot drep pool
+pattern DelegateAndVote p v i
+    = ApplyTransition (VoteAndDelegate (Just v) (Just p)) i
+
+pattern Registered :: Status drep pool
+pattern Registered = Active Nothing Nothing
+
+pattern Delegating :: pool -> Status drep pool
+pattern Delegating p = Active Nothing (Just p)
+
+pattern Voting :: drep -> Status drep pool
+pattern Voting v = Active (Just v) Nothing
+
+pattern DelegatingAndVoting :: pool -> drep -> Status drep pool
+pattern DelegatingAndVoting p v = Active (Just v) (Just p)
diff --git a/lib/wallet/src/Cardano/Wallet/Delegation/Properties.hs b/lib/wallet/src/Cardano/Wallet/Delegation/Properties.hs
index cdf1e8624ec..7ad4b783112 100644
--- a/lib/wallet/src/Cardano/Wallet/Delegation/Properties.hs
+++ b/lib/wallet/src/Cardano/Wallet/Delegation/Properties.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE NamedFieldPuns #-}
 
 -- |
 -- Copyright: © 2022–2023 IOHK
@@ -8,8 +8,7 @@
 --
 -- Properties of the delegations-history model.
 module Cardano.Wallet.Delegation.Properties
-    ( GenSlot
-    , Step (..)
+    ( Step (..)
     , properties
     )
 where
@@ -20,15 +19,14 @@ import Cardano.Wallet.Delegation.Model
     ( History
     , Operation (..)
     , Status (..)
+    , applyTransition
     , slotOf
     , status
     )
-import Control.Applicative
-    ( (<|>)
-    )
 import Test.QuickCheck
     ( Gen
     , Property
+    , conjoin
     , counterexample
     , forAll
     , (===)
@@ -43,39 +41,27 @@ data Step slot drep pool = Step
     }
     deriving (Show)
 
--- | Compute a not so random slot from a 'History' of delegations.
-type GenSlot slot drep pool = History slot drep pool -> Gen slot
-
-property'
-    :: (Ord a, Show a, Show drep, Show pool, Eq drep, Eq pool)
-    => (History a drep pool -> Gen a)
-    -> Step a drep pool
-    -> (Status drep pool -> Status drep pool -> Property)
+setsTheFuture
+    :: (Ord slot, Show slot, Show drep, Show pool, Eq drep, Eq pool)
+    => (History slot drep pool -> Gen slot)
+    -> Step slot drep pool
+    -> (slot -> Operation slot drep pool)
+    -> (Status drep pool -> Status drep pool)
     -> Property
-property' genSlot Step{old_ = xs, new_ = xs', delta_ = diff} change =
-    let x = slotOf diff
-        old = status x xs
-    in  forAll (genSlot xs') $ \y ->
-            let new = status y xs'
+setsTheFuture genSlot Step{old_=history, new_=history', delta_} op transition =
+    let x = slotOf delta_
+        old = status x history
+    in  conjoin
+        [ delta_ === op x
+        , forAll (genSlot history') $ \y ->
+            let new = status y history'
             in  case compare y x of
-                    LT -> new === status y xs
-                    _ -> change old new
-
-precond
-    :: (Eq drep, Eq pool, Show drep, Show pool)
-    => (Status drep pool -> (Bool, Maybe x))
-    -> (Maybe x -> Status drep pool)
-    -> Status drep pool
-    -> Status drep pool
-    -> Property
-precond check target old new
-    | (fst $ check old) = counterexample "new target"
-        $ new === (target (snd $ check old))
-    | otherwise = counterexample "no changes"
-        $ new === old
+                    LT -> new === status y history
+                    _ -> new === transition old
+        ]
 
--- | Properties replicated verbatim from specifications. See
--- 'specifications/Cardano/Wallet/delegation.lean'
+-- | Properties replicated verbatim from specifications.
+-- See 'specifications/Cardano/Wallet/Delegation.agda'.
 properties
     :: (Show slot, Show drep, Show pool, Ord slot, Eq drep, Eq pool)
     => (History slot drep pool -> Gen slot)
@@ -83,30 +69,17 @@ properties
     -> Property
 properties genSlot step =
     let that msg = counterexample ("falsified: " <> msg)
-        prop cond target =
+        setsTheFuture' op =
             counterexample (show step)
-                $ property' genSlot step
-                $ precond cond target
+                . setsTheFuture genSlot step op
     in  case delta_ step of
-            Deregister _ ->
-                that "deregister invariant is respected"
-                    $ prop
-                        ( \case
-                            Active _ _ -> (True, Nothing)
-                            _ -> (False, Nothing)
-                        )
-                        (const Inactive)
-            VoteAndDelegate v p _ -> do
-                that "delegate and/or vote invariant is respected"
-                    $ prop
-                        ( \case
-                            Inactive -> (True, Just Inactive)
-                            Active v' p'-> (True, Just (Active v' p'))
-                        )
-                        $ \case
-                            Just (Active v' p') -> Active (v <|> v') (p <|> p')
-                            Just Inactive -> Active v p
-                            _ -> error "VoteAndDelegate branch broke"
+            ApplyTransition t _ ->
+                that "ApplyTransition invariant is respected"
+                    $ setsTheFuture'
+                        (ApplyTransition t)
+                        (applyTransition t)
             Rollback _ ->
-                that "rollback invariant is respected"
-                    $ property' genSlot step (===)
+                that "Rollback invariant is respected"
+                    $ setsTheFuture'
+                        Rollback
+                        id
diff --git a/specifications/Cardano/Wallet/Delegation.agda b/specifications/Cardano/Wallet/Delegation.agda
new file mode 100644
index 00000000000..942626cd4b4
--- /dev/null
+++ b/specifications/Cardano/Wallet/Delegation.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --erasure #-}
+module
+    Cardano.Wallet.Delegation
+      (Slot : Set)
+      (_<=_ : Slot → Slot → Set)
+      (_<_ : Slot → Slot → Set)
+      (DRep : Set)
+      (Pool : Set)
+  where
+
+open import Haskell.Prelude using (_≡_; Maybe; Just; Nothing)
+open import Data.Product public using () renaming
+  ( _×_ to _⋀_
+  )
+
+{-----------------------------------------------------------------------------
+    Delegation status
+------------------------------------------------------------------------------}
+
+data Status : Set where
+  Inactive   : Status
+  Active     : Maybe DRep → Maybe Pool → Status 
+
+-- | Transitions between delegation status
+data Transition : Set where
+  Deregister      : Transition
+  VoteAndDelegate : Maybe DRep → Maybe Pool → Transition
+
+insertIfJust : ∀ {a : Set} → Maybe a → Maybe a → Maybe a
+insertIfJust (Just x) _ = Just x
+insertIfJust Nothing my = my
+
+applyTransition : Transition → Status → Status
+applyTransition Deregister _
+  = Inactive
+applyTransition (VoteAndDelegate da db) Inactive
+  = Active da db
+applyTransition (VoteAndDelegate da db) (Active a b)
+  = Active (insertIfJust da a) (insertIfJust db b)
+
+{-----------------------------------------------------------------------------
+    Delegation history
+------------------------------------------------------------------------------}
+
+data Operation : Set where
+  ApplyTransition : Transition → Slot → Operation
+  Rollback : Slot → Operation
+
+record HistoryApi : Set₁ where
+  field
+    History : Set
+    status : Slot → History → Status
+
+    applyOperation : Operation → History → History
+
+open HistoryApi
+
+-- Property that expresses how an operation at a slot
+-- changes the History data structure.
+setsTheFuture
+  : ∀ (api : HistoryApi)
+      (op : Slot → Operation)
+      (transition : Status → Status)
+  → Set
+setsTheFuture api op transition =
+  ∀ (x : Slot) (history : History api)
+  → let old      = status api x history
+        history' = applyOperation api (op x) history
+    in
+      ∀ (y : Slot)
+      → let new = status api y history'
+        in  (y <  x → new ≡ status api y history)
+          ⋀ (x <= y → new ≡ transition old)
+
+
+record HistoryLaws (api : HistoryApi) : Set₁ where
+  field
+    prop-transitions
+      : ∀ (t : Transition)
+      → setsTheFuture api
+          (ApplyTransition t)
+          (applyTransition t)
+    
+    prop-rollback
+      : setsTheFuture api
+          Rollback
+          (λ old → old)
diff --git a/specifications/Cardano/Wallet/delegation.lean b/specifications/Cardano/Wallet/delegation.lean
deleted file mode 100644
index b77e6854d15..00000000000
--- a/specifications/Cardano/Wallet/delegation.lean
+++ /dev/null
@@ -1,90 +0,0 @@
-
-section
-
-parameter Slot : Type 
-parameter PoolId : Type 
-
--- Possible status for the delegation at a specific slot.
-inductive Status : Type
-    -- no pool assined and staking off
-    | Inactive : Status
-    -- no pool delegated and staking on
-    | Registered : Status
-    -- pool delegated and staking on
-    | Active  : PoolId -> Status
-open Status
-
-parameter after
-    :  Slot -- what is non-strictly after of
-    -> Slot -- reference 
-    -> Prop
-
-parameter before
-    :  Slot -- what is strictly before of
-    -> Slot -- reference 
-    -> Prop
-
-parameter Delegations : Type
-
-parameter status : Slot -> Delegations -> Status
-
-def Delta := Slot -> Delegations -> Delegations
-def Change := Status -> Status -> Prop
-
-def property 
-  :  Delta -> Change -> Prop 
-  := λ delta change
-  , ∀ (x : Slot) (y : Slot) (xs : Delegations)
-  , let   xs'  := delta x xs
-  ,       old  := status x xs  -- at slot 'x'
-  ,       new  := status y xs' -- forall slots
-  in 
-    before y x → new = status y xs  -- don't change the past
-    ∧ after y x → change old new
-        -- future status determined by status at slot x
-
--- Set staking on, from slot.
-parameter register : Delta
--- Set staking off and undelegate if necessary, from slot.
-parameter deregister : Delta
--- Delegate to given pool, if registered or active, from slot.
-parameter delegate :  PoolId -> Delta
--- Forget changes, from slot.
-parameter rollback : Delta 
-
-def precond (check : Status -> Prop) (target : Status) : Change 
-    := λ old new
-    , let cond := check old 
-      in (cond → new = target) ∧ ((¬ cond) → new = old)
-
-structure DelegationsProps :=
-
-  (register_property
-   : property register 
-        ( precond 
-           (λ old, old = Inactive) 
-           Registered
-        )
-  )
-
-  (deregister_property
-   : ∀ p , property deregister
-      (precond
-        (λ old, old = Registered ∨ old = Active p)
-        Inactive
-      )
-  )
-
-  (delegate_property
-  : ∀ p p' , property (delegate p) 
-      ( precond 
-          (λ old, old = Registered ∨ old = Active p') 
-          (Active p)
-      )
-  )
-
-  (rollback_property
-  : property rollback (λ old new, old = new)
-  ) 
-
-end
\ No newline at end of file
diff --git a/specifications/Cardano/Wallet/delegation.md b/specifications/Cardano/Wallet/delegation.md
index 549e6303672..43400222c6f 100644
--- a/specifications/Cardano/Wallet/delegation.md
+++ b/specifications/Cardano/Wallet/delegation.md
@@ -84,7 +84,7 @@ History of delegations
 
 Each delegation certificate that is sent to the blockchain can induce a status transition. The possible transitions are:
 
-1. _degister_ : remove the reward account
+1. _deregister_ : remove the reward account
 1. _register_ : register a reward account
 2. _delegate_ : delegate stake to a stake pool identifier
 3. _vote_ : delegate voting power to a rep