Derive the spec by running the thing. Freeze it. Gate the drift.

You write a module's meaning — its types, its validity rules, its operator functions. Everything checkable about it is then derived from the code, committed as a file, and re-checked on every build: the behaviour spec, the module boundaries, the mutation-testing verdicts, even the CI pipeline itself. You stop hand-writing the copies of your intent that normally rot (tests, configs, docs) and start reviewing them as diffs instead.

This page is layered: each section opens plainly and folds its full-density version behind a click. Reading top to bottom without clicking gives you the whole idea; the folds carry the precision. For the long-form walk with one running example, take the tour.

The bet, stated falsifiably: a module boundary can be specified precisely enough that the tests validating it write themselves. The yardstick is mutation — plant bugs in the interior and count what survives. The interior of the lead example (a full expression-language interpreter) carries zero tests of its own, and every viable mutant dies anyway.

cargo run --example gate    # every gate CI runs, locally, from the same declaration
cargo test --workspace      # all suites + every drift gate + in-process mutation

You write two or three small functions. The discovery engine runs them against a grid of inputs, tries every law shape in its catalog, and writes down everything it could not break — in plain language, with the equation underneath. This is a real committed file, spec/bridged-bool.spec:

- not twice returns the original value.
      not(not(x)) = x
- not turns and into or.
      not((x and y)) = (not(x) or not(y))
- and with true leaves a value unchanged.
      (true and x) = x

Nobody typed those sentences. Commit the file, and every cargo test re-derives it from the live code and fails on any difference — so an unintended behaviour change is a red build that names the exact sentence that appeared or vanished, and an intended one is a plain-English diff your reviewer approves. The committed diff IS the ratification. The file is a lock: same lifecycle as Cargo.lock, but for behaviour.

You can also run the loop in reverse — declare what you intend before the code earns it:

expects {
    commutative(join);
    identity(join, bottom);
    nontrivial(tick);          // an INEQUATION: the clock must actually move something
}

and the distance report tells you exactly what's missing, like a compiler error for behaviour: MISSING: identity(join, bottom). Expectations get you TO the lock; the lock keeps you there.

#[algebra(Lattice, "tri lattice")]
pub mod lattice {
    #[derive(Shaped, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
    pub enum Tri { Lo, Mid, Hi }

    pub fn meet(a: Tri, b: Tri) -> Tri { a.min(b) }
    pub fn join(a: Tri, b: Tri) -> Tri { a.max(b) }
}

spec-lock is the whole freeze/gate/ratify mechanic as one zero-dependency crate — Lock { name, path, live } plus bless and check. If your project can derive any deterministic text about itself (an API census, a schema dump, a config baseline, an exception register), spec-lock turns it into a drift-gated, review-ratified artifact in minutes; the first production adoption applied it to five substrates in a day, by agents who had never seen this repo, from this README alone. Its sibling fire-drill is the opposite polarity: a standing battery of known-bad fixtures proving your gates can still FIRE. And delta-render is the newest: generated incremental-computation code whose optimisation rules are licensed by discovered specs. Adopt as much or as little as pays.

The same move — declare, derive, freeze, gate — applies at every level of a program:

The pipeline row deserves a plain-language beat, because everyone has lived the alternative: a hand-authored ci.yml that nothing cross-checks, drifting from the README's instructions for years. Here the gates are declared once as data — each with its command, its cadence, and a sentence saying what it promises — and the YAML is rendered from that table. A hand edit to the YAML fails cargo test inside the very workflow the YAML executes, and cargo run --example gate runs the same table locally: green locally and green in CI are the same claim.

Every law any spec can state is one of the shapes in a single ratified catalog — and that catalog is not documentation of the engine, it is the engine: discovery is a generic interpreter over the catalog's data. Adding a new kind of law to the language means adding one stanza of data, and every theory in every project benefits the moment it lands.

