diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md
index 2ad6c96c8a..dc83c7ac81 100644
--- a/.github/CODE_QUALITY.md
+++ b/.github/CODE_QUALITY.md
@@ -15,6 +15,10 @@ Lean Pool uses deterministic CI for mechanical quality checks and LLM review for
 - `lake exe lint-style` on `LeanPool`
 - `python -m lean_pool.quality --repo ..`
 
+With `warningAsError = true` in `lakefile.toml`, every Lean warning is a
+compile error (locally too). The warning scan over the build log remains for
+warnings Lake itself prints.
+
 The Lean workflow runs on Lean, Lake, project metadata, quality-checker, and workflow changes. It restores and saves Lake caches and pulls Mathlib oleans with `lake exe cache get` when the cache is cold.
 
 Lean Pool uses one `public import LeanPool.<Project>.Imports` per project in
diff --git a/AGENTS.md b/AGENTS.md
index 3c2bf66ec8..2f18b3ee51 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -148,6 +148,8 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 **Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter` and `lake exe lint-style` on `LeanPool`, the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md).
 
+Warnings are not allowed. `lakefile.toml` sets `warningAsError = true`, so any warning (an unused variable, a deprecated lemma, a linter hit) fails `lake build` on your machine just as it does in CI. Fix the code; suppressing the warning is not allowed either.
+
 **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`.
 
 ## Coding guidelines
diff --git a/CLAUDE.md b/CLAUDE.md
index 3c2bf66ec8..2f18b3ee51 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -148,6 +148,8 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 **Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter` and `lake exe lint-style` on `LeanPool`, the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md).
 
+Warnings are not allowed. `lakefile.toml` sets `warningAsError = true`, so any warning (an unused variable, a deprecated lemma, a linter hit) fails `lake build` on your machine just as it does in CI. Fix the code; suppressing the warning is not allowed either.
+
 **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`.
 
 ## Coding guidelines
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 1f2f7e212c..2cb4e6e4d0 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -49,6 +49,8 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 
 **Lean.** CI runs `lake exe mk_all --check`, `lake build LeanPool`, `lake exe runLinter` and `lake exe lint-style` on `LeanPool`, the quality checker (see [`lean_action_ci.yml`](.github/workflows/lean_action_ci.yml)). Conventions live in [`.github/CODE_QUALITY.md`](.github/CODE_QUALITY.md).
 
+Warnings are not allowed. `lakefile.toml` sets `warningAsError = true`, so any warning (an unused variable, a deprecated lemma, a linter hit) fails `lake build` on your machine just as it does in CI. Fix the code; suppressing the warning is not allowed either.
+
 **Python.** From `python/`: `uv run ruff check`, `uv run ruff format`, and `uv run --group test pytest`.
 
 ## Coding guidelines
diff --git a/lakefile.toml b/lakefile.toml
index b1ca063e71..c602afbc90 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -9,6 +9,10 @@ pp.unicode.fun = true # pretty-prints `fun a ↦ b`
 relaxedAutoImplicit = false
 weak.linter.mathlibStandardSet = true
 maxSynthPendingDepth = 3
+# Every warning is a compile error, so local builds fail exactly like CI and a
+# cached build can never hide one. Pool files cannot override it: option changes
+# are banned by the quality gate.
+warningAsError = true
 
 [[require]]
 name = "TauCeti"