Skip to content

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

46 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

spec-forge

A Claude Code skill that adversarially certifies a specification as behaviorally complete — before any code is written.

The goal is not a longer spec. It is a spec with no observable residual freedom:

Spec S is behaviorally complete iff every implementation satisfying S is observationally equivalent to every other, under a declared observation alphabet Σ.

Names, formatting, and internal structure are not in Σ, so a complete spec does not have to mention them. What it must not do is leave a coding agent guessing about behavior that Σ can see.

Why this exists

If you hand a spec to a coding agent and it stalls — asking questions, or worse, silently inventing unstated behavior — the spec was underdetermined. That is measurable without rendering the application:

A spec is underdetermined exactly where an adversary can exhibit two implementations that both satisfy it and diverge on Σ.

That divergence is the gap, it is localized, and it is already a test case. spec-forge runs adversaries to produce those distinguishing pairs, has a human ratify each one, and turns the ratified answers into clauses and into the acceptance suite. You never author the acceptance suite; you harvest it from the ambiguity resolution.

Two limits are stated up front, because pretending otherwise would be a lie:

  1. The limit is Rice, not Gödel. "Is S complete?" is undecidable in general, so the process is adversarial and statistical and issues a certificate, never a proof. The certificate has a mandatory RESIDUALS section.
  2. Completeness is relative to (agent class A, toolchain T). spec_bits + prior_bits + toolchain_bits ≥ behavioral_entropy. A non-zero integer type discharges "quantity is always ≥ 1" totally and unspoofably; a language without that type needs prose plus a runtime validator plus a property test to get the same teeth. The same spec can be complete in Rust and incomplete in Python, so the certificate names A and T.

Acceptance criterion

Spec completeness = the coding agent's question count + its uncited-decision count. Both zero, or you are not done.

Not "a human read it and liked it." That is not a gate, it is a chore, and it is the first thing anyone skips.

Installing

The repo root is the skill. Put it where Claude Code looks for skills:

git clone https://github.com/blentz/spec-forge ~/.claude/skills/spec-forge

Then ask Claude something like "is this spec complete?" or "certify this spec" and the skill triggers. Python assets are stdlib-only; spec_gate.sh needs bash and python3.

Prerequisite: the Workflow tool. Every phase from 1 on is a Workflow({ scriptPath }) call, and it is not delegable — subagents do not get the tool, so you cannot hand this skill to a general-purpose agent and walk away. Drive it from the main loop.

