How we verify

Compiler correctness claims are cheap. This page describes what actually runs, step by step and with its figures, so you can judge how much weight every claim on this site carries. Nothing here is a plan: each gate named below exists in the repositories today and ran for the release this page is dated at.

The picture

The corpus

Each program carries a manifest declaring what to compile, how, and what to expect. One program declares many runs — a typical execution test declares twelve, covering six optimization configurations across both architectures. That is what the test-run figure counts.

The programs fall into seven categories, each with its own kind of expectation:

The scale of the thing

The last row is larger than the first. There is more Mica under test than there is Go doing the compiling, which is the ratio we want and the reason the figures are published rather than summarised: a corpus that grows more slowly than the compiler is a corpus falling behind.

The standard library is counted on its own because most of it is written in Mica — the compiler compiles its own library — and folding it into either the compiler or the test figure would hide that.

Every number on this page is read out of the repositories by a script at release time, or measured by the run it describes. None of them is typed by hand.

Axes under test

Programs are not merely run once and diffed. They are swept across:

• Optimization profiles — debug, checked, release, and the optimizing lowering with every guard on
• Individual passes — constant folding, peephole, inlining, loop optimization, SSA versus direct lowering, graph versus stub allocation
• Architecture — x86_64 and AArch64, one native and one under an emulator on a developer’s machine, both native at a release
• String encoding — UTF-8 and UTF-32, which is a per-binary property
• Deployment class — the hosted heap and the fixed arena
• Carrier count — single and multicore

Optimizer statistics are themselves pinned as expectations. If a change causes the inliner to decline a site it used to accept, or the peephole pass to fire a different number of times, the suite notices — so a silent performance regression is a test failure rather than something discovered in a benchmark months later.

The ladder, step by step

Nothing merges without the ladder. It builds the compiler and the standard library once, then runs the following, in this order. The cheap gates come first, so a crossed boundary or a stale pin is reported in seconds rather than after a quarter of an hour of tests that would all have passed.

1. The dependency gate. The compiler’s internal package-to-package import edges — 270 of them — are pinned in a file, and the gate fails on any difference in either direction. A new edge is a package boundary crossed without a decision; a removed edge is worth recording in the commit that earned it. The gate needs no build and runs in seconds. It is what keeps the backend free of the frontend, so that a language other than Mica can drive the same backend through the Dragon SDK.
2. The type-kind totality gates. Every kind of type must be classified in the one table every walk over type parameters reads, and the frontend’s textual instantiation road must agree with it; a kind added without both answers fails by name before a single program compiles.
3. The harness’s own tests. The test framework reads the compiler’s counter names and optimization spellings, so its 164 tests run inside the ladder: a counter the compiler adds without its label fails here.
4. The run-count pins. Each suite’s planned run count is enumerated before anything runs and compared with its pinned figure — stress 13,047/0, direct lowering 12,952/0, race 12,952/0 — in both directions. A pass says only that nothing disagreed; the pin says how much ran, so a case silently lost reads as a failure rather than as a quieter pass, and a corpus that grew without anyone recording it reads as one too.
5. The formatting check. The Go tree must be formatted; an unformatted file would otherwise land as a large diff in whatever commit next touched it.
6. The standard library at every tier. The units of the standard library are the largest body of Mica the project owns. They compile at every optimization tier here, not only at the one they ship at, because a path exercised by exactly one build is an untested path — and two compiler defects were once waiting on the tiers nothing compiled.
7. The price gate. Every benchmark kernel’s retired-instruction count under callgrind is pinned — 23 kernels — and measured with the compiler the ladder just built; a kernel over its pin by more than one percent is a red gate that names the kernel, the pin and the measurement. The count does not move with the machine’s mood, which is why it is the regression road, while the documented-machine run below stays the publication road.
8. Three concurrent suites, each in its own workspace, each sharded across several processes:
   • Stress — the whole corpus through the compiler binary, on both architectures, including the stress cases with their compile-time budgets.
   • Direct lowering — the same corpus through the non-SSA lowering path, kept green deliberately as a differential oracle against the SSA path. Two independent lowerings that must agree is a strong check on both.
   • Race — the corpus through an in-process driver with Go’s race detector armed, the only mode that puts the compiler’s own concurrency under scrutiny. A suite passes only when its process exited cleanly, its summary’s verdict reads passed, and its run count matches the pin.
