diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml
index 0e502f296cbc..77896a76dd6d 100644
--- a/.github/workflows/build-template.yml
+++ b/.github/workflows/build-template.yml
@@ -308,12 +308,31 @@ jobs:
         run: |
           build/$TARGET_STAGE/bin/lean --stats src/Lean.lean
         if: ${{ !matrix.cross }}
+      # Tests must not write into the checked-in source tree; scratch output belongs in an
+      # ignored path. Making tracked files read-only catches a test that edits one even if it
+      # restores the file afterwards, which the tree comparison below cannot see.
+      - name: Protect Source Tree
+        run: |
+          git status --porcelain -unormal | sort > "$RUNNER_TEMP/tree-before"
+          git ls-files -z | xargs -0 chmod a-w
+        if: matrix.test
       - name: Test
         id: test
         run: |
           ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
         if: matrix.test
+      # restore write access before any later step (stage 2, benchmarks, `update-stage0`) runs
+      - name: Unprotect Source Tree
+        run: git ls-files -z | xargs -0 chmod u+w
+        if: always() && matrix.test
+      - name: Check Source Tree Clean
+        run: |
+          git status --porcelain -unormal | sort > "$RUNNER_TEMP/tree-after"
+          diff -u "$RUNNER_TEMP/tree-before" "$RUNNER_TEMP/tree-after" && exit 0
+          echo "::error::the test suite left files in the checked-in source tree; write them to an ignored path instead"
+          exit 1
+        if: matrix.test && steps.test.conclusion != 'skipped'
       # copy failed tests' output into the `<failure>` elements shown by the test summary
       - name: Embed Test Output
         run: |
diff --git a/tests/README.md b/tests/README.md
index 1bfc07a0ba10..5f0c989dfe52 100644
--- a/tests/README.md
+++ b/tests/README.md
@@ -145,6 +145,22 @@ Otherwise, create a new test directory or pile:
    by updating the directory structure section above.
 5. Optionally update [`lint.py`](lint.py) if it makes sense.
 
+### Keep the source tree clean
+
+A test may not write into the checked-in source tree. CI enforces this by making tracked files
+read-only for the duration of the test run and by comparing `git status` before and after, so a
+test that violates it fails even if it tidies up afterwards.
+
+In practice this means:
+
+* Scratch output must land in an ignored path. Follow the pile's convention where there is one:
+  the `_tmp_` prefix in [`compile`](compile/.gitignore) and [`compile_bench`](compile_bench/.gitignore),
+  `produced.*` under [`lake`](lake/.gitignore) and [`pkg`](pkg/.gitignore). Otherwise add a
+  `.gitignore` entry next to the test.
+* A test that needs to edit its own inputs, or to initialize a Git repository, must work on a
+  copy. Lake tests have `copy_to_work` in [`lake/tests/common.sh`](lake/tests/common.sh) for this;
+  it copies into the ignored `work/` directory and `cd`s there.
+
 ## How to write a benchmark?
 
 When writing a benchmark, consider that most benchmarks are also executed as tests.