A generated spec sounds great until you ask whether it's weak. The answer is blunt: plant a bug on purpose and see if anything goes red. A planted bug nothing notices is a survivor — a real finding, stated exactly: there is a bug the spec cannot see. Every survivor either gets a law/test that kills it or a one-line justification in a hand-maintained exception register the build enforces ("2 new findings, 1 resolved" is the whole review).

One declaration — value objects with executable validity rules, operators, seams, declared expectations — generates a whole workspace member, down to the target spec files discovery should reproduce once you fill in the marked MEANING: holes. What remains to author is exactly the irreducible part: what the operators mean.

The engine's law graph doubles as a modularity instrument: it can tell you a module is secretly two modules, that a layer wants to exist, or that a bag of functions contains three coherent groups and some misfits. All of it is a suggestion a reviewer ratifies, never a constraint — reports suggest; locks gate.

Beneath discovery sits a boundary grammar where claims that can be statically false are build errors: unvalidated values can't reach evaluation, effect ceilings and cost budgets reject at compile time, and whether a module is a "boundary" at all is computed and committed as a census rather than asserted by naming convention.

You change something; cargo test goes red naming the exact stale artifact and its regeneration command; you regenerate; the diff that lands in your commit is the review. Never hand-edit a generated artifact — a missing lock is stale, never fresh.

cargo run --example gate runs every every-change gate from the same declaration CI executes; cargo run --example discovered_spec prints the live specs; each analysis above has its own example binary.

Discovery refutes, it never proves: grids are bounded, term enumeration is depth-bounded, batteries are samples. A discovered law is one the bounded grid could not refute; a witness law refutes triviality without proving richness; a mutation survivor is "indistinguishable on this grid", never an equivalence proof. Reports suggest; locks gate. What remains irreducibly human (or agent): the validity rules, the operator meanings, ratifying each diff, rejection tests, and the trust root — rustc, cargo-mutants, typewit.

This project advances by thrown bricks, and some of its best came from outside: the bias shapes exist because a hostile domain embarrassed the monoid laws, the witness shapes because the mutation harness named what equations cannot say, fire-drill because a production adoption's field notes described three vacuous gates in one day — and the human-facing tour because a reader said the docs lost them. If you are working with this library and you see an idea the method is missing — a lock it should have, a shape the catalog lacks, a friction worth dissolving, a place a gate went quiet — file an issue, in field-note form: what you were doing, what the method could not say or catch, what you built around it. Wrong ideas are cheap; the roadmap exists to catch the good ones.

• docs/tour.md — the long-form gentle walk: five stations, one running example, a marked exit after each.
• docs/discovery.md — the discovery half, precisely: theories, the grid, the catalog's fields and driver semantics, expectations, every lock kind, seams and system!, genesis, the world lock, the gate registry, algebra mutation.
• docs/compile-time.md — the compile-time half, layered like this page: the edge grammar end to end, with the graded category, the gradings' self-proofs, and the probe taxonomy one fold in.
• docs/ci-discipline.md — the extractable pattern (deterministic spec → frozen file → drift gate → diff-scoped mutation) and the standalone spec-lock crate that carries it to any project.
• docs/roadmap.md — the brick chronicle: what's built, what's next, and the findings that redirected the method.
• docs/experience.md — the authoring-experience program and its residuals.
• CLAUDE.md — the working discipline, distilled for agent sessions.

[dependencies]
boundary-spec = "0.1"

Model the domain as value objects and operators (#[algebra] for the hands-free path, theory! where an observation or grid is a deliberate choice), declare what you intend with expects, freeze with Spec::of::<T>().lock_in(your_spec_dir), and gate the drift with spec_lock::check in a test. Freeze the mutation verdict beside it (MutationReport::of::<T>().lock_in(...)) and your theory core's mutation testing runs in-process, in milliseconds, with no CI job — reserve cargo-mutants for your plumbing (downstream-fixture is the copyable proof; the substitution is measured in docs/discovery.md). The interior stays ordinary Rust — rigidity lives at the boundary, paid once.

Dual-licensed under either of Apache-2.0 or MIT, at your option. Unless you state otherwise, any contribution you submit for inclusion shall be dual-licensed as above, without additional terms.