diff --git a/include/stack_macros.h b/include/stack_macros.h
index 6351e14bb..926e7743d 100644
--- a/include/stack_macros.h
+++ b/include/stack_macros.h
@@ -93,21 +93,67 @@
          * - `vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName );`
          *
         */
-       #define taskCHECK_FOR_STACK_OVERFLOW()                                                            \
-        {                                                                                                \
+        #define taskCHECK_FOR_STACK_OVERFLOW()   VF__taskCHECK_FOR_STACK_OVERFLOW()
+
+        void VF__taskCHECK_FOR_STACK_OVERFLOW()
+        /*@ requires prvTCB_p(?gCurrentTCB, ?ulFreeBytesOnStack) &*&
+                     pubTCB_p(gCurrentTCB, ?uxCriticalNesting) &*&
+                    // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()`
+                        interruptState_p(coreID_f(), ?state) &*&
+                        interruptsDisabled_f(state) == true &*&
+                        pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB);
+        @*/
+        /*@ ensures prvTCB_p(gCurrentTCB, ulFreeBytesOnStack) &*&
+                     pubTCB_p(gCurrentTCB, uxCriticalNesting) &*&
+                    // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()`
+                        interruptState_p(coreID_f(), state) &*&
+                        interruptsDisabled_f(state) == true &*&
+                        pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB);                                            \
+        @*/                                                                                               \
+        {                                                                                                 \
+            /*@ open prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/                                       \
+            /*@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack,                                 \
+                        ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) );                                 \
+             @*/                                                                                          \
+            /*@ open stack_p_2(_, _, _, _, _, _); @*/                                                     \
+            /* The detour below allows us to skip proving that `ulFreeBytes`                              \
+             * is a multiple of `sizeof(StackType_t)`.                                                    \
+             */                                                                                           \
+            /*@ integers__to_chars(pxTopOfStack+1); @*/                                                   \
+            /*@ chars_join((char*) pxStack); @*/                                                          \
+            /*@ chars_to_integers_(pxStack, sizeof(StackType_t), false, 4); @*/                           \
             TCB_t* tcb0 = pxCurrentTCB;                                                                   \
-            const uint32_t * const pulStack = ( uint32_t * ) tcb0->pxStack;                      \
+            const uint32_t * const pulStack = ( uint32_t * ) tcb0->pxStack;                               \
             const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5;                                        \
-                                                                                                        \
+                                                                                                          \
+            /*@ bool gOverflow = false; @*/                                                               \
             if( ( pulStack[ 0 ] != ulCheckValue ) ||                                                      \
                 ( pulStack[ 1 ] != ulCheckValue ) ||                                                      \
                 ( pulStack[ 2 ] != ulCheckValue ) ||                                                      \
                 ( pulStack[ 3 ] != ulCheckValue ) )                                                       \
             {                                                                                             \
+                /*@ gOverflow = true; @*/                                                                 \
+                /*@ integers__to_chars(pxStack); @*/                                                      \
+        	    /*@ chars_join((char*) pxStack); @*/                                                      \
+        	    /*@ chars_split((char*) pxStack, ulFreeBytesOnStack); @*/                                 \
+        	    /*@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack,                                  \
+                                    ulFreeBytes, ulUsedCells, ulUnalignedBytes);                          \
+                @*/                                                                                       \
+        	    /*@ close prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/                                  \
                 TCB_t* tcb1 = pxCurrentTCB;                                                               \
                 TCB_t* tcb2 = pxCurrentTCB;                                                               \
-                vApplicationStackOverflowHook( ( TaskHandle_t ) tcb1, tcb2->pcTaskName ); \
+                vApplicationStackOverflowHook( ( TaskHandle_t ) tcb1, tcb2->pcTaskName );                 \
             }                                                                                             \
+            /*@                                                                                           \
+            if(!gOverflow) {                                                                              \
+                integers__to_chars(pxStack);                                                              \
+        	    chars_join((char*) pxStack);                                                              \
+        	    chars_split((char*) pxStack, ulFreeBytesOnStack);                                         \
+        	    close stack_p_2(pxStack, ulStackDepth, pxTopOfStack,                                      \
+                                ulFreeBytes, ulUsedCells, ulUnalignedBytes);                              \
+        	    close prvTCB_p(gCurrentTCB, ulFreeBytesOnStack);                                          \
+            }                                                                                             \
+            @*/                                                                                           \
         }
     #else
         #define taskCHECK_FOR_STACK_OVERFLOW()                                                            \
diff --git a/include/task.h b/include/task.h
index 8bc75d1f3..7afb9743c 100644
--- a/include/task.h
+++ b/include/task.h
@@ -1863,6 +1863,12 @@ configSTACK_DEPTH_TYPE uxTaskGetStackHighWaterMark2( TaskHandle_t xTask ) PRIVIL
       */
      void vApplicationStackOverflowHook( TaskHandle_t xTask,
                                                char * pcTaskName );
+    /*@ requires prvTCB_p(xTask, ?ulFreeBytesOnStack) &*&
+                 pubTCB_p(xTask, ?uxCriticalNesting);
+     @*/
+    /*@ ensures prvTCB_p(xTask, ulFreeBytesOnStack) &*&
+                pubTCB_p(xTask, uxCriticalNesting);
+     @*/
 
 #endif
 
diff --git a/tasks.c b/tasks.c
index 1cc9b064e..61bd1fc65 100644
--- a/tasks.c
+++ b/tasks.c
@@ -56,7 +56,16 @@
 #include "FreeRTOS.h"
 #include "task.h"
 #include "timers.h"
-#include "stack_macros.h"
+
+#ifndef VERIFAST
+    /* Reason for rewrite:
+     * The stack macros rely on macros defined later in this file, e.g., 
+     * `pxCurrentTCB`. We need to delay this inclusion until the task macros 
+     * have been defined. Otherwise, VeriFast will report unknown symbols when
+     * checking the stack macro proofs.
+     */
+    #include "stack_macros.h"
+#endif /* VERIFAST */
 
 /* Verifast proof setup 
  * 
@@ -381,6 +390,18 @@ PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList;              /*< Poi
 PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList;      /*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */
 PRIVILEGED_DATA static List_t xPendingReadyList;                         /*< Tasks that have been readied while the scheduler was suspended.  They will be moved to the ready list when the scheduler is resumed. */
 
+
+#ifdef VERIFAST
+    /* Reason for rewrite:
+     * The stack macros rely on some of the macros defined above, e.g., 
+     * `pxCurrentTCB`. We need to delay this inclusion until the relevant task
+     * macros have been defined. Otherwise, VeriFast will report unknown symbols
+     * when checking the stack macro proofs.
+     */
+    #include "stack_macros.h"
+#endif /* VERIFAST */
+
+
 #if ( INCLUDE_vTaskDelete == 1 )
 
     PRIVILEGED_DATA static List_t xTasksWaitingTermination; /*< Tasks that have been deleted - but their memory not yet freed. */
diff --git a/verification/verifast/proof/stack_predicates.h b/verification/verifast/proof/stack_predicates.h
index b8eb15600..00c295708 100644
--- a/verification/verifast/proof/stack_predicates.h
+++ b/verification/verifast/proof/stack_predicates.h
@@ -28,7 +28,7 @@ predicate stack_p_2(StackType_t * pxStack,
     // `taskCHECK_FOR_STACK_OVERFLOW` macro on RP2040 port expects minimal stack size
     ulFreeBytes >= 0 &*&
     ulUsedCells >= 0 &*&
-    ulFreeBytes + ulUsedCells * sizeof(StackType_t) >= 3 * sizeof(StackType_t);
+    ulFreeBytes + ulUsedCells * sizeof(StackType_t) >= 4 * sizeof(StackType_t);
 
 predicate unalignedRestOfStack_p(char* p, uint32_t ulUnalignedBytes) =
     chars(p, ulUnalignedBytes, _);
diff --git a/verification/verifast/start-vfide--preprocessed.sh b/verification/verifast/start-vfide--preprocessed.sh
index e81f5a778..de528818f 100755
--- a/verification/verifast/start-vfide--preprocessed.sh
+++ b/verification/verifast/start-vfide--preprocessed.sh
@@ -13,7 +13,7 @@ PP_SCRIPT_DIR="$START_WD/custom_build_scripts_RP2040"
 PP_SCRIPT="./preprocess_tasks_c.sh"
 PP_TASK_C="$START_WD/preprocessed_files/tasks__pp.c"
 
-FONT_SIZE=16
+FONT_SIZE=17
 
 # Flags to SKIP expensive proofs:
 # - VERIFAST_SKIP_BITVECTOR_PROOF__STACK_ALIGNMENT