diff --git a/ci/plugins/mzcompose/hooks/command b/ci/plugins/mzcompose/hooks/command
index 9fd0938b3c561..b0e74df8d7a7e 100644
--- a/ci/plugins/mzcompose/hooks/command
+++ b/ci/plugins/mzcompose/hooks/command
@@ -444,6 +444,7 @@ cleanup() {
     && [ "$BUILDKITE_LABEL" != "Parallel Benchmark against QA Canary Environment" ] \
     && [ "$BUILDKITE_LABEL" != "Parallel Benchmark against QA Benchmarking Staging Environment" ] \
     && [ "$BUILDKITE_LABEL" != ":rust: Miri test (full)" ] \
+    && [ "$BUILDKITE_LABEL" != "Lean models" ] \
     && [[ ! "$BUILDKITE_LABEL" =~ Terraform\ .* ]] \
     && [[ ! "$BUILDKITE_LABEL" =~ Orchestratord\ .* ]] \
     && [[ ! "$BUILDKITE_LABEL" =~ Cluster\ spec\ sheet.* ]] \
diff --git a/ci/test/lint-main/checks/check-copyright.sh b/ci/test/lint-main/checks/check-copyright.sh
index 7ed9a509609a5..d415a11ddfb6a 100755
--- a/ci/test/lint-main/checks/check-copyright.sh
+++ b/ci/test/lint-main/checks/check-copyright.sh
@@ -32,6 +32,7 @@ copyright_files=$(grep -vE \
     -e '(^|/)Cargo\.lock$' \
     -e '(^|/)types\.lock$' \
     -e '(^|/)\.mzprofile$' \
+    -e '(^|/)lean-toolchain$' \
     -e '^src/mz-deploy/src/cli/scaffold/gitignore$' \
     -e '^test/mz-deploy/projects/multi-profile/v1/models/app/core/ambiguous\.sql$' \
     -e '^about\.toml$' \
diff --git a/ci/test/pipeline.template.yml b/ci/test/pipeline.template.yml
index e64cff9510b85..07a48b84b491c 100644
--- a/ci/test/pipeline.template.yml
+++ b/ci/test/pipeline.template.yml
@@ -668,6 +668,18 @@ steps:
     agents:
       queue: hetzner-aarch64-4cpu-8gb
 
+  - id: lean
+    label: Lean models
+    depends_on: build-aarch64
+    timeout_in_minutes: 30
+    plugins:
+      - ./ci/plugins/mzcompose:
+          composition: lean
+    agents:
+      queue: hetzner-aarch64-4cpu-8gb
+    coverage: skip
+    sanitizer: skip
+
   - id: mcp
     label: MCP e2e
     depends_on: build-aarch64
diff --git a/misc/images/lean/.gitignore b/misc/images/lean/.gitignore
new file mode 100644
index 0000000000000..13d97841216ee
--- /dev/null
+++ b/misc/images/lean/.gitignore
@@ -0,0 +1,3 @@
+/lean-toolchain
+/lakefile.toml
+/lake-manifest.json
diff --git a/misc/images/lean/Dockerfile b/misc/images/lean/Dockerfile
new file mode 100644
index 0000000000000..1af5e087847e5
--- /dev/null
+++ b/misc/images/lean/Dockerfile
@@ -0,0 +1,76 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+# Lean 4 toolchain for the Lake project in `misc/lean`. The toolchain comes
+# from that project's `lean-toolchain`, so a local elan install and this image
+# use the same Lean version. The project's dependencies are built into
+# `/workspace/.lake` at image build time.
+
+MZFROM debian-base
+
+ARG ELAN_VERSION=v4.2.4
+
+ENV ELAN_HOME=/opt/elan
+ENV PATH=$ELAN_HOME/bin:$PATH
+
+RUN apt-get update \
+    && TZ=UTC DEBIAN_FRONTEND=noninteractive apt-get install -y --no-install-recommends \
+        ca-certificates \
+        curl \
+        git \
+        jq \
+    && apt-get clean \
+    && rm -rf /var/lib/apt/lists/*
+
+COPY lean-toolchain /workspace/
+
+# NOTE: the toolchain is kept whole although checking proofs needs only part of
+# it. Batteries, a dependency of Aesop and Mathlib, has the `runLinter`
+# executable among its default targets. Linking it needs the toolchain's static
+# libraries and LLVM, so removing them breaks the dependency build below.
+RUN case "$(uname -m)" in \
+        x86_64) triple=x86_64-unknown-linux-gnu; sha256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 ;; \
+        aarch64) triple=aarch64-unknown-linux-gnu; sha256=05febd124d84ebf994b2e7479922a5650b1e950c17ae3bd1ddd776b65bb72bf9 ;; \
+        *) echo "unsupported architecture $(uname -m)" >&2; exit 1 ;; \
+    esac \
+    && curl -fsSL -o /tmp/elan.tar.gz \
+        "https://github.com/leanprover/elan/releases/download/$ELAN_VERSION/elan-$triple.tar.gz" \
+    && echo "$sha256  /tmp/elan.tar.gz" | sha256sum -c - \
+    && tar -C /tmp -xzf /tmp/elan.tar.gz \
+    && /tmp/elan-init -y --no-modify-path --default-toolchain "$(cat /workspace/lean-toolchain)" \
+    && rm /tmp/elan.tar.gz /tmp/elan-init \
+    && elan toolchain install "$(cat /workspace/lean-toolchain)" \
+    && chmod -R a+rX "$ELAN_HOME" \
+    && lean --version
+
+# Git refuses repositories owned by a different uid than the one running it,
+# and Lake then re-clones the baked dependencies.
+RUN git config --system --add safe.directory '*'
+
+WORKDIR /workspace
+
+COPY lakefile.toml lake-manifest.json /workspace/
+
+# Builds the dependency closure. Building the placeholder library alone only
+# clones the dependencies, because Lake compiles just the modules a target
+# imports, so each package's default targets are built by name. NOTE: a
+# package that declares no default targets builds nothing here and compiles
+# on every run instead. One `lake build` for all packages fails if any of them
+# fails. With no dependencies it builds the placeholder.
+RUN mkdir Mz \
+    && touch Mz.lean \
+    && targets="$(jq -r '.packages[] | "@" + .name' lake-manifest.json)" \
+    && lake build $targets \
+    && rm -rf Mz Mz.lean .lake/build \
+    && chmod -R a+rwX /workspace
+
+COPY mz-lake /usr/local/bin/
+
+ENTRYPOINT ["mz-lake"]
+CMD ["build"]
diff --git a/misc/images/lean/mz-lake b/misc/images/lean/mz-lake
new file mode 100755
index 0000000000000..c58d87f97da96
--- /dev/null
+++ b/misc/images/lean/mz-lake
@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+#
+# mz-lake: copy the Lake project mounted at /src into /workspace and run
+# `lake` there with the given arguments.
+
+set -euo pipefail
+
+# Mounting the project over /workspace would hide /workspace/.lake, which
+# holds the dependency closure built into the image. The host's own .lake is
+# skipped for the same reason. The entries are copied one by one because
+# copying `.` itself makes a non-root user try to change the mode and mtime
+# of the root-owned /workspace, which fails.
+cd /src
+find . -mindepth 1 -maxdepth 1 ! -name .lake -exec cp -R -t /workspace {} +
+
+cd /workspace
+exec lake "$@"
diff --git a/misc/images/lean/mzbuild.yml b/misc/images/lean/mzbuild.yml
new file mode 100644
index 0000000000000..9c438548ba87d
--- /dev/null
+++ b/misc/images/lean/mzbuild.yml
@@ -0,0 +1,26 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+name: lean
+description: Lean 4 toolchain and dependency closure for the models in misc/lean.
+# Only the files that pin the toolchain and the dependencies are copied, so
+# editing a model does not change the image fingerprint.
+pre-image:
+  - type: copy
+    source: misc/lean
+    destination: .
+    matching: lean-toolchain
+  - type: copy
+    source: misc/lean
+    destination: .
+    matching: lakefile.toml
+  - type: copy
+    source: misc/lean
+    destination: .
+    matching: lake-manifest.json
diff --git a/misc/lean/.gitignore b/misc/lean/.gitignore
new file mode 100644
index 0000000000000..bfb30ec8c762c
--- /dev/null
+++ b/misc/lean/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/misc/lean/Mz.lean b/misc/lean/Mz.lean
new file mode 100644
index 0000000000000..d0ffff89084fe
--- /dev/null
+++ b/misc/lean/Mz.lean
@@ -0,0 +1,10 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+
+import Mz.Collection
diff --git a/misc/lean/Mz/Collection.lean b/misc/lean/Mz/Collection.lean
new file mode 100644
index 0000000000000..4511f4cd8b96e
--- /dev/null
+++ b/misc/lean/Mz/Collection.lean
@@ -0,0 +1,200 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+
+/-!
+# Collections of updates
+
+A collection is a list of `(record, diff)` updates. Its meaning is the
+multiplicity of each record, the sum of that record's diffs. Two collections
+are equivalent when they agree on every multiplicity, regardless of how the
+updates are ordered or split.
+
+`consolidate` merges updates to the same record and drops the ones that cancel.
+It is correct when it preserves every multiplicity, leaves no zero diff, and
+leaves at most one update per record.
+-/
+
+namespace Mz
+
+abbrev Collection (α : Type) := List (α × Int)
+
+namespace Collection
+
+variable {α : Type} [DecidableEq α]
+
+/-- The multiplicity of `x` in `c`. -/
+def count : Collection α → α → Int
+  | [], _ => 0
+  | (a, d) :: rest, x => (if a = x then d else 0) + count rest x
+
+/-- Flips the sign of every diff. -/
+def negate (c : Collection α) : Collection α :=
+  c.map fun (a, d) => (a, -d)
+
+/-- Adds `d` to the update for `a`, dropping that update if it cancels. -/
+def insert (a : α) (d : Int) : Collection α → Collection α
+  | [] => if d = 0 then [] else [(a, d)]
+  | (b, e) :: rest =>
+    if b = a then
+      if d + e = 0 then rest else (a, d + e) :: rest
+    else
+      (b, e) :: insert a d rest
+
+/-- Merges updates to the same record and drops the ones that cancel. -/
+def consolidate : Collection α → Collection α
+  | [] => []
+  | (a, d) :: rest => insert a d (consolidate rest)
+
+theorem count_append (c₁ c₂ : Collection α) (x : α) :
+    count (c₁ ++ c₂) x = count c₁ x + count c₂ x := by
+  induction c₁ with
+  | nil => simp [count]
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    simp [count, ih, Int.add_assoc]
+
+theorem count_negate (c : Collection α) (x : α) :
+    count (negate c) x = -count c x := by
+  induction c with
+  | nil => simp [negate, count]
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    simp only [negate, List.map_cons, count] at ih ⊢
+    rw [ih]
+    split <;> omega
+
+/-- Appending a collection's negation cancels it. -/
+theorem count_append_negate (c : Collection α) (x : α) :
+    count (c ++ negate c) x = 0 := by
+  rw [count_append, count_negate]
+  omega
+
+theorem count_insert (a : α) (d : Int) (c : Collection α) (x : α) :
+    count (insert a d c) x = (if a = x then d else 0) + count c x := by
+  induction c with
+  | nil =>
+    simp only [insert, count]
+    split <;> simp [count, *]
+  | cons u rest ih =>
+    obtain ⟨b, e⟩ := u
+    by_cases hb : b = a
+    · subst hb
+      by_cases hz : d + e = 0
+      · rw [insert, ite_eq_left rfl, ite_eq_left hz, count]
+        by_cases hx : b = x <;> simp [hx] <;> omega
+      · rw [insert, ite_eq_left rfl, ite_eq_right hz, count, count]
+        by_cases hx : b = x <;> simp [hx] <;> omega
+    · rw [insert, ite_eq_right hb, count, count, ih]
+      omega
+
+/-- Consolidation preserves the multiplicity of every record. -/
+theorem count_consolidate (c : Collection α) (x : α) :
+    count (consolidate c) x = count c x := by
+  induction c with
+  | nil => rfl
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    simp only [consolidate, count_insert, ih, count]
+
+/-- Every update has a nonzero diff. -/
+def NoZeros (c : Collection α) : Prop :=
+  ∀ u ∈ c, u.2 ≠ 0
+
+theorem noZeros_insert (a : α) (d : Int) (c : Collection α) (h : NoZeros c) :
+    NoZeros (insert a d c) := by
+  induction c with
+  | nil =>
+    simp only [insert]
+    split
+    · simp [NoZeros]
+    · simp [NoZeros, *]
+  | cons u rest ih =>
+    obtain ⟨b, e⟩ := u
+    have hrest : NoZeros rest := fun v hv => h v (List.mem_cons_of_mem _ hv)
+    have he : e ≠ 0 := h (b, e) List.mem_cons_self
+    simp only [insert]
+    split
+    · split
+      · exact hrest
+      · intro v hv
+        cases List.mem_cons.mp hv with
+        | inl hv => subst hv; assumption
+        | inr hv => exact hrest v hv
+    · intro v hv
+      cases List.mem_cons.mp hv with
+      | inl hv => subst hv; exact he
+      | inr hv => exact ih hrest v hv
+
+/-- Consolidation leaves no update with a zero diff. -/
+theorem noZeros_consolidate (c : Collection α) : NoZeros (consolidate c) := by
+  induction c with
+  | nil => simp [consolidate, NoZeros]
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    exact noZeros_insert a d _ ih
+
+/-- The records that have an update. -/
+def keys (c : Collection α) : List α :=
+  c.map Prod.fst
+
+theorem mem_keys_insert {a x : α} {d : Int} {c : Collection α}
+    (h : x ∈ keys (insert a d c)) : x = a ∨ x ∈ keys c := by
+  induction c with
+  | nil =>
+    simp only [insert] at h
+    split at h <;> simp_all [keys]
+  | cons u rest ih =>
+    obtain ⟨b, e⟩ := u
+    simp only [insert] at h
+    split at h
+    · split at h <;> simp_all [keys]
+    · simp only [keys, List.map_cons, List.mem_cons] at h ⊢
+      rcases h with h | h
+      · exact Or.inr (Or.inl h)
+      · rcases ih h with h | h
+        · exact Or.inl h
+        · exact Or.inr (Or.inr h)
+
+theorem nodup_insert (a : α) (d : Int) (c : Collection α) (h : (keys c).Nodup) :
+    (keys (insert a d c)).Nodup := by
+  induction c with
+  | nil =>
+    simp only [insert]
+    split <;> simp [keys]
+  | cons u rest ih =>
+    obtain ⟨b, e⟩ := u
+    simp only [keys, List.map_cons, List.nodup_cons] at h
+    obtain ⟨hb, hrest⟩ := h
+    simp only [insert]
+    split
+    · subst_vars
+      split
+      · exact hrest
+      · simp only [keys, List.map_cons, List.nodup_cons]
+        exact ⟨hb, hrest⟩
+    · simp only [keys, List.map_cons, List.nodup_cons]
+      refine ⟨fun hmem => ?_, ih hrest⟩
+      rcases mem_keys_insert hmem with h | h
+      · contradiction
+      · exact hb h
+
+/-- Consolidation leaves at most one update per record. -/
+theorem nodup_consolidate (c : Collection α) : (keys (consolidate c)).Nodup := by
+  induction c with
+  | nil => simp [consolidate, keys]
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    exact nodup_insert a d _ ih
+
+example : consolidate ([(1, 2), (2, 1), (1, -2)] : Collection Nat) = [(2, 1)] := by
+  decide
+
+end Collection
+
+end Mz
diff --git a/misc/lean/README.md b/misc/lean/README.md
new file mode 100644
index 0000000000000..7e7206d40f741
--- /dev/null
+++ b/misc/lean/README.md
@@ -0,0 +1,33 @@
+# Lean models
+
+This directory is a Lake project for Lean 4 models of Materialize.
+Each model lives under `Mz/`, and `lake build` checks every module there, whether or not `Mz.lean` imports it.
+The `lean` CI step runs that build, and `warningAsError` in `lakefile.toml` makes any `sorry` or warning fail it.
+`Mz/Collection.lean` is a sample: it models collections of `(record, diff)` updates and proves that consolidation preserves multiplicities.
+
+## Running
+
+Check all models in Docker, the same way CI does:
+
+```sh
+bin/mzcompose --find lean run default
+```
+
+Arguments replace the default `build` and go to `lake`, for example `bin/mzcompose --find lean run default env lean Mz/Collection.lean`.
+Only `lake build` applies the options in `lakefile.toml`, so `lake env lean` reports a `sorry` as a warning and succeeds.
+Separate arguments that start with `-` from the workflow's own options with `--`.
+
+For editor support, install [elan](https://github.com/leanprover/elan) and open this directory.
+elan picks the Lean version from `lean-toolchain`.
+
+## Toolchain and dependencies
+
+The `lean` mzbuild image in `misc/images/lean` installs the toolchain named in `lean-toolchain` and builds the dependencies in `lakefile.toml` and `lake-manifest.json` into the image.
+Those three are the only files from this directory that are inputs to the image, so editing a model reuses the published image.
+To change the Lean version, edit `lean-toolchain`.
+To add a dependency, add a `[[require]]` to `lakefile.toml`, pin it by `rev`, and commit the `lake-manifest.json` that `lake update` writes.
+
+## Checking a model
+
+A proof only says something about the system if the model can fail.
+Before relying on a model, break it in a way the theorems should catch, for example by removing a guard, and confirm the build fails.
diff --git a/misc/lean/lake-manifest.json b/misc/lean/lake-manifest.json
new file mode 100644
index 0000000000000..255f99002a1e0
--- /dev/null
+++ b/misc/lean/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "mz",
+ "lakeDir": ".lake"}
diff --git a/misc/lean/lakefile.toml b/misc/lean/lakefile.toml
new file mode 100644
index 0000000000000..ece1262e8ac67
--- /dev/null
+++ b/misc/lean/lakefile.toml
@@ -0,0 +1,20 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+name = "mz"
+defaultTargets = ["Mz"]
+# Makes `sorry` and every other warning fail the build, so an unfinished
+# proof cannot pass CI.
+leanOptions = { warningAsError = true }
+
+[[lean_lib]]
+name = "Mz"
+# Builds every module under `Mz/`, not only those `Mz.lean` imports, so an
+# unimported model cannot skip the check.
+globs = ["Mz.*"]
diff --git a/misc/lean/lean-toolchain b/misc/lean/lean-toolchain
new file mode 100644
index 0000000000000..ba8ebf2dbaf6a
--- /dev/null
+++ b/misc/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.1
diff --git a/misc/lean/mzcompose b/misc/lean/mzcompose
new file mode 100755
index 0000000000000..1f866645dabc8
--- /dev/null
+++ b/misc/lean/mzcompose
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+#
+# mzcompose — runs Docker Compose with Materialize customizations.
+
+exec "$(dirname "$0")"/../../bin/pyactivate -m materialize.cli.mzcompose "$@"
diff --git a/misc/lean/mzcompose.py b/misc/lean/mzcompose.py
new file mode 100644
index 0000000000000..f4cede04fcf3b
--- /dev/null
+++ b/misc/lean/mzcompose.py
@@ -0,0 +1,32 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+"""
+Builds and checks the Lean 4 models in this directory.
+"""
+
+from materialize.mzcompose.composition import Composition, WorkflowArgumentParser
+from materialize.mzcompose.service import Service
+
+SERVICES = [
+    Service(
+        name="lean",
+        config={
+            "mzbuild": "lean",
+            "volumes": [".:/src:ro"],
+        },
+    ),
+]
+
+
+def workflow_default(c: Composition, parser: WorkflowArgumentParser) -> None:
+    """Run `lake` with the given arguments, `lake build` by default."""
+    parser.add_argument("lake_args", nargs="*", default=["build"])
+    args = parser.parse_args()
+    c.run("lean", *args.lake_args, rm=True)
diff --git a/misc/python/materialize/mzbuild.py b/misc/python/materialize/mzbuild.py
index b3026b8bc16f5..34f5b5f30a67a 100644
--- a/misc/python/materialize/mzbuild.py
+++ b/misc/python/materialize/mzbuild.py
@@ -602,14 +602,18 @@ def __init__(self, rd: RepositoryDetails, path: Path, config: dict[str, Any]):
 
     def run(self, prep: Any) -> None:
         super().run(prep)
-        for src in self.inputs():
+        for src in self._source_files():
             dst = self.path / self.destination / src
             dst.parent.mkdir(parents=True, exist_ok=True)
             shutil.copy(self.rd.root / self.source / src, dst)
 
-    def inputs(self) -> set[str]:
+    def _source_files(self) -> set[str]:
+        """The files to copy, relative to `source`."""
         return set(git.expand_globs(self.rd.root / self.source, self.matching))
 
+    def inputs(self) -> set[str]:
+        return {str(Path(self.source) / src) for src in self._source_files()}
+
 
 class CargoPreImage(PreImage):
     """A `PreImage` action that uses Cargo."""