Draft Paper / Technical Specification (v0.2)
GenesisCode v0.2 is an AI-native programming system built around a sharply minimized pure kernel and an aggressively modern verification-and-provenance envelope that governs how programs evolve—whether written by humans or proposed by large language models (LLMs). The kernel is a small functional calculus (Gλ) with immutable data, lexical closures, and a single universal abstraction—contracts—that implement message-based behavior and delegation through an explicit, inspectable protocol. Unlike “minimalist manifesto languages,” GenesisCode v0.2 makes its core claims mechanically enforceable: it standardizes unforgeable seals to harden protocol invariants; it pushes all nondeterminism (I/O, time, randomness, network, LLM calls) behind a capability boundary with deterministic effect logs and replay semantics; and it introduces an Obligation Engine that requires packages and extensions to carry evidence artifacts (tests, property checks, proofs, resource budgets, determinism claims, capability policies, compiler equivalence checks) before they can be accepted by tooling or registries.
GenesisCode is “AI-native” in a strict sense: there is one canonical intermediate representation (CoreForm) that fits in small context windows; structural validators reject malformed or policy-violating code before execution; semantic patch artifacts replace raw text edits; and AI becomes a proposal generator whose outputs are accepted only when obligations are satisfied and provenance is recorded. The result is a language system that feels near-magical not because it embeds AI into semantics, but because it constrains, verifies, and explains program evolution with a small trusted computing base (TCB), modern compilation techniques (shapes, inline caches, e-graphs), and optional advanced stacks (row-polymorphic contract types with effect rows, refinement proofs, translation validation). This paper specifies Gλ, the hardened contract protocol, the effect-log execution model, the obligation/provenance architecture, the type and proof stacks, the optimization strategy, and a realistic implementation roadmap.
Most “AI-native language” proposals confuse AI integration with AI reliability. GenesisCode v0.2 is built on the opposite premise:
AI output is untrusted by default. Reliability comes from a tiny deterministic core, explicit effect boundaries, hardened protocols, and mandatory evidence.
GenesisCode v0.2 combines several ideas into one coherent, enforceable system:
- Gλ (Genesis Calculus): a small pure core with canonical AST and a clearly bounded TCB.
- Contracts with hardened dispatch: message-based behavior + delegation + extension, with unforgeable seals so protocol results cannot be spoofed.
- Deterministic effect logs: effects are expressed as sealed requests; execution produces a replayable trace artifact, making AI and I/O auditable.
- Obligation Engine: packages must carry evidence artifacts (tests/proofs/bounds/policies/equivalence checks) and can be rejected mechanically.
- Semantic patching: code evolution is captured as verified, structural “patch artifacts,” not ad hoc text diffs—ideal for AI-driven changes.
- Optional advanced stacks: row-polymorphic contract typing + effect rows; refinement proofs; e-graph optimization; translation validation that keeps compilers outside the TCB.
If you want expert CS people to react with “this is dangerous (in a good way),” the obligation/provenance + replay model is the centerpiece.
- Small Trusted Computing Base (TCB): trust as little as possible.
- Determinism by default: pure evaluation is deterministic; nondeterminism must pass through explicit capabilities.
- Hard protocol invariants: dispatch, unhandled, error, effect request shapes are non-spoofable.
- Evidence-carrying software: code must ship with obligations and artifacts that justify trust.
- AI as proposer, not authority: accept changes only when obligations pass and provenance is recorded.
- Performance path without compromising trust: modern optimization with validation.
- Not a “one true syntax” language (stacks can vary).
- Not “prove everything” from day one (proof stacks are optional; tests are baseline obligations).
- Not “compiler-first” (interpreter + validation first; compilation later with translation validation).
GenesisCode splits the world into layers:
TCB-A (Minimal):
- Kernel evaluator for Gλ (pure)
- Immutable primitive operations (pure)
- Seal primitive (unforgeability guarantee)
If you trust only TCB-A, you get deterministic evaluation of pure programs and robust protocol tokens.
TCB-B (Operational):
4) Capability runner (effect interpreter)
5) Effect-log replay checker (can be small)
6) Package verifier (hash/signature/policy)
Non-TCB (should be validated):
7) Optimizing compiler, JIT, e-graph rewriter, WASM backend
These can be made non-TCB by requiring translation validation evidence as obligations.
This explicit TCB story is what experts look for.
GenesisCode standardizes exactly one canonical representation:
CoreForm is a canonical S-expression AST (not just syntax). All surface syntaxes and DSLs must desugar to CoreForm.
CoreForm nodes are built from:
- Symbols
- Pairs (lists)
- Vectors/Maps (optional but recommended)
- Literals (nil, bool, int, bytes/string)
- Sealed values (see §6)
- LLMs target one form, not many.
- Structural validators can be simple and strict.
- Semantic patches can operate on stable AST shapes.
- Provenance hashes are stable and reproducible.
Gλ is the smallest normative semantic core. Everything else is desugaring or library.
Terms e:
x(variable)λx. e(single-argument lambda)e1 e2(application)quote(v)(quote datum)prim(op, v1, …, vn)(total primitive ops on immutable data)seal()(fresh unforgeable token)seal(v, s)(seal datumvunder tokens)unseal(w, s)(attempt to unsealwwith tokens)
Note: if, let, multi-arg functions, modules, etc. are desugaring, not kernel.
- Immutable data: nil, bool, int, bytes/string, symbol, pair, vector/map
- Closures:
<λx.e, env> - Sealed values:
⟦v⟧s(sealed datum v under seal token s) - Seal tokens
s: unforgeable, fresh, and only comparable by identity (eq?)
- Only
seal()produces a fresh token. - The only way to access the payload of
⟦v⟧sisunseal(⟦v⟧s, s). - Any mismatch returns a benign failure value (e.g.,
nilor a sealed error), never the payload.
This single primitive eliminates spoofing of “unhandled/effect/error” tags.
Standard call-by-value evaluation with lexical scoping. Primitive ops are total (or return explicit error values rather than throwing host exceptions).
A contract is a closure that processes a single message datum. Contracts are ordinary values in Gλ/CoreForm.
A message is a datum of the shape:
(msg op payload)
whereopis a qualified symbol andpayloadis any datum.
Qualified symbols prevent collision:
pkg/module::name(or internal(ns name)representation)
The Prelude defines three seals (created once at startup and stored in trusted Prelude bindings):
S_UNHANDLEDS_EFFECTS_ERROR
And standardized constructors:
UNHANDLED(msg) := seal((unhandled msg), S_UNHANDLED)EFFECT(req) := seal((effect req), S_EFFECT)ERROR(info) := seal((error info), S_ERROR)
Only the Prelude (or code given those seals explicitly) can construct values recognized as unhandled/effect/error by the dispatcher/runner. User code can still represent similar structures, but cannot spoof the sealed form.
This is the “minimal but serious” upgrade that makes experts stop calling the protocol a convention.
Each contract has:
handler : msg -> valueproto : contract | nilmeta : map- optionally a
shape-id(see optimization)
Normative dispatch algorithm:
dispatch(c, msg):
r = c.handler(msg)
if is_sealed_unhandled(r) and c.proto != nil:
return dispatch(c.proto, msg)
else:
return r
is_sealed_unhandled is defined by attempting unseal(r, S_UNHANDLED).
extend(base, overrides, meta+) -> newContract:
- new handler checks
overridesbyop - if no match: returns
UNHANDLED(msg) proto = basemeta = merge(base.meta, meta+)
No mutation. No secret inheritance rules.
Standard ops:
meta→ returns meta mapproto→ returns proto pointer or nilshape→ returns shape-id (if present)explain→ returns a pure trace object showing resolution path:- which contracts were consulted
- which override matched (if any)
- final result (sealed/unsealed)
This is a core AI-native debugging tool.
Effects are not “values you return and hope a runner interprets.” v0.2 standardizes an effect program representation and a trace artifact.
Represent effectful computations as a free structure:
Pure(v)Perform(op, payload, k)wherekis a continuationresult -> effectProgram
In CoreForm this is typically a tagged structure; the important part is standardization.
An actual “please perform this effect” boundary value is:
EFFECT( request )
whererequestcontains:op(qualified symbol)payload(datum)continuation(in effect-IR form)
This prevents spoofing “effect” values that might trick runners into privilege escalation.
A capability is an authority object provided by the host runner, not by pure code:
- filesystem, network, time, randomness, LLM, etc.
Programs cannot access capabilities unless the runner provides them.
Every effect interpretation produces an effect log artifact:
Each entry includes:
- request hash (op + payload hash + continuation hash)
- decision: allowed/denied
- response hash (and optionally full response data depending on policy)
- capability identity (which authority responded)
- optional timestamp only if time capability is permitted
Given:
- a program
Pproducing an effect program - an effect log
L
replay(P, L) must:
- produce the same final value, or
- fail with a structured replay mismatch error.
This is foundational for:
- auditability
- deterministic CI
- “AI-assisted builds you can reproduce”
LLM generation is an effect op, e.g.:
ai/generate- payload includes prompt, model identifier, parameters
- response includes generated CoreForm + provenance metadata
Crucially:
- outputs are logged
- replay can pin generation outputs
- registries can require that AI outputs are attached as signed artifacts
This makes “AI-native” defensible to experts.
This is the v0.2 centerpiece.
An obligation is a declarative requirement plus verification procedure and evidence artifacts. Examples:
- Unit tests must pass.
- Property tests must pass with recorded seeds.
- Coverage threshold must be ≥ X (tooling obligation).
- No capability escalation: declared capabilities must be a superset of actual used effect ops.
- Determinism claim: pure modules must not emit EFFECT values.
- Resource budgets: time/memory limits in benchmark harness.
- Typecheck: the type stack must accept the module.
- Refinement proof: discharge a predicate using SMT/interactive proof.
- Translation validation: optimized/compiled output is equivalent under a spec.
Obligations are modular: stacks can introduce new obligation types.
Evidence is stored as immutable artifacts referenced by hash:
- test logs (including effect logs)
- coverage reports
- proof objects / SMT traces
- benchmark results
- equivalence certificates
A registry (or local policy) can reject packages unless:
- obligations declared by the package are satisfied, and/or
- registry-required obligations are satisfied (e.g., minimum tests + determinism + signed provenance)
This is how you prevent “AI wrote it, trust me.”
Packages are content-addressed:
- artifact hash includes code + obligations + evidence + dependency graph + toolchain ID
- optional signatures + transparency log (append-only)
This aligns with modern supply chain expectations and makes the system feel “adult.”
LLMs are great at proposing edits. They are terrible at being trusted editors. v0.2 standardizes semantic patches.
A patch is a typed, structural transformation over CoreForm, such as:
- “replace handler for op X in contract Y”
- “add new override mapping”
- “strengthen obligation set”
- “refactor pure function f by rewrite rule R”
A patch is accepted only if:
- Structural validation passes (well-formed CoreForm, no forbidden forms)
- Dependency constraints hold
- Obligations re-check successfully (or remain valid under incremental checking)
- Provenance recorded (including AI proposal source if used)
Instead of asking AI to “edit the file,” you ask it to produce a patch artifact, and the system verifies the patch. This dramatically reduces hallucination damage.
Types are not in the kernel; they are an enforceable stack plus obligations.
A contract is typed by the operations it handles:
Contract { op1: A1 -> R1, op2: A2 -> R2 | r }
where r is a row variable representing the rest of the interface (row polymorphism).
This matches extension perfectly:
- extending a contract adds fields to the row
- delegation is typed as “proto provides row r”
Functions can declare effect requirements:
A -> B ! {io, ai, time}
and pure code is ! {}.
Allow:
- inferred types for common code
- explicit types for public interfaces
- gradual “unknown” (
?) for early-stage code
Add refinement types as an advanced stack:
Int{n >= 0}Map{k:Key -> v:Val | preservesInvariant(...)}
Proof obligations can be discharged by SMT or interactive proofs and recorded as evidence artifacts.
This is where “provably safe concurrent map” stops being a slogan.
GenesisCode can be fast without trusting a huge compiler.
Each contract can have a stable shape-id derived from:
- override table structure
- proto’s shape-id
Dispatch can be accelerated by:
- polymorphic inline caches (PICs) keyed by
(shape-id, op) - compiled jump tables for frequently used shapes
Because the kernel is pure, aggressive equational optimization is viable:
- normalize CoreForm
- build an e-graph
- apply rewrite rules (beta, fusion, algebraic simplifications, deforestation where safe)
- extract minimal-cost program
To keep the optimizer/compiler outside the TCB, require evidence:
- run equivalence checks on a test suite (baseline)
- optionally use symbolic testing or proof-carrying rewrite traces (advanced)
The key is the architecture: optimization is powerful, but not trusted by default.
The runtime can target WASM for portability:
- kernel stays pure
- capability runner bridges to host APIs
- effect logs remain the audit trail across platforms
No magic claims needed—just a clean layering story.
v0.2 avoids relying on a mystical fixed-point kernel definition. The kernel is Gλ; “Genesis” is a standard library root contract with meta/proto behavior.
However, a self-referential “Genesis fixed point” can be derived in a stack as a demonstration of expressiveness:
- fixed-point combinators exist in pure Gλ
- self-hosting can be built as obligations mature
- but the language doesn’t bet its implementability on a clever tautology
This is how you keep beauty without sacrificing engineering credibility.
Intent: an immutable variable with get and set, where set returns a new variable and does not mutate the original.
v0 = makeVar(42)dispatch(v0, (msg get nil)) => 42v1 = dispatch(v0, (msg set 100))dispatch(v1, (msg get nil)) => 100dispatch(v0, (msg get nil)) => 42
Obligations:
- unit tests above
- determinism: must not emit EFFECT
- typecheck:
Contract { get: Unit -> Int, set: Int -> Contract{...} }
Explainability:
explain(v1, msg get nil)returns the exact resolution path and override source.
This example is simple, but it exercises the hardened protocol and obligation framing.
Goal: “Generate a persistent ordered map implementation.”
Workflow:
- User writes tests + property tests + performance budget obligation.
- AI proposes a semantic patch adding module
ordered-map. - Tooling validates structure, runs tests, records effect logs for:
- AI generation step (ai/generate)
- any benchmark harness effects (time capability)
- Package is accepted only if obligations pass; AI output provenance is attached.
If the AI used nondeterministic sampling, replay pins the exact output by replaying the effect log (or by caching the generation response artifact).
This is the real “AI-native magic”: not generation, but verified evolution with replay.
- CoreForm parser/printer
- Gλ evaluator
- immutable data
- seal/unseal primitives
- Prelude: contracts, dispatch, extend, explain
- standardized effect program representation
- runner with capability injection
- effect log format + replay checker
- baseline policies (deny by default)
- package manifest with obligations
- evidence artifact store (content-addressed)
- CI-grade runner that enforces obligations
- patch artifact schema
- patch validator
- incremental obligation checking
- checker as obligation
- optional gradual typing
- interpreter instrumentation for shapes
- optional compiler backend
- equivalence evidence as obligations
This roadmap emphasizes what makes the project beyond SOTA: trust architecture + verification envelope, not premature compiler heroics.
GenesisCode v0.2 is designed to be impressive to experts for the right reasons:
- The kernel is small and precisely bounded (Gλ + seals).
- Protocol invariants are hardened (unforgeable UNHANDLED/EFFECT/ERROR).
- Effects are explicit, capability-gated, and auditable (deterministic effect logs + replay).
- Software must justify itself (obligations + evidence artifacts).
- AI is integrated as a proposer with recorded provenance, not as a magical oracle.
- Performance is attainable with modern techniques while keeping optimizers outside the TCB (shapes, PICs, e-graphs, translation validation).
- Multiple paradigms are supported without core bloat (stacks), including serious typing and proofs.
If v0.1 was “a minimalist language that’s friendly to LLMs,” v0.2 is a stronger claim:
A minimal deterministic calculus plus an evidence-and-provenance system that makes AI-assisted programming auditable, reproducible, and policy-constrained—without trusting the AI, the network, or the compiler.
That is the “near magical” effect experts respect.
A conforming GenesisCode v0.2 system provides:
Kernel (TCB-A):
- CoreForm canonical representation
- Gλ evaluator (λ, application, quote, primitives)
- Total immutable primitives (pair/symbol/int/bytes/etc.)
seal()andunseal()with unforgeability guarantee
Prelude:
5. Contract constructor (handler/proto/meta)
6. Hardened UNHANDLED/EFFECT/ERROR via seals
7. Normative dispatch, extend, explain
Effects + Auditability:
8. Standard effect IR (Pure/Perform) or equivalent
9. Capability runner (deny-by-default)
10. Effect log generation + replay checker
Obligations + Supply Chain:
11. Package format with obligations + evidence artifacts
12. Content-addressed hashing and dependency pinning
13. Policy hooks for registry acceptance
AI-Native Evolution:
14. Structural validators for CoreForm + patches
15. Semantic patch artifact format + validation pipeline
Optional stacks (non-required but v0.2 vision-complete):
16. Row-polymorphic contract typing + effect rows
17. Refinement proof stack
18. Optimization via shapes/PICs/e-graphs + translation validation as obligations
If you want, I can also produce (1) a formal-ish small-step semantics appendix for Gλ + seals, (2) a concrete CoreForm schema for effect logs + patch artifacts, and (3) a minimal “GenesisCode Registry Policy” spec that reads like something serious organizations would actually adopt.
Below is a handoff technical document you can paste into your repo (or hand directly to a Codex Desktop / GPT‑5.3‑Codex agent). It’s written to be maximally actionable from day 0: repo structure, invariants, module boundaries, file formats, tests, and a task plan that takes advantage of Codex threads + worktrees + skills.
I’ve also included templates for AGENTS.md and a Codex Skill you can drop into .agents/skills/ so the agent reliably follows the same workflow every time. Codex explicitly supports project-level instruction files (AGENTS.md / AGENTS.override.md) and skill folders with SKILL.md. (OpenAI Developers)
Implement GenesisCode v0.2 as specified in the accompanying paper:
- Kernel: Gλ (pure), immutable data, lexical closures, and the seal/unseal primitive to support unforgeable protocol tags.
- Prelude: contracts + hardened protocol (UNHANDLED/EFFECT/ERROR are sealed), delegation via
dispatch, immutable extension viaextend, observability viaexplain. - Effects: explicit capability runner + deterministic effect logs + replay checker.
- Obligation Engine: packages carry obligations + evidence artifacts; local tooling enforces acceptance policies.
- Semantic patches: changes are represented as structural patch artifacts and validated, not just text diffs.
This guide focuses on building a high-quality, minimal-TCB interpreter + toolchain with crisp boundaries so later stacks (types, refinement, e-graphs, compiler) can be added without rework.
TCB-A (must remain tiny):
- Gλ evaluator (pure)
- immutable primitives (pure)
- seal/unseal implementation (unforgeable tokens)
Everything else (runner, registry policy, optimizers) should be treated as higher-layer tooling.
- Kernel evaluation must not touch filesystem, time, randomness, network, environment vars, or the LLM.
- Any nondeterminism must be represented as an effect program and interpreted by the runner.
UNHANDLED/EFFECT/ERROR must be unforgeable by user code:
- Use seal tokens created by Prelude (
S_UNHANDLED,S_EFFECT,S_ERROR). - Recognition checks must use
unseal, never raw structure matching.
User-visible failures must be represented as:
- sealed
ERROR(...)values, or - explicit error returns (Result) in Rust internals, converted to a sealed ERROR at the boundary.
- CoreForm parser + printer (canonical S-exprs)
- Gλ evaluator:
lambda, application,quote, and a small set of total immutable primitives - Immutable value types: nil/bool/int/bytes(or string)/symbol/pair (+ map/vector strongly recommended)
- Seals:
seal()produces unforgeable token;seal(value, token);unseal(sealed, token) - Prelude module:
- contract constructor
- hardened UNHANDLED/EFFECT/ERROR
dispatch,extend,explain
- Standard effect IR (Pure/Perform w/ continuation)
- Capability runner (deny-by-default)
- Effect log format (deterministic, content-addressed)
- Replay checker that validates a run against an effect log
- Package manifest format with obligations and evidence pointers
- Content-addressed artifact store (hash-based)
- Test runner + evidence artifacts (test logs + effect logs)
- Policy gate: “package accepted only if obligations pass”
- Patch artifact schema for structural changes
- Patch apply + validator
- Patch acceptance pipeline reruns relevant obligations
- Row-polymorphic contract type checker + effect rows as an obligation
- Refinement proof stack
- Optimizer (shapes/PICs/e-graphs) with translation validation obligations
- WASM build target for interpreter/runner (keep the architecture ready)
Use a Rust workspace so tooling and libraries stay modular:
genesiscode/
Cargo.toml (workspace)
crates/
gc_coreform/ # AST + parser/printer + canonicalization
gc_kernel/ # Gλ evaluator + values + env + primitives + seals
gc_prelude/ # contracts + dispatch/extend/explain + sealed protocol
gc_effects/ # effect IR + runner interface + effect log + replay
gc_obligations/ # obligations engine + evidence store + policy
gc_patches/ # semantic patch schema + apply/validate
gc_cli/ # CLI executable wiring everything
prelude/
prelude.gc # Prelude in CoreForm (or embedded as Rust string initially)
tests/
spec/ # language-level golden tests (CoreForm programs)
fuzz/ # parser/eval fuzz harnesses
docs/
PAPER_v0.2.md # the paper you wrote
TECH_HANDOFF.md # this file
Rationale: keep the kernel clean; keep effect/obligation/patch machinery out of TCB-A.
- Parser must accept a minimal Lisp-like syntax: parentheses, symbols, integers, strings/bytes, quote sugar (
'x=>(quote x)). - Printer must emit a canonical, stable form (for hashing and patching).
- Canonicalization must preserve semantics but normalize irrelevant surface differences.
Define a single enum:
enum Term {
Nil,
Bool(bool),
Int(BigInt),
Bytes(Vec<u8>), // or String
Symbol(SymbolId), // interned
Pair(Box<Term>, Box<Term>),
Vector(Vec<Term>),
Map(BTreeMap<Term, Term>), // or persistent map wrapper
Quote(Box<Term>), // or (quote ...) as syntactic sugar
// optionally: locations/spans for better errors
}
Important: keep “Term” for immutable data and “Expr” for evaluable forms if you prefer, but don’t overcomplicate.
Pick a stable content hash (e.g., BLAKE3) for:
- canonical CoreForm
- evidence artifacts
- effect logs
- patch artifacts
Separate “Term” (syntax/data) from “Value” (runtime):
enum Value {
Data(Term), // immutable data
Closure { param: SymbolId, body: Expr, env: EnvRef },
Sealed { token: SealId, payload: Box<Value> },
SealToken(SealId),
// Optional: native function for primitives
NativeFn(NativeFnId),
}
Use persistent environments for purity and easier debugging:
Env = persistent_map(SymbolId -> Value) + parent pointer
Call-by-value, lexical scope.
Keep the kernel forms minimal; treat let, if, begin, multi-arg calls as desugaring helpers in the parser or Prelude.
Implement seal() as generating a fresh SealId that cannot be constructed by user code. This is a core security guarantee.
Kernel ops:
seal()->SealToken(id)seal(value, SealToken(id))->Sealed{id, payload=value}unseal(sealed, SealToken(id))-> returns payload if id matches else nil (or sealed ERROR; choose one and standardize)
A contract is a callable value with fields:
handler: Value(callable)proto: Option<Value>(contract or nil)meta: Value(map)- optional
shape_id(later optimization)
In Rust, store contracts as Rc<Contract> inside Value::Contract(...) or reuse closures with a special apply protocol.
Standardize (in docs + tests):
(msg op payload)whereopis a qualified symbol.
In Prelude initialization:
- create
S_UNHANDLED,S_EFFECT,S_ERRORviaseal()
Define functions:
UNHANDLED(msg)returnsseal((unhandled msg), S_UNHANDLED)EFFECT(req)returnsseal((effect req), S_EFFECT)ERROR(info)returnsseal((error info), S_ERROR)
Define predicates:
is_unhandled(x)usesunseal(x, S_UNHANDLED)- same for effect/error
Implement exactly:
- call contract handler with msg
- if result is sealed UNHANDLED and proto exists: recurse to proto
- else return result
Create a new contract whose handler:
- checks override table for
op - if found: call override handler
- else return sealed UNHANDLED(msg)
Proto points to base.
Must return a pure trace object capturing:
- contracts visited (ideally by stable contract-id or hash)
- whether each step matched an override
- the final result
This is essential for debugging + for AI to self-correct.
Represent effectful computations as:
Pure(v)Perform(op, payload, k)wherekis continuationresult -> EffectProgram
The runner interprets effect programs, not arbitrary “effect values”.
Runner must be deny-by-default; capabilities are injected by host configuration.
Examples:
io/fs.readio/fs.writesys/time.nowai/generate
Define a log entry struct:
- request hash (op + payload hash + continuation hash)
- decision (allowed/denied)
- response hash (+ optional response payload if policy allows)
- capability identity
- optional timestamp only if time capability is granted (and then the timestamp becomes part of the log)
Logs must be stable: same program + same log => same replay result.
Implement replay(program, log) that:
- steps program
- when
Performencountered, consumes next log entry - checks request hash matches
- returns recorded response
- errors loudly on mismatch (sealed ERROR or Rust error mapped to ERROR)
package.toml:
- name/version
- dependencies pinned by content hash
- modules list
- obligations list
- evidence pointers (hashes)
A content-addressed store:
store/<hash>containing JSON/TOML blobs, logs, reports.
Implement these first:
unit_tests_passdeterminism_claim(module must not produce sealed EFFECT)capabilities_declared(declared caps must cover observed effect ops)replayable_tests(test run must record effect logs and replay must pass)
Later obligations:
- property tests with recorded seeds
- coverage thresholds
- resource budgets (bench harness)
- translation validation certificates
Represent patches structurally:
- replace node at path
- add module
- remove module
- update dependency
- update obligation set
- add evidence artifact pointers
Paths should be defined over canonical CoreForm AST.
- Validate patch schema
- Apply patch to canonical AST(s)
- Validate structural invariants (no forbidden ops/forms)
- Re-run required obligations (or incremental subset)
- Record provenance + evidence artifacts
Implement genesis CLI with:
genesis fmt <file>— canonical formattinggenesis eval <file>— evaluate pure CoreFormgenesis test— run obligations/tests, produce evidence artifactsgenesis run <file> --caps <policy>— run with capability runner, emit effect loggenesis replay <file> --log <logfile>— replay deterministic rungenesis pack— build package artifact + manifest + hashesgenesis apply-patch <patchfile>— apply semantic patch + rerun obligationsgenesis explain <expr>— orgenesis explain <file> --msg ...for dispatch traces
- Golden tests: CoreForm programs + expected outputs
- Protocol tests: spoof attempts against UNHANDLED/EFFECT/ERROR should fail (sealed checks)
- Determinism tests: same input => same output; effect logs replay identically
- Fuzzing:
- parser roundtrip (parse -> print -> parse)
- evaluator should never panic
- Metamorphic tests:
- alpha-renaming invariance
- canonical formatting invariance
In Rust:
- avoid
unwrap()in code paths reachable from user input - map internal errors to sealed ERROR values at boundaries
Add docs/spec/ that restates the normative rules (dispatch, seals, replay). Keep it small and enforced by tests.
Codex Desktop is explicitly built to run multiple tasks in parallel with worktrees and built-in Git tooling. (OpenAI Developers) Use that structure from the start:
Create separate threads (each gets its own worktree):
- Kernel thread: CoreForm + evaluator + seals
- Prelude thread: contracts + dispatch/extend/explain + sealed protocol
- Effects thread: effect IR + runner + logs + replay
- Obligations thread: package + evidence store + test runner
- Patches thread: patch schema + apply + validator
- CLI thread: command wiring + UX + docs
Codex app explicitly supports worktrees for parallel tasks and built-in Git review/commit workflows. (OpenAI Developers)
Codex reads AGENTS.md before doing work, and supports layered overrides via AGENTS.override.md discovered from repo root down to current directory. It concatenates them in order, with closer directories overriding earlier guidance; there’s also a default size cap (32 KiB) for combined instructions. (OpenAI Developers)
Create AGENTS.md at repo root:
# GenesisCode v0.2 — Codex Working Agreement
## Mission
Implement GenesisCode v0.2 exactly per docs/PAPER_v0.2.md and docs/TECH_HANDOFF.md.
## Non-negotiable invariants
- Kernel (Gλ) must be pure and deterministic. No filesystem/time/network/LLM inside the evaluator.
- UNHANDLED/EFFECT/ERROR must be unforgeable using seal tokens created by Prelude.
- Never panic on user input. Convert errors to sealed ERROR values at boundaries.
- Effect runner must be deny-by-default and must produce deterministic effect logs + replay checker.
## Repo conventions
- Language: Rust (workspace in crates/).
- Always run: cargo fmt, cargo clippy, cargo test before committing.
- Keep TCB-A minimal: evaluator + immutable primitives + seals only.
## Development flow
- Make small commits with passing tests.
- Add golden tests for every semantic rule you implement.
- Prefer implementing behavior in libraries over adding kernel special forms.
- When uncertain, write a failing test first and make it pass.
## Deliverables checklist
- CoreForm parser/printer
- Gλ evaluator + seals
- Prelude: contracts + dispatch/extend/explain + sealed protocol
- Effects: effect IR + runner + logs + replay
- Obligations engine + package format + evidence store
- Semantic patches + validator
- CLI that ties it all together
If you want a stricter rule set for, say, crates/gc_kernel/, add:
crates/gc_kernel/AGENTS.override.md
# Kernel rules (override)
- Do not add new effects or IO primitives.
- Do not add new kernel special forms without updating docs/spec and adding golden tests.
- Avoid any dependency that is not essential for correctness.
Codex will automatically prefer AGENTS.override.md over AGENTS.md in a directory and will layer from the git root down to the working directory. (OpenAI Developers)
Codex skills are a supported way to package instructions/resources/scripts so the agent can reliably follow workflows; skills use progressive disclosure and are discovered in .agents/skills/ directories (scanned upward toward repo root). (OpenAI Developers)
Create:
.agents/skills/genesiscode-spec-first/SKILL.md
---
name: genesiscode-spec-first
description: >
Use this skill when implementing or modifying any GenesisCode semantics or tooling.
It enforces spec-first development: write/extend golden tests, implement minimal code,
avoid expanding the kernel, and keep protocol markers unforgeable with seals.
---
## Rules
1) Before implementing a feature, add or update:
- docs/spec/ (normative rule)
- tests/spec/ (golden tests)
2) Implement with smallest TCB-A changes possible.
3) Add negative tests for spoofing UNHANDLED/EFFECT/ERROR.
4) Ensure no panics on user input. Convert to sealed ERROR.
5) For effectful features:
- add effect-log tests
- add replay tests
6) Before merging:
- run cargo fmt
- run cargo clippy
- run cargo test
## Output expectations
- Keep PRs small and reviewable.
- Include a short "Semantics changed" note when behavior changes.
You can explicitly invoke a skill in Codex (e.g., with $ selection) or let it be auto-chosen based on its description. (OpenAI Developers)
When you start the first Codex Desktop thread, paste something like:
You are implementing GenesisCode v0.2 in this repo. Read docs/PAPER_v0.2.md and docs/TECH_HANDOFF.md. Follow AGENTS.md. Start with Milestone A only: CoreForm parser/printer + Gλ evaluator + seals + Prelude contracts (hardened UNHANDLED/EFFECT/ERROR + dispatch/extend/explain).
Constraints: keep TCB-A minimal; no IO/time/network in kernel; no panics; every semantic rule requires golden tests; protocol tags must be unforgeable via seals.
Deliver: working CLI commands genesis fmt, genesis eval, and a green cargo test suite for Milestone A.
GPT‑5.3‑Codex is explicitly described as being able to handle long-running tasks with tool use and complex execution, and the Codex app is designed for supervising parallel agent work via threads/worktrees. (OpenAI)
If you want, I can also generate a complete docs/spec/ starter (normative rules in one place) plus an initial tests/spec/ golden suite (seal spoof tests, dispatch chain tests, determinism tests) so the Codex agent starts with a concrete acceptance harness on day 1.
This document is the writing bible for GenesisCode. It defines how code should be shaped, named, structured, documented, tested, and packaged so that:
- programs are pure by default and auditable when effectful
- contracts are predictable and introspectable
- extensions are verifiable (obligations + evidence)
- diffs and semantic patches remain stable
- LLMs can generate and refactor code reliably
Where something is not yet implemented, treat this as the target behavior and stable convention.
GenesisCode has one canonical IR: CoreForm S-expressions. Any “sweet” syntax must desugar to CoreForm.
Rule: Published libraries and reference implementations should be written (or emitted) in canonical CoreForm formatting even if authored with sugar.
The kernel is pure and deterministic. Anything involving I/O, time, randomness, network, or LLM calls must be expressed as an effect program and interpreted by a capability runner.
Rule: Pure functions never “accidentally” trigger effects.
UNHANDLED/EFFECT/ERROR are sealed so user code cannot spoof them.
Rule: You do not pattern-match on raw (unhandled ...). You use the standard predicates/unsealers.
Packages must ship with obligations + evidence (tests, property checks, replay logs, proofs, budgets).
Rule: If it’s not backed by obligations, it’s not “real code” yet.
- 2 spaces, no tabs.
- Closing parens belong at the end of the last line of the form.
- One “major form” per line at top-level (
def,module, etc.).
Good
(def add
(fn (x)
(fn (y)
(prim int/add x y))))
Bad
(def add (fn (x) (fn (y) (prim int/add x y))))
- Hard max: 100 columns
- Prefer breaking long maps/vectors and long call forms onto multiple lines.
Since evaluation is unary/curry-based, you’ll often see nested calls.
Preferred for readability: keep application visually grouped:
((f x) y)
If your formatter prints (f x y) as sugar, it must desugar canonically to ((f x) y).
- Lists:
'(a b c)is allowed sugar for(quote (a b c)) - Maps/vectors should be printed with stable ordering and stable key formatting.
Operations are always qualified symbols to avoid collisions:
Format
pkg/module::op-name
Examples:
core/contract::metacore/contract::protocore/contract::dispatchio/fs::readai/llm::generate
Rule: Never use bare ops like get, set, read in published code.
- Functions, values, ops: kebab-case
- Modules: kebab-case path segments (
my-lib/data, notMyLib/Data) - Constants (rare): kebab-case is still preferred; if you need emphasis, use
*stars*:*s-unhandled*(seal token)*genesis*(root contract)
For map keys, use colon-prefixed symbols:
:intent:doc:examples:caps:obligations:tests
These are still just symbols, but the colon convention signals “data key.”
A file should define a module’s public surface and private helpers.
Module header convention
(def core/module::meta
{:module "my-lib/data"
:intent "Persistent data structures"
:doc "…"
:exports [my-lib/data::map
my-lib/data::filter]
:caps [] ; pure module => empty
:obligations [core/obligation::unit-tests
core/obligation::determinism]})
Exports are always explicit and qualified. Avoid “export everything” patterns; they destroy auditability.
GenesisCode’s universal abstraction is the contract. Contracts are invoked with a message datum:
(msg op payload)
Prefer payloads as maps with keyword keys, not positional tuples, for clarity and AI reliability.
Good
(msg my-lib/counter::add {:delta 1})
Bad
(msg my-lib/counter::add 1)
Exceptions:
- Ultra-hot primitives where performance matters (stack may allow positional payloads)
- Tiny internal helpers in private modules
The canonical handler signature is:
handler : msg -> value
Write handlers so that:
- they parse
opandpayloadexplicitly - they return sealed UNHANDLED(msg) if they do not handle an op
- they never “silently” return nil for unknown ops
Template
(def my-lib/counter::make
(fn (n0)
(core/contract::extend
core/contract::genesis
{my-lib/counter::get
(fn (msg) n0)
my-lib/counter::add
(fn (msg)
(let ((p (core/msg::payload msg))
(d (core/map::get p :delta)))
(my-lib/counter::make
(prim int/add n0 d))))}
{:intent "Immutable counter"
:caps \[\]
:tests \[my-lib/counter::tests\]})))
Note: core/msg::payload, core/map::get, etc. are standard-library placeholders in this style guide. The early implementation should provide these helpers quickly because they dramatically reduce errors and improve AI generation.
- A contract should only delegate via
core/contract::dispatch(or equivalent standard function). - Handler should not “manually” walk proto chains unless it’s a tooling module.
Every meaningful contract should support:
core/contract::metacore/contract::proto
Even if your handler doesn’t implement them, genesis (as proto) should.
If a contract is part of public API, include an obligation/test asserting that:
core/contract::explainreturns a trace that includes the expected op resolution path.
This helps humans and LLMs debug.
Unknown op handling must return sealed UNHANDLED(msg).
Rule: Never return raw (unhandled msg) and never return nil for unhandled ops.
Errors are values, not host crashes.
Rule: Prefer returning sealed ERROR(info) over ambiguous sentinel values.
Recommended error payload shape:
{:error/code "my-lib/not-found"
:error/message "Key not found"
:error/context {:key k
:module "my-lib/data"}}
If you call something that may return ERROR, you must either:
- propagate it unchanged, or
- explicitly handle it with a documented policy
A pure function returns a value.
An effectful function returns an effect program (not “random effects happening inside evaluation”).
Every effectful module must declare required capabilities in metadata:
{:caps [io/fs::read io/fs::write sys/time::now]}
Rule: If :caps is empty, obligations should enforce that the module never emits EFFECT values.
The style guide recommends standard constructors (names may vary in implementation, but keep semantics):
core/effect::pure : v -> programcore/effect::perform : op -> payload -> (result -> program) -> programcore/effect::bind : program -> (v -> program) -> program(optional convenience)
Example: read file
(def my-lib/io::read-all
(fn (path)
(core/effect::perform
io/fs::read
{:path path}
(fn (bytes)
(core/effect::pure bytes)))))
When you write effectful code:
- keep payloads small and stable
- avoid embedding gigantic AST blobs in payloads unless necessary
- prefer content hashes in payloads for large artifacts
Example:
(core/effect::perform
ai/llm::generate
{:prompt-hash prompt-h
:model "gpt-5.3-codex"
:params {:temperature 0.2}}
...)
For any published module, you should provide:
- unit tests
- determinism/replay tests (as applicable)
- protocol spoofing negative tests (for prelude/security code)
- Test names:
"module::behavior - scenario" - Obligation identifiers are qualified symbols.
Example:
(def my-lib/counter::tests
[(test "my-lib/counter::get - initial"
(check-eq 0
(core/contract::dispatch
(my-lib/counter::make 0)
(msg my-lib/counter::get nil))))
(test "my-lib/counter::add - returns new"
(let ((c0 (my-lib/counter::make 0))
(c1 (core/contract::dispatch
c0 (msg my-lib/counter::add {:delta 1}))))
(begin
(check-eq 0 (core/contract::dispatch c0 (msg my-lib/counter::get nil)))
(check-eq 1 (core/contract::dispatch c1 (msg my-lib/counter::get nil))))))])
Property tests must record seeds in evidence artifacts so reruns are deterministic.
If you add a proof/refinement obligation, the module must also include:
- a precise statement of the property in
:doc - a minimal set of examples showing its meaning
GenesisCode will use structural patches. Code should be written to minimize meaningless changes.
- Keep override maps sorted by op symbol.
- Keep module metadata keys in a stable order:
:module, :intent, :doc, :exports, :caps, :obligations, :tests, :examples.
Avoid huge “megadefs” that make patches noisy.
Don’t generate symbol names dynamically for public API.
When messages carry structured payload maps, patches can add keys without breaking callers.
Every public function/contract must include an intent line in metadata (or in a doc form) that is short and literal.
Good: "Persistent ordered map with immutable updates"
Bad: "A magical container of destiny"
Document:
- purity/effect behavior
- time/space notes if important
- error behavior (what ERROR codes can occur)
- obligations guaranteed by evidence
Examples should be runnable snippets (or tests). Avoid pseudo-code in docs if it can become stale.
Even before implementation, reserve these namespaces:
core/msg::*— message constructors/accessorscore/msg::opcore/msg::payloadcore/msg::make(construct(msg op payload))
core/contract::*core/contract::genesiscore/contract::dispatchcore/contract::extendcore/contract::explaincore/contract::metacore/contract::proto
core/effect::*core/effect::purecore/effect::performcore/effect::bind
core/obligation::*core/obligation::unit-testscore/obligation::determinismcore/obligation::replayable-testscore/obligation::capabilities-declared
core/error::*core/error::is-errorcore/error::codecore/error::message
Keeping these stable pays huge dividends later.
If you want GPT‑style agents to produce consistently correct code:
- Don’t rely on implicit conventions or “magic” macros in core libs.
- Keep local helper functions small and named.
Deeply nested lambdas are correct but hard to read. Use let-style bindings (even if desugared) to name intermediate values.
Nil should mean “empty list / nothing,” not “error,” not “unhandled.”
LLMs should be prompted: “Add tests + determinism obligations.”
If behavior depends on delegation/overrides, make it traceable.
A canonical formatter should:
- Use 2-space indentation.
- Place each
defon its own block. - Print maps with stable key order:
- keywords first (sorted)
- then symbols (sorted)
- Print vectors with one item per line if > 3 items or if any item is a compound form.
- Normalize quote sugar (
'x) optionally, but output must be stable.
(def my-lib/counter::meta
{:module "my-lib/counter"
:intent "Immutable counter contract"
:doc "Counter supports get and add. Pure, deterministic."
:exports [my-lib/counter::make]
:caps []
:obligations [core/obligation::unit-tests
core/obligation::determinism]
:tests [my-lib/counter::tests]})
(def my-lib/counter::make
(fn (n0)
(core/contract::extend
core/contract::genesis
{my-lib/counter::get
(fn (msg) n0)
my-lib/counter::add
(fn (msg)
(let ((p (core/msg::payload msg))
(d (core/map::get p :delta)))
(my-lib/counter::make (prim int/add n0 d))))}
{:intent "Immutable counter instance"
:caps \[\]
:doc "Instance contract. get returns current count; add returns new instance."
:tests \[\]})))
(def my-lib/counter::tests
[(test "my-lib/counter::get - initial"
(check-eq 0
(core/contract::dispatch
(my-lib/counter::make 0)
(msg my-lib/counter::get nil))))
(test "my-lib/counter::add - returns new"
(let ((c0 (my-lib/counter::make 0))
(c1 (core/contract::dispatch
c0
(msg my-lib/counter::add {:delta 1}))))
(begin
(check-eq 0 (core/contract::dispatch c0 (msg my-lib/counter::get nil)))
(check-eq 1 (core/contract::dispatch c1 (msg my-lib/counter::get nil))))))])
This is the “look” you want from day one: predictable naming, explicit ops, explicit payload maps, obligations, tests, no ambiguity.
These are style-adjacent design choices that affect how code looks:
- String vs bytes: Do we have both? If yes, standardize literal syntax.
- Map literal syntax: If CoreForm uses
{}sugar, define canonical printing order. - Qualified symbol encoding: Is
pkg/mod::namea single symbol or structured(ns name)? (Either is fine; style assumes you can print aspkg/mod::name.) - Nil vs empty list: treat nil as empty list; lists are pairs ending in nil.
- Error unsealing behavior:
unsealmismatch returns nil vs ERROR—pick one and enforce via tests.
If you want, I can turn this into:
- a short “GenesisCode Formatting Spec” that a formatter can implement
- a lint rule set (“no bare ops”, “must declare caps”, “must include :intent”, “must not return nil for unhandled”)
- a Codex prompt template that tells the agent exactly how to emit code in this style every time