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:
SpecS
is behaviorally complete iff every implementation satisfyingS
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.
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:
The limit is Rice, not GΓΆdel."IsS
complete?" is undecidable in general, so the process is adversarial and statistical and issues acertificate, never a proof. The certificate has a mandatory RESIDUALS section.** 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 namesA
andT
.
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.
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.
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.
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:
A--transcripts
is not optional.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 ownvoid: 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
andforge verify
check the receipt against what the workflow says it targeted, and VOID on disagreement. A misaimed canary does not fail β it finds someothergap 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.| 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 |
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.
- 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)
.
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
GNU Affero General Public License v3.0. See LICENSE.