diff --git a/tasks.c b/tasks.c
index 84f3c8b33..1e5541eb9 100644
--- a/tasks.c
+++ b/tasks.c
@@ -929,6 +929,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
                     prvTCB_p(gCurrentTCB, ulFreeBytesOnStack);
     @*/
     {
+        //@ open taskISRLockInv();
+        //@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) );
+        //@ assert( gTopReadyPriority == uxTopReadyPriority);
         UBaseType_t uxCurrentPriority = uxTopReadyPriority;
         BaseType_t xTaskScheduled = pdFALSE;
         BaseType_t xDecrementTopPriority = pdTRUE;
@@ -939,8 +942,33 @@ static void prvYieldForTask( TCB_t * pxTCB,
         #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) )
             BaseType_t xPriorityDropped = pdFALSE;
         #endif
+        //@ close taskISRLockInv();
 
         while( xTaskScheduled == pdFALSE )
+        /*@ invariant 
+                // requires clause
+                    0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
+                    xCoreID == coreID_f() &*&
+                    // interrupts are disabled and locks acquired
+                        interruptState_p(xCoreID, state) &*&
+                        interruptsDisabled_f(state) == true &*&
+                        taskLockInv() &*&
+                        isrLockInv() &*&
+                        taskISRLockInv()
+                    &*&
+                    // opened predicate `coreLocalInterruptInv_p()`
+                        pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& 
+                        pubTCB_p(gCurrentTCB, 0) &*&
+                        integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _)
+                    &*&
+                    // read access to current task's stack pointer, etc
+                        prvTCB_p(gCurrentTCB, ulFreeBytesOnStack)
+                &*&
+                // additional knowledge
+                    0 <= uxCurrentPriority &*& uxCurrentPriority <= gTopReadyPriority &*&
+                    gTopReadyPriority < configMAX_PRIORITIES
+                    ;
+        @*/
         {
             #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) )
                 {
diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index 948b4d93d..7646dea79 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -88,7 +88,12 @@ predicate isrLockInv() =
 fixpoint int taskISRLockID_f();
 
 predicate taskISRLockInv() = 
-    integer_((int*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*&
+    integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _)
+    &*&
+    // top ready priority must be in range
+        integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*&
+        0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES
+    &*&
     readyLists_p() &*&
     // Update: The current task on this core is interrupt protected.
     // TODO: Exclude from `allTasks`.