From Test Suite to Validation System

The line we crossed

A test suite asserts behavior you thought to check. It grows by addition: find a gap, write a test, feel better. Its quiet failure mode is that it measures effort, not coverage of the risk — and it cannot tell you what it has never seen.

A validation system makes four additional claims, and each one is a mechanism, not a feeling:

1. Every claim is tied to evidence — bidirectionally, with no orphan tests and no unbacked claims.
2. Evidence is versioned — “92/92 covered” means nothing without against which corpus, which compiler, which revision.
3. The checker itself is checked — the tool that validates your language is itself a safety-critical artifact.
4. Evidence has tiers — “tested”, “mechanically analyzed”, and “machine-checked proof” are different strengths, and the packaging makes the difference legible.

Two weeks ago we had (1) partially — a claims ledger with 92 manual claims and a lint gate. We had none of (2), (3), or (4). This post is about what building them taught us.

The survey that reframed the problem

We started where you should: what do the people who really certify do? The reading list was CompCert, DO-330, Csmith, Rust's Crater, Alive2, and SPARK — and it was humbling how little of it is about writing more tests.

CompCert carries a machine-checked proof that its output implements its source semantics — and in March 2026 it became the first compiler to earn DO-178C/DO-333/DO-330 certification credits. The lesson was not “write a proof” (we cannot; the cost scales with language size). The lesson was that certification authorities accept tiered evidence — proof credits where proofs exist, requirements-based testing where they do not, packaged per objective.

Alive2 showed the practical middle path: translation validation, run daily on LLVM's own test suite, with a public bug ledger. Automatic verification of optimizations with counterexamples — no proof of the compiler required.

Csmith found bugs in every production C compiler with one method: millions of randomly generated UB-free programs under a differential oracle. CsmithEdge then documented the ceiling: generators that achieve correctness by restricting program shapes bias toward the idiomatic and hide exactly the edge bugs. Keep that sentence in mind; it comes back at the end.

Rust's Crater ships a compiler weekly without silent regressions by building the whole ecosystem under toolchain N and N+1 and diffing. SPARK reframed the language itself: design so the important claims are provable — “absence of runtime errors” as a shipped deliverable.

DO-330 was the surprise. It is not about testing your software at all — it is about qualifying the tools you used, requiring requirements-based tests of the tool, structural coverage of the tool during its own test run, and bidirectional traceability with untraceable tests removed. If your compiler is part of your safety argument, the compiler is a safety-critical artifact and gets audited like one.

We came back with seven ranked adoption items. Here is what each taught.

The seven instruments

1. Byte parity across build profiles

Doctrine already said “profiles are semantics” — the same suite must pass under --release and --debug. But our profile sweep only compared pass/fail. A miscompile that changes printed output while keeping tests green — a float rendered differently, an evaluation order flipped — passed. The GCC torture-test practice is stricter: same source, all optimization levels, byte-comparable behavior. Our parity gate now requires byte-identical transcripts across three profiles for 97 suites. Any diff is a miscompile in the optimization delta, by construction.

Lesson: a pass/fail contract can only see failures the test already asserts. Byte parity sees everything the program prints.

2. A regression net across compiler versions

Three times this campaign, the SDK moved underneath us silently, and each time a different instrument caught it late. Rust solves this with Crater; our version of the same idea diffs the 152 committed per-suite transcripts across SDK versions and gates on verdict flips: a test flipping ok→FAILED is a regression candidate, FAILED→ok is a fix that must cite its ticket, and every unclassified change fails the run. An annotations ledger carries the justifications.

Its first real run found that 29 transcripts had never been committed — two corpus packages had local ignore rules that silently excluded them from version-pinned evidence. A regression net is only as good as what it covers, and it audited itself on day one.

3. Qualifying the tool itself

Nothing measured which parts of the compiler the corpus exercises. Statement-level coverage of the shipped compiler turned out to be impossible — it is self-hosted, and instrumenting the artifact you certify changes the artifact — so we built the honest DO-330 equivalent: coverage over the tool's requirements surface. Every flag and subcommand in --help (59 surfaces) must be exercised by the corpus tooling or carry a written justification. Every warning channel must fire on cue — verified by effect, not by flag acceptance. And a new category of signal we had ignored: IR diversity. An LLVM opcode emitted by exactly one corpus file is a codegen path with zero redundancy; three were pinned, and a new one now fails the report.

This channel earned its keep immediately: one retained-memory warning turns out not to fire on any of the shapes its own manual documents, and one violation diagnostic flags the standard library's own print call as package-private. Both are now ticketed upstream.

Lesson: the certification instinct — audit the tool, not just the artifact — finds real defects even when the textbook instrumentation is unavailable.

4. Volume, and the cost of restriction

Our metamorphic fuzzer ran 60 programs per run. Csmith's method is volume — millions of programs over years — so we scaled to 1,000+ per run with per-program seed pinning, auto-reduction of any divergence (CReduce-style), and a fingerprint ledger that deduplicates findings. A thousand programs now take 6.6 minutes and run green.

