diff --git a/ci/test/lean-semantics.sh b/ci/test/lean-semantics.sh
new file mode 100755
index 0000000000000..5f1243709b86d
--- /dev/null
+++ b/ci/test/lean-semantics.sh
@@ -0,0 +1,43 @@
+#!/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.
+#
+# lean-semantics.sh: build the Lean 4 compute protocol semantics
+# model in `doc/developer/semantics`. The Lean toolchain version is
+# read from `lean-toolchain` and forwarded to the Dockerfile in the
+# same directory, so the elan toolchain pin used by local developers
+# and the CI image stay in lockstep.
+#
+# The Docker image is built locally on the agent and reused across CI
+# runs by Docker's layer cache. There is no registry push. The image
+# is cheap to rebuild from cold (no Mathlib dependency, see the
+# Dockerfile's comment).
+
+set -euo pipefail
+
+cd "$(dirname "$0")/../.."
+
+semantics_dir="doc/developer/semantics"
+lean_toolchain="$(tr -d '[:space:]' < "$semantics_dir/lean-toolchain")"
+image_tag="mz-lean-semantics:latest"
+
+docker build \
+    --build-arg "LEAN_TOOLCHAIN=$lean_toolchain" \
+    --tag "$image_tag" \
+    -f "$semantics_dir/Dockerfile" \
+    "$semantics_dir"
+
+docker run --rm \
+    --user "$(id -u):$(id -g)" \
+    -v "$PWD/$semantics_dir/MzCompute:/workspace/MzCompute" \
+    -v "$PWD/$semantics_dir/MzCompute.lean:/workspace/MzCompute.lean" \
+    -w /workspace \
+    "$image_tag" \
+    lake build
diff --git a/ci/test/pipeline.template.yml b/ci/test/pipeline.template.yml
index 9a013e7a8982d..877f936a891b9 100644
--- a/ci/test/pipeline.template.yml
+++ b/ci/test/pipeline.template.yml
@@ -201,6 +201,19 @@ steps:
         coverage: skip
         sanitizer: skip
 
+      - id: lean-semantics
+        label: ":lean: Lean semantics"
+        command: ci/test/lean-semantics.sh
+        inputs:
+          - doc/developer/semantics
+          - ci/test/lean-semantics.sh
+        depends_on: []
+        timeout_in_minutes: 15
+        agents:
+          queue: hetzner-x86-64-4cpu-8gb
+        coverage: skip
+        sanitizer: skip
+
       - id: lint-macos
         label: ":rust: macOS Clippy"
         # Running on a manually installed macOS agent, so make sure we don't go out of disk
