diff --git a/docs/src/apalache/installation/jvm.md b/docs/src/apalache/installation/jvm.md
index f704b6b9d2..3987a96fb4 100644
--- a/docs/src/apalache/installation/jvm.md
+++ b/docs/src/apalache/installation/jvm.md
@@ -10,17 +10,15 @@ a directory of your choice. Depending on your OS, you have two options.
 *Option 1: Linux, macOS.* You can run the script `./bin/apalache-mc`, or,
 better, add the `./bin` directory to your `PATH` and run `apalache-mc`.
 
-*Option 2: Windows.* You have to run Java directly with
+*Option 2: Windows.* You can run the script `./bin/apalache-mc.bat`
 
-  ```
-  java.exe -jar ./lib/apalache.jar <args>
-  ```
+Alternatively, you can run Java directly with
 
-  The arguments `<args>` are explained in [Running the Tool](../running.md).
+```
+java.exe -jar ./lib/apalache.jar <args>
+```
 
-If you would like to contribute a command-line script for running Apalache in
-Windows, please [open a pull
-request](https://github.com/informalsystems/apalache/blob/main/CONTRIBUTING.md#making-a-pull-request).
+The arguments `<args>` are explained in [Running the Tool](../running.md).
 
 [Eclipse Temurin]: https://adoptium.net/
 [Zulu]: https://www.azul.com/downloads/?version=java-17-lts&package=jdk#download-openjdk
diff --git a/docs/src/apalache/installation/source.md b/docs/src/apalache/installation/source.md
index f285d3d443..a5f5ec985c 100644
--- a/docs/src/apalache/installation/source.md
+++ b/docs/src/apalache/installation/source.md
@@ -26,8 +26,8 @@ If you prefer to keep the built package inside of the Apalache source
 repository, you have three options after running `make`:
 
 - Add the `./bin` directory in the source repository to your `PATH`, which will
-  make `apalche-mc` available.
-- Install [direnv][] and run `direnv allow`, which will put `apalche-mc` in your
+  make `apalache-mc` available.
+- Install [direnv][] and run `direnv allow`, which will put `apalache-mc` in your
   path when you are inside the Apalache repo directory.
 - Run `./bin/apalache-mc` directly.
 
diff --git a/script/release-prepare.sh b/script/release-prepare.sh
index 3d623dcbef..be5d5d9bda 100755
--- a/script/release-prepare.sh
+++ b/script/release-prepare.sh
@@ -36,7 +36,7 @@ then
     # Explicitly set the release version
     sbt "setVersion ${RELEASE_VERSION}"
 else
-    # Derive the relesae version by removing the -SNAPSHOT suffix
+    # Derive the release version by removing the -SNAPSHOT suffix
     sbt removeVersionSnapshot
     RELEASE_VERSION=$("$DIR"/get-version.sh)
 fi
diff --git a/src/universal/bin/apalache-mc.bat b/src/universal/bin/apalache-mc.bat
new file mode 100644
index 0000000000..962158597b
--- /dev/null
+++ b/src/universal/bin/apalache-mc.bat
@@ -0,0 +1,39 @@
+@echo off
+rem Run the APALACHE model checker
+rem
+rem NOTE: The primary intended use for this script is to be copied into the
+rem packaged produced.
+rem
+rem Gabriela Moreira, 2024
+
+rem Set the directory where the script is run from
+set "DIR=%~dp0"
+
+rem Set the path to the APALACHE JAR file
+set "APALACHE_JAR=%DIR%\..\lib\apalache.jar"
+
+rem Set JVM arguments
+set "JVM_ARGS="
+
+rem Check if the APALACHE JAR file exists
+if not exist "%APALACHE_JAR%" (
+    echo ERROR: No file found at %APALACHE_JAR%
+    echo Ensure you have run 'make package' and are running the script from the
+    echo distribution package, or else set APALACHE_JAR to point to your custom
+    echo build jar.
+    exit /b 1
+)
+
+rem Check if the heap size is already set
+echo %JVM_ARGS% | findstr /C:"-Xmx" >nul || echo %JVM_ARGS% | findstr /C:"-XX:MaxRAMPercentage" >nul || set "JVM_ARGS=-Xmx4096m"
+
+rem Check whether the command-line arguments contain the debug flag
+echo %* | find "--debug" >nul && (
+    echo # Tool home: %DIR%
+    echo # Package:   %APALACHE_JAR%
+    echo # JVM args: %JVM_ARGS%
+    echo #
+)
+
+rem Run the Java command
+java %JVM_ARGS% -jar "%APALACHE_JAR%" %*