diff --git a/kernel/src/interfaces_impl/cspace.rs b/kernel/src/interfaces_impl/cspace.rs
index 8ac58cc..30d0461 100644
--- a/kernel/src/interfaces_impl/cspace.rs
+++ b/kernel/src/interfaces_impl/cspace.rs
@@ -197,7 +197,10 @@ pub fn finaliseCap(capability: &cap, _final: bool, _exposed: bool) -> finaliseCa
             fc_ret.cleanupInfo = cap_null_cap::new().unsplay();
             return fc_ret;
         }
-        cap_tag::cap_reply_cap | cap_tag::cap_null_cap | cap_tag::cap_domain_cap => {
+        cap_tag::cap_reply_cap => {
+			// TODO: MCS
+		}
+		cap_tag::cap_null_cap | cap_tag::cap_domain_cap => {
             fc_ret.remainder = cap_null_cap::new().unsplay();
             fc_ret.cleanupInfo = cap_null_cap::new().unsplay();
             return fc_ret;
diff --git a/kernel/src/syscall/invocation/invoke_tcb.rs b/kernel/src/syscall/invocation/invoke_tcb.rs
index 954d80d..d68ef8b 100644
--- a/kernel/src/syscall/invocation/invoke_tcb.rs
+++ b/kernel/src/syscall/invocation/invoke_tcb.rs
@@ -212,7 +212,7 @@ pub fn installTCBCap(
     newCap: &cap,
     srcSlot: &mut cte_t,
 ) -> exception_t {
-    let mut rootSlot = target.get_cspace_mut_ref(tcbBuffer);
+    let mut rootSlot = target.get_cspace_mut_ref(index);
     let e = rootSlot.delete_all(true);
     if e != exception_t::EXCEPTION_NONE {
         return e;
diff --git a/sel4_task/src/scheduler.rs b/sel4_task/src/scheduler.rs
index 144e423..285dd22 100644
--- a/sel4_task/src/scheduler.rs
+++ b/sel4_task/src/scheduler.rs
@@ -451,6 +451,12 @@ fn chooseThread() {
                 }
             };
             assert_ne!(thread, 0);
+			assert!(convert_to_mut_type_ref::<tcb_t>(thread).is_schedulable());
+			#[cfg(feature="KERNEL_MCS")]
+			{
+				assert!(convert_to_mut_type_ref::<sched_context_t>(convert_to_mut_type_ref::<tcb_t>(thread).tcbSchedContext).refill_sufficient(0));
+				assert!(convert_to_mut_type_ref::<sched_context_t>(convert_to_mut_type_ref::<tcb_t>(thread).tcbSchedContext).refill_ready());
+			}
             convert_to_mut_type_ref::<tcb_t>(thread).switch_to_this();
         } else {
             #[cfg(target_arch = "aarch64")]
@@ -669,7 +675,7 @@ pub fn commitTime() {
                 assert!(current_sched_context.refill_sufficient(ksConsumed));
                 assert!(current_sched_context.refill_ready());
 
-                if (current_sched_context.is_round_robin()) {
+                if current_sched_context.is_round_robin() {
                     assert!(current_sched_context.refill_size() == MIN_REFILLS);
                     (*current_sched_context.refill_head()).rAmount -= ksConsumed;
                     (*current_sched_context.refill_tail()).rAmount += ksConsumed;