Then CsmithEdge's warning materialized in our own house. Our safe grammar was built from verified-green cells only — sound by construction, and blind by construction. The complement generator composes the boundary families the escape-analysis grids enumerate — hoisted scratch arrays, factory drops, parameter stores — and uses the analyzer contract itself as the oracle: dump verdicts must be backed by a witness, and runtime memory growth must agree with the verdict.

5. Two-channel evidence, or: how our own tool caught our own tool

Here is the story worth the whole post. The edge-grammar fuzzer's day one suggested that the leak families we had tracked for weeks were fixed — runtime flat at 100k and 1M iterations. We nearly filed that as a win.

The store-grid rebuild said otherwise. We gave every pinned family two legs: the existing dump leg (what the analyzer claims) and a new runtime leg (what the memory does). The true hoisted scratch-array shape leaks 16 B/iter with dump and runtime agreeing. The fuzzer's “fixed” reading was an artifact — its generator had been allocating the scratch array inside the loop, the naive always-free form, not the documented pattern.

So we published the correction ourselves: “the leak is NOT fixed; our measurement was an artifact; here is the generator bug.” And the corrected picture is genuinely useful: for three other tracked families, the leak halves ARE fixed (dead stores elided at codegen) while the analyzer still claims witness-less definite — meaning each ticket splits into a fixed leak half and an open grade half, which is a different defect class with a different fix.

Lesson: one measurement channel is an opinion. Two independent channels that must agree turn divergences into findings and artifacts into corrections. The grid forced us to retract ourselves before anyone else did.

6. Both directions of every contract

A warning channel is not validated by a shape that fires it. It is validated by a shape that fires it and correct code next to it that must stay silent. The warning grid pins 11 trigger cells and 10 silence cells across every warning channel — and the silence cells are the ones that found the false positive. During development, the vacuous-match guard caught two cells passing for the wrong reason (an empty flag made every match trivially true). A checker that cannot fail is not a checker; this one now provably fails both ways.

7. Packaging: the binder and the stamp

The DO-330 insight is that certification is packaging as much as measurement. Two final pieces:

The qualification binder: 20 objectives, each mapped to evidence with an explicit tier — PROOF (machine-checked), ANALYSIS (mechanical instrument over artifacts), TEST (executed assertions). One page answers “what is proved vs analyzed vs tested,” and an objective whose evidence did not run renders red — an unrun gate is worth zero.

The provenance stamp: every report now carries {plan revision × SDK version × corpus hash × git rev}, deterministic and field-isolated. A report without the stamp is not evidence, and neither is an unversioned claim. The regression diff consumes the stamp to auto-pair snapshots across SDK bumps.

The lessons, stated plainly

“Production ready” decomposes into evidence, and evidence decomposes into tiers. Testing shows the absence of the bugs you thought of. Analysis extends coverage mechanically. Proof closes domains completely. None of them subsumes another; a certification that does not say which tier backs each claim is selling a mixture as purity.

The tool is part of the surface. Every defect the warning grid and surface-coverage instruments found was a compiler defect, not a corpus gap. Teams qualify their test suites and never audit the compiler consuming them — DO-330 exists because that instinct is backwards.

Restriction has a price, and you pay it invisibly. Every safe grammar is also a blind spot. CsmithEdge warned it; four days later our own fuzzer proved it by misreading a tracked leak family's status for exactly the reason the paper predicts. Build the complementary, unsafe-ish generator on purpose, with a different oracle.

One channel is an opinion. Dump verdicts and runtime memory are independent witnesses. Where they agree, you have a fact. Where they diverge, you have a finding — and the divergence class tells you what kind: claim-vs-codegen disagreement is worse than imprecision.

Corrections are a competency. The best thing our instruments did this fortnight was force us to publicly retract our own result before anyone else did. A validation system that cannot embarrass its authors is not measuring.

Silence must be tested. Every false positive we found was a missing silence contract. Trigger-only testing inflates confidence in channels that are simultaneously deaf (miss real triggers) and noisy (cry wolf on correct code).

And the honest boundary stays. Statement-level coverage of the compiler is still impossible without an instrumented build. Shape depth on the big SDK packages is still the weakest tier. The formal kernels cover numeric domains and memory lifetimes, not the full language. Certification is a staircase, and the boundary you can state is worth more than a ceiling you can only hope for.

What we would tell a team starting tomorrow

1. Inventory your claims and tie each to evidence both directions, enforced by a gate, not a convention.
2. Stamp every artifact with {what, against what, when} or accept that none of it is evidence.
3. Add one differential channel you do not control (another compiler, another profile, another version) — it is worth more than another thousand self-consistent tests.
4. Give every pinned expectation two legs if you can — a claim and a consequence — and treat disagreement as the most valuable signal you own.
5. Audit the tool. Then audit the audit. Both will find something.

The full survey with sources, the instrument contracts, and the acceptance evidence behind every objective live with the project's verification tooling. The staircase continues.