How we verify

The gates and the figures below state the compiler as of release 7.7.7.

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 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: the ladder runs each architecture’s legs natively on a machine of that architecture, and a release proves its packages, walks every tutorial and runs every benchmark natively on both
• 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
• Small machines — one processor, and a hard limit on a program’s address space

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

Every change to the compiler’s code, tests or scripts passes the ladder before it merges into a release branch, and the ladder tests the tree the merge would make: the change’s branch with the release branch merged in. A change whose release branch moved on while its ladder ran is tested again before it merges. The ladder runs in seven parts side by side: five on x86-64 machines of our own, each part on the first that comes free, and two on AArch64 machines of our own, so each architecture’s runs are judged natively on its own processor — the runs that must run natively, the cases written for the address or thread sanitizer and the debugger’s among them. Each part builds the compiler and the standard library once and runs its own share of the steps below, and the ladder passes only when every part of both architectures passed on one tree. Run whole on one machine, the steps fall into four stages, 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; the pipeline’s fast checks run the same opening gates on every push.

Before the build

1. The dependency gate. The compiler’s internal package-to-package import edges — 353 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 grammar, and every page that quotes the compiler. The grammar on this site, the language description’s examples, the style guide’s rules and the words the editor highlights are each held to what the compiler gives, so none of them drifts from it unseen — the other surfaces below say how.
3. The format proof. mica --format must never change what a program means. Every source the project keeps — the corpus, the standard library’s units, the starter repository’s examples — is formatted and held to its original: the same tokens, the same comments, the same reading by the parser, and the layout’s own invariants. A source the formatter refuses is admitted only where the compiler’s parser refuses it too. Inside the suites below, the first run of every case is built once more from its formatted copy, and the two builds must be one program.
4. The type-kind totality gates and the coverage gate. 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. The coverage gate does the same one level up: every node kind of the syntax tree and every operation of the intermediate code stands in a table with the checks that judge it, read from the code, and a member that arrives with no check and no stated reason why it needs none fails by name, so its protection is decided in the commit that adds it.
5. The failure-code gate. Every number the compiler prints with a diagnostic, a refusal or an internal error names exactly one failure, so a search for it finds one meaning. Each part of the compiler counts its failures from a base of its own, and the gate reads every table as the code declares it and refuses two whose numbers meet, by name, in the commit that would make them meet.
6. The harness’s own tests. The test framework reads the compiler’s counter names and optimization spellings, so its 326 tests run inside the ladder: a counter the compiler adds without its label fails here.
7. The run-count pins. Each suite’s planned run count is enumerated before anything runs and compared with its pinned figure — stress 27,614/0, direct lowering 27,503/0, race 27,503/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.
8. The formatting checks and the length ceiling. The Go tree must be formatted, the Python the project keeps — the debugger’s scripts, the gates, the calculators of expected values — must pass its linter and formatter, and every C file of the runtime and the standard library must stand as one pinned release of clang-format writes it; an unformatted file would otherwise land as a large diff in whatever commit next touched it. Beside them stands a ceiling on a Go file’s length: a file past a thousand lines grows no further unless the commit that grows it records the decision.
9. The generated cases and the half-precision conversions. The cases a model writes — the compile-time constants and the device cases — must each be the checked-in case byte for byte, so nobody who regenerates them rewrites one with an answer the compiler no longer gives. And every float16 and bfloat16 pattern the runtime widens, and every float32 pattern it narrows to both, is held bit for bit to the C compiler’s own conversions.

After the build

