dnaContract · v1 BUILT · F0–F6 + SLM and "tissue" waves + mini-F7 · 2026-08-20

Anatomy of v1

A living compiler of ontologies — built and passed its exams in a single day: 10 exams (95+ items green), 63 tests, the onto engine. The genome is executable; contracts are proved by the court; a change of behavior turns into a question; the ribosome writes algorithms with a live SLM for $0.001; a fresh agent shipped a feature on the first try. v0 = archgen (a donor of scars); final state — PLAN.md/JOURNAL.md.

The whole picture at once

The main difference from v0 and from draft-0 of this same spec: this is not a pipeline with a "build" stage. At the center is an organism that lives by interpreting the genome from second zero and is correct by definition. Around it are three loops: metabolism (measured heat → warming hot paths with code), interview (underspecification → question → genome diff) and measurements (measured displaces declared in the formulas). There is no deploy: there is a genome version × a degree of warm-up.

Human / LLM via MCP genes · bind/pins · MCP tools · interview answers (ack_behavior_change) propose (MCP/CLI) — the only write path; the warden daemon picks it up via watch Loading onto:N → hub-IR · Expr → typed AST Mutation gates (mutgate) checkers · COURT (DISPROVED = reject) · semdiff → ack — same ones for warden and propose REJECT with reasons ORGANISM — alive from second zero reference interpreter executes Expr rules; slow, but correct BY DEFINITION; eternal fallback warmed bodies JIT cache: idiomatic code for hot paths; passport verified: proved|fuzzed cooled ones — evicted event log · replay · monitors · SKILL ORGAN /skill/<name> (certified cache) subtracting its own actions; dedup by window; warden: molt 0.3s, REVOKE on quota no deploy: uv tool install + systemd (onto unit); NOT built: in-process JIT (D28), the live seam theory/ + provenance executable formulas with preconditions; classes Derived/Declared/Measured, contagion rule; CI recomputes constants with lineage Placer — control loop costs × measured demand → warm-up plan, evictions, layouts; refusal with arithmetic; molt proposal — by the ladder of rights measured heat: traffic, latencies, η what to warm up Ribosome — CEGIS SLM writes SKILLS (rules are printed, D27); live CEGIS: red → counterexample → GREEN (fact); semantic cache — a repeat with no network candidate body Court SMT: body ≡ reference, post/inv — theorems; fuzz — where undecidable; mutants calibrate the prover; the passport is honest counterexample → into the prompt (CEGIS); doesn't converge → step up proved → into the warm-up cache Interview two candidates passed the contracts, but diverge → the solver synthesizes a divergence input → a question with ready-made options to extend the contract underspecification question with an executable counterexample → answer = genome diff via propose; ledger remembers — the question does not repeat measured η, L, demand LEDGER every arrow in this diagram is a record: generation, proof, rejection, question, answer, warm-up, eviction, molt, revocation of rights. "Why did the module have that right" — always answerable.
The organism and three loops — now all of it is working code. The mutation gates (mutgate) are the same for the warden daemon and propose/MCP; the interview loop is built into the flow (a behavior change without ack is rejected with an executable example); metabolism is measured live (the wallet was moved out at 945 events/s). Honestly not built: the per-rule-correct JIT (D28) and the live traffic seam.
green: proved / measured / reference amber: interview / counterexample / island red: rejection with a reason

Passed by exams (all items green)

ExamKey facts
F0 decisions and skeletonExpr spike: py-ast won; the SMT court shown already in the spike (a mutant caught [av=0, cap=1]); linters go red on smuggled-in code
F1 living reference (5/5)organism WITHOUT code generation: judge 5/5, kill -9 → replay byte-for-byte together with the dedup window; smuggler (204 AST nodes) rejected as a skill; conformance corpus 240
F2 court and first tissue (9/9)post/conserves PROVED; 21/21 mutants distinguished; interview on scar-13 with ready-made patches; go: the same judge 5/5, warmed path ~29,000×, floorDiv trap caught by the corpus
F3 second language (9/9)one genome → interpreter + go + python, one judge, snapshots identical, core git diff EMPTY (I1 in practice); the python printer = ast.unparse
F4 composition and genes (10/10)the payments gene in hotel and shop byte-for-byte; genome/phenotype 0.19 (target ⅓; v0 ≈ 0.75); explain slice 37%; the court proved the EQUIVALENCE of a mutant (D32)
F5 metabolism (8/8)load shift (wallet 945 events/s measured) → molt_proposal (gain 117.5s > build 5s) → move-out, bodies byte-for-byte; REFUSE "0.0001ms < floor 0.0064ms, pay with…"; lesson D34 — measurement parity
F6 life (9/9)a feature by genome alone (molt 0.3s, data alive); schema change: without a functor a refusal, with a functor the log migrated with a backup; storm → REVOKE of rights; auto-molt by heat; replay does not spin the monitors (D36)
SLM wave (5/5)live CEGIS: qwen3-coder red → counterexample into the prompt → GREEN attempt 2; fast attempt 1; complexity budget t(4n)/t(n)=4.3≤8 (D38); a repeat — cache with no network; ~2.8k tokens
"tissue" wave (8/8)court+semdiff in the flow (mutgate, D40); skill organ /skill (D41); propose+MCP mouth (D42); the warden daemon picked up the mutation itself; uv tool install verified
mini-F7 other handsa fresh agent with no context: a freeze feature via genome, validate+court ALL PROVED ON THE FIRST TRY, a live noop(guard); its DX findings → docs/OPERATOR.md

