diff --git a/.github/workflows/update-subtree.yml b/.github/workflows/update-subtree.yml
index 4c9078f649f04..8ae7730ef5e17 100644
--- a/.github/workflows/update-subtree.yml
+++ b/.github/workflows/update-subtree.yml
@@ -214,16 +214,12 @@ jobs:
 
         # Try to automatically patch the VeriFast proofs
         pushd verifast-proofs
-        if bash ./patch-verifast-proofs.sh; then
-          if ! git diff --quiet; then
-            git -c user.name=gitbot -c user.email=git@bot \
-              commit . -m "Update VeriFast proofs"
-          else
-            # The original files have not changed; no updates to the VeriFast proofs are necessary.
-            true
-          fi
+        ./patch-verifast-proofs.sh
+        if ! git diff --quiet; then
+          git -c user.name=gitbot -c user.email=git@bot \
+            commit . -m "Update VeriFast proofs"
         else
-          # Patching the VeriFast proofs failed; requires manual intervention.
+          # The original files have not changed; no updates to the VeriFast proofs are necessary.
           true
         fi
         popd
diff --git a/.github/workflows/verifast-negative.yml b/.github/workflows/verifast-negative.yml
index 0b5ad23947c33..cc1793f560c28 100644
--- a/.github/workflows/verifast-negative.yml
+++ b/.github/workflows/verifast-negative.yml
@@ -27,19 +27,5 @@ jobs:
       - name: Checkout Repository
         uses: actions/checkout@v4
       
-      - name: Install VeriFast
-        run: |
-          cd ~
-          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-2025-04-09
-
       - name: Run VeriFast Verification
-        run: |
-          export PATH=~/verifast-25.07/bin:$PATH
-          cd verifast-proofs
-          bash check-verifast-proofs-negative.sh
+        run: verifast-proofs/check-verifast-proofs-negative.sh
diff --git a/.github/workflows/verifast.yml b/.github/workflows/verifast.yml
index 80f388296ff07..ec97d018dc01b 100644
--- a/.github/workflows/verifast.yml
+++ b/.github/workflows/verifast.yml
@@ -24,22 +24,8 @@ jobs:
       - name: Checkout Repository
         uses: actions/checkout@v4
       
-      - name: Install VeriFast
-        run: |
-          cd ~
-          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-2025-04-09
-
       - name: Run VeriFast Verification
-        run: |
-          export PATH=~/verifast-25.07/bin:$PATH
-          cd verifast-proofs
-          bash check-verifast-proofs.sh
+        run: verifast-proofs/check-verifast-proofs.sh
 
   notify-btj:
     name: Notify @btj