10. The runtime contract. Every program links a runtime written in C and reaches it by name alone. A contract the compiler carries inside itself names every entry a program can call, and every link checks its runtime against it before a single tool runs, so a runtime missing an entry is refused by that entry’s name rather than met as a linker’s complaint or a jump into nothing. The ladder holds both halves on every build: the contract must still be what the compiler’s own tables give, every runtime archive the build made must satisfy it, and the check must still refuse an archive that is no runtime at all, so it cannot rot into a check that passes everything.
11. The published schemas and the editor. The schemas editors check a project file and an interop contract against must be the compiler’s own, so an editor never judges a file by rules the compiler no longer keeps. And the editor is held to the build: every errors and execution case the editor can state is compiled by the build and by the language server’s check, and the two must give one set of diagnostics — code, severity, line, column and words.
12. The heap facts. Every runtime entry is declared as reaching the heap or not, and as waiting or not, and a heapless routine or a signal handler is held to those declarations at every call. The declarations are derived again from both architectures’ compiled call graphs, and one a graph contradicts fails by name.
13. The command line’s refusals. 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.
14. The starter repository. Every example, benchmark and library a user clones first is rebuilt with the compiler this ladder just made, so no compiler merges that cannot build them.
15. The same program every time. The starter repository’s GPT is compiled twice per architecture at the full optimization level and twice at the debug tier, by separate compiler processes, and each pair’s assembly must be one image byte for byte. And the same source, compiler and flags must give the same bytes in every build folder: programs that place code on a GPU, a plain program at every tier and a library as an archive and a shared object are each built twice for both architectures, in two folders of different names, and every file the two builds wrote — the program or library, every object and every assembly source — must be the same byte for byte.
16. 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.
17. The size, memory and price gates. The stripped size of the reference programs, what they hold in memory as they run, and the retired instructions of every benchmark kernel are pinned, and measured with the compiler the ladder just built — the code the optimizer writes below says how.

The corpus, many ways at once

18. 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.

    The format proof’s second half runs here too: the first run of every case, built once more from its formatted copy. So does the execution corpus once more, with the graph-colouring register allocator, inlining and the loop passes forced into every release build, which otherwise runs them only at the full optimization level, so each pass also meets the less optimized code of the other builds, and every program’s answer is judged.

19. The three C sanitizers — the execution corpus under the address sanitizer, the cases that walk the runtime’s deepest C under the undefined-behaviour sanitizer, and the task, process, stream and generator cases under the thread sanitizer: the C beneath every program below.

20. The small machine — the corpus run the way a small board runs a program. Every concurrency-bearing case runs with each program confined to one processor, once the runtime’s own check has stated that it found one, and must give its expected answer; the cases that allocate where a small machine runs out first run under a hard limit on the address space, and each must give its answer or stop with the runtime’s documented out-of-memory report. A signal, a hang or any other report fails the run, and a leg in which nothing ran out proves no out-of-memory road, so it fails too.

21. The three arms — the multicore gate, the C shim and the memory checker, below.

A suite passes only when its process exited cleanly, its summary’s verdict reads passed, and its run count matches the pin. Every run outside the sanitizers is bounded by ten times the time it took on a recorded ladder, and never less than ten seconds, so a hang is named by its case rather than by the job’s clock.

After the suites

22. The assembly waste ledger. The optimized assembly the stress suite wrote for every execution case is read for code that does nothing — the code the optimizer writes.
23. 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, at the checked tier too. Beside them, long single expressions must compile inside a budget of their own, so a walk repeated at every level of an expression is caught as surely as one repeated per line. A change is also timed beside the compiler it is based on, built from that commit and run on the same machine at the same hour, and a case it compiles more slowly than its base by more than a stated tolerance fails by name, with both times. The compiler’s compile-time scaling is a guarded property, not a hope.

A compiler warning fails the suite, and so does a remark a case does not expect: every compile runs with the compiler’s remarks on, and every remark a run speaks must be one its manifest admits. There is no accumulating backlog of tolerated diagnostics.

The three arms

Three arms join the corpus suites on every ladder the pipeline runs, and a release is stamped only by a ladder that ran all three. The multicore gate and the memory checker run in the ladder’s memory part, beside the sanitizers and the small-machine legs, and the C shim in the part that measures sizes, memory and prices, whose budgeted compiles wait until it has finished, so its load never reaches their clocks; on AArch64 all three run in the part that runs the runtime’s checkers and the measured gates. Each arm is reported as runs and failures on the facts page:

