diff --git a/.github/workflows/verifast-negative.yml b/.github/workflows/verifast-negative.yml
index c9ccf44cf0b7a..0b5ad23947c33 100644
--- a/.github/workflows/verifast-negative.yml
+++ b/.github/workflows/verifast-negative.yml
@@ -30,16 +30,16 @@ jobs:
       - name: Install VeriFast
         run: |
           cd ~
-          curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
-          # https://github.com/verifast/verifast/attestations/4911733
-          echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8  verifast-25.02-linux.tar.gz' | shasum -a 256 -c
-          tar xf verifast-25.02-linux.tar.gz
+          curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/8998468
+          echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b  verifast-25.07-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.07-linux.tar.gz
 
       - name: Install the Rust toolchain used by VeriFast
-        run: rustup toolchain install nightly-2024-11-23
+        run: rustup toolchain install nightly-2025-04-09
 
       - name: Run VeriFast Verification
         run: |
-          export PATH=~/verifast-25.02/bin:$PATH
+          export PATH=~/verifast-25.07/bin:$PATH
           cd verifast-proofs
           bash check-verifast-proofs-negative.sh
diff --git a/.github/workflows/verifast.yml b/.github/workflows/verifast.yml
index 728623ace2a66..80f388296ff07 100644
--- a/.github/workflows/verifast.yml
+++ b/.github/workflows/verifast.yml
@@ -27,17 +27,17 @@ jobs:
       - name: Install VeriFast
         run: |
           cd ~
-          curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
-          # https://github.com/verifast/verifast/attestations/4911733
-          echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8  verifast-25.02-linux.tar.gz' | shasum -a 256 -c
-          tar xf verifast-25.02-linux.tar.gz
+          curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
+          # https://github.com/verifast/verifast/attestations/8998468
+          echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b  verifast-25.07-linux.tar.gz' | shasum -a 256 -c
+          tar xf verifast-25.07-linux.tar.gz
 
       - name: Install the Rust toolchain used by VeriFast
-        run: rustup toolchain install nightly-2024-11-23
+        run: rustup toolchain install nightly-2025-04-09
 
       - name: Run VeriFast Verification
         run: |
-          export PATH=~/verifast-25.02/bin:$PATH
+          export PATH=~/verifast-25.07/bin:$PATH
           cd verifast-proofs
           bash check-verifast-proofs.sh
 
diff --git a/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs b/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs
index 286e12d9bf40f..2519bb997b4ca 100644
--- a/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs
+++ b/verifast-proofs/alloc/collections/linked_list.rs/verified/linked_list.rs
@@ -23,7 +23,7 @@ use super::SpecExtend;
 use crate::alloc::{Allocator, Global};
 use crate::boxed::Box;
 
-//@ use std::alloc::{alloc_block_in, Layout, Global, Allocator};
+//@ use std::alloc::{alloc_id_t, alloc_block_in, Layout, Global, Allocator};
 //@ use std::option::{Option, Option::None, Option::Some};
 //@ use std::ptr::{NonNull, NonNull_ptr};
 
@@ -70,7 +70,7 @@ struct Node<T> {
 
 /*@
 
-pred Nodes<T>(alloc_id: any, n: Option<NonNull<Node<T>>>, prev: Option<NonNull<Node<T>>>, last: Option<NonNull<Node<T>>>, next: Option<NonNull<Node<T>>>; nodes: list<NonNull<Node<T>>>) =
+pred Nodes<T>(alloc_id: alloc_id_t, n: Option<NonNull<Node<T>>>, prev: Option<NonNull<Node<T>>>, last: Option<NonNull<Node<T>>>, next: Option<NonNull<Node<T>>>; nodes: list<NonNull<Node<T>>>) =
     if n == next {
         nodes == [] &*& last == prev
     } else {