agentlanguages.dev
verification camp · also orchestration

Codex.

Self-hosting literate language on bare-metal x86-64: dependent, linear, and effect types, proof blocks, hard real-time enforcement, 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); ARM64 and RISC-V cross-compilation via plugs; PTX (NVIDIA) and SPIR-V (Vulkan/OpenCL) GPU targets; 53 transpiler plugs total 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 28,000 lines of Codex across 54 files and is a hard fixed point of itself: the canonical artefact is a 2.3 MB self-sustaining CDX binary that boots under the project’s own WHP-based virtual machine or QEMU multiboot, compiles the full source in a project-measured 22 seconds on bare metal, and verifies its own Ed25519 signature. A 137-test battery (consolidated from 232 individual tests) gates every change alongside the fixed-point checks; the full gate — CDX build, sign, canary, text round-trip, semantic equivalence, CDX fixed point, and BVT — completes in roughly 140 seconds.

Around the compiler sit 377 library modules across 26 quires (data structures, cryptography, networking, AI inference, game engine, 3D engine, UI toolkit, signal processing, compression, encoding, simulation, and hard real-time primitives), an OS kernel with 22 bare-metal drivers (xHCI, NE2K, Intel HDA, Bochs VBE, and others), a full TCP/IP networking stack (Ethernet through TLS), a preemptive scheduler with IPC channels, an identity and trust lattice, and a deterministic replay subsystem. Nine IoT board drivers (STM32F4, ESP32-C6, Raspberry Pi 4, nRF52840, RP2040, nRF9160, STM32L4, FE310, and QEMU virt) cover ARM, RISC-V, and hosted targets with 88 register-level sub-tests; the IoT protocol stack implements MQTT v5.0, CoAP, and LwM2M, and a compliance-evidence module maps 60 regulatory requirements across the EU Cyber Resilience Act, ETSI EN 303 645, NISTIR 8259A, and IEC 62443 to language features that satisfy each one.

The plug architecture ships 53 transpiler plugs across programming languages (Ada through Zig), UI frameworks (Angular through WPF), GPU targets (PTX for NVIDIA, SPIR-V for Vulkan/OpenCL), and binary formats (CDX, ELF, PE, GPT/FAT images). ARM64 and RISC-V cross-compilation plugs produce ELF binaries; on the project’s own micro-benchmarks, its codegen matches or beats GCC -O0 across four cases and emits fewer instructions than MSVC /O2 on a tight accumulator loop (14 versus 23) — single hand-written workloads measured by the project, not an independent suite. SIMD ships as first-class Vector N T types with dependent lane counts and SSE2 packed codegen.

630 application modules span 47 apps: an ERP suite with five industry verticals, an e-commerce platform, a relational database server with MVCC and WAL, a creative suite (3D modelling, image editing, animation, audio/DAW, video compositing), a collectible card game platform with web portal, a desktop environment, and 20 single-purpose web apps on a shared runtime. The project reports the C# transpiler plug emitting the full compiler (2,376 definitions), with the result compiling under dotnet build with zero errors, and an 8 MB UEFI-bootable GPT disk image running on real x86-64 hardware with an interactive coloured developer console.

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, organised into ranges — 0xxx infrastructure and lexer, 1xxx parser, 2xxx type checker, 3xxx name resolver, 4xxx proof and capability, 6xxx punctual enforcement, 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.
  • Vera verification Both verification camp, both span into orchestration. Vera checks with Z3 SMT and drops variable names; Codex checks with a five-phase verifier, dependent types, and the self-hosting fixed point. Vera targets WebAssembly; Codex targets bare metal.
§ 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 2026
OS quires land (22 kernel drivers, networking stack, trust lattice, deterministic replay), plug architecture ships, custom WHP-based VM replaces QEMU for the build loop.
Jun 2026
Dependent types (PropEqTy, proof erasure), type classes (dictionary passing), linear types (orthogonal to mutable), punctual hard real-time keyword, SIMD/Vector types with SSE2 codegen, ARM64 and RISC-V cross-compilation, PTX and SPIR-V GPU plugs. 53 transpiler plugs, 377 library modules, 630 application modules across 47 apps.