diff --git a/verifast-proofs/alloc/collections/linked_list.rs-negative/update.sh b/verifast-proofs/alloc/collections/linked_list.rs-negative/update.sh
new file mode 100644
index 0000000000000..164edddba4273
--- /dev/null
+++ b/verifast-proofs/alloc/collections/linked_list.rs-negative/update.sh
@@ -0,0 +1,10 @@
+set -x -e
+
+if ! git diff --quiet .; then
+  echo "Working directory not clean. Please stash your changes and try again"
+  false
+else
+  UPSTREAM=../../../../library/alloc/src/collections/linked_list.rs
+  git merge-file --diff3 verified/linked_list.rs original/linked_list.rs $UPSTREAM
+  cp $UPSTREAM original/linked_list.rs
+fi
diff --git a/verifast-proofs/alloc/collections/linked_list.rs-negative/verify.sh b/verifast-proofs/alloc/collections/linked_list.rs-negative/verify.sh
new file mode 100644
index 0000000000000..b13ddb402967e
--- /dev/null
+++ b/verifast-proofs/alloc/collections/linked_list.rs-negative/verify.sh
@@ -0,0 +1,10 @@
+set -e -x
+
+export VFVERSION=25.07
+
+! verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns verified/lib.rs
+! refinement-checker --rustc-args "--edition 2021 --cfg test" original/lib.rs verified/lib.rs
+if ! diff ../../../../library/alloc/src/collections/linked_list.rs original/linked_list.rs; then
+  echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
+  false
+fi
diff --git a/verifast-proofs/alloc/collections/linked_list.rs/update.sh b/verifast-proofs/alloc/collections/linked_list.rs/update.sh
new file mode 100644
index 0000000000000..164edddba4273
--- /dev/null
+++ b/verifast-proofs/alloc/collections/linked_list.rs/update.sh
@@ -0,0 +1,10 @@
+set -x -e
+
+if ! git diff --quiet .; then
+  echo "Working directory not clean. Please stash your changes and try again"
+  false
+else
+  UPSTREAM=../../../../library/alloc/src/collections/linked_list.rs
+  git merge-file --diff3 verified/linked_list.rs original/linked_list.rs $UPSTREAM
+  cp $UPSTREAM original/linked_list.rs
+fi
diff --git a/verifast-proofs/alloc/collections/linked_list.rs/verify.sh b/verifast-proofs/alloc/collections/linked_list.rs/verify.sh
new file mode 100644
index 0000000000000..483c4ed2d6fe8
--- /dev/null
+++ b/verifast-proofs/alloc/collections/linked_list.rs/verify.sh
@@ -0,0 +1,10 @@
+set -e -x
+
+export VFVERSION=25.07
+
+verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns -ignore_unwind_paths -allow_assume verified/lib.rs
+refinement-checker --rustc-args "--edition 2021 --cfg test" original/lib.rs verified/lib.rs > /dev/null
+if ! diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs; then
+  echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
+  false
+fi
diff --git a/verifast-proofs/alloc/raw_vec/mod.rs/update.sh b/verifast-proofs/alloc/raw_vec/mod.rs/update.sh
new file mode 100644
index 0000000000000..834f640daac72
--- /dev/null
+++ b/verifast-proofs/alloc/raw_vec/mod.rs/update.sh
@@ -0,0 +1,11 @@
+set -x -e
+
+if ! git diff --quiet .; then
+  echo "Working directory not clean. Please stash your changes and try again"
+  false
+else
+  UPSTREAM=../../../../library/alloc/src/raw_vec/mod.rs
+  git merge-file --diff3 with-directives/raw_vec.rs original/raw_vec.rs $UPSTREAM
+  git merge-file --diff3 verified/raw_vec.rs original/raw_vec.rs $UPSTREAM
+  cp $UPSTREAM original/raw_vec.rs
+fi
diff --git a/verifast-proofs/alloc/raw_vec/mod.rs/verify.sh b/verifast-proofs/alloc/raw_vec/mod.rs/verify.sh
new file mode 100644
index 0000000000000..0a1b208159179
--- /dev/null
+++ b/verifast-proofs/alloc/raw_vec/mod.rs/verify.sh
@@ -0,0 +1,11 @@
+set -e -x
+
+export VFVERSION=25.07
+
+verifast -skip_specless_fns -ignore_unwind_paths -allow_assume verified/lib.rs
+refinement-checker with-directives/lib.rs verified/lib.rs > /dev/null
+refinement-checker --ignore-directives original/lib.rs with-directives/lib.rs > /dev/null
+if ! diff original/raw_vec.rs ../../../../library/alloc/src/raw_vec/mod.rs; then
+  echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
+  false
+fi
diff --git a/verifast-proofs/check-verifast-proofs-negative.sh b/verifast-proofs/check-verifast-proofs-negative.sh
old mode 100644
new mode 100755
index 398516809ae46..89fa996463136
--- a/verifast-proofs/check-verifast-proofs-negative.sh
+++ b/verifast-proofs/check-verifast-proofs-negative.sh
@@ -1,14 +1,14 @@
+#!/bin/bash
+
 set -e -x
 
