diff --git a/AGENTS.md b/AGENTS.md
index e6d83bd..6610f29 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -71,7 +71,9 @@ This is a Phoenix Liveview monorepo, the blogging library is in blogex, the appl
 Main make targets:
 
 - `make check` - cheap static gate for both apps (no DB): app `credo --strict` +
-  format, blogex compile (warnings fatal) + format, then `scripts/check-pins.sh`
+  format **check** (`mix format --check-formatted`), blogex compile (warnings
+  fatal) + format **check**, then `scripts/check-pins.sh`. It never rewrites
+  files.
 - `make precommit` - alias of `check`; fast, safe to run on every commit
 - `make test` - both suites (app needs PostgreSQL on localhost:5432)
 - `make verify` - the Lens pass: `check`, then per-app heavy sensors and both suites
@@ -86,6 +88,10 @@ no coverage, about a second. `make precommit` is the same target. Per app,
 `mix precommit` (run inside `app/` or `blogex/`) is the fuller loop: compile with
 warnings fatal, format, test. Run these as often as you like while working.
 
+`make check` never writes files. A formatting failure means run `make format`
+(both apps). The mutating loops are the explicit ones: `make format` and the
+per-app `mix precommit`, which still formats as you work.
+
 **Lens pass (every push, and before handing off).** `make verify` runs `check`
 first (cheapest), then per app: one suite run that exports its coverage, then
 that app's sensors (sobelow, coverage, CRAP, mutation, as those yaks land), which
diff --git a/Makefile b/Makefile
index f4ef9f1..cef69d1 100644
--- a/Makefile
+++ b/Makefile
@@ -62,9 +62,11 @@ test:
 test-elisp:
 	emacs --batch -Q -l org -l ox-md -l scripts/roam-export-blog.el -l scripts/roam-export-blog-test.el -f ert-run-tests-batch-and-exit
 
-# Format code
+# Format code in both apps. Mutating convenience target: `check` (and so
+# `verify`) never writes. If a gate fails on formatting, run this.
 format:
-	@make -C app format
+	@$(MAKE) -C app MISE_BIN=$(MISE_BIN) format
+	@$(MAKE) -C blogex MISE_BIN=$(MISE_BIN) format
 
 # Serve the app
 serve:
diff --git a/app/Makefile b/app/Makefile
index bf9c005..db6e82b 100644
--- a/app/Makefile
+++ b/app/Makefile
@@ -3,10 +3,12 @@
 MISE_BIN ?= mise
 MISE_EXEC = $(MISE_BIN) exec --
 
-.PHONY: check precommit deps assets compile test test.coverage coverage crap format credo verify
+.PHONY: check precommit deps assets compile test test.coverage coverage crap format format.check credo verify
 
-# Run all static analysis checks (no database required)
-check: credo format
+# Run all static analysis checks (no database required). `format.check` only
+# reports: a gate that rewrites the files it judges can never fail. Fix
+# formatting with `make format`.
+check: credo format.check
 
 # Precommit target for CI/pre-commit hooks
 precommit: check compile
@@ -62,10 +64,18 @@ crap:
 	@test -f cover/default.coverdata || { echo "crap: no exported coverage - run 'make test.coverage' first" >&2; exit 1; }
 	MIX_ENV=test $(MISE_EXEC) mix crap
 
-# Format code
+# Format code. MUTATES the tree; deliberately not part of `check` (nor of the
+# Lens pass), which must never write: a gate that fixes what it judges can never
+# fail, and would dirty the tree a push is about to send. `make check` uses
+# `format.check` below instead.
 format:
 	$(MISE_EXEC) mix format
 
+# Verify formatting without writing. Fails with the offending files, so the fix
+# is explicit: run `make format` (or `make -C app format`).
+format.check:
+	$(MISE_EXEC) mix format --check-formatted
+
 # =============================================================================
 # Playwright e2e browser tests
 # =============================================================================
diff --git a/blogex/Makefile b/blogex/Makefile
index 879afb9..bcce088 100644
--- a/blogex/Makefile
+++ b/blogex/Makefile
@@ -3,15 +3,17 @@
 MISE_BIN ?= mise
 MISE_EXEC = $(MISE_BIN) exec --
 
-.PHONY: check precommit deps compile test test.coverage coverage crap format verify
+.PHONY: check precommit deps compile test test.coverage coverage crap format format.check verify
 
 # Cheap static gate for this library (no database, no coverage). Runs from the
-# root `make check`, which loops app then blogex.
+# root `make check`, which loops app then blogex. `format.check` only reports:
+# a gate that rewrites the files it judges can never fail. Fix formatting with
+# `make format`.
 #
 # Sensor slot: add `credo` once the "credo strict, tuned config (both apps)"
 # yak lands blogex's credo dep + .credo.exs. Do not list it before then — a
 # gate that claims a check it did not run is worse than no gate.
-check: compile format
+check: compile format.check
 
 # Per-app precommit loop: same target name and alias shape as app/, so both
 # apps share one habit (compile --warning-as-errors, format, test).
@@ -58,10 +60,18 @@ crap:
 	@test -f cover/default.coverdata || { echo "crap: no exported coverage - run 'make test.coverage' first" >&2; exit 1; }
 	MIX_ENV=test $(MISE_EXEC) mix crap
 
-# Format code
+# Format code. MUTATES the tree; deliberately not part of `check` (nor of the
+# Lens pass), which must never write: a gate that fixes what it judges can never
+# fail, and would dirty the tree a push is about to send. `make check` uses
+# `format.check` below instead.
 format:
 	$(MISE_EXEC) mix format
 
+# Verify formatting without writing. Fails with the offending files, so the fix
+# is explicit: run `make format` (or `make -C blogex format`).
+format.check:
+	$(MISE_EXEC) mix format --check-formatted
+
 # =============================================================================
 # Lens pass (heavy checks; root `make verify` runs this before every push)
 # =============================================================================