0What the human writes

The only source code is the genome: a composition of modules with explicit interfaces. A module declares exports (events, entities, queries, skills), requires (what it expects from others) and contracts (invariants, conservations, idempotence). Kinds of modules: entity module (state + rules "state × event → state", rule bodies are executable Expr expressions), skill gene (algorithm: signature + properties + reference oracle + budget), overlays (level, invariant, read model), membrane (external + hand-written island). The root genome — imports, binding, demand spectrum, pins.

New in v1: a significant part of the contracts the human does not write but chooses — by answering interview questions (stage 9). The goal: > half of the genome's contract lines are born from answers, not from one's head.

shop.onto — root genome import + bind · demand spectrum · layout pins · nothing more import + parameters (key type, names) — monomorphization at link time inventory · entity module exports: entity sku; events OrderPlaced/Cancelled contracts: conserves, idempotent, post rules: executable Expr billing · entity module requires: OrderPlaced exports: Invoice, events InvoiceIssued contracts: sum(paid) ≤ … matching · skill gene exports: match_orders signature + 5 properties + reference oracle + budget ns/op billing consumes OrderPlaced from inventory: only through requires/exports. You cannot rewrite someone else's rule — extending a provider = its new version with a functor. The gene is the unit of exchange (gene pool, §12).
Composition through interfaces, not inheritance. A consumer by construction cannot break the provider — conservativeness (thm. 6) is checked per module. One module is reused across different genomes; the body cache travels with it.

1Loading: versions and hub-IR

The genome language is also an ontology and it too molts. Each file carries the version onto: N; in memory there is one internal model hub-IR (typed, without extra=allow); converters translate any file version into the hub. Everything further down the diagram sees only the hub. A change of vocabulary = a new converter + onto fix (auto-rewrite of files), not "eternal support" and not "everyone broken." Precedents: k8s apiVersion, Rust editions, go fix. The self-application test: an engine that cannot migrate its own language has no right to promise migration of others' schemas.

genome A · onto: 1 old file — is read genome B · onto: 2 yesterday's genome C · onto: 3 current version converter v1→hub v2→hub v3→hub hub-IR the single internal model, typed, Expr already parsed into AST consumers checkers · interpreter · Placer · court · dialects · ribosome · migrator — see only the hub onto fix — automatically rewrites the file to the current version (functor thm. 6 applied to the language itself); the old version is read for K releases, then honestly dies.
Hub-and-spoke. The growth of the language is disciplined twice: patterns before primitives (UNEXPRESSIBLE — the gate of IR growth) and versions with auto-fix for the inevitable changes.

2Expr: the expression language (SMT-compatible)

All the "smart strings" of the genome — postconditions, guards, conservations, invariant predicates, skill properties, queries — are one expression language (a borrowing candidate — CEL; decided by the F0 spike). Literals, fields, arithmetic, comparisons, logic, aggregates, lambdas; no loops. Rule bodies — Expr plus assignments (a restriction: an AST node limit; anything harder is a skill).

New requirement in v1 (§9): the semantics of Expr must have a direct SMT encoding (linear integer arithmetic + bounded aggregates) — on this depends what the court can prove rather than fuzz. Everything that breaks the encoding goes into skills.

post: "s.available >= 0 && s.available <= s.capacity" parser + typechecker (does s.available exist? type int? is post — bool?) && >= <= s.available 0 s.available s.capacity four consumers of one tree go-stdlib s.Available >= 0 && … python / rust dialect printers interpreter reference semantics (§10) SMT encoder court theorems (§9) The same AST: printing to dialects, execution (reference), proofs (SMT), mutants (tree transformations). Strings are never parsed by regex again (S2), and Go does not live in the core (S1).
One tree — four consumers. The two green ones are the new pillars of v1: the interpreter makes the genome executable, the SMT encoder makes the contracts provable. Both requirements shape the design of Expr from day one.