9. The compile-time budgets. Programs of a thousand, ten thousand and a hundred thousand lines compile once more, alone, after the suites, and each must finish inside its budget — the hundred-thousand-line program in 10 seconds at most. The compiler’s compile-time scaling is a guarded property, not a hope.

A compiler warning fails the suite. There is no accumulating backlog of tolerated diagnostics.

The arms before a release

Three sequential arms join the ladder before a release. They run after the concurrent suites so their slowdowns never contend with the budgeted compiles, and each is reported as runs and failures on the facts page:

• Multicore (296/0) — the whole tasking corpus rebuilt for the concurrent runtime must print byte for byte what the sequential build prints, on both architectures, at debug and release; two entry programs that suspend the first task before any other exists run across every carrier count; and the runtime’s own heap is exercised by stress drivers under ThreadSanitizer in both memory classes.
• The C shim (64/0) — every driver written against the Dragon SDK’s C header is compiled, and its emitted assembly is linked and executed per architecture and per optimization regime, the running program’s bytes compared against a machine-derived expectation. Wirth’s PL/0 compiler, written twice, in C against the header and in Mica against the embedded surface, is among those drivers, and the two must agree byte for byte in every output.
• The memory checker (529/0) — every heap-, obligation- and string-tagged program runs host-native at every tier and memory class under valgrind with full leak checking, except that a run expected to end in a trap counts errors but not leaks; an invalid access or a leak fails the leg. One record is suppressed, with its reason kept beside the arm: the concurrent runtime’s carrier threads are detached by design and alive at exit.

Beyond the ladder: the probes

Some properties no expectation file can state. Each has its own probe, run at a release and whenever the part it guards changes:

• Double-compile determinism. The whole corpus is compiled twice by two separate compiler processes, and the two runs’ assembly and object files — every case, every tier, both architectures, about sixteen thousand files a side — must be byte-identical. A compiler that is not deterministic is a compiler nobody can bisect; this turns that class into a red row.
• Reproducible builds. The determinism probe compiles the same source on both architectures across runs and pins the bytes, so a divergence that every expectation-based gate would pass twice is caught once.
• Undefined behaviour in the runtime. The runtime floor every program links is rebuilt with the C compiler’s undefined-behaviour sanitizer in its trap-on-error form, the shipped compiler and library are staged beside the sanitized archives, and a corpus of tape- and tensor-heavy programs is compiled against that floor and executed: an undefined operation in the runtime, or an emitted frame that hands a kernel a misaligned pointer, dies on a hardware trap instead of passing.
• The command line’s refusals. Eight hostile command lines must each answer with one curated sentence and the help hint — never a raw operating-system error, never the flag table, never a linker’s own output.
• The GPU, on real cards. The device probe runs on the machine that owns the card: every kernel is held against its serial reference, and a training run made twice on one card must leave the same learned weights byte for byte.
• The adversarial sweep. Compiling programs are mutated into the shapes a rule should refuse — an address that outlives its cell, a container grown while walked, a cell released twice through two names — and each runs under valgrind, the checked tier and a 64 KB arena before it counts. The sweep of 283 programs before 7.5 found 41 defects, every one now a refusal that names its rule, closed with a refusal case and a legal twin, and the whole probe set is replayed against each fix so a family of shapes closes rather than the one that was filed.

The package proof

A package that lists the right files can still not work. So the proof is not a listing: the built package is unpacked into an empty root, the path and the library search are pointed at that root alone, and a real program is compiled, linked and executed from it — including a program that places a tensor on the GPU, linked against the packaged device floor and the machine’s real driver. The upgrade from the previous release’s package is simulated the same way. This runs on both architectures at every release, each on a native machine.

The publish script refuses to run on a dirty tree, so every published artifact maps to one commit, and the site’s own pipeline fetches each package by its recorded checksum: a package that does not match its manifest never reaches the download page.

On machines anyone can rent

Two roads take the verification off the developer’s desk and onto machines anyone can rent, so that neither architecture depends on a machine that has to be awake.

