agentlanguages.dev
verification camp · also orchestration

Codex.

Self-hosting literate language on bare-metal x86-64: dependent, linear, and effect types, proof blocks, and a byte-identical fixed point as the acceptance gate for every change. Authored and maintained end-to-end by AI agents.

authorDamian Tedrow (with a multi-agent AI team)
implementationCodex (self-hosted; the bootstrap reference compiler is retired)
targetBare-metal x86-64 (CDX binary, no OS or libc); transpiler plugs for ~48 targets including WebAssembly
licenceNot published
first seenMarch 2026
maturityworking compiler
markdowncodex.md

The thesis.

Codex — Damian Tedrow’s self-hosting language, unrelated to OpenAI’s coding model of the same name — starts from the position that the verification camp usually argues toward and then removes the floor: if agents are going to author the system, the system should not rest on anything the agents did not build. The compiler is written in Codex, compiles itself on bare-metal x86-64 with no operating system, no libc, and no garbage collector, and the acceptance test for every change is regeneration byte-identity — the self-host compiled by its own output must equal itself, bit for bit, signature aside. There is no separate specification document to drift from; the fixed point is the specification.

The repository remembers everything. The language says what you mean. The machine checks that you meant it.

The second commitment is literacy. Prose is not comment syntax; it is part of the chapter, written at low indentation under section headers, and it survives the text round-trip gate like any other content. The founding document asks for a language that “exists for human reading and machine,” and the format treats both audiences as readers of the same book.

What it looks like.

Chapter: Dice
 A bounded integer cannot leave its range; the overflow mode
 says what happens at the edge.
  faces : Integer between 1 and 20 = 20
  describe : Integer -> Text
  describe (roll) =
   if roll == 20 then "critical"
   else if roll == 1 then "fumble"
   else show roll
  opening : [Console] Nothing =
   print-line-uni ("you rolled " & describe faces)

The entry point is opening, not main. [Console] is the effect row; a function that prints must say so in its type. Prose lines at low indentation are part of the chapter, not comments — the literate format is load-bearing and survives the round-trip gate.

Distinctive moves.

Maturity.

The compiler is roughly 32,000 lines of Codex across 53 files and is a hard fixed point of itself: the canonical artifact is a ~2.1 MB self-sustaining CDX binary that boots under the project’s own WHP-based virtual machine or QEMU multiboot, compiles the full source, and verifies its own signature. A 217-test battery gates every change alongside the fixed-point checks. Around the compiler sit OS quires (22 bare-metal drivers including xHCI, NE2K, and Intel HDA, a networking stack, deterministic replay, the trust lattice), 113 transpiler plug modules covering ~48 targets, and the ~4,500-line C hypervisor that hosts the build loop. The bootstrap reference compiler was retired on 24 April 2026 and is kept only as historical record; no other-language toolchain remains in the chain. The strain to watch is the one the project chose deliberately: bare-metal memory ceilings make compiler heap usage a first-class engineering campaign, run with measured per-change verdicts.

Agent tooling.

CLAUDE.md is the operating contract: build gates, process rules, and prohibitions that agents follow verbatim, with per-agent identity files and a documented Perforce protocol for parallel streams. The compiler emits numbered diagnostics from a central registry (CdxCodes, 61 codes at the public cut, organised into ranges — 0xxx infrastructure and lexer, 1xxx parser, 2xxx type checker, 3xxx name resolver, 4xxx proof and capability, 9xxx compiler-internal) written to state what went wrong, where, and the suggested fix — diagnostics are treated as a feature with their own design rule. The build surface is fully scriptable (single-command gates, parallel test battery, single-file compile), deterministic replay ships as an OS quire, and the development history itself — bootstrap stages, gate results, measured memory campaigns — is recorded in-tree as the working memory of the agent team that maintains it.

design DNA
  • AILANG verification Both are agent-authored languages with effect typing. AILANG enforces capability rows over a Go-implemented runtime; Codex self-hosts -- the agents maintain the compiler that compiles itself, on bare metal with no runtime underneath.
  • MoonBit verification Both verification camp with broad toolchains. MoonBit bets on training-data depth and semantics-aware token sampling; Codex bets on the fixed point -- byte-identical regeneration as the gate every change must pass.
§ history

Timeline.

14 Mar 2026
Founding specification and first commit are simultaneous; the goal is a single literate language to replace accumulated repository hosting, with code that reads like a book.
Mar 2026
The compiler self-hosts roughly a week from the first commit.
24 Apr 2026
All four bootstrap stages green, 41 days from start: the reference compiler is permanently retired and the self-host is a byte-identical fixed point of itself on bare metal.
May-Jun 2026
OS quires land (22 kernel drivers, networking stack, trust lattice, deterministic replay), 48 transpiler plugs, a custom WHP-based VM for the build loop; an ongoing memory campaign requires a measured heap and time-complexity verdict on every change.