The workflows/*.js files are Workflow scripts, not Node programs. node workflows/ontology.js will fail: agent(), parallel(), and phase() are injected by the Workflow runtime.

The pipeline

Phase 0    OBSERVATION.md     declare Σ — what counts as observable
Phase 0.5  SPEC.md            CLAUSIFY: prose → S-NNN clauses
Phase 1    ONTOLOGY.md        subject × stimulus grid; the adversary work-list
Phase 2    WITNESSES.md       underdetermination loop — run until DRY        ←──────┐
Phase 2b   contradiction      contradiction hunter — run until CLEAN                │
Phase 2c   ratification       did the answer actually ANSWER? earns `seen`          │
Phase 3    spec-mutation      anti-vacuity: every clause must carry bits            │
Phase 4    CERTIFICATE.md     Σ, A, T, dry rounds, RESIDUALS                        │
Phase 5    DISCHARGE.md       route each clause to its cheapest enforcement rung    │
Phase 6    build loop         harness first, implementation last  ─────────────────┘
                                                    uncited decision = new witness

Phase 1 is 3% of the spend and finds the worst defects — including entities the author never named, which cannot show up as a MISSING cell because they have no cell. Never skip it.

Driving it

Use the driver. Do not drive it by hand.

assets/forge.py init   spec/                      # scaffold EMPTY templates
assets/forge.py status spec/                      # loop state, Σ lint, void counters
assets/forge.py next   spec/                      # what to run now, and why
assets/forge.py next   spec/ --sigma              # the `sigma` arg every workflow needs

assets/forge.py redact spec/ underdetermination \
  --cells cells.json --round 0 --out canary/SPEC.md  # the canary's spec + its receipt

assets/forge.py record spec/ underdetermination out.json --transcripts .forge-transcripts/under-0/
assets/forge.py ratify spec/ decisions.json       # → ledger + clauses + PENDING verification
assets/forge.py verify spec/ ratification.json    # → and only NOW is `seen` earned

assets/spec_gate.sh spec/                         # every mechanical check, one command

Two rules the driver enforces mechanically, because leaving them to an agent's good intentions is "human review is not a guardrail" applied to the agent:

  • --transcripts is not optional. A record without it VOIDS the round, deliberately. Blindness is not a promise an agent makes; it is a property of a run, checked against that run's own transcripts. A round you cannot prove was blind is a round you cannot use.
  • A round whose canary failed is VOID, not DRY. forge record reads the workflow's own void: true and refuses to advance the dry counter. You cannot forget it or talk yourself out of it.
  • The canary must be aimed where the workflow aimed it. Canary liveness is tested by giving a probe a spec with specific clauses physically stripped out. forge redact picks those clauses the same way the workflow does and leaves a receipt; forge record and forge verify check the receipt against what the workflow says it targeted, and VOID on disagreement. A misaimed canary does not fail — it finds some other gap and passes.

ratify exists because a resolution must land in three places or the pipeline lies: the ledger (WITNESSES.md, which is the acceptance suite Phase 6 harvests), the clause it forced into existence, and the seen key so the next round does not re-surface it. A DON'T-CARE is the easiest to lose, because it produces no clause and so looks like nothing happened — it is a carve-out, it goes in the ledger and in RESIDUALS, and the harness must not assert either branch.

The gates

tool when what it refuses
assets/forge.py every phase the driver: void/dry accounting, seen earning, phase gating
assets/blindness_lint.py every forge record --transcripts a round whose agents read source, an oracle, or a reference — greps the run's own transcripts, including Bash, not just Read/Grep/Glob
assets/grid_lint.py after Phase 1 an incomplete cross-product, a dangling or orphan citation, an unjustified IGNORE, weasel text; also emits --fanout, the Phase 2 work-list
assets/citation_lint.py during Phase 6 code→clause and clause→code; a clause nothing cites is a silently-dropped requirement
assets/cert_lint.py before Phase 4 ships a stale hash pin, a missing (A,T), too few non-void dry rounds, unattested blindness, pending verification, surviving zero-bit clauses, unresolved contradictions, a missing discharge table, missing RESIDUALS. Warns on discarded rounds — blindness failures and misaimed canaries
assets/redact_spec.py Phase 2 / 2c canaries a canary that only asks an agent to ignore clauses it can still read
assets/spec_gate.sh CI, and before trusting a certificate runs all of the above: Σ, structure, certificate, consistency, blindness, provenance — plus a syntax check on workflows/*.js, because a phase that dies on a SyntaxError never ran

Cost

Measured on a real 9-clause pass, not estimated.

phase agents tokens what it bought
Phase 2 underdetermination 30 727k 4 root causes
Phase 3 spec-mutation 20 476k 9 clauses
Phase 5 discharge 10 401k the discharge table
Phase 2b contradiction 17 387k 2 contradictions
Phase 2c ratification 11 258k 3 answers checked
Phase 6 build 2 169k harness + implementation
Phase 1 ontology 2 66k 19 absent entities, including a shopping cart with no price

The one lever that mattered: Phase 2c has already proved each clause load-bearing, so Phase 3 does not need to re-prove it. Passing provenClosed to spec-mutation.js made those clauses cost zero agents while carrying stronger evidence — a killing input a human actually ratified. Full pass went from 127 agents / 3574k to 92 agents / 2482k, identical verdicts.

On a small spec (one function, one module), set adversary replication to 1 per cell and recover replication across rounds instead of within them. If grid_lint --fanout asks for more adversaries than clauses × 3, the subject axis has degenerated — that is a Phase 1 finding, not a budget problem.

Anti-patterns

  • Skipping Phase 0. The loop drowns in naming bikeshed and the user learns to ignore witnesses.
  • Shipping Phase 2 without Phase 3. You have built a machine that teaches users to pad.
  • One judge. Judges are agreeable by construction.
  • Counting a dry round with no canary. That is fatigue, not convergence.
  • Letting the agent that produced a witness also resolve it — it now authors both the question and the answer.
  • An IGNORE cell with no written justification.
  • A certificate with no RESIDUALS.
  • Treating "complete" as absolute rather than relative to (A, T).

Layout

SKILL.md                              the skill itself — the full method
assets/*.template                     OBSERVATION / SPEC / ONTOLOGY / WITNESSES / CERTIFICATE
assets/forge.py                       the driver
assets/*_lint.py, spec_gate.sh        the mechanical gates
workflows/*.js                        Workflow scripts, one per phase
references/lessons.md                 the scars: how an agent games each gate. Read first.
references/observation-alphabets.md   Σ: twelve dimensions, class templates, five mistakes
references/ontology-grid.md           Phase 1: subject × stimulus, verdicts, fan-out policy
references/toolchain-profiles/        Python (highest spec bar) and Rust (lowest), side by side

License

GNU Affero General Public License v3.0. See LICENSE.

About

A Claude Code skill that adversarially certifies a specification as behaviorally complete — before any code is written.

Resources

Stars

0 stars

Watchers

0 watching

Forks

Contributors

Languages