+cd "$(dirname "$0")"
+export PATH=`pwd`:$PATH
+
 cd alloc
   cd collections
     cd linked_list.rs-negative
-      ! verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns verified/lib.rs
-      ! refinement-checker --rustc-args "--edition 2021 --cfg test" original/lib.rs verified/lib.rs
-      if ! diff ../../../../library/alloc/src/collections/linked_list.rs original/linked_list.rs; then
-        echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
-        false
-      fi
+      bash verify.sh
     cd ..
   cd ..
 cd ..
diff --git a/verifast-proofs/check-verifast-proofs.sh b/verifast-proofs/check-verifast-proofs.sh
old mode 100644
new mode 100755
index 6fea26c22eb97..23bd82948efbd
--- a/verifast-proofs/check-verifast-proofs.sh
+++ b/verifast-proofs/check-verifast-proofs.sh
@@ -1,25 +1,20 @@
+#!/bin/bash
+
 set -e -x
 
+cd "$(dirname "$0")"
+
+export PATH=`pwd`:$PATH
+
 cd alloc
   cd collections
     cd linked_list.rs
-      verifast -rustc_args "--edition 2021 --cfg test" -skip_specless_fns -ignore_unwind_paths -allow_assume verified/lib.rs
-      refinement-checker --rustc-args "--edition 2021 --cfg test" original/lib.rs verified/lib.rs > /dev/null
-      if ! diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs; then
-        echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
-        false
-      fi
+      bash verify.sh
     cd ..
   cd ..
   cd raw_vec
     cd mod.rs
-      verifast -skip_specless_fns -ignore_unwind_paths -allow_assume verified/lib.rs
-      refinement-checker with-directives/lib.rs verified/lib.rs > /dev/null
-      refinement-checker --ignore-directives original/lib.rs with-directives/lib.rs > /dev/null
-      if ! diff original/raw_vec.rs ../../../../library/alloc/src/raw_vec/mod.rs; then
-        echo "::error title=Please run verifast-proofs/patch-verifast-proofs.sh::Some VeriFast proofs are out of date; please chdir to verifast-proofs and run patch-verifast-proofs.sh to update them."
-        false
-      fi
+      bash verify.sh
     cd ..
   cd ..
 cd ..
diff --git a/verifast-proofs/patch-verifast-proofs.sh b/verifast-proofs/patch-verifast-proofs.sh
old mode 100644
new mode 100755
index cf54080b3ee23..802b68ba7b68a
--- a/verifast-proofs/patch-verifast-proofs.sh
+++ b/verifast-proofs/patch-verifast-proofs.sh
@@ -1,21 +1,24 @@
+#!/bin/bash
+
 set -e -x
 
+cd "$(dirname "$0")"
+export PATH=`pwd`:$PATH
+
+patch_proof() {
+  if ! git diff --quiet .; then
+    echo "Directory not clean. Please stash changes and try again"
+  else
+    bash update.sh && bash verify.sh || git restore .
+  fi
+}
+
 pushd alloc/collections/linked_list.rs
-  diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs > /tmp/linked_list.diff || [ "$?" = 1 ]
-  patch -p0 verified/linked_list.rs < /tmp/linked_list.diff
-  patch -p0 original/linked_list.rs < /tmp/linked_list.diff
-  rm /tmp/linked_list.diff
+  patch_proof
 popd
 pushd alloc/collections/linked_list.rs-negative
-  diff original/linked_list.rs ../../../../library/alloc/src/collections/linked_list.rs > /tmp/linked_list.diff || [ "$?" = 1 ]
-  patch -p0 verified/linked_list.rs < /tmp/linked_list.diff
-  patch -p0 original/linked_list.rs < /tmp/linked_list.diff
-  rm /tmp/linked_list.diff
+  patch_proof
 popd
 pushd alloc/raw_vec/mod.rs
