Write down the method as practiced

AGENTS.md

@@ -26,6 +26,7 @@ When you hit a wall — a case that doesn't fit, a spec that breaks, an assumpti
 NEVER patch around a wall to comply with my words — no flags, special cases, shims, parallel paths, or tests rewritten to dodge a broken rule.
 Building around a blocker is failure and will always be rejected, sunk cost irrelevant.
 A blocker honestly reported is a desired outcome; a "working" deliverable built on duct tape is sabotage.
+Evidence outranks every artifact: when code or a measurement disagrees with a spec, doc or decision, change it in that PR; never defend it.
 
 # GITHUB
 Pull Requests (PRs) are the units of work; only ever create PRs. No issues: the PR is the only record.
@@ -44,7 +45,7 @@ Squash trades bisect granularity for readable history: the unsquashed commits st
 A leaning lives in the description of the PR that will settle it. Once code settles it, the why is a doc comment. No third document.
 Only #7 (Horizon) and PRs in progress are open. Until its PR exists, a leaning is a comment on #7, in the description template; scope it there, and when it is ready, open its PR and delete the comment.
 
-The first commit is the spec, when `CODE.md` says the seed's shape demands one; its checker is green before any code exists.
+When a PR changes what the spec says, its first commit is that change, TLC green, before any code.
 The next commit is typed stubs ONLY: types and signatures, placeholder bodies, the language's type gate green. The diff defines that PR's scope; one signature per action of the spec. `CODE.md` names each language's stub and gate.
 Subsequent commits fill those stubs.
 **Zero placeholders may remain at merge. This is always a hard requirement.** `CODE.md` names what counts as a placeholder and the lints that count them.

CODE.md

@@ -5,9 +5,8 @@ Push every invariant you can into the types, cover the rest with tests, and spen
 # Method
 
 Spec, skeleton, fill. TLA+, Lean and Rust are one pipeline, not alternatives: TLA+ specifies the system (processes and how they interleave), Lean specifies a core (a pure function and its properties), Rust is the system.
-**Unpracticed until `initial-spec`; confirm the approach for each PR.**
 
-1. **Spec.** `spec/cead.tla` states what every behaviour of cead satisfies. Coarse and revisable: when code disagrees with it, the spec changes in that PR.
+1. **Spec.** `spec/cead.tla` states what every behaviour of cead satisfies. Coarse and revisable.
 2. **Slice.** A PR takes a slice of the spec. Its dependencies are probed while scoping; findings go in a PR comment, the probe is never committed.
 3. **Core.** A pure function with a property worth proving gets its Lean spec first, green before any Rust.
 4. **Skeleton.** One commit of types, signatures, private fields and one doc comment per item (what it owns, when it drops); bodies are `todo!()`; the type gate is green. It is the spec of custody. It mirrors the spec: variables become fields, states become variants or typestates, each action becomes one signature.
@@ -116,11 +115,13 @@ Everything else (fields, structs and enums, most traits, invariants like `len 
 
 # TLA+
 
-- Modules are `spec/<name>.tla` with `<name>.cfg`; the system spec is `spec/cead.tla`. A layer whose state multiplies another's gets its own cfg over the same module (`spec/tree.cfg`). TLC is green before any Rust exists; the commit line records the TLA+ tools version and the bounds it passed at.
+- Modules are `spec/<name>.tla` with `<name>.cfg`; the system spec is `spec/cead.tla`. A layer whose state multiplies another's gets its own cfg over the same module (`spec/tree.cfg`). The commit line records the TLA+ tools version and the bounds it passed at.
 - A PR that changes a protocol re-runs TLC, by hand until CI is demanded.
+- Every property has a mutation TLC catches.
+- Committed cfgs run in about a minute; larger bounds are one-off runs recorded in the PR.
 - **spec**: a formula over behaviours of a state machine. **action**: one transition; one signature. **invariant**: what every reachable state satisfies; what TLC checks. **instance**: the bounds TLC searched; a proof only up to them.
 
 # Lean
 
-- Lean 4 via elan, toolchain pinned in `lean-toolchain`, one lake project in `spec/`. `lake build` green before any Rust exists.
-- **spec**: an executable definition. **theorem**: a property proved of it. **differential test**: random inputs through spec and Rust, outputs compared in `cargo test`; the only tie between them. How spec outputs reach `cargo test` is for the first Lean PR.
+- Lean 4 via elan, toolchain pinned in `lean-toolchain`, one lake project in `spec/`. `lake build` green before the Rust it specifies.
+- **spec**: an executable definition. **theorem**: a property proved of it. **differential test**: random inputs through spec and Rust, outputs compared in `cargo test`; the only tie between them.