spec-lean

Files (15)

• SKILL.md
• build.md · references/
• checks.md · references/
• memory.md · references/
• plan.md · references/
• verify.md · references/
• check_commit.py · scripts/
• checks.md · scripts/fixtures/
• plan.md · scripts/fixtures/
• verification.md · scripts/fixtures/
• lessons.py · scripts/
• selftest.py · scripts/
• validate_checks.py · scripts/
• validate_plan.py · scripts/
• validate_verification.py · scripts/

SKILL.md (first lines)

# Spec, Lean

Freeze the obligations. Free the plan. Prove it with someone who did not build it.

```
┌──────┐   ┌────────┐   ┌───────┐   ┌────────┐
│ PLAN │ → │ CHECKS │ → │ BUILD │ → │ VERIFY │
└──────┘   └────────┘   └───────┘   └────────┘
 read it    obligations   yours       always
```

Four moves, two artifacts before code, one after. A human confirms **what** must be true and
**how** it is being built in one document, and only then does any of it become an obligation with
a proof attached. There is no task breakdown, and the plan carries no component catalogue: what is
hard to reverse gets a one-way door with its literal shape, and everything reversible is decided
while building and reviewed in the diff.

## Why this shape

The dominant failure of a coding agent is not bad reasoning, it is a requirement that was read
and never became an active obligation - and then a completion claim on top of it. The
mitigation that measures well is a **small, frozen, external obligation set** plus a
**verifier that is not the author**; a self-check reproduces the author's own blind spot. So
this skill spends its budget on those two things and refuses to spend it on choreographing how
the model works.

Two consequences worth stating up front, because they are what make this different from a
conventional spec-driven flow:

- **Granularity is not quality.** Splitting a feature into fifteen one-file tasks buys
  ordering, not correctness, and it costs a re-read of the process on every task. Proof
  coverage buys correctness.
- **A plan the model must obey competes with the obligations for attention.** Fields like
  `Where`, `Tools`, `Depends on` are the model's job to decide, so they are not written down.

## Critical rules

The pinned set. These hold even if no reference file is read, and they are the only rules that
never scale down with the profile.

1. Every check is **one observable claim with a concrete value** plus the **proof** - the test
   or command whose exit code settles it. No proof, no check.
2. Tests assert what the checks say, never what the code happens to do. Never write a test by
   reading the implementation.
3. Never weaken an assertion, delete a test, or skip one to make a suite pass. A genuinely
   wrong check is a stop-and-ask, not an edit.
4. Checks and `Test policy` rows are fixed once approved. In the design, `Landing`, `Relations`
   and `Surface` are additive - a door discovered while building gets a row before the code that
   closes it, and a row the user approved is never rewritten. `Flow` and `Impact` are neither:
   they are **kept true**, so a different path changes the hop in that path's commit.
5. The **Verifier is a fresh sub-agent**, never the author, never optional, never waiting to
   be asked. Whoever holds the whole feature dispatches it after the **last commit of the
   feature** lands - over `<feature base>..HEAD`, with **every** check. Never by a builder,
   and never as a child of one. A builder finishes, reports, and stops. The work is not done
   at the last commit; it is done when the Verifier's report accounts for every check.
6. **The profile is a floor and it is not a secret.** The verification report names it, or "no
   faults injected" reads exactly like forgetting to inject them.
7. The completion gate is a script, not a feeling: `validate_verification.py` must exit 0.
8. **Blast radius:** an approved spec authorizes local edits and local commits. `git push`,
   deploy, and production data changes need an explicit go-ahead for that action.

## Profile

The project declares how much runs, in `AGENTS.md` or equivalent. Absent a declaration:
`standard`. Same three levels as `tlc-implement`, gated the same way, so moving between the two
skills needs no second vocabulary.

```markdown
## spec-lean

profile: standard
budget: 180k
```

| Profile | Adds | Cannot catch |
| --- | --- | --- |
| `light` | proofs run at `HEAD` with each named test shown to exist and run, one located assertion per check, level and sampling gaps, `Swept existing` re-read | a set member with no proof; a test that would pass under a wrong implementation |
| `standard` (default) | the `Coverage` join recomputed, `Test policy` rows with a verdict each, one fault per assertion surface | a check that contradicts a binding source; a screen nobody built |
| `ui` | binding sources opened and compared, per-screen enumeration of copy **and** arrangement | only spacing, colour and type weight, enumerated per screen |

Each step adds a **class of failure detected**, so a cheap profile is not a discount on the
same product - read the right column before choosing it. Two things about `light` are worth
saying out loud, because its own row says them and they are easy to skim past: it will not
notice an enumerated set member that nobody proved, and it will not notice a test that passes
under a wrong implementation. `standard` exists for exactly those two.

`ui` costs nothing on work with no interface: every screen step is conditional on a screen
existing. A step whose input is empty costs a line, not a pass ("no set rows", "no binding
source").

The `Coverage` join is **written** into `checks.md` at every profile - the join is what makes an
omission structural, and that costs nothing at authoring time. What `standard` buys is the
Verifier **recomputing** it from the authority over each set instead of reading the author's
table back.

The profile is a pin, not a preference, and unlike `tlc-implement` that is enforced rather than
asked for: `validate_verification.py` fails a report whose profile differs from the one
`checks.md` was approved under, and fails a `standard` report with no fault rows or no
recomputed coverage, and a `ui` report with no binding-sources section. So a step that did not
run stays distinguishable from a step that was forgotten, which is the whole reason to declare
a floor.

Where the profile looks too thin for the feature in hand, say so in one line and let the user
raise it. Doing more than the profile in silence costs the predictability that made declaring
it worthwhile.

## Artifacts

```
.notebook/specs/
├── STATE.md                    # Decisions log (AD-NNN) + Handoff snapshot
├── LESSONS.md                  # rendered by scripts/lessons.py - never hand-edit
├── lessons.json                # machine-owned
└── features/<feature>/
    ├── plan.md                 # problem, flow, impact, then the rest of the shape, then criteria; audit last
    ├── checks.md               # claims + proofs, the coverage join, test policy, swept
    └── verification.md         # the Verifier's report
```

From leaofelipe/ia-stuff, CC-BY-4.0.

More from leaofelipe/ia-stuff