Modula-9.

Nothing here is asserted; it is compared against an oracle.

The thesis.

Reviewability and correctness are treated as the same problem. If an agent writes code and no human reads it closely, the language has to make mechanical checking and human review cheap at once, which rules out both an untyped scripting language whose errors surface at runtime and a proof-carrying one whose obligations only another expert can audit.

The answer is a conservative grammar aimed at a specific failure profile: a generator is fluent, confident, and has no memory of what went wrong last time, so the constructs where fluent-but-wrong code still compiles are removed. No implicit conversions, including widenings, and no INTEGER or REAL, only exact widths, so a wire format and a type agree by construction or the program does not build. No NIL: a possibly-absent pointer has type OPT and cannot be read without a guard. CASE over a variant record must cover every arm. Every exception a procedure can raise appears in its RAISES clause, derived by the checker from explicit raises plus the declared sets of everything it calls. PURE is checked by the rule that a pure procedure may call only pure ones, which makes “no I/O” true without the checker needing to recognise I/O at all. Macros, conditional compilation, operator overloading and Pascal’s WITH are refused, so a reviewer never reconstructs which text was compiled. The definition module carries the whole contract — types, failure modes, allocation, thread-safety — which is also what makes an interface mechanically extractable for a model.

Correctness then comes from comparison rather than specification. Rather than asking the author to write one, an implementation is validated by running it against the existing implementation of the same computation and requiring the outputs to agree — and the reference is ordinary code in an ordinary language: the Python a team is trying to replace, the Fortran kernel that has produced the numbers for twenty years. In data science and finance that reference nearly always already exists, so the specification burden that has historically kept formal methods niche is absorbed by code someone already wrote and already trusts. The discipline sits in the repository rather than the language: nothing in the grammar names a reference, and the compiler will build a module that has never been compared with anything.

The evidence for the premise is the project itself: a co-authorship trailer on 409 of 430 development commits from 20 August 2026. The public mirror squashes history per release and does not show them, so the figure is the project’s account rather than something the mirror can be read for. The house rules follow from the fact rather than decorating it — a measurement for every claim, a cited failure for every feature, and a gate for anything that can drift are what let a person stay answerable for code they did not type.

What it looks like.

DEFINITION MODULE Mat ;
TYPE
  Matrix ;                        (* opaque; lives in a POOL *)
EXCEPTION
  SizeError (got, want: I64) ;
PROCEDURE New (VAR pool: POOL ; rows, cols: I64) : PTR Matrix IN pool
  RAISES SizeError ;
PROCEDURE Get (m: PTR Matrix ; r, c: I64) : F64 ;
PROCEDURE SubRowVector (VAR pool: POOL ; m: PTR Matrix ;
                        RO v: SLICE OF F64)
  : PTR Matrix IN pool
  RAISES SizeError ;
END Mat.

Distinctive moves.

• Checking that cannot be switched off. No flag, pragma or build profile removes the checks, so the code that ships is the code that was checked. The mandatory set: bounds on every subscript and sub-slice; overflow on integer +, - and *; zero and MIN/-1 on DIV and MOD; range on every checked conversion; finiteness before float-to-integer, so Trunc(NaN) raises ValueRange rather than fabricating INT64_MIN; and a trap on an impossible variant tag. Modular arithmetic must be spelled +%, -%, *%. The compiler eliminates nothing statically — it emits every check and leaves the provably redundant ones to gcc.
• Differential execution as the acceptance gate. Gates compare against recorded output: goldens produced by an oracle run, checked in and never regenerated by the gate that reads them, on the rule that a gate which regenerates its own expectation cannot fail. Inputs are real or hand-curated rather than generated — a seeded zarr store, a 207 MB ICOS FLUXNET CSV, 497 ERA5 GRIB messages — with no property-based generation and no fuzzing. Where much of the verification camp makes a per-function contract mandatory, M9 requires none beyond the definition module’s signature; the comparison is a discipline the project imposes on itself.
• Language-agnostic references. Comparators in use are GNU Modula-2, Object Pascal, gfortran, numpy, scipy, polars, pyarrow, the C APIs of netCDF and ecCodes, and the Rust zarrs crate. Invocation is per-gate and unabstracted: some oracles run once and their output is checked in, some are linked into the same C driver and compared with memcmp, one is a live Python service the port replays HTTP requests against, its commit pinned in a file and asserted before any replayed byte is believed. Agreement is byte-identical where exactness is expected, and within a stated tolerance — 1e-13 against numpy’s linear algebra — where an independent implementation orders the arithmetic differently.
• C as the only dependency. No LLVM, no runtime to install, no cross-compilation story. The 0.3.1 packages were built on six distributions spanning gcc 11.5.0 to 16.2.1, each recording its distribution, gcc version and smoke test in a checked-in receipt, and one gate builds the whole compiler with fpc, gfortran and python3 replaced on PATH by scripts that fail loudly. The runtime assumes POSIX rather than bare C, and every published package is x86-64 Linux; no other platform is claimed.
• Inherited grammar. Seventy productions against a self-imposed ceiling of a hundred, and sixty keywords. The departures carry their evidence: relations bind tighter than AND and AND tighter than OR, because the corpus wrote that shape six times and Wirth precedence would have rejected all six; identifiers contain no underscores, so a foreign C name binds as a string literal and the two namespaces never mix.

