Are you an LLM? Read llms.txt for a summary of the docs, or llms-full.txt for the full context.
Skip to content

SpecGen

A framework for protocols whose spec, code, and deploy are the same artifact. Humans write intent and review the resolved spec; SpecGen formats the prose, extracts claims, induces a protocol DSL, binds it to Lean, generates the implementation, runs every downstream witness against the generated SDK, checks the published bytes equal the generated bytes, attests the deployment, and emits a signed report any agent can verify in ten deterministic steps.

When the gate is green you don't have a spec and an implementation and a deployment that you hope agree — you have one artifact in three forms, each cryptographically linked to the others.

How it works

The loop makes each form a verifiable derivation of the one above it:

  1. Intent → prose. Humans write seed intent and formatted prose in ordinary protocol language, carrying RFC 2119 normative force.
  2. Prose → claims. The loop extracts claim sidecars bound to exact source spans of the prose.
  3. Claims → Lean. Each claim binds to Lean definitions and theorems — the canonical form a kernel checks.
  4. Lean → reference. An executable Lean model becomes the runnable reference (the referee).
  5. Lean → code. CodeGen emits the SDKs, the node, the Rust/WASM kernel, and the Cloudflare Worker from that Lean — every emit byte-deterministic, each artifact's sha256 pinned in a manifest.
  6. Witnesses. Downstream consumers run their own tests against the generated SDK and emit a signed receipt naming exactly which bytes they ran.
  7. Release gate. A Lean-anchored gate is true iff the structural invariants, operational witnesses, provenance records, and content-review decisions all agree.
  8. Signed report. When the gate is green, SpecGen emits a signed report a third party can verify in ten pure, deterministic steps — no rebuild, no network, no trust in the publisher.

A human can enter the loop at any point — prose, a claim, Lean, an implementation observation, or a witness failure — and the loop reconciles the other forms until it reaches the ceiling.

What makes it sound

The DSL vocabulary is empirically auto-created by agents and continuously revised — but it's never accepted as "vibe text." The loop admits a structure only when selectors bind to prose, claims bind to Lean, theorems compile, generated artifacts match their hashes, and witnesses pass against the generated SDK. The LLM proposes structure; the validators and the Lean kernel decide.

Protocol-agnostic

SpecGen ships the kernel, schemas, validator, codegen seams, witness registry, publish chain, and verifier — and zero application content. The ENC protocol is one instance that supplies its own Lean, prose, claims, and a single config; CodeGen is that instance's emit layer.

See also