NanoLang.

The thesis.

NanoLang takes the verification camp’s diagnosis literally: if LLMs are going to write code, the language should refuse to accept their work without tests, and the language’s core should have proofs to back its promises. Every function declaration must be paired with a shadow test block; the compiler rejects functions without one. The proved core (NanoCore) has 6,170 lines of Coq across 9 files, 193 theorems and lemmas, zero axioms, zero Admitted — the proofs cover preservation, progress, determinism, semantic equivalence of big-step and small-step, and evaluator soundness against a fuel-based reference interpreter extractable to OCaml. The README announces it in first person: “I refuse to compile a function unless you provide a shadow test block for it.”

"I am a minimal programming language designed for machines to write and humans to read. I require tests, I use unambiguous syntax, and my core is formally proved."

The distinctive move is the depth of what is actually proved — and the honesty about what is not. NanoCore covers integers, booleans, strings, arithmetic, conditionals, mutable variables, while loops, lambda/application, arrays, records, recursive functions, variants, and pattern matching. Algebraic effects, async/await, FFI, the VM, and the multi-target codegen sit outside the proof set, and formal/README.md says so plainly. Vera proves contracts at the function level via Z3; NanoLang proves the type system itself, from below. Same camp, complementary layers.

What it looks like.

fn greet(name: string) -> string {
  return (+ "Hello, " name)
}
shadow greet {
assert (== (greet “World”) “Hello, World”)
}
fn main() -> int {
(println (greet “World”))
return 0
}
shadow main { assert true }

Distinctive moves.

• Mandatory shadow tests. No function compiles without a shadow block. The smallest legal program contains shadow main { assert true } — the discipline applies to the trivial case alongside the substantive one.
• Coq proofs, zero axioms. 193 theorems and lemmas across Syntax.v, Semantics.v, Typing.v, Soundness.v, Progress.v, Determinism.v, Equivalence.v, EvalFn.v, and Extract.v. No Admitted lemmas; the proofs go through. Built on Rocq Prover (Coq) ≥ 9.0.
• NanoCore is the proved subset, not the whole language. The proved fragment is honest about its scope. Effects, async, FFI, the VM, and codegen are out-of-scope for the formal work and the project documents that directly.
• NanoISA VM with co-process FFI. Stack-based VM, 178 opcodes, reference-counted GC. External calls run in a separate co-process (nano_cop); if they crash, the VM survives. Trap model separates computation from I/O.
• Multi-target codegen. Default target is C transpilation. Also --target wasm (with source-map sidecar and Ed25519 signing), llvm, ptx, riscv. Production parity is claimed for C and WebAssembly; the other backends are present in the toolchain.
• Dual notation, prefix and infix. (+ a b) and a + b are both legal. The prefix form is described as unambiguous and is the form the formal semantics is stated against.
• First-person persona. README, diagnostics, and AGENTS.md instruct agents to write in NanoLang’s voice. Documented under docs/PERSONA.md as a design choice, not a quirk.

Maturity.

v3.3.7 (April 2026), 51 tagged releases, ~2,156 commits, bootstrap 100% (the compiler compiles itself). Apache-2.0. Hardware support: Ubuntu 22.04+ on x86_64 and ARM64, macOS 14+ Apple Silicon, FreeBSD; Windows via WSL2 only. The author is Jordan Hubbard — co-founder of FreeBSD in 1993, currently Senior Director for GPU Compute Software at Nvidia — and the project’s GitHub topics include thought-exercise and vibe-coding, applied by the author himself. The README’s “Totally True and Not At All Embellished History” notes the language has “been used in production by exactly one person, who also wrote it.” That candour matches the catalogue’s tone: the engineering is real, the framing is honest about what the engineering is for.

Agent tooling.

The repository root ships AGENTS.md, CLAUDE.md, MEMORY.md (self-described as “my training reference for patterns and idioms”), spec.json (machine-readable formal specification), .mcp.json, and config folders for Claude, Cursor, and Factory. The IDE surface includes a Language Server (bin/nanolang-lsp) and Debug Adapter (bin/nanolang-dap) plus a VS Code extension; the web playground supports share permalinks and live evaluation. The agent-facing surface is wider than most catalogue entries — NanoLang ships not just orientation files but its own corpus.