Maturity.

Self-hosting at v0.3.1 (30 August 2026). Lexer, parser, printer, checker and C11 generator are written in M9 with the emitted C checked in, so a fresh clone builds with cc alone; the bootstrap gate compares 31 modules across three stages and requires stage 3 to equal stage 2 to equal stage 1. The standard library is 32 modules and about 27,600 lines. There is no language server, no formatter and no package registry. The repository carries the language report as normative specification beside the compiler, the Object Pascal oracle, the gate scripts and the material they compare against — the must-not-compile museum, the checker probes, the Modula-2 and Object Pascal originals the corpus restates, the benchmark programs — so the differential claims can be re-run rather than taken.

Three deployments, and the tutorial is the smallest and the most self-referential. tutorial.modula9.net is written in M9: the HTTP server and the pipeline driving m9c, cc and bwrap are M9, with JavaScript only for the editable cells, so the language hosts the document that teaches it and compiles what readers submit. Its twelve chapters are public at atverm/M9Tutorial and held to the compiler the way everything else here is — twenty example programs, fourteen run and compared byte for byte with what the chapters print and six required to fail with the diagnostic the text quotes, plus forty-one fenced blocks that must equal the gated file each names, and a second gate repeating the set against the compiler in the latest release so the pages cannot describe a language the shipped package does not have.

The other two are ports, and they verify differently. FLEXPART-M9 is a transcription of the FLEXPART v11 dispersion model — 52 modules and roughly 30,900 lines of M9 from 45,368 lines of Fortran — running production cases through a job queue; comparison is bit-identity, with the original subroutine copied into the gate, compiled by gfortran, driven from the same C driver and compared by memcmp. The ICOS zarr proxy is nine modules and about 11,100 lines replacing a 6,400-line FastAPI service, and its gate compares neither source nor linked subroutines: it replays HTTP requests against the running Python and matches status, content-type and body byte for byte, holding one deliberate divergence to exactly. Both proxies are deployed behind one nginx switch on the same port, with exactly one running. Both ports are in private repositories and cannot be verified from the public one.

What they found is kept as a ledger rather than a patch set, since a transcription that quietly corrected the model would be one whose differences nobody could bound afterwards: 42 entries against FLEXPART v11, plus a dozen transcription mistakes the harness caught in the port itself. Those are the more informative half, because none was catchable statically — a module variable transcribed as both a record field and a parameter, a loop that ran one step too many because an exit sat mid-body in the Fortran. The proxy replay caught its own instance: a passport citation carrying á went out as a literal \u00e1, a client-visible difference every crafted test store had missed by being ASCII. The limits are stated with the results — agreement holds only over the inputs actually run, and one untranscribed call is invisible precisely because the data carries no message that would expose it. The oracle itself needed pinning: gfortran 15 at -O2 changes its own answer under -ftree-vectorize, one single-precision ULP on 152 of 960 elements, so every oracle is built -fno-tree-vectorize and checked against its own -O0 build first.

On three published benchmarks, each diffed for identical output before any clock is read, M9 is at parity with C on floating point (mandelbrot N=4000, 0.73 s for both) and marginally ahead of unchecked C on integer work with every check active (fannkuch-redux n=11, 1.90 s against 1.94 s), while Rust leads both integer benchmarks and Scala leads on allocation churn. The 3% figure is isolated by hand-editing the generated fannkuch C into variants that change one thing each; removing every bounds check, verified by grep -c m9_at reaching zero, bought 1.81 s. Figures are one machine, best of three or five, and the project publishes its losses alongside. One finding qualifies the 3% usefully: the checks’ indirect cost is the larger one, since a checked procedure body rarely fits gcc’s default inlining budget of 15 instructions, so m9c ships --param max-inline-insns-auto=200 alongside -O2 and -flto — worth 2.4× on one measured kernel, more than deleting the checks outright would have been.

Agent tooling.

m9c --doc writes a module’s definition as Markdown, listing undocumented names marked rather than omitted; the 29 generated references are checked in and held byte-identical by a gate. m9c --json writes the same gather as data: per procedure its kind, line, rendered signature, parameters as name/mode/type triples, result, RAISES list and attribute. The manual page states the motivation in agent terms — that the commonest mistake a fluent generator makes is a real name it did not look up, and that a table of names copied into a prompt drifts within a day. Both run the checker first, on the grounds that documentation for a program the checker rejects describes a program that does not exist, and the same path feeds the VS Code extension’s hover and completion. A message/cause/fix table covering every refusal the checker can produce is generated from the same negative programs the two checkers are held to, so a refusal with no explanation fails the build. m9c --no-unsafe refuses a program whose import closure declares an UNSAFE or foreign unit outside the trusted library directories, which is what lets the tutorial service compile strangers’ code with the OS sandbox as a second wall rather than the only one.

Diagnostics are human-readable text with line and column, not JSON, and there are no stable error codes. There is no MCP server and no language server. Two Claude Code skill files exist in the development tree and are gated there, but they are not published, and nor is the project’s own memory file.