diff --git a/doc/developer/design/20260724_compute_protocol_semantics.md b/doc/developer/design/20260724_compute_protocol_semantics.md
new file mode 100644
index 0000000000000..cd760c5b1b1be
--- /dev/null
+++ b/doc/developer/design/20260724_compute_protocol_semantics.md
@@ -0,0 +1,261 @@
+# Compute protocol semantics (Lean 4 model), Phase 1: staging and command/response legality
+
+- Associated: MaterializeInc/materialize#36614 (Lean 4 mechanization precedent, error-handling semantics. Unmerged, referenced as prior art only, not a dependency)
+
+## The problem
+
+The compute protocol (`src/compute-client/src/protocol/{command,response,history}.rs`)
+encodes several non-obvious invariants only in prose: a three-stage handshake,
+per-command legality preconditions tied to `GlobalId`s, frontier monotonicity
+and terminality for responses, and a 1:1 contract between `Peek` and
+`PeekResponse`. These invariants are load-bearing (violating them causes
+replica undefined behavior per the doc comments) but are currently checked
+only by code review and by whatever the implementation happens to enforce.
+There is no artifact that states the invariants independently of the
+implementation, so it is hard to know whether the invariants are mutually
+consistent, whether a proposed protocol change preserves them, or whether the
+prose is complete.
+
+There is no open GitHub issue tracking this work. It originated from a
+conversation about whether the protocol's invariants could be captured in a
+semantic model and checked with a proof assistant, following the precedent
+set by #36614's Lean 4 mechanization of the error-handling design.
+
+This doc proposes a Lean 4 model of the protocol's control-plane contract: a
+state machine plus a small set of safety theorems that codifies the doc
+comments as checked mathematics. The goal is to verify the model's internal
+consistency (the invariants do not contradict each other, a well-formed
+execution cannot get stuck), not to verify the Rust implementation against
+the model.
+
+This is Phase 1 of a three-phase layered plan. Phase 2 (read-hold lifecycle
+against `AllowCompaction`) and Phase 3 (command sharing and response
+reconciliation across replicas and workers) extend Phase 1's state machine
+rather than starting fresh. They are not covered by this doc.
+
+## Success criteria
+
+- A Lean 4 project (a new `lean_lib` in a `doc/developer/semantics/` package,
+  see Project Structure) defines `ProtocolState`, `Event` (mirroring
+  `ComputeCommand` / `ComputeResponse`), and a `step : ProtocolState → Event →
+  Option ProtocolState` relation whose preconditions match the "invalid to" /
+  "must" statements in `command.rs`, `response.rs`, and `protocol.rs`.
+- At least the seven theorems listed under Solution Proposal are stated and
+  proved with no `sorry`, each traceable to an explicit doc-comment contract.
+- The model builds in CI via a `ci/test/lean-semantics.sh` harness, bootstrapped
+  as part of this phase (see Project Structure). This does not depend on
+  #36614 landing first.
+- A reader can go from a doc-comment sentence in `command.rs` / `response.rs`
+  to the Lean lemma that encodes it, and back.
+
+## Out of scope
+
+- Payload semantics: the contents of `Row`, `DataflowDescription`,
+  `RelationDesc`, and similar types are opaque and uninterpreted in the
+  model. Phase 1 is about control flow and identifiers, not data.
+- Read-hold / `since` correctness against `AllowCompaction`. That is a
+  controller-side accounting property (Phase 2), not a protocol-legality
+  property. Phase 1 only models what the wire contract says about
+  `AllowCompaction`, which is silent on monotonicity of the frontier the
+  controller chooses to send.
+- Multi-replica and multi-worker command sharing and response demuxing
+  (Phase 3).
+- Liveness ("must eventually respond", "must eventually report empty
+  frontiers"). Phase 1 proves safety only: what must hold if an event
+  occurs, not that a required event eventually occurs.
+- Wire transport (bincode / CTP encoding, delivery scheduling). In-order,
+  reliable delivery is a hypothesis of the model, not something proved.
+- Verifying the Rust implementation against the model. Out of scope for the
+  whole layered project, not only Phase 1.
+
+## Solution proposal
+
+Model the protocol as a single event stream folded through one
+state-transition relation, with safety properties stated as invariants
+preserved by that fold. This is the same technique #36614 uses for
+`Collection.refines` / `NoRowErr`: define state and step, prove step
+preserves the invariant, induct over the execution.
+
+### State and events
+
+`ProtocolState` tracks exactly what the doc comments make legality depend
+on:
+
+- `created : Set GlobalId`, ids exported by a `CreateDataflow` seen so far.
+  `CreateDataflow`'s command payload keeps its export id set (`Finset
+  GlobalId`) concrete even though the rest of `DataflowDescription` is
+  opaque, since export-id freshness is itself a Phase 1 legality theorem
+  (see Target theorems).
+- `scheduled`, `allowedWrites : Set GlobalId`.
+- `since : GlobalId → Option (Antichain Timestamp)`, most recent
+  `AllowCompaction` frontier per id.
+- `reportedFrontiers : GlobalId → FrontierKind → Option (Antichain
+  Timestamp)`, last `Frontiers` response per id per kind (write / input /
+  output), used to check monotonicity and terminality of future responses.
+- `peeks : Uuid → PeekState` where `PeekState := Pending | Answered`.
+- `stage : Stage` where `Stage := Creation | Initialization | Computation`,
+  plus `helloSeen` / `createInstanceSeen` flags to pin the first two events.
+
+`Event := Cmd ComputeCommand | Resp ComputeResponse`, an inductive mirror of
+the two real Rust enums. Fields with no bearing on protocol-level legality
+(`RelationDesc`, `Row`, `DataflowDescription`'s internals, `RowSetFinishing`,
+and similar) are left out of the mirror types entirely rather than
+reconstructed field for field or carried as an opaque placeholder: nothing in
+this phase's theorems needs them, so there is nothing to represent. Fields
+legality does depend on (`GlobalId`, `Uuid`, `Antichain Timestamp`, the
+`PeekTarget`'s id) are kept concrete.
+
+Leaving a field out erases whatever structural facts it carried, not only its
+data content. For example `Peek::literal_constraints`'s documented "the
+vector is never empty" becomes unstatable once that field is gone. This is an
+accepted Phase 1 cut, not an oversight: only the seven theorems below are
+committed deliverables, and structural payload facts unrelated to them are
+left for a later phase to pick up if they turn out to matter.
+
+### Step relation
+
+`step : ProtocolState → Event → Option ProtocolState`. Each command or
+response variant gets one equation. Example shapes, illustrative rather than
+final Lean syntax:
+
+- `step s (Cmd (CreateDataflow exports _)) = if exports ∩ s.created = ∅ ∧ exports.Nodup then some {s with created := s.created ∪ exports} else none`
+- `step s (Cmd (Schedule id)) = if id ∈ s.created ∧ s.since id ≠ some ∅ then some {s with scheduled := s.scheduled.insert id} else none`
+- `step s (Cmd (AllowWrites id)) = if id ∈ s.created ∧ s.since id ≠ some ∅ then some {s with allowedWrites := s.allowedWrites.insert id} else none`
+- `step s (Resp (Frontiers id fr)) = if id ∈ s.created ∧ frontierAdvances s id fr then some (s.withReportedFrontiers id fr) else none`
+- `step s (Cmd (Peek p)) = if p.uuid ∉ s.peeks.keys then some {s with peeks := s.peeks.insert p.uuid Pending} else none`
+- `step s (Resp (PeekResponse uuid _ _)) = if s.peeks.find? uuid = some Pending then some {s with peeks := s.peeks.insert uuid Answered} else none`
+
+`Schedule` and `AllowWrites` both check `s.since id ≠ some ∅`: `command.rs`
+states it is invalid to send either once the collection has been allowed to
+compact to the empty frontier (the canonical drop). `CreateDataflow` checks
+its export ids are pairwise distinct (`exports.Nodup`) and disjoint from
+everything already created, mirroring `command.rs`'s "dataflow exports have
+unique IDs... do not repeat (within a single protocol iteration)".
+
+A `none` result models the "may cause undefined behavior" clause: the model
+has nothing further to say about what happens next, matching the doc's
+contract rather than inventing recovery behavior the real protocol does not
+specify.
+
+An execution is `List Event`, well-formed iff folding `step` from an initial
+empty state never produces `none`.
+
+### Target theorems
+
+1. `hello_create_instance_first`: in any well-formed execution, the first
+   event is `Cmd (Hello _)` and the second is `Cmd (CreateInstance _)`.
+2. `create_before_reference`: any event that names `id` other than the
+   `CreateDataflow` that creates it (Schedule, AllowWrites, AllowCompaction,
+   Peek on an index target, Frontiers, SubscribeResponse, CopyToResponse)
+   occurs strictly after `id`'s `CreateDataflow` in the execution. `Status`
+   is excluded: `ComputeResponse::Status` carries no `GlobalId` in the
+   current protocol (`StatusResponse` is an unimplemented placeholder), so
+   the doc's per-collection `Status` obligation isn't statable against the
+   real enum yet. Revisit if `Status` grows collection-scoped variants.
+3. `no_reference_after_drop`: `Schedule`, `AllowWrites`, and `Peek` (index
+   target) on `id` are only legal while `since id` has not yet reached the
+   empty frontier. Once an `AllowCompaction` with the empty frontier for
+   `id` has taken effect, no later event may `Schedule`, `AllowWrites`, or
+   `Peek` against it.
+4. `create_dataflow_ids_fresh`: a `CreateDataflow`'s export ids are pairwise
+   distinct and disjoint from every id created earlier in the execution.
+5. `frontiers_monotone_and_terminal`: for each id and frontier kind, the
+   sequence of reported frontiers in a well-formed execution is
+   non-decreasing, and once a kind reports the empty frontier for an id, no
+   later event reports a non-empty value for that (id, kind).
+6. `peek_response_unique`: for each `Uuid`, a well-formed execution contains
+   at most one `PeekResponse` for it, and if present, it is preceded by
+   exactly one `Peek` command with the same uuid.
+7. `cancel_requires_peek`: `CancelPeek uuid` is only legal after a `Peek`
+   with matching uuid.
+
+Each theorem's statement should be traceable to the specific doc-comment
+sentence it encodes, linked from the Lean docstring rather than narrated in
+the proof.
+
+### Project structure
+
+`doc/developer/semantics/` (Docker image, pinned Mathlib version,
+`lakefile.toml`, `ci/test/lean-semantics.sh` harness) does not exist on this
+branch: it was built on #36614's still-unmerged fork branch. Phase 1
+bootstraps this scaffolding itself, following #36614's shape as prior art
+(same Lean/Mathlib pin approach, same Docker-image-plus-CI-script structure)
+without depending on that PR landing. Concretely: a `doc/developer/semantics/`
+package with a `lakefile.toml` declaring an `MzCompute` `lean_lib` target, a
+`Dockerfile` and `ci/test/lean-semantics.sh` harness for CI, and a
+`MzCompute/` module directory with its own root import file. If #36614 lands
+first, the two efforts reconcile by merging into a single `lakefile.toml`
+with two `lean_lib` targets (`Mz` and `MzCompute`) sharing one Docker image.
+Until then `MzCompute` stands alone. It is designed as a separate library and
+namespace from the start rather than planned as a merge into `Mz`, since
+`Mz`'s docstring (on the #36614 branch) scopes it to scalar evaluation and
+collection semantics, a different subsystem (data plane, not control plane).
+Own `compute-protocol.md` reading-order doc, matching the naming #36614 uses
+for `model.md` / `transforms.md`, to keep the two efforts easy to merge later.
+
+## Minimal viable prototype
+
+A single Lean module defining `ProtocolState` / `Event` / `step` and proving
+`hello_create_instance_first` and `create_before_reference`, the two
+simplest and most structural theorems, is the MVP. It validates the
+state/step shape before investing in the frontier-monotonicity and
+peek-uniqueness proofs, which touch more of the state and are more likely to
+reveal that the chosen state shape is wrong.
+
+## Alternatives
+
+**Fully integrated single model (stages, read holds, and replica fan-out
+together).** Considered and rejected for Phase 1: it would catch
+cross-cutting invariants at subsystem boundaries, but the combined state
+space is large before anything is proved, and it front-loads the exact
+complexity a layered approach exists to avoid. Worth revisiting once Phases
+1 through 3 exist independently, as a possible Phase 4 "boundary" pass.
+
+**Fully separate models per phase, no shared kernel.** Rejected: each phase
+would carry its own simplified assumptions about the other phases, and the
+subtle bugs this protocol actually has tend to live at exactly those
+boundaries (for example, a race between `AllowCompaction` and an in-flight
+`Peek`). The layered approach instead has Phase 2 and Phase 3 extend Phase
+1's `ProtocolState` / `Event` / `step`, so cross-phase reasoning stays
+possible without Phase 1 paying Phase 3's cost.
+
+**Trace well-formedness predicate instead of a state machine.** An
+alternative shape defines well-formedness directly as a predicate over
+`List Event` (for example, "id's `CreateDataflow` appears before any other
+event naming id") rather than through a `step` relation. The two shapes are
+formally interchangeable: any such predicate can be written as a fold that
+threads state through the list, which is exactly what `step` does under a
+different name. The reason to prefer `step` isn't expressiveness, it's
+reuse: `step` names and exposes the intermediate state (`ProtocolState`) as
+a first-class definition that Phase 2 can literally extend with a few more
+fields and Phase 3 can literally lift to a product over replicas, whereas a
+predicate's internal fold state is private to its own proof and would need
+to be re-extracted and renamed for each later phase to build on.
+
+**New standalone Lean project instead of a second `lean_lib` in the existing
+package.** Rejected for now: it duplicates the Docker image, Mathlib pin,
+and CI harness for no isolation benefit `MzCompute` does not already get
+from being a separate library target. Worth reconsidering if the two
+subsystems' dependency needs diverge enough to matter, for instance if
+`MzCompute` never needs Mathlib and its presence meaningfully slows
+iteration.
+
+## Open questions
+
+- Does "protocol iteration" in the doc comments (peek uuid uniqueness,
+  `Hello` nonce uniqueness) mean one CTP connection's lifetime, or does the
+  model need to handle reconnection (a second `Hello` after a connection
+  drop) within Phase 1? The current proposal assumes a single connection per
+  execution and defers reconnection modeling to a later phase. Confirm this
+  does not undercut the Phase 1 theorems' relevance to the real,
+  reconnecting system.
+- `UpdateConfiguration` and `Hello` are broadcast to all workers rather than
+  routed through the first worker only. Phase 1 treats the protocol as a
+  single logical stream (one controller, one logical receiver) and defers
+  the worker-fan-out distinction entirely to Phase 3. Confirm the Phase 1
+  theorems remain meaningful stated over the logical single-stream view.
+- Should `frontiers_monotone_and_terminal` also state the doc's stronger
+  requirement that the first reported frontier of any kind is not less than
+  the dataflow's initial `as_of`? That requires `CreateDataflow`'s `as_of`
+  to be tracked in state, currently left opaque. Left for the Phase 1
+  implementation to decide once the state shape is in hand.
diff --git a/doc/developer/semantics/.dockerignore b/doc/developer/semantics/.dockerignore
new file mode 100644
index 0000000000000..01f8cdb637da2
--- /dev/null
+++ b/doc/developer/semantics/.dockerignore
@@ -0,0 +1 @@
+.lake/
diff --git a/doc/developer/semantics/.gitignore b/doc/developer/semantics/.gitignore
new file mode 100644
index 0000000000000..b914de79dca12
--- /dev/null
+++ b/doc/developer/semantics/.gitignore
@@ -0,0 +1,2 @@
+# Lake build cache.
+.lake/
diff --git a/doc/developer/semantics/Dockerfile b/doc/developer/semantics/Dockerfile
new file mode 100644
index 0000000000000..12d169f9f3a34
--- /dev/null
+++ b/doc/developer/semantics/Dockerfile
@@ -0,0 +1,60 @@
+# 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 image for building the compute protocol semantics
+# model in this directory. The Lean version is supplied via build
+# arg, which `ci/test/lean-semantics.sh` reads from `lean-toolchain`,
+# so the elan toolchain pin used by local developers and the CI image
+# stay in lockstep.
+#
+# Unlike a Mathlib-backed Lean project, this one has no `[[require]]`
+# in `lakefile.toml`: the compute protocol model is finite-state and
+# needs nothing beyond core Lean (structural recursion, `List`,
+# `Option`, `Bool`). This keeps the image small and the build fast.
+# If a later phase needs Mathlib, add a `[[require]]` entry and a
+# `lake exe cache get` step here, following the pattern in the (at
+# time of writing, unmerged) MaterializeInc/materialize#36614.
+#
+# Runtime contract: the source under `MzCompute/` and `MzCompute.lean`
+# is bind-mounted over the image's empty placeholders. Lake writes
+# build artifacts to the image's overlay filesystem. They are
+# ephemeral and discarded when the container exits.
+
+FROM ubuntu:26.04
+
+ARG LEAN_TOOLCHAIN
+
+ENV ELAN_HOME=/opt/elan
+ENV PATH=$ELAN_HOME/bin:$PATH
+ENV HOME=/tmp
+
+RUN apt-get update \
+    && DEBIAN_FRONTEND=noninteractive apt-get install -y --no-install-recommends \
+        ca-certificates \
+        curl \
+        git \
+    && rm -rf /var/lib/apt/lists/*
+
+RUN curl --proto '=https' --tlsv1.2 -sSf \
+        https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+        | sh -s -- --default-toolchain "$LEAN_TOOLCHAIN" -y --no-modify-path \
+    && chmod -R a+rX "$ELAN_HOME" \
+    && lean --version
+
+RUN git config --system --add safe.directory '*'
+
+WORKDIR /workspace
+
+COPY lakefile.toml lean-toolchain ./
+
+RUN mkdir -p MzCompute \
+    && touch MzCompute.lean \
+    && lake update \
+    && lake build \
+    && chmod -R a+rwX /workspace
diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
new file mode 100644
index 0000000000000..9abf012bf4037
--- /dev/null
+++ b/doc/developer/semantics/MzCompute.lean
@@ -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.
+--
+-- Root import file for the `MzCompute` library. Each module below is
+-- added by the plan task that introduces it.
+
+import MzCompute.Basic
+import MzCompute.Event
+import MzCompute.State
+import MzCompute.Run
+import MzCompute.Staging
+import MzCompute.Legality
+import MzCompute.Frontiers
+import MzCompute.Peeks
diff --git a/doc/developer/semantics/MzCompute/Basic.lean b/doc/developer/semantics/MzCompute/Basic.lean
new file mode 100644
index 0000000000000..6374c3cbd3fa5
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Basic.lean
@@ -0,0 +1,135 @@
+-- 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.
+--
+-- Core types shared by the compute protocol model: identifiers,
+-- frontiers, and the small enums `step` (see `State.lean`) dispatches
+-- on.
+
+namespace MzCompute
+
+/-- Compute-collection identifier. Only equality matters for
+protocol-level legality, so a bare `Nat` stands in for the real
+`mz_repr::GlobalId`. -/
+abbrev GlobalId := Nat
+
+/-- Peek request identifier, standing in for `uuid::Uuid`. Also reused
+for `Hello`'s nonce, which the model does not otherwise constrain
+(see the design doc's open question on reconnection). -/
+abbrev Uuid := Nat
+
+/-- A single-dimensional frontier over `mz_repr::Timestamp`. Because
+`Timestamp` is totally ordered, an antichain over it has at most one
+element: `.empty` models the empty antichain (the terminal frontier,
+nothing more will ever be written), `.at t` models the singleton
+antichain `{t}`. -/
+inductive Frontier where
+  | at (t : Nat)
+  | empty
+  deriving Repr
+
+/-- `Frontier.advances new old` holds (as `true`) exactly when `new`
+is at least as advanced as `old` (`new ⊒ old` in `response.rs`'s
+terms). `.empty` is the top element: nothing exceeds it, and only
+`.empty` can follow it. `.at 0` doubles as the "nothing reported yet"
+sentinel (see `State.lean`), which is sound because `Nat`'s minimum
+value is `0`: any real first report `.at t` satisfies `t ≥ 0`. -/
+def Frontier.advances (new old : Frontier) : Bool :=
+  match old, new with
+  | .empty, .empty => true
+  | .empty, .at _ => false
+  | .at _, .empty => true
+  | .at o, .at n => Nat.ble o n
+
+/-- The three frontier kinds a `Frontiers` response can report, per
+`response.rs`'s `FrontiersResponse`. -/
+inductive FrontierKind where
+  | write | input | output
+  deriving Repr
+
+/-- The three protocol stages from `protocol.rs`'s module doc. -/
+inductive Stage where
+  | creation | initialization | computation
+  deriving Repr
+
+def Stage.isCreation : Stage → Bool
+  | .creation => true
+  | _ => false
+
+/-- Lifecycle of a single `Peek` (identified by its `uuid`), per the
+1:1 `Peek`/`PeekResponse` contract in `command.rs`/`response.rs`. -/
+inductive PeekState where
+  | notSeen | pending | answered
+  deriving Repr
+
+def PeekState.isNotSeen : PeekState → Bool
+  | .notSeen => true
+  | _ => false
+
+def PeekState.isPending : PeekState → Bool
+  | .pending => true
+  | _ => false
+
+def PeekState.isAnswered : PeekState → Bool
+  | .answered => true
+  | _ => false
+
+/-- A `step` arm's precondition check: `some s` if `cond` holds, else
+`none`. A `none` result models the doc comments' "undefined behavior"
+clause: the model has nothing further to say, rather than inventing
+recovery behavior the protocol does not specify. -/
+def guard (cond : Bool) (s : α) : Option α :=
+  if cond then some s else none
+
+/-- A successful `guard` returns its payload unchanged. -/
+theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : x = y := by
+  unfold guard at h
+  cases cond with
+  | true => simpa using h
+  | false => simp at h
+
+/-- A successful `guard` witnesses its condition held. -/
+theorem guard_cond {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : cond = true := by
+  unfold guard at h
+  cases cond with
+  | true => rfl
+  | false => simp at h
+
+/-- Whether an optional new frontier report (`none` = this kind was
+not reported this time) is compatible with the previously reported
+value. `none` is always compatible: an absent field means "unchanged",
+per `FrontiersResponse`'s doc comment. -/
+def checkAdvance (new? : Option Frontier) (old : Frontier) : Bool :=
+  match new? with
+  | none => true
+  | some new => Frontier.advances new old
+
+/-- Applies an optional new frontier report, keeping the old value
+when the report is absent. -/
+def applyAdvance (new? : Option Frontier) (old : Frontier) : Frontier :=
+  match new? with
+  | none => old
+  | some new => new
+
+end MzCompute
+
+namespace MzCompute
+
+example : Frontier.advances (.at 5) (.at 3) = true := by rfl
+example : Frontier.advances (.at 2) (.at 3) = false := by rfl
+example : Frontier.advances .empty (.at 3) = true := by rfl
+example : Frontier.advances (.at 3) .empty = false := by rfl
+example : Frontier.advances .empty .empty = true := by rfl
+example : checkAdvance none (.at 3) = true := by rfl
+example : checkAdvance (some (.at 2)) (.at 3) = false := by rfl
+example : applyAdvance none (.at 3) = .at 3 := by rfl
+example : applyAdvance (some (.at 5)) (.at 3) = .at 5 := by rfl
+
+end MzCompute
diff --git a/doc/developer/semantics/MzCompute/Event.lean b/doc/developer/semantics/MzCompute/Event.lean
new file mode 100644
index 0000000000000..43859743d85cf
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Event.lean
@@ -0,0 +1,103 @@
+-- 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.
+--
+-- Inductive mirror of `ComputeCommand` (command.rs) and
+-- `ComputeResponse` (response.rs). Payload fields with no bearing on
+-- protocol-level legality (`RelationDesc`, `Row`, `DataflowDescription`'s
+-- internals, `RowSetFinishing`, and similar) are left out entirely
+-- rather than modeled as an opaque placeholder: nothing in this
+-- model's theorems needs them, so there is nothing to erase. See
+-- doc/developer/design/20260724_compute_protocol_semantics.md's
+-- "State and events" section for the opaque/concrete boundary this
+-- follows.
+
+import MzCompute.Basic
+
+namespace MzCompute
+
+/-- `Peek`'s target, per `command.rs`'s `PeekTarget`. Only `.index`
+peeks are required to reference a previously created collection (see
+theorem 2 in `Staging.lean`). `.persist` peeks target a storage
+collection this model does not track. -/
+inductive PeekTarget where
+  | index (id : GlobalId)
+  | persist (id : GlobalId)
+  deriving Repr
+
+/-- Mirrors `command.rs`'s `ComputeCommand`. -/
+inductive ComputeCommand where
+  | hello (nonce : Uuid)
+  | createInstance
+  | initializationComplete
+  | updateConfiguration
+  | createDataflow (exports : List GlobalId)
+  | schedule (id : GlobalId)
+  | allowWrites (id : GlobalId)
+  | allowCompaction (id : GlobalId) (frontier : Frontier)
+  | peek (uuid : Uuid) (target : PeekTarget)
+  | cancelPeek (uuid : Uuid)
+  deriving Repr
+
+/-- Mirrors `response.rs`'s `ComputeResponse`. `frontiers` carries the
+three optional per-kind reports from `FrontiersResponse` directly
+(write, input, output), rather than one event per kind, matching the
+real wire response. -/
+inductive ComputeResponse where
+  | frontiers (id : GlobalId) (write input output : Option Frontier)
+  | peekResponse (uuid : Uuid)
+  | subscribeResponse (id : GlobalId)
+  | copyToResponse (id : GlobalId)
+  | status
+  deriving Repr
+
+inductive Event where
+  | cmd (c : ComputeCommand)
+  | resp (r : ComputeResponse)
+  deriving Repr
+
+def Event.isHello : Event → Bool
+  | .cmd (.hello _) => true
+  | _ => false
+
+def Event.isCreateInstance : Event → Bool
+  | .cmd .createInstance => true
+  | _ => false
+
+/-- Whether `e` is one of the event kinds `command.rs`/`response.rs`
+require a prior `CreateDataflow` for `id`: `Schedule`, `AllowWrites`,
+`AllowCompaction`, `Peek` on an index target, `Frontiers`,
+`SubscribeResponse`, `CopyToResponse`. `Status` is excluded: it
+carries no `GlobalId` in the current protocol (see theorem 2's doc
+comment in `Staging.lean`). `CreateDataflow` itself is excluded: it is
+the event that satisfies the requirement, not one that needs it. -/
+def Event.references : Event → GlobalId → Bool
+  | .cmd (.schedule id'), id => id' == id
+  | .cmd (.allowWrites id'), id => id' == id
+  | .cmd (.allowCompaction id' _), id => id' == id
+  | .cmd (.peek _ (.index id')), id => id' == id
+  | .resp (.frontiers id' _ _ _), id => id' == id
+  | .resp (.subscribeResponse id'), id => id' == id
+  | .resp (.copyToResponse id'), id => id' == id
+  | _, _ => false
+
+end MzCompute
+
+namespace MzCompute
+
+example : Event.isHello (.cmd (.hello 0)) = true := by rfl
+example : Event.isHello (.cmd .createInstance) = false := by rfl
+example : Event.isCreateInstance (.cmd .createInstance) = true := by rfl
+example : Event.references (.cmd (.schedule 7)) 7 = true := by rfl
+example : Event.references (.cmd (.schedule 7)) 8 = false := by rfl
+example : Event.references (.resp .status) 7 = false := by rfl
+example : Event.references (.cmd (.createDataflow [7])) 7 = false := by rfl
+example : Event.references (.cmd (.peek 0 (.persist 7))) 7 = false := by rfl
+example : Event.references (.cmd (.peek 0 (.index 7))) 7 = true := by rfl
+
+end MzCompute
diff --git a/doc/developer/semantics/MzCompute/Frontiers.lean b/doc/developer/semantics/MzCompute/Frontiers.lean
new file mode 100644
index 0000000000000..baa7313493ba7
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Frontiers.lean
@@ -0,0 +1,150 @@
+-- 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.
+--
+-- Theorem 5: reported frontiers never regress, and once a kind
+-- reports the empty frontier for an id, it stays empty.
+
+import MzCompute.State
+import MzCompute.Run
+
+namespace MzCompute
+
+theorem Frontier.advances_refl (f : Frontier) : Frontier.advances f f = true := by
+  cases f with
+  | «at» t => simp [Frontier.advances, Nat.ble_eq]
+  | empty => rfl
+
+theorem Frontier.advances_trans {a b c : Frontier}
+    (hab : Frontier.advances b a = true) (hbc : Frontier.advances c b = true) :
+    Frontier.advances c a = true := by
+  cases a with
+  | empty => cases b with
+      | empty => cases c with
+          | empty => rfl
+          | «at» _ => simp [Frontier.advances] at hbc
+      | «at» _ => simp [Frontier.advances] at hab
+  | «at» o =>
+      cases b with
+      | empty => cases c with
+          | empty => rfl
+          | «at» _ => simp [Frontier.advances] at hbc
+      | «at» m =>
+          cases c with
+          | empty => rfl
+          | «at» n =>
+              simp only [Frontier.advances] at hab hbc ⊢
+              exact Nat.ble_eq_true_of_le
+                (Nat.le_trans (Nat.le_of_ble_eq_true hab) (Nat.le_of_ble_eq_true hbc))
+
+/-- Only `.empty` can advance past `.empty`. -/
+theorem Frontier.advances_empty_inv (new : Frontier) (h : Frontier.advances new .empty = true) :
+    new = .empty := by
+  cases new with
+  | empty => rfl
+  | «at» _ => simp [Frontier.advances] at h
+
+/-- A passing `checkAdvance` guarantees the applied result advances the
+old value: when the report is absent the value is unchanged (reflexive),
+and when present the guard is exactly `Frontier.advances`. -/
+theorem checkAdvance_advances (new? : Option Frontier) (old : Frontier)
+    (h : checkAdvance new? old = true) : Frontier.advances (applyAdvance new? old) old = true := by
+  cases new? with
+  | none => exact Frontier.advances_refl old
+  | some new => simpa [checkAdvance, applyAdvance] using h
+
+/-- Theorem 5, single-step form. Encodes response.rs:37-42
+(monotonicity) and :44-51 (terminality, which is the same fact
+specialized to `old = .empty` via `advances_empty_inv`). -/
+theorem frontiers_advance (s s' : ProtocolState) (id : GlobalId) (w i o : Option Frontier)
+    (h : step s (.resp (.frontiers id w i o)) = some s') (k : FrontierKind) :
+    Frontier.advances (s'.reportedFrontiers id k) (s.reportedFrontiers id k) = true := by
+  simp only [step, guard] at h
+  split at h
+  · rename_i hcond
+    injection h with h
+    subst h
+    simp only [Bool.and_eq_true] at hcond
+    obtain ⟨⟨⟨⟨-, -⟩, hw⟩, hi⟩, ho⟩ := hcond
+    cases k with
+    | write => simpa using (checkAdvance_advances w (s.reportedFrontiers id .write) hw)
+    | input => simpa using (checkAdvance_advances i (s.reportedFrontiers id .input) hi)
+    | output => simpa using (checkAdvance_advances o (s.reportedFrontiers id .output) ho)
+  · contradiction
+
+/-- Theorem 5, lifted across a whole execution. -/
+theorem reportedFrontiers_monotone (s0 s : ProtocolState) (es : List Event)
+    (h : run s0 es = some s) (id : GlobalId) (k : FrontierKind) :
+    Frontier.advances (s.reportedFrontiers id k) (s0.reportedFrontiers id k) = true := by
+  induction es generalizing s0 with
+  | nil => simp [run] at h; subst h; exact Frontier.advances_refl _
+  | cons e rest ih =>
+      unfold run at h
+      cases hstep : step s0 e with
+      | none => simp [hstep] at h
+      | some s1 =>
+          simp [hstep] at h
+          have h1 : Frontier.advances (s1.reportedFrontiers id k) (s0.reportedFrontiers id k) = true := by
+            cases e with
+            | resp r =>
+                cases r with
+                | frontiers id' w i o =>
+                    by_cases hid : id' = id
+                    · subst id'; exact frontiers_advance s0 s1 id w i o hstep k
+                    · -- A Frontiers response for a different id leaves
+                      -- `reportedFrontiers id k` untouched.
+                      simp only [step] at hstep
+                      have hs := guard_eq_some hstep
+                      subst hs
+                      have hne : (id == id') = false := by
+                        simp only [beq_eq_false_iff_ne, ne_eq]
+                        exact fun heq => hid heq.symm
+                      simp only [hne, if_false, Bool.false_eq_true]
+                      exact Frontier.advances_refl _
+                | peekResponse _ =>
+                    simp only [step] at hstep
+                    have hs := guard_eq_some hstep; subst hs
+                    exact Frontier.advances_refl _
+                | subscribeResponse _ =>
+                    simp only [step] at hstep
+                    have hs := guard_eq_some hstep; subst hs
+                    exact Frontier.advances_refl _
+                | copyToResponse _ =>
+                    simp only [step] at hstep
+                    have hs := guard_eq_some hstep; subst hs
+                    exact Frontier.advances_refl _
+                | status =>
+                    simp only [step] at hstep
+                    have hs := guard_eq_some hstep; subst hs
+                    exact Frontier.advances_refl _
+            | cmd c =>
+                cases c <;>
+                  (simp only [step] at hstep
+                   have hs := guard_eq_some hstep
+                   subst hs
+                   exact Frontier.advances_refl _)
+          exact Frontier.advances_trans h1 (ih s1 h)
+
+/-- Theorem 5, terminality corollary: once a kind reports empty, it
+stays empty for the rest of the execution. -/
+theorem reportedFrontiers_terminal (s0 s : ProtocolState) (es : List Event)
+    (h : run s0 es = some s) (id : GlobalId) (k : FrontierKind)
+    (hempty : s0.reportedFrontiers id k = .empty) :
+    s.reportedFrontiers id k = .empty :=
+  Frontier.advances_empty_inv _ (hempty ▸ reportedFrontiers_monotone s0 s es h id k)
+
+/-- Theorem 5, combined statement: monotonicity plus terminality, over
+an execution rooted at `initState`. -/
+theorem frontiers_monotone_and_terminal (es : List Event) (s : ProtocolState)
+    (h : run initState es = some s) (id : GlobalId) (k : FrontierKind) :
+    Frontier.advances (s.reportedFrontiers id k) (initState.reportedFrontiers id k) = true ∧
+      (initState.reportedFrontiers id k = .empty → s.reportedFrontiers id k = .empty) :=
+  ⟨reportedFrontiers_monotone initState s es h id k,
+   fun hempty => reportedFrontiers_terminal initState s es h id k hempty⟩
+
+end MzCompute
diff --git a/doc/developer/semantics/MzCompute/Legality.lean b/doc/developer/semantics/MzCompute/Legality.lean
new file mode 100644
index 0000000000000..730de42d8a574
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Legality.lean
@@ -0,0 +1,122 @@
+-- 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.
+--
+-- Theorems 3-4: a dropped collection can't be referenced again, and
+-- CreateDataflow's export ids are fresh.
+
+import MzCompute.State
+import MzCompute.Run
+
+namespace MzCompute
+
+/-- Theorem 3, part 1. Encodes command.rs:152-153. -/
+theorem schedule_fails_when_dropped (s : ProtocolState) (id : GlobalId) (h : s.dropped id = true) :
+    step s (.cmd (.schedule id)) = none := by
+  simp [step, guard, h]
+
+/-- Theorem 3, part 2. Encodes command.rs:162-163. -/
+theorem allowWrites_fails_when_dropped (s : ProtocolState) (id : GlobalId) (h : s.dropped id = true) :
+    step s (.cmd (.allowWrites id)) = none := by
+  simp [step, guard, h]
+
+/-- Theorem 3, part 3. `command.rs` does not give index-peek-after-drop
+the same explicit "invalid to" wording as Schedule/AllowWrites, but a
+dropped collection's arrangement is gone, so this model treats it the
+same way (see the design doc's Solution Proposal). -/
+theorem peekIndex_fails_when_dropped (s : ProtocolState) (id uuid : Uuid) (h : s.dropped id = true) :
+    step s (.cmd (.peek uuid (.index id))) = none := by
+  simp [step, guard, h]
+
+/-- `dropped` only ever grows: no step un-drops a collection. -/
+theorem dropped_monotone (s s' : ProtocolState) (e : Event) (h : step s e = some s') (id : GlobalId) :
+    s.dropped id = true → s'.dropped id = true := by
+  intro hd
+  cases e with
+  | cmd c =>
+      cases c with
+      | allowCompaction id' frontier =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          simp [hd]
+      | _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact hd
+  | resp r =>
+      cases r <;>
+        (simp only [step] at h
+         have hs := guard_eq_some h
+         subst hs
+         exact hd)
+
+/-- Theorem 3, lifted across a whole execution. Once `id` is dropped,
+no later `Schedule`, `AllowWrites`, or index-target `Peek` for `id`
+can succeed. -/
+theorem no_reference_after_drop (pre mid : List Event) (e : Event) (id uuid : Uuid)
+    (s s' s'' : ProtocolState)
+    (_hpre : run initState pre = some s)
+    (hdrop : s.dropped id = true)
+    (hmid : run s mid = some s')
+    (he : e = .cmd (.schedule id) ∨ e = .cmd (.allowWrites id) ∨ e = .cmd (.peek uuid (.index id)))
+    (hstep : step s' e = some s'') : False := by
+  have hdrop' : s'.dropped id = true := by
+    clear _hpre he hstep
+    induction mid generalizing s with
+    | nil => simp [run] at hmid; subst hmid; exact hdrop
+    | cons e0 rest ih =>
+        unfold run at hmid
+        cases hstep0 : step s e0 with
+        | none => simp [hstep0] at hmid
+        | some s1 =>
+            simp only [hstep0] at hmid
+            exact ih s1 (dropped_monotone s s1 e0 hstep0 id hdrop) hmid
+  rcases he with he | he | he
+  · rw [he, schedule_fails_when_dropped s' id hdrop'] at hstep; simp at hstep
+  · rw [he, allowWrites_fails_when_dropped s' id hdrop'] at hstep; simp at hstep
+  · rw [he, peekIndex_fails_when_dropped s' id uuid hdrop'] at hstep; simp at hstep
+
+/-- Decodes `freshExports`'s `Bool` into the two `Prop`s `command.rs`
+states in English: no id in `exports` is already created, and
+`exports` has no internal duplicate. -/
+theorem freshExports_sound (created : GlobalId → Bool) (exports : List GlobalId)
+    (h : freshExports created exports = true) :
+    (∀ id ∈ exports, created id = false) ∧ exports.Nodup := by
+  induction exports with
+  | nil => exact ⟨by simp, List.nodup_nil⟩
+  | cons id rest ih =>
+      simp only [freshExports, Bool.and_eq_true] at h
+      obtain ⟨⟨hnc, hne⟩, hrest⟩ := h
+      obtain ⟨ihc, ihn⟩ := ih hrest
+      refine ⟨?_, ?_⟩
+      · intro id' hmem
+        simp only [List.mem_cons] at hmem
+        rcases hmem with rfl | hmem
+        · simpa using hnc
+        · exact ihc id' hmem
+      · rw [List.nodup_cons]
+        refine ⟨?_, ihn⟩
+        intro hmem
+        exact absurd (List.elem_eq_true_of_mem hmem) (by simpa using hne)
+
+/-- Theorem 4. Encodes command.rs:107-108: a CreateDataflow's export
+ids are pairwise distinct and disjoint from every id created earlier
+in the execution. -/
+theorem create_dataflow_ids_fresh (s s' : ProtocolState) (exports : List GlobalId)
+    (h : step s (.cmd (.createDataflow exports)) = some s') :
+    (∀ id ∈ exports, s.created id = false) ∧ exports.Nodup := by
+  simp only [step, guard] at h
+  split at h
+  · rename_i hcond
+    rw [Bool.and_eq_true] at hcond
+    exact freshExports_sound s.created exports hcond.2
+  · contradiction
+
+end MzCompute
diff --git a/doc/developer/semantics/MzCompute/Peeks.lean b/doc/developer/semantics/MzCompute/Peeks.lean
new file mode 100644
index 0000000000000..fcd589032d5ef
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Peeks.lean
@@ -0,0 +1,215 @@
+-- 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.
+--
+-- Theorems 6-7: at most one PeekResponse per Peek, and CancelPeek
+-- requires a prior Peek.
+
+import MzCompute.State
+import MzCompute.Run
+
+namespace MzCompute
+
+theorem peekResponse_requires_pending (s s' : ProtocolState) (uuid : Uuid)
+    (h : step s (.resp (.peekResponse uuid)) = some s') :
+    s.peeks uuid = .pending ∧ s'.peeks uuid = .answered := by
+  simp only [step, guard] at h
+  split at h
+  · rename_i hcond
+    injection h with h
+    subst h
+    refine ⟨?_, by simp⟩
+    cases hp : s.peeks uuid with
+    | pending => rfl
+    | notSeen => simp [hp, PeekState.isPending] at hcond
+    | answered => simp [hp, PeekState.isPending] at hcond
+  · contradiction
+
+theorem peek_requires_notSeen (s s' : ProtocolState) (uuid : Uuid) (target : PeekTarget)
+    (h : step s (.cmd (.peek uuid target)) = some s') :
+    s.peeks uuid = .notSeen ∧ s'.peeks uuid = .pending := by
+  simp only [step] at h
+  have hcond := guard_cond h
+  have hs := guard_eq_some h
+  subst hs
+  refine ⟨?_, by simp⟩
+  cases hp : s.peeks uuid with
+  | notSeen => rfl
+  | pending => simp [hp, PeekState.isNotSeen] at hcond
+  | answered => simp [hp, PeekState.isNotSeen] at hcond
+
+/-- Once `.answered`, a peek's state stays `.answered`: no `step` arm
+moves a peek out of `.answered`. -/
+theorem peeks_answered_monotone (s s' : ProtocolState) (e : Event) (h : step s e = some s')
+    (uuid : Uuid) : s.peeks uuid = .answered → s'.peeks uuid = .answered := by
+  intro ha
+  cases e with
+  | cmd c =>
+      cases c with
+      | peek uuid' _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          have hcond := guard_cond h
+          subst hs
+          simp only []
+          split
+          · rename_i heq
+            have huuid : uuid = uuid' := eq_of_beq heq
+            subst huuid
+            simp only [Bool.and_eq_true] at hcond
+            obtain ⟨⟨_, hnot⟩, _⟩ := hcond
+            rw [ha] at hnot
+            simp [PeekState.isNotSeen] at hnot
+          · exact ha
+      | _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact ha
+  | resp r =>
+      cases r with
+      | peekResponse uuid' =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          simp only []
+          split
+          · rfl
+          · exact ha
+      | _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact ha
+
+/-- Theorem 7. Encodes command.rs:248-250. -/
+theorem cancel_requires_peek (s s' : ProtocolState) (uuid : Uuid) (h : step s (.cmd (.cancelPeek uuid)) = some s') :
+    s.peeks uuid ≠ .notSeen := by
+  simp only [step, guard] at h
+  split at h
+  · rename_i hcond
+    intro hcontra
+    simp [hcontra, PeekState.isNotSeen] at hcond
+  · contradiction
+
+/-- A single step either leaves a peek's `notSeen`-ness reflected in the
+prior state, or is exactly the `Peek` that first touched this uuid. Only
+a `Peek uuid _` moves `peeks uuid` out of `notSeen`. A `PeekResponse
+uuid` also writes `peeks uuid`, but its guard already required the peek
+to be `pending`, so the prior state was not `notSeen` either. -/
+theorem peeks_notSeen_of_step (s s' : ProtocolState) (e : Event) (uuid : Uuid)
+    (h : step s e = some s') (hns : s'.peeks uuid ≠ .notSeen) :
+    s.peeks uuid ≠ .notSeen ∨ ∃ target, e = .cmd (.peek uuid target) := by
+  cases e with
+  | cmd c =>
+      cases c with
+      | peek uuid' target =>
+          by_cases huuid : uuid' = uuid
+          · exact Or.inr ⟨target, by rw [huuid]⟩
+          · left
+            simp only [step] at h
+            have hs := guard_eq_some h
+            subst hs
+            simp only [] at hns
+            have hne : (uuid == uuid') = false := by
+              simp only [beq_eq_false_iff_ne, ne_eq]
+              exact fun heq => huuid heq.symm
+            simpa only [hne, if_false, Bool.false_eq_true] using hns
+      | _ =>
+          left
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact hns
+  | resp r =>
+      cases r with
+      | peekResponse uuid' =>
+          left
+          simp only [step] at h
+          have hs := guard_eq_some h
+          have hcond := guard_cond h
+          subst hs
+          by_cases huuid : uuid' = uuid
+          · subst huuid
+            simp only [Bool.and_eq_true] at hcond
+            obtain ⟨_, hpend⟩ := hcond
+            cases hp : s.peeks uuid' with
+            | pending => simp
+            | notSeen => rw [hp] at hpend; simp [PeekState.isPending] at hpend
+            | answered => simp
+          · simp only [] at hns
+            have hne : (uuid == uuid') = false := by
+              simp only [beq_eq_false_iff_ne, ne_eq]
+              exact fun heq => huuid heq.symm
+            simpa only [hne, if_false, Bool.false_eq_true] using hns
+      | _ =>
+          left
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact hns
+
+theorem peeks_notSeen_of_run_from (es : List Event) (s0 s : ProtocolState) (h : run s0 es = some s)
+    (uuid : Uuid) (hns : s.peeks uuid ≠ .notSeen) :
+    s0.peeks uuid ≠ .notSeen ∨ ∃ target, .cmd (.peek uuid target) ∈ es := by
+  induction es generalizing s0 with
+  | nil => simp [run] at h; subst h; exact Or.inl hns
+  | cons e rest ih =>
+      unfold run at h
+      cases hstep : step s0 e with
+      | none => simp [hstep] at h
+      | some s1 =>
+          simp only [hstep] at h
+          rcases ih s1 h with h1 | ⟨target, hmem⟩
+          · rcases peeks_notSeen_of_step s0 s1 e uuid hstep h1 with h0 | ⟨target, heq⟩
+            · exact Or.inl h0
+            · exact Or.inr ⟨target, by rw [heq]; exact List.mem_cons_self⟩
+          · exact Or.inr ⟨target, List.mem_cons_of_mem e hmem⟩
+
+/-- Lifting `peeks_answered_monotone` across a whole execution. -/
+theorem peeks_answered_run (es : List Event) (s s' : ProtocolState) (uuid : Uuid)
+    (h : run s es = some s') : s.peeks uuid = .answered → s'.peeks uuid = .answered := by
+  induction es generalizing s with
+  | nil => intro ha; simp [run] at h; subst h; exact ha
+  | cons e rest ih =>
+      intro ha
+      unfold run at h
+      cases hstep0 : step s e with
+      | none => simp [hstep0] at h
+      | some sm =>
+          simp only [hstep0] at h
+          exact ih sm h (peeks_answered_monotone s sm e hstep0 uuid ha)
+
+/-- Theorem 6. Encodes response.rs:66-69: exactly one PeekResponse per
+Peek. Phrased as "a second PeekResponse for the same uuid, anywhere
+later in a well-formed execution, is impossible". See the design
+doc's "Target theorems" section for why this form captures
+uniqueness. -/
+theorem peek_response_unique (pre mid : List Event) (uuid : Uuid) (s1 s2 s3 s4 : ProtocolState)
+    (_hpre : run initState pre = some s1)
+    (hstep1 : step s1 (.resp (.peekResponse uuid)) = some s2)
+    (hmid : run s2 mid = some s3)
+    (hstep2 : step s3 (.resp (.peekResponse uuid)) = some s4) : False := by
+  have h2 : s2.peeks uuid = .answered := (peekResponse_requires_pending s1 s2 uuid hstep1).2
+  have h3 : s3.peeks uuid = .answered := peeks_answered_run mid s2 s3 uuid hmid h2
+  have h4 : s3.peeks uuid = .pending := (peekResponse_requires_pending s3 s4 uuid hstep2).1
+  rw [h3] at h4
+  exact absurd h4 (by simp)
+
+/-- Theorem 6, provenance half: a `PeekResponse` is always preceded by
+a matching `Peek`. -/
+theorem peek_response_preceded_by_peek (pre : List Event) (uuid : Uuid) (s s' : ProtocolState)
+    (hpre : run initState pre = some s)
+    (hstep : step s (.resp (.peekResponse uuid)) = some s') :
+    ∃ target, .cmd (.peek uuid target) ∈ pre := by
+  have hp : s.peeks uuid = .pending := (peekResponse_requires_pending s s' uuid hstep).1
+  rcases peeks_notSeen_of_run_from pre initState s hpre uuid (by simp [hp]) with h0 | hex
+  · simp [initState] at h0
+  · exact hex
+
+end MzCompute
diff --git a/doc/developer/semantics/MzCompute/Run.lean b/doc/developer/semantics/MzCompute/Run.lean
new file mode 100644
index 0000000000000..e80c4b613bfdd
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Run.lean
@@ -0,0 +1,71 @@
+-- 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.
+--
+-- Folding `step` over a list of events into an execution, and the
+-- well-formedness predicate the plan's theorems are stated over.
+
+import MzCompute.State
+
+namespace MzCompute
+
+def initState : ProtocolState := {}
+
+/-- Folds `step` over `es` starting from `s`, short-circuiting to
+`none` at the first illegal event. -/
+def run (s : ProtocolState) : List Event → Option ProtocolState
+  | [] => some s
+  | e :: rest =>
+      match step s e with
+      | none => none
+      | some s' => run s' rest
+
+/-- An execution is well-formed iff folding `step` from `initState`
+never hits an illegal event. -/
+def WellFormed (es : List Event) : Prop := ∃ s, run initState es = some s
+
+end MzCompute
+
+namespace MzCompute
+
+/-- A minimal legal trace: handshake, create a dataflow exporting id
+`1`, schedule it, report its write frontier advancing to `5`, peek it,
+answer the peek, then drop it. -/
+def legalTrace : List Event :=
+  [ .cmd (.hello 0)
+  , .cmd .createInstance
+  , .cmd .initializationComplete
+  , .cmd (.createDataflow [1])
+  , .cmd (.schedule 1)
+  , .resp (.frontiers 1 (some (.at 5)) none none)
+  , .cmd (.peek 10 (.index 1))
+  , .resp (.peekResponse 10)
+  , .cmd (.allowCompaction 1 .empty)
+  ]
+
+example : WellFormed legalTrace := by
+  refine ⟨?_, ?_⟩
+  · exact (run initState legalTrace).get (by decide)
+  · rfl
+
+/-- Same trace, but with the `Schedule` moved before `CreateDataflow`:
+illegal per command.rs:148-150. -/
+def illegalTrace : List Event :=
+  [ .cmd (.hello 0)
+  , .cmd .createInstance
+  , .cmd .initializationComplete
+  , .cmd (.schedule 1)
+  , .cmd (.createDataflow [1])
+  ]
+
+example : ¬ WellFormed illegalTrace := by
+  rintro ⟨s, hs⟩
+  rw [show run initState illegalTrace = none from rfl] at hs
+  cases hs
+
+end MzCompute
diff --git a/doc/developer/semantics/MzCompute/Staging.lean b/doc/developer/semantics/MzCompute/Staging.lean
new file mode 100644
index 0000000000000..5261ba361dd1e
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Staging.lean
@@ -0,0 +1,186 @@
+-- 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.
+--
+-- Staging-order theorems: the first two commands of any legal
+-- execution are `Hello` then `CreateInstance`, and any event naming a
+-- collection `id` requires a prior `CreateDataflow` exporting `id`.
+-- These are the plan's Minimal Viable Prototype, validating the
+-- state/step/run shape before the drop, frontier, and peek theorems.
+
+import MzCompute.Run
+
+namespace MzCompute
+
+/-- Theorem 1. Encodes protocol.rs:52-58: Hello is the first command
+of the Creation stage. -/
+theorem hello_first (e : Event) (rest : List Event) (s : ProtocolState)
+    (h : run initState (e :: rest) = some s) : e.isHello = true := by
+  unfold run at h
+  cases e with
+  | cmd c =>
+      cases c with
+      | hello _ => rfl
+      | _ => simp [step, guard, initState, Stage.isCreation] at h
+  | resp r =>
+      cases r <;> simp [step, guard, initState, Stage.isCreation] at h
+
+/-- Theorem 1, continued. Encodes protocol.rs:52-58: CreateInstance is
+the second command, completing the Creation stage. -/
+theorem create_instance_second (e1 e2 : Event) (rest : List Event) (s : ProtocolState)
+    (h : run initState (e1 :: e2 :: rest) = some s) : e2.isCreateInstance = true := by
+  have he1 : e1.isHello = true := hello_first e1 (e2 :: rest) s h
+  unfold run at h
+  cases e1 with
+  | cmd c =>
+      cases c with
+      | hello n =>
+          cases e2 with
+          | cmd c2 =>
+              cases c2 with
+              | createInstance => rfl
+              | _ => simp [run, step, guard, initState, Stage.isCreation] at h
+          | resp r2 => cases r2 <;> simp [run, step, guard, initState, Stage.isCreation] at h
+      | _ => simp [Event.isHello] at he1
+  | resp _ => simp [Event.isHello] at he1
+
+/-- A single step either preserves `created` or, for a `CreateDataflow`
+event, adds exactly its export list. -/
+theorem created_of_step (s s' : ProtocolState) (e : Event) (h : step s e = some s') (id : GlobalId) :
+    s'.created id = true →
+      s.created id = true ∨ ∃ exports, e = .cmd (.createDataflow exports) ∧ exports.elem id = true := by
+  intro hc
+  cases e with
+  | cmd c =>
+      cases c with
+      | createDataflow exports =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          simp only [Bool.or_eq_true] at hc
+          rcases hc with h1 | h2
+          · exact Or.inl h1
+          · exact Or.inr ⟨exports, rfl, h2⟩
+      | _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact Or.inl hc
+  | resp r =>
+      cases r <;>
+        (simp only [step] at h
+         have hs := guard_eq_some h
+         subst hs
+         exact Or.inl hc)
+
+/-- Generalization of `created_of_run` over the starting state, the
+form the induction needs. -/
+theorem created_of_run_from (es : List Event) (s0 s : ProtocolState) (h : run s0 es = some s)
+    (id : GlobalId) (hc : s.created id = true) :
+    s0.created id = true ∨
+      ∃ (pre : List Event) (exports : List GlobalId) (suf : List Event),
+        es = pre ++ [.cmd (.createDataflow exports)] ++ suf ∧ exports.elem id = true := by
+  induction es generalizing s0 with
+  | nil => simp [run] at h; subst h; exact Or.inl hc
+  | cons e rest ih =>
+      unfold run at h
+      cases hstep : step s0 e with
+      | none => simp [hstep] at h
+      | some s1 =>
+          simp only [hstep] at h
+          rcases ih s1 h with h1 | ⟨pre, exports, suf, heq, hel⟩
+          · rcases created_of_step s0 s1 e hstep id h1 with h0 | ⟨exports, heq, hel⟩
+            · exact Or.inl h0
+            · exact Or.inr ⟨[], exports, rest, by simp [heq], hel⟩
+          · exact Or.inr ⟨e :: pre, exports, suf, by simp [heq], hel⟩
+
+/-- Lifting `created_of_step` across a whole execution: if `id` is
+created at the end, some `CreateDataflow` event in the execution
+exported it. -/
+theorem created_of_run (es : List Event) (s : ProtocolState) (h : run initState es = some s)
+    (id : GlobalId) (hc : s.created id = true) :
+    ∃ (pre : List Event) (exports : List GlobalId) (suf : List Event),
+      es = pre ++ [.cmd (.createDataflow exports)] ++ suf ∧ exports.elem id = true := by
+  rcases created_of_run_from es initState s h id hc with h0 | hex
+  · simp [initState] at h0
+  · exact hex
+
+/-- Theorem 2. Encodes command.rs:148-153, :158-163, :185-187,
+:219-224 and response.rs:52-54, :106-107, :120-121: any event naming
+`id` (other than the `CreateDataflow` that creates it) requires a
+prior `CreateDataflow` exporting `id`. -/
+theorem create_before_reference (pre : List Event) (mid : Event) (id : GlobalId)
+    (s s' : ProtocolState)
+    (hpre : run initState pre = some s)
+    (hstep : step s mid = some s')
+    (href : mid.references id = true) :
+    ∃ (pre' : List Event) (exports : List GlobalId) (suf : List Event),
+      pre = pre' ++ [.cmd (.createDataflow exports)] ++ suf ∧ exports.elem id = true := by
+  have hc : s.created id = true := by
+    cases mid with
+    | cmd c =>
+        cases c with
+        | schedule id' =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | allowWrites id' =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | allowCompaction id' _ =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | peek _ target =>
+            cases target with
+            | index id' =>
+                simp only [Event.references, beq_iff_eq] at href
+                subst href
+                simp only [step] at hstep
+                have hcond := guard_cond hstep
+                simp only [Bool.and_eq_true] at hcond
+                simp_all
+            | persist _ => simp [Event.references] at href
+        | _ => simp [Event.references] at href
+    | resp r =>
+        cases r with
+        | frontiers id' _ _ _ =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | subscribeResponse id' =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | copyToResponse id' =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | _ => simp [Event.references] at href
+  exact created_of_run pre s hpre id hc
+
+end MzCompute
diff --git a/doc/developer/semantics/MzCompute/State.lean b/doc/developer/semantics/MzCompute/State.lean
new file mode 100644
index 0000000000000..e5b48b033b4ca
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/State.lean
@@ -0,0 +1,169 @@
+-- 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.
+--
+-- The protocol state machine: `ProtocolState` plus the `step`
+-- relation whose guards encode `command.rs`/`response.rs`'s "invalid
+-- to" / "must" contracts. A `none` result means the doc comments call
+-- the transition undefined behavior. The model stops there rather
+-- than inventing recovery semantics the protocol does not specify.
+
+import MzCompute.Basic
+import MzCompute.Event
+
+namespace MzCompute
+
+/-- Everything `step`'s guards depend on. `created`/`scheduled`/
+`allowedWrites`/`dropped` are total functions `GlobalId → Bool`
+rather than a set or map type, so the model needs no map/set library
+(see Global Constraints in the implementation plan: no Mathlib). -/
+structure ProtocolState where
+  stage : Stage := .creation
+  helloSeen : Bool := false
+  createInstanceSeen : Bool := false
+  /-- Ids exported by a `CreateDataflow` seen so far. -/
+  created : GlobalId → Bool := fun _ => false
+  scheduled : GlobalId → Bool := fun _ => false
+  allowedWrites : GlobalId → Bool := fun _ => false
+  /-- Whether `id` has been allowed to compact to the empty frontier,
+  the canonical "drop" per `command.rs`'s `AllowCompaction` doc. -/
+  dropped : GlobalId → Bool := fun _ => false
+  /-- Last reported value per id and frontier kind. `.at 0` is both
+  the real value `0` and the "nothing reported yet" sentinel. See
+  `Frontier.advances`'s doc comment for why that is sound. -/
+  reportedFrontiers : GlobalId → FrontierKind → Frontier := fun _ _ => .at 0
+  peeks : Uuid → PeekState := fun _ => .notSeen
+
+/-- `true` iff every id in `exports` is currently un-created and the
+list has no internal duplicates, matching `command.rs`'s "dataflow
+exports have unique IDs... do not repeat". Written by hand recursion
+rather than `List.Nodup`/`List.Pairwise` (Mathlib-only in the relevant
+form. See Global Constraints). -/
+def freshExports (created : GlobalId → Bool) : List GlobalId → Bool
+  | [] => true
+  | id :: rest => !created id && !rest.elem id && freshExports created rest
+
+/-- The protocol step relation. Each `ComputeCommand`/`ComputeResponse`
+variant gets one equation. The comment above each cites the
+`command.rs`/`response.rs` sentence its guard encodes. -/
+def step (s : ProtocolState) : Event → Option ProtocolState
+  -- protocol.rs: Hello is the first command of the Creation stage.
+  | .cmd (.hello _) =>
+      guard (s.stage.isCreation && !s.helloSeen)
+        { s with helloSeen := true }
+  -- protocol.rs: CreateInstance completes the Creation stage and
+  -- begins Initialization.
+  | .cmd .createInstance =>
+      guard (s.stage.isCreation && s.helloSeen && !s.createInstanceSeen)
+        { s with createInstanceSeen := true, stage := .initialization }
+  -- protocol.rs: InitializationComplete marks the end of the
+  -- Initialization stage.
+  | .cmd .initializationComplete =>
+      guard (match s.stage with | .initialization => true | _ => false)
+        { s with stage := .computation }
+  -- protocol.rs: UpdateConfiguration is a computation-stage command.
+  | .cmd .updateConfiguration =>
+      guard (!s.stage.isCreation) s
+  -- command.rs:107-108: dataflow exports have unique IDs and do not
+  -- repeat.
+  | .cmd (.createDataflow exports) =>
+      guard (!s.stage.isCreation && freshExports s.created exports)
+        { s with created := fun id => s.created id || exports.elem id }
+  -- command.rs:148-153: Schedule requires a prior CreateDataflow and
+  -- is invalid once the collection has been allowed to compact to
+  -- the empty frontier.
+  | .cmd (.schedule id) =>
+      guard (!s.stage.isCreation && s.created id && !s.dropped id)
+        { s with scheduled := fun id' => id' == id || s.scheduled id' }
+  -- command.rs:158-163: AllowWrites requires a prior CreateDataflow
+  -- and is invalid once the collection has been dropped.
+  | .cmd (.allowWrites id) =>
+      guard (!s.stage.isCreation && s.created id && !s.dropped id)
+        { s with allowedWrites := fun id' => id' == id || s.allowedWrites id' }
+  -- command.rs:185-187, :200-201: AllowCompaction requires a prior
+  -- CreateDataflow. An empty frontier is the canonical way to drop a
+  -- collection.
+  | .cmd (.allowCompaction id frontier) =>
+      let isEmpty := match frontier with | .empty => true | .at _ => false
+      guard (!s.stage.isCreation && s.created id)
+        { s with dropped := fun id' => s.dropped id' || (id' == id && isEmpty) }
+  -- command.rs:219-224: an index-target Peek requires a prior
+  -- CreateDataflow for the target and is treated as illegal once the
+  -- target has been dropped, matching Schedule/AllowWrites. Persist-target
+  -- peeks require neither.
+  -- command.rs:223-224: the peek's uuid must be unique.
+  | .cmd (.peek uuid target) =>
+      guard (!s.stage.isCreation && (s.peeks uuid).isNotSeen
+             && (match target with | .index id => s.created id && !s.dropped id | .persist _ => true))
+        { s with peeks := fun u => if u == uuid then .pending else s.peeks u }
+  -- command.rs:248-250: CancelPeek requires a prior matching Peek.
+  | .cmd (.cancelPeek uuid) =>
+      guard (!s.stage.isCreation && !(s.peeks uuid).isNotSeen) s
+  -- response.rs:37-52: Frontiers reports must never regress, and
+  -- response.rs:52-54 requires a prior CreateDataflow.
+  | .resp (.frontiers id write? input? output?) =>
+      guard (!s.stage.isCreation && s.created id
+             && checkAdvance write? (s.reportedFrontiers id .write)
+             && checkAdvance input? (s.reportedFrontiers id .input)
+             && checkAdvance output? (s.reportedFrontiers id .output))
+        { s with reportedFrontiers := fun id' k =>
+            if id' == id then
+              match k with
+              | .write => applyAdvance write? (s.reportedFrontiers id .write)
+              | .input => applyAdvance input? (s.reportedFrontiers id .input)
+              | .output => applyAdvance output? (s.reportedFrontiers id .output)
+            else s.reportedFrontiers id' k }
+  -- response.rs:66: exactly one PeekResponse per Peek, so this
+  -- requires the peek to currently be pending.
+  | .resp (.peekResponse uuid) =>
+      guard (!s.stage.isCreation && (s.peeks uuid).isPending)
+        { s with peeks := fun u => if u == uuid then .answered else s.peeks u }
+  -- response.rs:106-107: SubscribeResponse requires a prior
+  -- CreateDataflow.
+  | .resp (.subscribeResponse id) =>
+      guard (!s.stage.isCreation && s.created id) s
+  -- response.rs:120-121: CopyToResponse requires a prior
+  -- CreateDataflow.
+  | .resp (.copyToResponse id) =>
+      guard (!s.stage.isCreation && s.created id) s
+  -- response.rs:130-131: Status has no effect on collection
+  -- lifecycles and carries no GlobalId in the current protocol. Like
+  -- every other response, it is only legal once the connection is
+  -- established, i.e. past the Creation stage. A response arriving
+  -- before Hello/CreateInstance is undefined behavior.
+  | .resp .status =>
+      guard (!s.stage.isCreation) s
+
+end MzCompute
+
+namespace MzCompute
+
+-- Hello is legal from the initial state.
+example : (step {} (.cmd (.hello 0))).isSome = true := by decide
+-- CreateInstance is illegal before Hello.
+example : step {} (.cmd .createInstance) = none := by decide
+-- Schedule is illegal before any CreateDataflow.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true }
+    (.cmd (.schedule 7)) = none := by decide
+-- Schedule is legal once id 7 has been created.
+example : (step { stage := .computation, createInstanceSeen := true, helloSeen := true, created := fun id => id == 7 }
+    (.cmd (.schedule 7))).isSome = true := by decide
+-- Schedule is illegal once id 7 has been dropped.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true, created := fun id => id == 7, dropped := fun id => id == 7 }
+    (.cmd (.schedule 7)) = none := by decide
+-- CreateDataflow rejects a duplicate id within the same export list.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true }
+    (.cmd (.createDataflow [7, 7])) = none := by decide
+-- An index-target Peek is illegal once its target id has been dropped.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true, created := fun id => id == 7, dropped := fun id => id == 7 }
+    (.cmd (.peek 0 (.index 7))) = none := by decide
+-- A second PeekResponse for an already-answered uuid is illegal.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true, peeks := fun u => if u == 0 then .answered else .notSeen }
+    (.resp (.peekResponse 0)) = none := by decide
+
+end MzCompute
diff --git a/doc/developer/semantics/README.md b/doc/developer/semantics/README.md
new file mode 100644
index 0000000000000..d136e618bc28b
--- /dev/null
+++ b/doc/developer/semantics/README.md
@@ -0,0 +1,36 @@
+# Lean 4 compute protocol semantics
+
+A mechanized model of Materialize's compute protocol control-plane
+contract: the staging handshake and per-command/per-response legality
+rules documented in `src/compute-client/src/protocol/{command,
+response}.rs`.
+
+Read `compute-protocol.md` first for the reading order and a
+cross-reference from doc-comment sentence to Lean theorem.
+
+This is Phase 1 of a three-phase plan (see
+`doc/developer/design/20260724_compute_protocol_semantics.md`): only
+staging and command/response legality are modeled here. Read-hold
+lifecycle against `AllowCompaction` and multi-replica/worker command
+sharing are later phases, not yet started.
+
+## Relationship to MaterializeInc/materialize#36614
+
+That (at time of writing, unmerged) PR builds a different Lean 4
+model in this same directory: `Mz`, covering scalar evaluation and
+collection semantics (the data plane), under Lean namespace `Mz`.
+This directory's `MzCompute` library covers the compute protocol (the
+control plane) instead, under its own namespace, and was bootstrapped
+independently (its own `Dockerfile`/`lakefile.toml`/CI script) because
+`doc/developer/semantics/` did not yet exist on this codebase's
+history when this work started. If #36614 lands, the two efforts
+reconcile into one `lakefile.toml` with two `lean_lib` targets sharing
+one Docker image. See that PR's design doc and this directory's for
+each library's own scope.
+
+## Build
+
+`ci/test/lean-semantics.sh` builds the `mz-lean-semantics` Docker
+image and runs `lake build` inside it. For one-shot probes (`lake env
+lean`, inspecting a `sorry`'s goal state, and similar), use
+`bin/in-image` once the image exists.
diff --git a/doc/developer/semantics/bin/in-image b/doc/developer/semantics/bin/in-image
new file mode 100755
index 0000000000000..6781af7e64d78
--- /dev/null
+++ b/doc/developer/semantics/bin/in-image
@@ -0,0 +1,40 @@
+#!/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.
+#
+# in-image: run a command inside the `mz-lean-semantics` Docker
+# image with the project's `MzCompute/` and `MzCompute.lean`
+# bind-mounted.
+#
+# Examples:
+#   bin/in-image lake build
+#   bin/in-image lake env lean MzCompute/State.lean
+#
+# The script assumes the image is already built. Run
+# `ci/test/lean-semantics.sh` once to build it.
+
+set -euo pipefail
+
+script_dir="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+semantics_dir="$(cd "$script_dir/.." && pwd)"
+image_tag="mz-lean-semantics:latest"
+
+if ! docker image inspect "$image_tag" >/dev/null 2>&1; then
+    echo "error: image $image_tag not found. Run ci/test/lean-semantics.sh first." >&2
+    exit 1
+fi
+
+exec docker run --rm -i \
+    --user "$(id -u):$(id -g)" \
+    -v "$semantics_dir/MzCompute:/workspace/MzCompute" \
+    -v "$semantics_dir/MzCompute.lean:/workspace/MzCompute.lean" \
+    -w /workspace \
+    "$image_tag" \
+    "$@"
diff --git a/doc/developer/semantics/compute-protocol.md b/doc/developer/semantics/compute-protocol.md
new file mode 100644
index 0000000000000..4e22401360291
--- /dev/null
+++ b/doc/developer/semantics/compute-protocol.md
@@ -0,0 +1,38 @@
+# Compute protocol semantics: reading order and theorem cross-reference
+
+Phase 1 of `doc/developer/design/20260724_compute_protocol_semantics.md`:
+a Lean 4 model of the compute protocol's staging and command/response
+legality contract.
+
+## Reading order
+
+1. `MzCompute/Basic.lean`: identifiers, `Frontier`, and the small
+   enums (`Stage`, `PeekState`, `FrontierKind`) the model dispatches
+   on.
+2. `MzCompute/Event.lean`: the `ComputeCommand`/`ComputeResponse`/
+   `Event` mirror types.
+3. `MzCompute/State.lean`: `ProtocolState` and the `step` relation.
+   Start here to see how a `command.rs`/`response.rs` doc-comment
+   contract becomes a guard.
+4. `MzCompute/Run.lean`: folding `step` into an execution,
+   `WellFormed`, and two worked example traces (one legal, one not).
+5. `MzCompute/Staging.lean`, `Legality.lean`, `Frontiers.lean`,
+   `Peeks.lean`: the seven theorems, grouped by which part of the
+   protocol they cover.
+
+## Theorem cross-reference
+
+| Theorem | Module | Encodes |
+| --- | --- | --- |
+| `hello_first` / `create_instance_second` | `Staging.lean` | `protocol.rs:52-58` |
+| `create_before_reference` | `Staging.lean` | `command.rs:148-153,158-163,185-187,219-224`, `response.rs:52-54,106-107,120-121` |
+| `no_reference_after_drop` | `Legality.lean` | `command.rs:152-153,162-163` |
+| `create_dataflow_ids_fresh` | `Legality.lean` | `command.rs:107-108` |
+| `frontiers_monotone_and_terminal` | `Frontiers.lean` | `response.rs:37-51` |
+| `peek_response_unique` | `Peeks.lean` | `response.rs:66-69` |
+| `cancel_requires_peek` | `Peeks.lean` | `command.rs:248-250` |
+
+This table is the concrete form of the design doc's Success Criteria
+("a reader can go from a doc-comment sentence... to the Lean lemma
+that encodes it, and back"). Keep it in sync if a later phase adds or
+renames a theorem.
diff --git a/doc/developer/semantics/lakefile.toml b/doc/developer/semantics/lakefile.toml
new file mode 100644
index 0000000000000..18b29be5dfe8f
--- /dev/null
+++ b/doc/developer/semantics/lakefile.toml
@@ -0,0 +1,5 @@
+name = "mz-semantics"
+defaultTargets = ["MzCompute"]
+
+[[lean_lib]]
+name = "MzCompute"
diff --git a/doc/developer/semantics/lean-toolchain b/doc/developer/semantics/lean-toolchain
new file mode 100644
index 0000000000000..33e0c088939ad
--- /dev/null
+++ b/doc/developer/semantics/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.29.1