diff --git a/math/vampire/Portfile b/math/vampire/Portfile
index 73f9d9f142385..6605f6c035f2d 100644
--- a/math/vampire/Portfile
+++ b/math/vampire/Portfile
@@ -4,19 +4,19 @@ PortSystem          1.0
 PortGroup           cmake 1.1
 PortGroup           github 1.0
 
-# Temporarily remains commit-based until the next release
-# due to important fixes being added by the upstream recently.
-github.setup        vprover vampire 1b080631257a403681d1287f87f8d3ac1ee97c63
-version             2024-05-31
+github.setup        vprover vampire 4.9 v casc2024
+revision            0
+epoch               1
 categories          math science
 platforms           darwin freebsd
 maintainers         {landonf @landonf} openmaintainer
 description         Vampire Theorem Prover
 long_description    High performance automated theorem prover.
 
-checksums           rmd160  e09d316e9fda2479726491f197d8b4edbf5e2e2f \
-                    sha256  f0f1ee2bbd10b82e0373a53357572f5f3801568e5c67aaba2fdc5209b8091a34 \
-                    size    1466583
+checksums           rmd160  e62573a009237c43c550837ad5f34476fbdaa235 \
+                    sha256  7d0101dc296d0f6fb4f3326febf6a3f3bfd3400b36249a91794789c68a855f3d \
+                    size    1502934
+github.tarball_from releases
 
 # Vampire is BSD-licensed, embedded minisat is MIT-licensed
 license             BSD MIT
@@ -25,11 +25,14 @@ github.tarball_from archive
 
 patchfiles          patch-CMakeLists.txt.diff
 
+# https://github.com/vprover/vampire/pull/593
+patchfiles-append   0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch
+
 cmake.build_type    Release
 cmake.generator     Ninja
 
 compiler.cxx_standard \
-                    2014
+                    2017
 
 configure.args-append \
                     -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON
diff --git a/math/vampire/files/0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch b/math/vampire/files/0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch
new file mode 100644
index 0000000000000..15ce50ce62a2a
--- /dev/null
+++ b/math/vampire/files/0001-Allocator.cpp-fix-for-macOS-where-aligned_alloc-may-.patch
@@ -0,0 +1,31 @@
+From 94819be610e27eff71e2d692c618345d405dcd17 Mon Sep 17 00:00:00 2001
+From: Sergey Fedorov <barracuda@macos-powerpc.org>
+Date: Tue, 3 Sep 2024 18:38:34 +0800
+Subject: [PATCH] Allocator.cpp: fix for macOS where aligned_alloc may not be
+ supported
+
+--- Lib/Allocator.cpp
++++ Lib/Allocator.cpp
+@@ -19,6 +19,10 @@
+ #include "Allocator.hpp"
+ #include "Lib/Timer.hpp"
+ 
++#ifdef __APPLE__
++#include <AvailabilityMacros.h>
++#endif
++
+ #ifndef INDIVIDUAL_ALLOCATIONS
+ Lib::SmallObjectAllocator Lib::GLOBAL_SMALL_OBJECT_ALLOCATOR;
+ #endif
+@@ -43,9 +47,10 @@
+   ALLOCATED += size;
+   {
+     Lib::TimeoutProtector tp;
++#if !defined(__APPLE__) || (defined(__APPLE__) && MAC_OS_X_VERSION_MIN_REQUIRED >= 101300)
+     if(void *ptr = std::aligned_alloc(align, size))
+       return ptr;
+-
++#endif
+     // we might be here because `aligned_alloc` is finicky (Apple, looking at you)
+     // so try again with `malloc` and hope for good alignment
+     if(void *ptr = std::malloc(size))