The harness in the cloud. A cloud machine of either architecture is created for the length of one run and given back. The payload carries artifacts, never source: a compiler binary, the archives it links, a harness binary and the test cases — the same things any user of the released compiler has — with a manifest naming the commit and the architecture. The results come back, and the machine is destroyed under a trap that fires on failure and on interruption alike.

The benchmarks on documented machines. Every published performance figure comes from one run on named machine types — t2a-standard-4 for AArch64 and t2d-standard-4 for x86_64, in europe-west4-a — one throw-away machine per architecture, both compilers at O2, every Mica safety check on. Every kernel is written twice, in Mica and in C with the same algorithm, and the renderer validates before it writes a single number: the documented machine type and region, one compiler line on both machines, every Mica output identical to its C reference, every library self-check identical on both architectures, every kernel within its memory budget. A run that fails any of these renders nothing, by name. Four metrics are kept because any one alone would mislead: retired instructions (deterministic, and the harshest view), the processor’s cycles where a machine offers them, the wall clock (what a person waits for), and peak resident memory. Performance carries the method, the facts page the tables.

The devkit’s own gates. The tools that create those machines are tested too: 6 gates run the real tools on fresh containers and assert what the machine looks like afterwards — 16 provisioning cases, 4 cases against a faked cloud command line that records every call, the development container’s configuration reproduced as the editor reads it, every script parsed under the shell macOS ships, every generated first-boot document parsed as the cloud reads it, and 6 cases over the benchmark road against a recorded run. Said plainly, because a gate silent about its edges is over-trusted: the cloud verbs are exercised against a faked command line, which proves the tool’s own decisions and nothing about the cloud’s answers, and no gate creates a real cloud machine — that costs money and stays a human step.

The other surfaces

The compiler is one of five things a user meets, and each of the other four has its gate.

• The starter repository. Every push builds every example and every benchmark kernel inside the published image — the exact environment a user has — so that drift between the examples and the compiler is a red mark rather than a discovery; every notebook’s cells are re-run and each fresh output held against its recorded fence, the same verification the editor’s Verify command performs; and the devkit’s static and behaviour gates run on every branch.
• The editor extension. Packaging is a chain that stops at its first refusal: the validator checks the manifest, the language configuration, the grammar and the glyph table against each other; 26 tests run; the package is built; and a content gate reads the finished package and refuses one that carries anything credential-shaped — a gate that exists because of a near miss, not a hypothetical.
• This site. The tutorial gate compiles every Mica code block of the learn pages with the released compiler and classifies each block — a complete program, declarations, statements, or a sketch — so a chapter whose words drift from the compiler is named. Every figure on the facts page is generated from the repositories at release, and every benchmark table is rendered from the run’s own files.
• The harness itself carries its own tests, run in the ladder as step three above.

How an expectation is made

• A printed value is computed by hand or by machine before the program runs, never copied from the program’s output: an execution test’s expected total is the closed form of what it put in.
• A diagnostic is pinned from the compiler’s actual report, row by row in report order, so a message that moves or changes wording fails the case.
• Optimizer statistics are pinned too. If a change causes the inliner to decline a site it used to accept, or the peephole pass to fire a different number of times, the suite notices.
• Every memory rule is proved in both memory classes: a program that must reclaim per round runs two thousand rounds inside a 64 KB arena, where one leaked backing per round exhausts the arena and a peak is told from a leak by running a tenth of the rounds.
• A debugger case is a transcript. The expectation is the gdb session itself — the breakpoints hit, the values shown — so the debug information is tested the way a person uses it.

Quality gates inside the compiler

Separately from tests, the compiler validates its own invariants at two checkpoints, after semantic analysis and after intermediate-code generation, whenever --quality is on — and it is on for every compile of every test program. These are not assertions left in by accident: they exist to root-cause an internal compiler error at the phase that introduced it rather than at the phase that tripped over the result.

Figures as of 2026-09-13, compiler 7.5.0. Gate results from the release ladder of 2026-09-13 at the v7.5.0 tag: stress 13,047/0, direct lowering 12,952/0, race 12,952/0, multicore 296/0, C shim 64/0, memory checker 529/0, 270 pinned package edges, 23 pinned kernels.