3Checkers

4Living reference: the interpreter

The backbone of v1 (SPEC §10): the genome is executable on its own. Rules — Expr with assignments — are executed by the reference interpreter: an event arrived → the guard checked → the rule body computed → the state updated → the event to the log. The HTTP harness, event log, replay, snapshots — a generic runtime, one for all genomes. Slow? Yes. But correct by definition — the reference is the meaning of the program. The organism lives and answers the judge before the first line of generated code is written, and the interpreter forever remains the fallback: an evicted warmed body — the path simply returned to the reference.

This inverts v0: there the code was the only way to live, and "meaning" was smeared across bodies from the SLM (two bodies with different semantics passed the same gates — scar S13). In v1 the meaning lives in the genome literally — the SLM translates it into a fast idiomatic form rather than composing it.

5Metabolism: heat instead of a build

The "build" and "deploy" stages are absent. In their place is the life cycle of each path (rule, query, a whole deployable):

interpreted reference; correct; enough for cold paths heat: measured traffic > threshold materialized Placer decided → ribosome writes → court proved ≡ reference into the warm-up cache runs warmed idiomatic dialect code; verified: proved cooled (traffic gone) → eviction: the path returns to the interpreter — with no loss of correctness The same thing at the layout level: a hot domain the Placer proposes to move out into a service (molt by the ladder of rights), a cooled one — to collapse back. Architecture is a control loop, not a decision made in a meeting.
Metabolism. "Code is a cache of the genome" — literally: the phenotype is the warmed part of the cache, and the cache has eviction. Rollback = revert the genome + regeneration; the notion of "deploy" does not exist (NOT §27).

Costs and demand for the Placer are measured (the "monitors" stage on the overall diagram), the formulas come from theory/ with provenance classes: Declared (hand, bootstrap) contaminates everything it passes through; Measured displaces Declared over the course of life; CI recomputes all Derived. The word "certificate" is allowed only for the measured. The METRICS of each exam carries a table "formula → the decisions it made" — an empty row means a decoration formula (scar S3).

6Dialect: the warm-up tissue

A dialect = language + framework + gates + mixins, a catalog-plugin with a fixed interface (types, naming, emit(AST), templates, ribosome, gates, skeleton, migrate, mixins). The core calls only the interface and knows not a single language — the grep linter I1 in CI, "if lang" is impossible (in v0 Go lived in seven layers — S1). Adding a language = adding a catalog; a dialect without a certificate (golden + full gates) does not materialize silently. Mixins — a finite curated set of reference examples of kinds of bodies (not business logic!), each passing the gates of its kind, the hash of the mixins is part of the cache key. No RAG over the codebase (NOT §16).