• Multicore (424/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 with one carrier and with two; and every refused spelling of the tasking flag must answer with its own message. Beside them, the runtime’s concurrent parts run under real threads in stress drivers compiled with ThreadSanitizer, each on a pool of one carrier, of two and of eight, after a planted race has proved that the sanitizer reports, and each must end clean — no data race, the exact result its closed form predicts, no hang: the heap and the checked tier’s own state in both memory classes, the work-stealing scheduler, its deadlines and the points where its carriers sleep and wake, the channel ring, tasks parked on sockets, pipes and files, a generator whose continuation migrates between carriers, the scratch block in which a UTF-32 program writes its text arguments as UTF-8 for the C function it calls, and the tensor kernels’ bands, whose bytes are held against an independent reference.
• The C shim (124/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 (5,871/0) — every heap-, obligation-, string-, descriptor-, generator-, task-, stream- and signal-tagged program runs host-native at every tier, memory class and tasking flavor under valgrind with full leak checking, its worker processes included, 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 carrier threads of a multicore program that ends abruptly, by an exit while its tasks still run or by a signal, end with the process, as the threads of a C program do. A program that ends quietly joins its carriers and gives everything back, and the runs that state so are judged without the suppression.

The code the optimizer writes

A program that computes the right answer can still carry code that does nothing, and an optimizer is judged by what it leaves out as much as by what it gets right. So the code every optimized build writes is verified, pinned and costed, beside the corpus that checks what it computes:

• The machine-code verifier. The last optimization rewrites the machine code itself, after every other check has run, so a verifier reads what it leaves behind. On both architectures it builds each routine’s control-flow graph, follows the registers, the stack and the frame through it to a fixed point, and holds the code to the rules every correct rewrite keeps: every branch lands on a label of its own routine, defined once; no register is read on a path before something writes it; the stack is back where it started at every return and keeps the calling convention’s alignment at every call; every register the convention preserves holds its caller’s value again at every return, and the return address is untouched; and every instruction’s operands are a form the processor accepts. Each rule is sound for code that follows the convention, so a finding is a real defect and never a guess. Every optimized compile of every test program runs it, and a finding stops the build with an internal error that names the routine, the instruction and the rule.
• Golden assembly. 30 small canonical programs — a greeting, a counted loop, an array sum, a string joined from pieces, a record copy, a case statement, a generator, a task and its join, a fallible call with its handler, recursion, narrow integers, a floating-point clamp and more — carry their whole optimized assembly as their expected output, at O1 and O2 on both architectures. A change to the code generator that adds, removes or reorders a single instruction in any of them fails until their files are written again, and the regenerated difference is the review of what the change does to the code everyday programs get.
• The waste ledger. Code that does nothing compiles, runs and passes every test, so no test notices when a change brings some in. After the suites, the optimized assembly of every execution case, at O1 and O2 on both architectures, is read for it: a store nothing reads, a value written to the stack and read straight back, a value reloaded after a call that a register could have kept, a test whose outcome the program’s own read-only data decides, a nop, a jump to the very next instruction. Each case’s count of each pattern is pinned, and a count over its pin fails the ladder with the case, the pattern, and the routine and line of the first finding. Where such code is right on purpose — a register’s save that a debugger reads to unwind through a routine that never returns — the exception is written down beside the pattern with its reason, never skipped in silence.
• The size gate. A static link copies into a program every runtime piece its code names, so a piece meant for a few programs can ride into every program, and nothing fails: each program only grows. The reference programs — a greeting, an everyday program with a map and a string buffer, and a concurrent one with tasks — are built at the debug and the shipping tier on both architectures, and the bytes of each stripped file, of its code and of the memory it reserves at start must stay within one percent of their pins. The facts page states what each one carries.
• The memory gate. A program can carry the same bytes on disk and still hold more as it runs. The same reference programs run natively, at the debug and the shipping tier in each memory class and tasking flavor pinned for them, and four figures are held to their pins: the peak resident memory, the least of seven runs; the smallest address space the program runs in, found under a hard limit raised from below and then halved down to one page, each limit tried many times so the C library’s random rounding of its heap is not counted; the zero-filled and the initialized data, Mica’s own apart from the C library’s, symbol by symbol; and the most bytes Mica’s own heap held at once. A figure past its band fails by the program’s name and the symbol that grew. A seeded fault follows, the runtime reserving 64 KiB more, and every row of the greeting must fail by that buffer’s name, so a gate that stopped seeing such a buffer is red as well.
• The price gate. Every benchmark kernel’s retired-instruction count under callgrind is pinned — 50 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.

A gain is recorded before it merges. The size, price and waste gates hold in both directions. A figure under its pin is a gain, and a change whose ladder measured one merges only once a commit in it records the gain, with the figure that ladder measured on its own machine — a pin taken on another machine counts differently. A gain left unrecorded would leave the pin where it stood, and a later loss of the same size would then pass unseen. A rise merges the same way, only once a commit names it with its cause and records the figure. A commit that changes nothing but those recorded figures is judged by the ladder that measured them: it passes only where every row it changes equals that ladder’s measurement, every gain and rise that ladder reported is recorded, and the branch it merges into still stands where that ladder merged it.

The program generator below asks the converse question every night: whether the optimizer removed the code it could prove dead.

The C beneath every program

Every Mica program stands on a runtime written in C — the allocator, strings, the scheduler, the gradient tape, the tensor kernels — and a defect there would reach every program at once, often without changing a single output. So that C runs under every checker built for the purpose:

• The address sanitizer, on every ladder. The execution corpus, the stress cases included, runs linked against the runtime built under it, so an out-of-bounds access, a use after free, a double free or a leak — in the runtime, in a case’s own C, or in a C library call the sanitizer intercepts — fails its run by the case’s name and the report’s first line; a run the sanitizer cannot judge, such as a fixed arena’s, is skipped with its reason. The runtime announces every switch between task and generator stacks to the sanitizer, so tasks, generators and streams run under it as cleanly as the rest.
• The undefined-behaviour sanitizer, on every ladder. The cases that walk the runtime’s deepest C — the gradient tape, the tensor kernels, the wide integers, the allocator, strings, regions and reclaim — are linked against the runtime built under it on both architectures, and a report fails its run with the C file and line it names. The defects it holds, such as a kernel handed a misaligned pointer or a signed overflow in a limb, change no output on either architecture, so no other gate would see them.
• valgrind, in the memory-checker arm above: every program of the heap, ownership, strings, descriptors, generators, tasks, streams and signals, at every tier and memory class, with every leak counted.
• The thread sanitizer, on every ladder. The task, process, stream and generator cases run on the multicore runtime, linked against the runtime built under it, so a data race in the runtime’s C or in a case’s own C fails its run with both accesses named; a run the sanitizer cannot judge is skipped with its reason. In the multicore arm’s stress drivers above, every concurrent part of the runtime runs under it on one, two and eight carriers.

The same sanitized runtimes ship as an optional package, so a program of yours links under any of them with --sanitize address, --sanitize undefined or, for a multicore program, --sanitize thread; sanitized builds says what that links and what it needs.

These tools watch the C. The checks Mica places in your own code — bounds, overflow, released cells — are the checked tier’s, listed trap by trap in the traps reference, and many of the corpus’s cases run at that tier beside the others.

Every night: programs no person wrote

A corpus holds the programs people thought of. Every night, a program generator writes programs nobody did and judges each one with the compiler’s own builds as oracles, on the release branch being built, so a defect a merge brought in is a bug report the next morning, with the smallest program that shows it.

Valid by construction. Each program grows from a seed into a model — types, variables, routines, statements, expressions — that one printer writes as Mica and one interpreter runs, so the trace the program must print is known before any compiler sees it. Every program is valid and free of undefined behaviour by construction: each expression carries the range its value lies in, a divisor never reaches zero, a shift stays inside its width, every real is a multiple of a power of two small enough that no operation rounds, and every heap cell is released exactly once on every path. So every difference between two builds is a defect. A seed names the same program on every machine, which is what makes every report repeatable, and each night judges a fixed count of the seeds its date names, which no other night judges.

The families. A program draws a few shape families, so it stays small enough to read while the families meet each other across the seeds: arithmetic over integers, reals and texts; records and arrays; cases and loops; heap cells, cells declared in loop bodies, containers and lists; addresses lent to routines; failures and their handlers; generators, tasks, streams and processes, among them tasks placed on worker processes, streams several producers feed, streams of descriptors a worker process fills, selects whose trace no scheduling order can change, failing tasks that cancel their siblings, blocks under a deadline, leaves that cross a live block, and records handed to a task that their owner then overwrites; loops inside on lost and on fail sections; deferred statements, among them a deferred loop over a generator that fails, and nested routines; integers of every width, signed and unsigned; constant tables, truth tables and arrays indexed by letters; conversions into subranges, enumerations and the other ranged types at and past their edges; generic functions, and generic routines that declare maps of their own; heapless routines that call the library; results clamped at a join; eight- and sixteen-bit results that wrap; keeper records whose borrowed fields view a lent cell; assertions over a cell their routine holds; and dead branches. Many families carry exactly the shapes behind defects that were fixed, so a fix that missed a road shows on a later night.

What every program is held to. Each program is built at the debug tier, at O1 and O2, and at the checked tier, for both architectures, and every build must print exactly the trace the model computed and exit cleanly. Builds that disagree are a difference; a trace every build agrees on that the model does not is a finding too, because every tier can agree on a wrong value, and only an oracle that knows what the program means sees that. Where a program lets an eight- or sixteen-bit result pass the end of its type, every build but the checked one must wrap it as the language defines, and the checked build must stop at the first such operation with the failure’s reason and the operation’s own line and column — the traps the traps reference lists.

Under the sanitizers. The debug build then runs once more on the machine’s own architecture under each of three sanitizers watching the runtime beneath it — the thread sanitizer, on the multicore runtime with a pool of a few carriers, the address sanitizer and the undefined-behaviour checks — and owes the same trace with no report. A report is a finding signed by its sanitizer, the error it names and the first place it names, so one defect files one report whichever program met it.

Ownership, both ways. The debug and the checked build of every program run under valgrind with every leak counted: a valid program that leaks, releases twice or touches released memory shows a hole in the ownership checks, and a valid program the checks refuse shows a false refusal. Each program also carries variants: the same program with exactly one violation of an ownership rule written in — a second release, a use after release, a leak, a use after a hand-over, a cell held across a suspension point, a keeper’s lent cell released by another name, an assertion that hands its cell away, a deferred statement that emits or passes a failure on — each kept only where the model’s own run meets the violation. A variant the compiler accepts is a finding. The variants carry on, every night, the adversarial sweep of 283 programs written to be wrongly accepted, which found 41 defects, every one now a refusal that names its rule.

Code the optimizer should have removed. Every program also plants dead branches: a branch the model proves can never run — a text assigned a literal and tested for emptiness right after, a loop’s index tested against the loop’s own bounds, a remainder against its divisor, an unsigned value below zero — whose one statement calls a marker routine the compiler cannot see into. An O1 or O2 build whose assembly still calls a marker kept code it could have proved dead. That is a finding, grouped by the proof the branch rests on, so one missed simplification is one report whatever program showed it.

Shrinking. A finding’s program is cut down to the smallest program that keeps the same finding: whole routines first, then statements in halving chunks, then expressions down to one of their operands or to a literal of their own type. Every candidate meets the interpreter first and then the builds the finding concerns, so the smaller program shows the same defect and not another.

A second source. Beside the generator’s programs, an expander takes the corpus’s own execution cases, whose expected output a person checked, and places each case’s body into contexts where its output cannot change — a procedure, a function, a procedure holding the body’s variables as its locals, a routine nested inside another, a loop that runs once — then holds every expanded program to the case’s expected output at every tier on both architectures. Each case is judged in every setting its own runs state — its memory class, its tasking flavor and carriers, its stack request and its string encoding. A context applies only where the language’s rules keep the output, and a self-check proves every context on probe programs before any case is judged.

One report per defect. Each finding group is filed as a bug report against the release being built, with its smallest program, the output it owes and the command that judges it again. A signature on every report keeps the same defect from being filed twice: a group whose shrunk program a report already carries is not filed again, and one whose kind an open report carries waits until that report is closed.

The GPU, on real cards

The corpus’s device cases execute only where a card answers, so every release runs them, and the GPU probe beside them, on an RTX 4090 with its host before it ships. They run from the release candidate’s own packages, the files a user installs, and a release with one of them failing does not ship. A change that reaches the device road runs them by hand on the card as well, before it merges.

In the device cases every exactly rounded operation is held to the processor’s bits in both widths, Exp, Ln and Tanh to NVIDIA’s documented bounds, every product to a float64 reference within a stated bound, and every reverse rule of the device tape to the processor’s gradients within a bound. The GPU probe trains the GPT’s device twin twice at full scale on the card, and the two runs must leave the same learned weights byte for byte.

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 real programs are compiled, linked and executed from it, the Dragon SDK’s C consumer among them, and one is linked for the other architecture and run under its emulator. A program that places a tensor on the GPU is compiled and linked from it too, against the packaged device floor, which opens NVIDIA’s libraries as the program first needs them, so the link succeeds on every machine. 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. Before this site links a new release, every package its download manifest names is downloaded the way a stranger downloads it, with no credential at all, and must match the checksums its release published; every rehearsal of a release asks the same of every package the live site offers.

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: 10 gates run the real tools and assert what they leave behind — 38 provisioning cases on fresh containers, 53 cases against a faked cloud command line that records every call, the ready report a new machine gives, the development container’s configuration reproduced as the editor reads it, every script parsed under the shell macOS ships, every help table held to one layout, every generated first-boot document parsed as the cloud reads it, the machine search held against a recorded catalogue, and 16 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 compiler’s own ladder rebuilds every example, benchmark and library of the repository with each compiler it makes.
• 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; 305 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. The words the editor highlights are the compiler’s: every context-sensitive word the compiler declares reaches the editor’s grammar, or stays out with its reason written beside it.
• This site. Every word that teaches or quotes the compiler is held to it:
  • The learn gate compiles every Mica code block of this site with the release candidate’s compiler, in the release’s dry run, as what its page marks it to be: a whole program, declarations, statements, statements inside the skeleton program the page names, or an excerpt found line by line in the program the page’s own commands build and compiled as that whole program. A block that quotes a compiler message or shows a sketch is marked as shown, with its reason, and never built. A block that does not build as marked, or carries no mark, stops the release by page and line. Every block is also read by the formatter, which names each block that strays from the house layout.
  • Before a release, every learn page is followed the way a reader follows it, in a fresh container of the release candidate’s image on both architectures: its commands run in a terminal, its programs are saved and built, its “Try it” edits are made, every output it shows is held against the run and every compiler message it quotes against the compiler’s own words. A release whose walk failed a step is refused.
  • The grammar pages are generated from the compiler’s one grammar source, and every source of the corpus, the starter repository’s included, is read both by the compiler’s parser and by the grammar alone, which must judge each source alike, use every production, see every refusal the parser can raise and need every lookahead it writes.
  • Every example of the language description is a case that runs on both architectures on every merge, shown with exactly the files it compiles and the output its runs are held to, and the style guide is held to the standard’s own checklist and to the formatter’s rule table.
  • Every figure on the facts page is generated from the repositories at release, every benchmark table is rendered from the run’s own files, and every internal link and anchor of the built site must reach what it names.
• The harness itself carries its own tests, run in the ladder before any build.

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.
• A golden file is written by its script alone. The harness’s update road compares a golden run and never writes it, so a change to a canonical program’s assembly is always a difference someone reads.
• Compile-time constants are computed by a model of their own. The cases that pin what the compiler folds are written from a model of the constant rules, and the ladder holds every checked-in case to what the model writes, byte for byte. The device cases and the cases of the ownership path sweep, every road that releases a cell, are held to their generators the same way on every push.
• 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 checks its own work as it goes. Some checks run in every compile anyone runs: the single-assignment form the optimizer works on is verified when it is built and again after the passes that rewrite it — every value defined once, and before each of its uses on every path; the register assignment is checked against the interference it must respect; the emitter refuses an input with a stage missing; the ownership analysis halts on an operation it has no rule for, and a build that drops its assertions halts where the releases it leaves out are not the ones the analysis read; and every link checks its runtime against the contract above. A broken invariant stops the compile with an internal error rather than writing a program.

More gates run at checkpoints of their own whenever --quality names them, and every compile of every test program names them all: after semantic analysis, on the analyzed syntax tree; after intermediate-code generation, on every instruction, the control flow and every symbol; after placement, on every home a value was given; and after the last optimization, on the machine code itself, as above. 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.

The tables these checks read cannot fall behind the language either. The tables of intrinsic kinds, runtime entries and intermediate operations are held to their vocabularies when the compiler starts, so an entry added without its decision stops every compile at once, and the coverage gate holds every node kind and every operation to the checks that judge it.

Figures as of 2026-11-10, compiler 7.7.7. Gate results from the release ladder of v7.7.7: stress 27,614/0, direct lowering 27,503/0, race 27,503/0, multicore 424/0, C shim 124/0, memory checker 5,871/0, 353 pinned package edges, 50 pinned kernels.