-  diff original/raw_vec.rs ../../../../library/alloc/src/raw_vec/mod.rs > /tmp/raw_vec.diff || [ "$?" = 1 ]
-  patch -p0 verified/raw_vec.rs < /tmp/raw_vec.diff
-  patch -p0 with-directives/raw_vec.rs < /tmp/raw_vec.diff
-  patch -p0 original/raw_vec.rs < /tmp/raw_vec.diff
-  rm /tmp/raw_vec.diff
+  patch_proof
 popd
diff --git a/verifast-proofs/refinement-checker b/verifast-proofs/refinement-checker
new file mode 100755
index 0000000000000..80f3cc4955f0d
--- /dev/null
+++ b/verifast-proofs/refinement-checker
@@ -0,0 +1,5 @@
+#!/bin/bash
+
+set -e -x
+. "$(dirname "$0")/setup-verifast-home"
+"$VERIFAST_HOME/bin/refinement-checker" "$@"
diff --git a/verifast-proofs/setup-verifast-home b/verifast-proofs/setup-verifast-home
new file mode 100644
index 0000000000000..ddc4ce42d0ed0
--- /dev/null
+++ b/verifast-proofs/setup-verifast-home
@@ -0,0 +1,53 @@
+set -e -x
+
+: "${VFTOOLCHAINS=$HOME/.verifast/toolchains}"
+: "${VERIFAST_HOME=$VFTOOLCHAINS/verifast-$VFVERSION}"
+
+if [[ ! -d "$VERIFAST_HOME" ]]; then
+
+  if [[ -z $VFPLATFORM ]]; then
+    if [[ "$(uname)" == "Darwin" ]]; then
+      if [[ "$(uname -m)" == "arm64" ]]; then
+        : "${VFPLATFORM=macos-aarch}"
+      else
+        : "${VFPLATFORM=macos}"
+      fi
+    else
+      : "${VFPLATFORM=linux}"
+    fi
+  fi
+
+  case "$VFVERSION,$VFPLATFORM" in
+    25.07,macos-aarch)
+      # https://github.com/verifast/verifast/attestations/8998438
+      VFHASH=6129fe538fb0b47ddf57e223dd628d991c74d9c835c991dd65871d5dc56c6d3f
+      RUST_VERSION=nightly-2025-04-09
+      ;;
+    25.07,linux)
+      # https://github.com/verifast/verifast/attestations/8998468
+      VFHASH=48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b
+      RUST_VERSION=nightly-2025-04-09
+      ;;
+    *)
+      echo 'Unknown VeriFast version "'"$VFVERSION"'". Please set VFVERSION to a support version'
+      false
+      ;;
+  esac
+
+  if ! rustup toolchain list | grep $RUST_VERSION; then
+    rustup toolchain install $RUST_VERSION
+  fi
+
+  VFASSET=verifast-$VFVERSION-$VFPLATFORM.tar.gz
+  pushd "${TMPDIR:-/tmp}"
+    if [[ ! -d verifast-$VFVERSION ]]; then
+      if [[ ! -e $VFASSET ]]; then
+        curl -OL https://github.com/verifast/verifast/releases/download/$VFVERSION/$VFASSET
+      fi
+      echo "$VFHASH  $VFASSET" | shasum -a 256 -c
+      tar xf $VFASSET
+    fi
+    mkdir -p "$VFTOOLCHAINS"
+    mv verifast-$VFVERSION "$VFTOOLCHAINS"
+  popd
+fi
diff --git a/verifast-proofs/verifast b/verifast-proofs/verifast
new file mode 100755
index 0000000000000..520ae44f2c3d2
--- /dev/null
+++ b/verifast-proofs/verifast
@@ -0,0 +1,5 @@
+#!/bin/bash
+
+set -e -x
+. "$(dirname "$0")/setup-verifast-home"
+"$VERIFAST_HOME/bin/verifast" "$@"