diff --git a/Makefile b/Makefile
index a1b28674..510dccdb 100644
--- a/Makefile
+++ b/Makefile
@@ -40,7 +40,10 @@
 #                                     boot it in QEMU and build the documents
 #                                     (Debian/Ubuntu, apt-get; sudo if not root).
 #                                     ARCH=amd64,aarch64,riscv64 sets up all
-#                                     three, for the full acceptance
+#                                     three, for the full acceptance. syft and
+#                                     Isabelle/HOL, not packaged, are downloaded,
+#                                     checked by SHA-256 and linked into
+#                                     /usr/local/bin (build/cache/tools)
 #   make <other goal>                 goes to v3/Makefile (make help-hosted)
 # ==============================================================================
 
@@ -242,9 +245,14 @@ write_stick:
 # the logs and DoE CSVs (.gitattributes), and the documents: the book (docs/book/Makefile's own
 # list) and the formal volumes and API reference (docs/formal/Makefile: pdflatex, doxygen, dot).
 # Per ISA: its QEMU, its UEFI firmware (kernel/Makefile's paths) and its compiler (kernel/Makefile
-# TOOLCHAIN; aarch64's loader is clang + lld-link). Not installed: syft, which make sbom and
-# boot_image need -- it is not packaged; see the message make sbom prints.
-INIT_COMMON  := build-essential make git git-lfs python3 xorriso mtools gdisk dosfstools fdisk \
+# TOOLCHAIN; aarch64's loader is clang + lld-link).
+# Not packaged, so downloaded, checked against the SHA-256 below and installed: syft (make sbom,
+# boot_image; the version sbom.spdx was made with) and Isabelle/HOL (isabelle build -D proof/;
+# the version proof/COVERAGE.md names). The archives are kept in build/cache/downloads and the
+# tools in build/cache/tools, which make clean keeps; each is linked into /usr/local/bin. syft's
+# sums are its release's checksums.txt; Isabelle publishes none, so its sums are of the archives
+# as downloaded on 2026-11-06 -- a download that differs is refused.
+INIT_COMMON  := build-essential make git git-lfs python3 curl ca-certificates xorriso mtools gdisk dosfstools fdisk \
                 pandoc latexmk texlive-xetex texlive-latex-base texlive-latex-recommended \
                 texlive-latex-extra texlive-pictures texlive-fonts-recommended lmodern \
                 fonts-dejavu fonts-dejavu-extra doxygen graphviz
@@ -256,6 +264,36 @@ INIT_ARCHES  := $(subst $(comma),$(space),$(ARCH))
 INIT_BAD     := $(filter-out amd64 aarch64 riscv64,$(INIT_ARCHES))
 SUDO         := $(if $(filter 0,$(shell id -u)),,sudo)
 