CORE hub-IR · Expr-AST · interpreter · checkers · Placer · court · migrator knows not a single language grep linter CI: a language name or "if dialect" in core/ = build error (I1) only dialect interface types: IR type → language type naming: field/rule → name emit: Expr-AST → string templates: skeleton ribosome: prompt/strip/ assemble/allowed_imports gates: build/lint/test/ bench (+fuzz runner) skeleton: import parser migrate: rename_in_body mixins/: examples + manifest unstable until 3 dialects — deliberately (PREDICTIONS #3) dialects/go-stdlib/ → gen_*.go, rules.go gates: go vet · go test fuzz runner: rapid dialects/python-fastapi/ → app/*.py, rules.py gates: pytest fuzz runner: hypothesis ✗ forbidden: a direct path core → files ("if lang == …") — the v0 rake, caught by the linter
The dialect plugin. Note the §9 win: proofs of "body ≡ reference" are not repeated per dialect — they are about meaning; the dialect is checked by golden tests and its own gates. The showcase exam F3: one genome → interpreter + go + python, one judge, zero core edits.

7Ribosome: the CEGIS loop

The model (a cheap local SLM; the provider is tissue) writes only bodies — fast idiomatic implementations of already known semantics (the reference is in the genome). The loop is CEGIS (counter-example guided inductive synthesis):

IR slice of the rule — O(k) signature · intent · contract · reference body · types. Finite. dialect mixins 1–3 certified examples of the body kind (by features) prompt + counterexamples from past attempts SLM · step N t=0, seed; ladder by capability body candidate solver (court §9) body ≡ reference? post/inv proved? UNSAT? no: counterexample (concrete inputs + divergence) → into the prompt; the best few-shot is about THIS rule proved → warm-up cache body cache hash(norm-AST+dialect+mixins+model+seed) doesn't converge → N+1; exhausted → island (ledger) The unit of materialization = the unit of the contract (S11). Skills: two-phase, the oracle = a hand-written reference; for rules the oracle = the reference interpreter — two-phase became universal.
The CEGIS ribosome. The solver's counterexample is more precise than any mixin: it describes exactly the error the model just made. The cache is keyed by semantics (the normalized AST), not by the prompt text — improving the prompt does not burn the bodies (the v0 "byte-for-byte" rake).

8Court: proofs instead of samples

The v0 gates checked only what was declared — and were called gates undeservedly (S4, S13). The v1 court is stratified by decidability:

9Interview by counterexamples

The mechanism that closes the main unsolved concern of v0 (#3 — "the human writes the contracts and they underspecify"). Underspecification stops being a silent hole and becomes a generator of questions:

body T1 clamps available body T2 does not clamp both passed ALL the declared contracts (scar S13 v0) solver: T1 ≡ T2? no → SYNTHESIS of a divergence input (u* = argmax of the divergence, v4) question to the operator "room is full, a free one arrived: available becomes 2 at capacity 1 — is that allowed?" + options: clamp · reject · invariant each option = a ready-made diff answer → propose(diff) the usual checkers; the contract extended re-court of the bodies ledger question asked and answered — does not repeat Hygiene (NOT §29): a question is legal only with an executable counterexample and ready-made options; the quality metric is the share of questions that changed the genome.
The interview — now IN THE FLOW OF LIFE (mutgate): warden/propose reject a change of a rule's behavior under the same contracts, citing an executable input and both outcomes; ack_behavior_change at the root = the operator's answer → molt. A curious fact of mini-F7: the fresh agent needed no questions at all — the contracts were proved on the first try.

10Life: warden and molt

The judge is an external black box (scenarios outside the genome, a coverage checker watches for drift — PREDICTIONS #8), common to the interpreter and any dialects. The warden is a daemon: a genome edit → checkers → molt (functor: the log migrates losslessly, the bodies of untouched rules are carried over, regeneration — only of the affected part) → the organism keeps living; downtime is seconds. Death of a certificate (measured diverged from declared, the DKW quota exhausted) → rights revoked in the same tick → a molt proposal; the system does not fix prod into an outdated ontology. Molt proposals from the Placer (move out a hot domain, collapse a cooled one) go by the ladder of rights: auto — within what was granted, higher — the human.

Every v0 rake → a v1 mechanism

v0 rake (archgen)The v1 mechanism that makes it impossible
Meaning smeared across bodies from the SLM; two bodies with different semantics passed the gates (S13) Meaning lives in the genome: the reference interpreter; a body must be ≡ the reference (provably)
Gates check only what was declared, by sampling (S4) The court: SMT theorems for the decidable, an honest proved/fuzzed passport, mutants calibrate the prover
The human writes contracts blind — concern #3 not closed Interview by counterexamples: underspecification → a question with an executable example → a genome diff
A build stage; monolith-centricity; a dead services target (S8) Metabolism: the interpreter is always alive, code is a JIT warm-up by heat, the Placer is a control loop, deploy abolished
Go in seven layers; a second language = `if` in six places (S1) The dialect plugin + grep linter I1; proofs are not repeated per dialect
Seven regex-DSLs printing Go (S2) One Expr: AST → printers + interpreter + SMT encoder + mutants
"From the theorem," but the input is by hand in YAML (S3) Provenance types with a contagion rule; measured displaces declared; CI recomputes Derived
IR = dicts, eternal legacy of sections; cache by prompt text (S6) hub-IR + onto:N + onto fix; cache by semantic hash; UNEXPRESSIBLE — the gate of IR growth
The genome no more compact than the code (S5) Defaults + modules + judge outside the genome + interview instead of manual invariants; metric ≤ 1/3
Ladder by size (S10); batches (S11); both arms measured by the author (S15) Ladder by measured capability; per-rule always; F7 end-to-end — shipping by other hands

How it was built and what remains

The whole path F0 → F6 + the SLM and "tissue" waves + mini-F7 was walked in a single day (2026-08-20), strictly one exam at a time; each wave — a commit with a journal. The predicted scars (PREDICTIONS.md) fired as safeguards: P2 (F1 bloat) was cut by interpreter-first, P7 holds the AST limit, P1 (interview spam) was refuted — the fresh agent needed no questions. Three lessons of the day: measurement parity across tiers (D34), a complexity budget instead of a speed one (D38), type constructors in the SLM sandbox.

The honest remainder (PLAN/UNEXPRESSIBLE, by real need): printing skills into the go dialect and the per-rule-correct in-process JIT (an embeddable interpreter, D28); the live traffic seam monolith↔service; the full F7 (human operator, clean machine) and the calendar week/month of F6 — the last two are fundamentally not closable from within a single session.