diff --git a/CHANGELOG.md b/CHANGELOG.md
index 409d7df9..3db4fa1d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,14 @@
 # Changelog
 
-## 2026-11-07 — LithosAnanke v4.0.0-alpha.2: the first published alpha
+## 2026-11-07 — LithosAnanke v4.0.0-alpha.3: the first published alpha
+
+`v4.0.0-alpha.2` (`2d43db25`) used the image's HOL-Library as intended, but its release run (200) ran
+the proofs with Isabelle's defaults -- Java's heap up to 4 GiB, a thread per CPU -- and they were
+killed in the StarForth session. Nothing was published; the tag stays where it is. The proofs now run
+capped (`scripts/nightly.sh proofs`: one thread, Java 512 MiB, Poly/ML 900 MiB; 47 s, ~1.8 GiB), and
+`v4.0.0-alpha.3` is the first alpha published. `docs/fabric/FABRIC-3.md` XLVII.6.
+
+## 2026-11-07 — LithosAnanke v4.0.0-alpha.2: not published
 
 `v4.0.0-alpha.1` (`233025da`) was accepted and tagged, but its release run (196) built HOL-Library
 from scratch in the proofs step and was killed: `release.yml`'s full `make init` replaced the
diff --git a/docs/fabric/FABRIC-3.md b/docs/fabric/FABRIC-3.md
index 755bc19a..e85a916d 100644
--- a/docs/fabric/FABRIC-3.md
+++ b/docs/fabric/FABRIC-3.md
@@ -6178,3 +6178,16 @@ packages, which also fetched Isabelle into the workspace and pointed `/usr/local
 2026-11-07): the tag stays where it is; `release.yml` runs `init INIT_PROOFS=0` (as
 `nightly-docs.yml` does), `LITHOS_VERSION` becomes `4.0.0-alpha.2`, and `v4.0.0-alpha.2` is the
 first published alpha.
+
+### 6. v4.0.0-alpha.2 not published either; v4.0.0-alpha.3
+
+PR #130 merged (`2d43db25`, acceptance run 199; run 197 before it failed one riscv64 check, #131);
+`v4.0.0-alpha.2` tagged there. Its release run (200) passed acceptance and used the image's
+Isabelle and HOL-Library, as XLVII.5 meant -- then the StarForth session was killed (exit 137) in
+the proofs: Isabelle ran with its defaults, Java's heap up to 4 GiB and a thread per CPU, more than
+the server (3.8 GiB, ~2.3 GiB free with the wikis stopped; perhaps a per-job cap besides). Capped
+-- one thread, Java 512 MiB, Poly/ML 900 MiB, in a settings file of a home made for the run, its
+heaps linked to the user's -- the session passes in 47 s at ~1.8 GiB, through
+`scripts/nightly.sh proofs` itself (`logs/20261107-195341`). Nothing was published. Ruled (Captain
+Bob, 2026-11-07): the tag stays; `LITHOS_VERSION` `4.0.0-alpha.3`, the first published alpha; the
+review list begun meanwhile goes to the milestone v4.0.0-alpha.4.
diff --git a/experiments/bare_metal/runs/doe-aarch64-20261107-195725.csv b/experiments/bare_metal/runs/doe-aarch64-20261107-195725.csv
new file mode 100644
index 00000000..e69de29b
diff --git a/experiments/bare_metal/runs/doe-amd64-20261107-195526.csv b/experiments/bare_metal/runs/doe-amd64-20261107-195526.csv
new file mode 100644
index 00000000..e69de29b
diff --git a/experiments/bare_metal/runs/doe-amd64-20261107-200233.csv b/experiments/bare_metal/runs/doe-amd64-20261107-200233.csv
new file mode 100644
index 00000000..e69de29b
diff --git a/experiments/bare_metal/runs/doe-riscv64-20261107-200055.csv b/experiments/bare_metal/runs/doe-riscv64-20261107-200055.csv
new file mode 100644
index 00000000..e69de29b
diff --git a/kernel/Makefile b/kernel/Makefile
index a7c86bb5..8c6fcbd6 100644
--- a/kernel/Makefile
+++ b/kernel/Makefile
@@ -98,6 +98,10 @@ endif
 #   v4.0.0-alpha.2 — the first published alpha: v4.0.0-alpha.1 (233025da) was accepted and tagged,
 #             but its release run's proofs step built HOL-Library from scratch and was killed, so
 #             nothing was published; the tag stays where it is (Captain Bob, 2026-11-07).
+#   v4.0.0-alpha.3 — the first published alpha: v4.0.0-alpha.2 (2d43db25) kept the image's
+#             HOL-Library, but its proofs ran with Isabelle's defaults (Java 4 GiB, a thread per CPU)
+#             and were killed in the StarForth session; nothing was published, the tag stays. The
+#             proofs now run capped (scripts/nightly.sh: 1 thread, Java 512 MiB, ML 900 MiB).
 # LITHOS_VERSION (kernel) and VERSION (embedded StarForth engine) are independent
 # and do not auto-sync (§XXX.4) — do not infer a relationship if they ever coincide.
 # Engine VERSION bumps at tag time by what actually changed (§XXX.6): major = any
@@ -106,7 +110,7 @@ endif
 # the messaging layer was replaced by kernel-Hermes, PLOT/FB-* relocated to Hestia —
 # all dictionary-visible, no FORTH-79 word semantics changed.
 VERSION       ?= 3.2.0
-LITHOS_VERSION ?= 4.0.0-alpha.2
+LITHOS_VERSION ?= 4.0.0-alpha.3
 
 # ==============================================================================
 # BUILD PATHS
diff --git a/logs/20261107-195341/isabelle/isabelle-20261107-195341.log b/logs/20261107-195341/isabelle/isabelle-20261107-195341.log
new file mode 100644
index 00000000..c0431ffe
--- /dev/null
+++ b/logs/20261107-195341/isabelle/isabelle-20261107-195341.log
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:9285ed754dd359088c45e18aca7cae2b92c6ac416c5ebc5fbd1c2e439ca8f6da
+size 7799
diff --git a/logs/20261107-195526/amd64/qemu-amd64-20261107-195526.log b/logs/20261107-195526/amd64/qemu-amd64-20261107-195526.log
new file mode 100644
index 00000000..25f98677
--- /dev/null
+++ b/logs/20261107-195526/amd64/qemu-amd64-20261107-195526.log
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:48198b8c97ce3e2281a81a95176f78a4172a9e4781581b486dba2eebe4cd7a39
+size 6637
diff --git a/logs/20261107-195725/aarch64/qemu-aarch64-20261107-195725.log b/logs/20261107-195725/aarch64/qemu-aarch64-20261107-195725.log
new file mode 100644
index 00000000..83a72869
--- /dev/null
+++ b/logs/20261107-195725/aarch64/qemu-aarch64-20261107-195725.log
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:f714b216d4a6a17441833eb11a6e63668fbe237a0eb6e4606c2c8ce7385c4fef
+size 5602
diff --git a/logs/20261107-200055/riscv64/qemu-riscv64-20261107-200055.log b/logs/20261107-200055/riscv64/qemu-riscv64-20261107-200055.log
new file mode 100644
index 00000000..05956b0e
--- /dev/null
+++ b/logs/20261107-200055/riscv64/qemu-riscv64-20261107-200055.log
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:e041be3ee3d920e25d0fcd8c97ddab1a06b1ad6b0ec1a1a5ec0b67a9f2b3de27
+size 7993
diff --git a/logs/20261107-200233/amd64/qemu-amd64-20261107-200233.log b/logs/20261107-200233/amd64/qemu-amd64-20261107-200233.log
new file mode 100644
index 00000000..3cde323f
--- /dev/null
+++ b/logs/20261107-200233/amd64/qemu-amd64-20261107-200233.log
@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:29a1b7f2d20198ffb62f11c066576fa09b29f4ecc5c2867890aafd45ea7503fc
+size 6708
diff --git a/scripts/nightly.sh b/scripts/nightly.sh
index 0b51dd10..49a7b2ca 100755
--- a/scripts/nightly.sh
+++ b/scripts/nightly.sh
@@ -16,7 +16,8 @@
 #   scripts/nightly.sh test-32
 #       make -C v4 test-32: v4 with 32-bit cells, every test (the acceptance's last part).
 #   scripts/nightly.sh proofs
-#       isabelle build -c -D proof/: the StarForth session checked afresh every run, whatever is
+#       isabelle build -c -D proof/, capped to fit the server (one thread, small heaps): the StarForth
+#       session checked afresh every run, whatever is
 #       cached (HOL-Library is reused: the CI image has it built, ci/runner-image); its log is
 #       logs/<TS>/isabelle/, as a boot's is.
 #   scripts/nightly.sh images
@@ -121,7 +122,19 @@ proofs)
     need "$OUT/.started"
     ts=$(date -u +%Y%m%d-%H%M%S)
     mkdir -p "logs/$ts/isabelle"
-    isabelle build -c -v -D proof/ 2>&1 | tee "logs/$ts/isabelle/isabelle-$ts.log"
+    # Within the server's memory: one thread, Java's heap 512 MiB, Poly/ML's 900 MiB -- the
+    # StarForth session peaks at ~1.7 GiB so (46 s), where Isabelle's defaults (Java 4 GiB, a thread
+    # per CPU) were killed (release run 200, v4.0.0-alpha.2). The caps go in a settings file of a
+    # home made for the run; its heaps are the user's own, linked in, and the image's HOL-Library
+    # is found as always, with Isabelle itself.
+    isahome=$(mktemp -d)
+    isaver=$(isabelle getenv -b ISABELLE_IDENTIFIER)
+    mkdir -p "$isahome/.isabelle/$isaver/etc" "$HOME/.isabelle/$isaver/heaps"
+    ln -s "$HOME/.isabelle/$isaver/heaps" "$isahome/.isabelle/$isaver/heaps"
+    printf '%s\n' 'ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms128m -Xmx512m -Xss16m"' \
+                  'ML_OPTIONS="--minheap 200 --maxheap 900"' > "$isahome/.isabelle/$isaver/etc/settings"
+    USER_HOME="$isahome" isabelle build -o threads=1 -c -v -D proof/ 2>&1 | tee "logs/$ts/isabelle/isabelle-$ts.log"
+    rm -rf "$isahome"
     ;;
 images)
     need "$OUT/StarshipOS.iso"