diff --git a/include/object/reply.h b/include/object/reply.h
index 81d6d79ed..8c3ec5875 100644
--- a/include/object/reply.h
+++ b/include/object/reply.h
@@ -11,12 +11,12 @@
 #include <object/structures.h>
 
 /* Unlink a reply from its tcb */
-static inline void reply_unlink(reply_t *reply)
+static inline void reply_unlink(reply_t *reply, tcb_t *tcb)
 {
     /* check the tcb and reply are linked correctly */
-    assert(thread_state_get_replyObject(reply->replyTCB->tcbState) == REPLY_REF(reply));
+    assert(reply->replyTCB == tcb);
+    assert(thread_state_get_replyObject(tcb->tcbState) == REPLY_REF(reply));
 
-    tcb_t *tcb = reply->replyTCB;
     thread_state_ptr_set_replyObject(&tcb->tcbState, REPLY_REF(0));
     reply->replyTCB = NULL;
     setThreadState(tcb, ThreadState_Inactive);
@@ -25,9 +25,9 @@ static inline void reply_unlink(reply_t *reply)
 /* Push a reply object onto the call stack */
 void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t canDonate);
 /* Pop the head reply from the call stack */
-void reply_pop(reply_t *reply);
+void reply_pop(reply_t *reply, tcb_t *tcb);
 /* Remove a reply from the call stack - replyTCB must be in ThreadState_BlockedOnReply */
-void reply_remove(reply_t *reply);
+void reply_remove(reply_t *reply, tcb_t *tcb);
 /* Remove a specific tcb, and the reply it is blocking on, from the call stack */
 void reply_remove_tcb(tcb_t *tcb);
 
diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index 3d05962a7..c37e8bacb 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -134,7 +134,7 @@ void doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot, bool_t grant)
     }
 
     tcb_t *receiver = reply->replyTCB;
-    reply_remove(reply);
+    reply_remove(reply, receiver);
     assert(thread_state_get_replyObject(receiver->tcbState) == REPLY_REF(0));
     assert(reply->replyTCB == NULL);
 #else
diff --git a/src/object/endpoint.c b/src/object/endpoint.c
index c567191f5..10fe8c9ec 100644
--- a/src/object/endpoint.c
+++ b/src/object/endpoint.c
@@ -85,7 +85,7 @@ void sendIPC(bool_t blocking, bool_t do_call, word_t badge,
 #ifdef CONFIG_KERNEL_MCS
         reply_t *reply = REPLY_PTR(thread_state_get_replyObject(dest->tcbState));
         if (reply) {
-            reply_unlink(reply);
+            reply_unlink(reply, dest);
         }
 
         if (do_call ||
@@ -326,7 +326,7 @@ void cancelIPC(tcb_t *tptr)
 #ifdef CONFIG_KERNEL_MCS
         reply_t *reply = REPLY_PTR(thread_state_get_replyObject(tptr->tcbState));
         if (reply != NULL) {
-            reply_unlink(reply);
+            reply_unlink(reply, tptr);
         }
 #endif
         setThreadState(tptr, ThreadState_Inactive);
@@ -381,7 +381,7 @@ void cancelAllIPC(endpoint_t *epptr)
 #ifdef CONFIG_KERNEL_MCS
             reply_t *reply = REPLY_PTR(thread_state_get_replyObject(thread->tcbState));
             if (reply != NULL) {
-                reply_unlink(reply);
+                reply_unlink(reply, thread);
             }
             if (seL4_Fault_get_seL4_FaultType(thread->tcbFault) == seL4_Fault_NullFault) {
                 setThreadState(thread, ThreadState_Restart);
diff --git a/src/object/objecttype.c b/src/object/objecttype.c
index 32722663c..1d36ebd56 100644
--- a/src/object/objecttype.c
+++ b/src/object/objecttype.c
@@ -139,10 +139,10 @@ finaliseCap_ret_t finaliseCap(cap_t cap, bool_t final, bool_t exposed)
             if (reply && reply->replyTCB) {
                 switch (thread_state_get_tsType(reply->replyTCB->tcbState)) {
                 case ThreadState_BlockedOnReply:
-                    reply_remove(reply);
+                    reply_remove(reply, reply->replyTCB);
                     break;
                 case ThreadState_BlockedOnReceive:
-                    reply_unlink(reply);
+                    reply_unlink(reply, reply->replyTCB);
                     break;
                 default:
                     fail("Invalid tcb state");
diff --git a/src/object/reply.c b/src/object/reply.c
index 6f702bb5f..3ff965311 100644
--- a/src/object/reply.c
+++ b/src/object/reply.c
@@ -51,14 +51,15 @@ void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t can
 }
 
 /* Pop the head reply from the call stack */
-void reply_pop(reply_t *reply)
+void reply_pop(reply_t *reply, tcb_t *tcb)
 {
     assert(reply != NULL);
-    assert(reply->replyTCB != NULL);
     assert(thread_state_get_tsType(reply->replyTCB->tcbState) == ThreadState_BlockedOnReply);
+    assert(thread_state_get_replyObject(tcb->tcbState) == REPLY_REF(reply));
+    assert(reply->replyTCB == tcb);
+
     /* unlink tcb and reply */
-    tcb_t *tcb = reply->replyTCB;
-    reply_unlink(reply);
+    reply_unlink(reply, tcb);
 
     word_t next_ptr = call_stack_get_callStackPtr(reply->replyNext);
     word_t prev_ptr = call_stack_get_callStackPtr(reply->replyPrev);
@@ -87,9 +88,11 @@ void reply_pop(reply_t *reply)
 }
 
 /* Remove a reply from the middle of the call stack */
-void reply_remove(reply_t *reply)
+void reply_remove(reply_t *reply, tcb_t *tcb)
 {
-    assert(thread_state_get_tsType(reply->replyTCB->tcbState) == ThreadState_BlockedOnReply);
+    assert(reply->replyTCB == tcb);
+    assert(thread_state_get_tsType(tcb->tcbState) == ThreadState_BlockedOnReply);
+    assert(thread_state_get_replyObject(tcb->tcbState) == REPLY_REF(reply));
 
     word_t next_ptr = call_stack_get_callStackPtr(reply->replyNext);
     word_t prev_ptr = call_stack_get_callStackPtr(reply->replyPrev);
@@ -97,15 +100,15 @@ void reply_remove(reply_t *reply)
     if (likely(next_ptr)) {
         if (likely(call_stack_get_isHead(reply->replyNext))) {
             /* head of the call stack -> just pop */
-            reply_pop(reply);
+            reply_pop(reply, tcb);
             return;
         }
         /* not the head, remove from middle - break the chain */
         REPLY_PTR(next_ptr)->replyPrev = call_stack_new(0, false);
-        reply_unlink(REPLY_PTR(reply));
-    } else if (reply->replyTCB) {
+        reply_unlink(REPLY_PTR(reply), tcb);
+    } else {
         /* removing start of call chain */
-        reply_unlink(reply);
+        reply_unlink(reply, tcb);
     }
 
     if (prev_ptr) {
@@ -137,5 +140,5 @@ void reply_remove_tcb(tcb_t *tcb)
 
     reply->replyPrev = call_stack_new(0, false);
     reply->replyNext = call_stack_new(0, false);
-    reply_unlink(reply);
+    reply_unlink(reply, tcb);
 }