+# The host the tools run on, not the ISA being built for: syft's and Isabelle's names for it.
+INIT_HOST    := $(shell uname -m)
+SYFT_VERSION := 1.52.0
+SYFT_ARCH    := $(if $(filter aarch64 arm64,$(INIT_HOST)),arm64,amd64)
+SYFT_TGZ     := syft_$(SYFT_VERSION)_linux_$(SYFT_ARCH).tar.gz
+SYFT_URL     := https://github.com/anchore/syft/releases/download/v$(SYFT_VERSION)/$(SYFT_TGZ)
+SYFT_SHA_amd64 := caeedb81fb0491615f1ebd1761e4145d41ee86dd2cc7bf80669f9f5ad9d6133d
+SYFT_SHA_arm64 := c46d5e4c28e12aa4c5becfaa343ef1c7f89045b6b895f2c21d471c62db09c706
+ISABELLE     := Isabelle2025-2
+ISABELLE_TGZ := $(ISABELLE)_$(if $(filter aarch64 arm64,$(INIT_HOST)),linux_arm,linux).tar.gz
+ISABELLE_URL := https://isabelle.in.tum.de/website-$(ISABELLE)/dist/$(ISABELLE_TGZ)
+ISABELLE_SHA_linux     := a20a507bc7c1270d8be96a9f3fbec06345387789d2dc2c4d3df6260d47bfb33c
+ISABELLE_SHA_linux_arm := 650a9669b4a087675afb34294d82ded2f0704d47d580dd9ed45cddc9f1764bdd
+INIT_DL      := build/cache/downloads
+INIT_TOOLS   := build/cache/tools
+
+# $(call fetch,file,url,sha256): the archive in $(INIT_DL), downloaded unless it is there and
+# its sum is right; a download whose sum is wrong is deleted and the build stops.
+define fetch
+	@mkdir -p $(INIT_DL)
+	@if ! echo "$(3)  $(INIT_DL)/$(1)" | sha256sum -c --status 2>/dev/null; then \
+	    echo "  FETCH   $(2)"; \
+	    curl -fsSL --retry 3 -o $(INIT_DL)/$(1).part $(2) && mv $(INIT_DL)/$(1).part $(INIT_DL)/$(1); \
+	    echo "$(3)  $(INIT_DL)/$(1)" | sha256sum -c --status || { \
+	        echo "init: $(1) does not have the SHA-256 this Makefile expects -- deleted, not installed"; \
+	        rm -f $(INIT_DL)/$(1); exit 1; }; \
+	fi
+	@echo "  OK      $(1) (sha256 $(3))"
+endef
+
 init:
 	@[ -n "$(INIT_ARCHES)" ] && [ -z "$(INIT_BAD)" ] || { \
 	    echo "Usage: make ARCH=<amd64|aarch64|riscv64>[,...] init   (e.g. ARCH=amd64,aarch64,riscv64)"; exit 1; }
@@ -265,8 +303,18 @@ init:
 	$(SUDO) env DEBIAN_FRONTEND=noninteractive apt-get install -y -qq \
 	    $(INIT_COMMON) $(foreach a,$(INIT_ARCHES),$(INIT_$(a)))
 	git lfs install --local
+	$(call fetch,$(SYFT_TGZ),$(SYFT_URL),$(SYFT_SHA_$(SYFT_ARCH)))
+	@mkdir -p $(INIT_TOOLS)/syft-$(SYFT_VERSION)
+	tar -xzf $(INIT_DL)/$(SYFT_TGZ) -C $(INIT_TOOLS)/syft-$(SYFT_VERSION) syft
+	$(SUDO) ln -sf $(abspath $(INIT_TOOLS))/syft-$(SYFT_VERSION)/syft /usr/local/bin/syft
+	$(call fetch,$(ISABELLE_TGZ),$(ISABELLE_URL),$(ISABELLE_SHA_$(patsubst $(ISABELLE)_%.tar.gz,%,$(ISABELLE_TGZ))))
+	@[ -x $(INIT_TOOLS)/$(ISABELLE)/bin/isabelle ] || { mkdir -p $(INIT_TOOLS) && tar -xzf $(INIT_DL)/$(ISABELLE_TGZ) -C $(INIT_TOOLS); }
+	$(SUDO) ln -sf $(abspath $(INIT_TOOLS))/$(ISABELLE)/bin/isabelle /usr/local/bin/isabelle
+	@syft version | sed -n 's/^Version: */  syft    /p'
+	@echo "  isabelle $$(isabelle version)"
 	@echo ""
-	@echo "Ready for $(INIT_ARCHES): make ARCH=<arch> clean qemu, make -C v4 test, make docs"
+	@echo "Ready for $(INIT_ARCHES): make ARCH=<arch> clean qemu, make -C v4 test, make docs,"
+	@echo "  make sbom, isabelle build -D proof/"
 
 help:
 	@sed -n '/^# TARGET is/,/^# =====/p' Makefile | sed '$$d; s/^# \{0,1\}//'