diff --git a/tests/bench/size/.gitignore b/tests/bench/size/.gitignore
new file mode 100644
index 000000000000..500b4a049a4a
--- /dev/null
+++ b/tests/bench/size/.gitignore
@@ -0,0 +1 @@
+/install/
diff --git a/tests/compile/compact_closure.lean b/tests/compile/compact_closure.lean
index e5113712ecc2..b3f9d76561c2 100644
--- a/tests/compile/compact_closure.lean
+++ b/tests/compile/compact_closure.lean
@@ -7,7 +7,7 @@ Tests `CompactedRegion.save`/`read` with `allowClosures := true`: closures (with
 are serialized in the `v3` olean format and round-trip within the same process.
 -/
 unsafe def main : IO Unit := do
-  let tmpFile : System.FilePath := "./_compact_closure_test.olean"
+  let tmpFile : System.FilePath := "./_tmp_compact_closure_test.olean"
 
   -- Simple closure with captured string
   let captured := "hello"
diff --git a/tests/compile/compact_closure_cross.lean b/tests/compile/compact_closure_cross.lean
index 0fd9754363f9..2caf13ccdbd5 100644
--- a/tests/compile/compact_closure_cross.lean
+++ b/tests/compile/compact_closure_cross.lean
@@ -8,7 +8,7 @@ loads and runs correctly in a *separate* process: the `v3` lib relocation table
 closure's fn pointer to the loader process's address space.
 -/
 unsafe def main (args : List String) : IO UInt32 := do
-  let tmpFile : System.FilePath := "./_compact_closure_cross_test.olean"
+  let tmpFile : System.FilePath := "./_tmp_compact_closure_cross_test.olean"
 
   match args with
   | ["save"] =>
diff --git a/tests/lake/tests/clone/.gitignore b/tests/lake/tests/clone/.gitignore
index e92569d01017..63dc061bdd94 100644
--- a/tests/lake/tests/clone/.gitignore
+++ b/tests/lake/tests/clone/.gitignore
@@ -1 +1,2 @@
 /hello
+/lean-toolchain
diff --git a/tests/lake/tests/common.sh b/tests/lake/tests/common.sh
index aa08e53381f3..903de68b3728 100644
--- a/tests/lake/tests/common.sh
+++ b/tests/lake/tests/common.sh
@@ -46,6 +46,17 @@ else
 fi
 norm_dirname() { norm_path "$(dirname -- "$1")";  }
 
+# Copy the given paths into the ignored `work/` directory and `cd` into it, so that tests
+# which mutate their inputs or initialize a Git repository leave the checked-in source tree
+# untouched. The copies are made writable because `cp` propagates the source mode and CI
+# runs the suite with tracked files read-only.
+copy_to_work() {
+  mkdir -p work
+  cp -r "$@" work/
+  chmod -R u+w work
+  cd work
+}
+
 init_git() {
   echo "# initialize test repository"
   set -x
diff --git a/tests/lake/tests/init/.gitignore b/tests/lake/tests/init/.gitignore
index 30f8a8f2777d..d5f9d151d6e3 100644
--- a/tests/lake/tests/init/.gitignore
+++ b/tests/lake/tests/init/.gitignore
@@ -9,3 +9,4 @@
 /meta
 /qed-lax
 /qed
+/mathlib_standards
diff --git a/tests/lake/tests/manifest/.gitignore b/tests/lake/tests/manifest/.gitignore
new file mode 100644
index 000000000000..15ffae388e05
--- /dev/null
+++ b/tests/lake/tests/manifest/.gitignore
@@ -0,0 +1 @@
+/lake-packages/
diff --git a/tests/lake/tests/manifest/test.sh b/tests/lake/tests/manifest/test.sh
index 0737b83a9fbd..2ccada6c8009 100755
--- a/tests/lake/tests/manifest/test.sh
+++ b/tests/lake/tests/manifest/test.sh
@@ -5,10 +5,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r bar foo lakefile.lean lake-manifest-*.json "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work bar foo lakefile.lean lake-manifest-*.json
 
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the bar repository on each test. This requires updating the
diff --git a/tests/lake/tests/noRelease/test.sh b/tests/lake/tests/noRelease/test.sh
index 73aeef8c5cb2..5643c25d4a49 100755
--- a/tests/lake/tests/noRelease/test.sh
+++ b/tests/lake/tests/noRelease/test.sh
@@ -5,10 +5,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r dep lakefile.lean Test.lean "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work dep lakefile.lean Test.lean
 
 NO_BUILD_CODE=3
 
diff --git a/tests/lake/tests/packageOverrides/test.sh b/tests/lake/tests/packageOverrides/test.sh
index 4d07ca20ab68..12c02c7d2106 100755
--- a/tests/lake/tests/packageOverrides/test.sh
+++ b/tests/lake/tests/packageOverrides/test.sh
@@ -5,10 +5,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r bar1 bar2 foo lakefile.lean packages.json "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work bar1 bar2 foo lakefile.lean packages.json
 
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the `bar1` repository on each test.
diff --git a/tests/lake/tests/rebuild/.gitignore b/tests/lake/tests/rebuild/.gitignore
index 31b4bffdf182..6a83bead6b6e 100644
--- a/tests/lake/tests/rebuild/.gitignore
+++ b/tests/lake/tests/rebuild/.gitignore
@@ -1,2 +1,2 @@
+/Foo/
 /Foo.lean
-/Foo/Test.lean
diff --git a/tests/lake/tests/reservoirConfig/test.sh b/tests/lake/tests/reservoirConfig/test.sh
index 7a8a027ba149..0c6979102f08 100755
--- a/tests/lake/tests/reservoirConfig/test.sh
+++ b/tests/lake/tests/reservoirConfig/test.sh
@@ -5,10 +5,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r lakefile.lean expected.json "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work lakefile.lean expected.json
 
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the repository on each test.
diff --git a/tests/lake/tests/shake/.gitignore b/tests/lake/tests/shake/.gitignore
deleted file mode 100644
index 94e6663c0cfb..000000000000
--- a/tests/lake/tests/shake/.gitignore
+++ /dev/null
@@ -1,11 +0,0 @@
-.lake/
-lake-manifest.json
-lake-packages/
-produced.out
-# Working files copied from input/
-/lakefile.toml
-/lean-toolchain
-/Main.lean
-/MainDep.lean
-/Lib/
-/lean-toolchain
diff --git a/tests/lake/tests/shake/DepMain.lean b/tests/lake/tests/shake/DepMain.lean
deleted file mode 100644
index 3942ecb0a47c..000000000000
--- a/tests/lake/tests/shake/DepMain.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-module
-
-import Main
-
-def myVal := mainVal
diff --git a/tests/lake/tests/shake/clean.sh b/tests/lake/tests/shake/clean.sh
index 853e580d4e7c..3f789d9f7ba2 100755
--- a/tests/lake/tests/shake/clean.sh
+++ b/tests/lake/tests/shake/clean.sh
@@ -1,4 +1,3 @@
 #!/usr/bin/env bash
-rm -rf .lake lake-manifest.json lake-packages
-rm -f lakefile.toml Main.lean
-rm -rf Lib
+rm -rf work
+rm -f produced.out
diff --git a/tests/lake/tests/shake/test.sh b/tests/lake/tests/shake/test.sh
index 559d14be2d49..06c130ed7b55 100755
--- a/tests/lake/tests/shake/test.sh
+++ b/tests/lake/tests/shake/test.sh
@@ -5,8 +5,8 @@ source ../common.sh
 
 # Test the `lake shake` command
 
-# Copy input project to working directory
-cp -r input/* .
+# `shake --fix` rewrites the sources it is given, so work on a copy
+copy_to_work input/*
 
 # Build the project first (shake needs .olean files)
 test_run build
@@ -20,11 +20,12 @@ match_pat 'remove.*Lib.B' produced.out
 lake_out shake --only DepMain
 
 # Test --fix mode: apply the fixes and verify the result
+cd ..
 ./clean.sh
-cp -r input/* .
+copy_to_work input/*
 test_run build
 test_run shake --fix Main
 test_run build
 
 # Verify Main.lean matches expected
-check_diff expected/Main.lean Main.lean
+check_diff ../expected/Main.lean Main.lean
diff --git a/tests/lake/tests/srcHash/test.sh b/tests/lake/tests/srcHash/test.sh
index 53a4839fe370..3ddcad909c8b 100755
--- a/tests/lake/tests/srcHash/test.sh
+++ b/tests/lake/tests/srcHash/test.sh
@@ -15,10 +15,7 @@ source ../common.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r dep lakefile.toml "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work dep lakefile.toml
 
 # Initialize the dependency
 echo "# SETUP: Create v1"
diff --git a/tests/lake/tests/toml/.gitignore b/tests/lake/tests/toml/.gitignore
new file mode 100644
index 000000000000..f82ed5e3d438
--- /dev/null
+++ b/tests/lake/tests/toml/.gitignore
@@ -0,0 +1 @@
+/toml-test/
diff --git a/tests/lake/tests/updateUnknown/clean.sh b/tests/lake/tests/updateUnknown/clean.sh
index ba9a125c4540..6107fef81887 100755
--- a/tests/lake/tests/updateUnknown/clean.sh
+++ b/tests/lake/tests/updateUnknown/clean.sh
@@ -1,3 +1,2 @@
-rm -rf .lake dep/.lake
-rm -f lake-manifest.json dep/lake-manifest.json
+rm -rf work
 rm -f produced.out
diff --git a/tests/lake/tests/updateUnknown/test.sh b/tests/lake/tests/updateUnknown/test.sh
index e8d82eb6266d..a67e6d130631 100755
--- a/tests/lake/tests/updateUnknown/test.sh
+++ b/tests/lake/tests/updateUnknown/test.sh
@@ -2,6 +2,9 @@
 source ../common.sh
 ./clean.sh
 
+# The manifest edit below rewrites `lakefile.toml`, so work on a copy
+copy_to_work lakefile.toml dep
+
 # Test that `lake update <pkg>` errors on unknown package names (typos and
 # case mismatches). Names that are current root requires or already in the
 # manifest are accepted (so selective update can still drop a removed require).
@@ -28,6 +31,3 @@ test_run update dep --keep-toolchain
 mv lakefile.toml.bak lakefile.toml
 
 test_run update --keep-toolchain
-
-# Cleanup
-./clean.sh
diff --git a/tests/lake/tests/versionTags/test.sh b/tests/lake/tests/versionTags/test.sh
index 3b2961b4593c..9bdfbff89d0f 100755
--- a/tests/lake/tests/versionTags/test.sh
+++ b/tests/lake/tests/versionTags/test.sh
@@ -4,10 +4,7 @@ source ./clean.sh
 
 # Copy test data to a working directory to avoid initializing a Git repository
 # inside the checked-in source tree
-WORK_DIR="$PWD/work"
-mkdir -p "$WORK_DIR"
-cp -r lakefile.lean "$WORK_DIR/"
-cd "$WORK_DIR"
+copy_to_work lakefile.lean
 
 # Since committing a Git repository to a Git repository is not well-supported,
 # We reinitialize the repository on each test.
diff --git a/tests/pkg/.gitignore b/tests/pkg/.gitignore
index 484bdc670f19..dc1689c1ecaa 100644
--- a/tests/pkg/.gitignore
+++ b/tests/pkg/.gitignore
@@ -1 +1,2 @@
 lake-manifest.json
+produced.*
diff --git a/tests/pkg/def_clash/.gitignore b/tests/pkg/def_clash/.gitignore
deleted file mode 100644
index 10ed5ae23f8d..000000000000
--- a/tests/pkg/def_clash/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-produced.out
diff --git a/tests/pkg/ver_clash/DiamondExample-D/.gitignore b/tests/pkg/ver_clash/DiamondExample-D/.gitignore
index 64698fc800e4..2b0095269262 100644
--- a/tests/pkg/ver_clash/DiamondExample-D/.gitignore
+++ b/tests/pkg/ver_clash/DiamondExample-D/.gitignore
@@ -1,2 +1 @@
 .lake
-produced.out