diff --git a/haskell/src/SEL4/Object/Interrupt.lhs b/haskell/src/SEL4/Object/Interrupt.lhs
index a276ca09b9170adce3cfb004b4b075a0ab1178c1..3a8f4e6c2ad0fb0e34ad5e82e8602287dcf1c3e3 100644
--- a/haskell/src/SEL4/Object/Interrupt.lhs
+++ b/haskell/src/SEL4/Object/Interrupt.lhs
@@ -131,6 +131,9 @@ When the last IRQ handler capability for a given IRQ is deleted, the capability
 > deletingIRQHandler :: IRQ -> Kernel ()
 > deletingIRQHandler irq = do
 >     slot <- getIRQSlot irq
+>     cap <- getSlotCap slot
+>     assert (isAsyncEndpointCap cap || isNullCap cap)
+>         "Cap in IRQ handler slot should be AsyncEP or Null."
 >     cteDeleteOne slot
 
 > deletedIRQHandler :: IRQ -> Kernel ()
diff --git a/haskell/src/SEL4/Object/Structures.lhs b/haskell/src/SEL4/Object/Structures.lhs
index 4b543f43a6f8b5bea558c48753982e9572a563b8..d467b7e6d84581cc780f117477191895bd94a701 100644
--- a/haskell/src/SEL4/Object/Structures.lhs
+++ b/haskell/src/SEL4/Object/Structures.lhs
@@ -101,6 +101,10 @@ This is the type used to represent a capability.
 > isUntypedCap (UntypedCap {}) = True
 > isUntypedCap _ = False
 
+> isAsyncEndpointCap :: Capability -> Bool
+> isAsyncEndpointCap (AsyncEndpointCap {}) = True
+> isAsyncEndpointCap _ = False
+
 \subsection{Kernel Objects}
 
 When stored in the physical memory model (described in \autoref{sec:model.pspace}), kernel objects must be encapsulated in "KernelObject", so the stored type is independent of the real type of the object.