How Do You Certify a Young Language to Be Production Ready?

There is a sentence every language author eventually has to face, usually from the person deciding whether their team will bet on it:

How do I know this thing is production ready?

For a language with ten years of production history, the answer is easy and cheap: point at the users. Postgres has thirty years of production scars. Java has twenty-five years of trading systems that did not fall over. The scars are the certification.

A young language has no scars. Worse, if you are building a language for an AI agent to write most of your code in — which is the premise SuperJ was designed around — you cannot even lean on “my senior engineers will review it.” The reviewer is also the machine. The scars have to be earned before the code ships, by construction, not after incidents.

This post is the answer we arrived at after a month of building exactly such a certification. It is not a story about intuition or vibes. It is a report of a measurement campaign with a number at the end — and it comes with the honest boundary of what such a certification cannot say, because the boundary is the part most language claims quietly skip. It ends with the audit we ran on our own certification, because a checker that cannot fail is not a checker, and we found five ways ours quietly couldn't.

The premise: “production ready” must decompose

“Production ready” is not one property. It is at least four, and they are tested differently:

1. The language does what its manual says — semantics match the spec.
2. The SDK does what its signatures say — every public API behaves.
3. The compiler emits code that preserves the source's meaning — the optimization pipeline does not corrupt programs.
4. The memory model guarantees what it promises — no silent leaks, deterministic reclamation.

Each of these needs a different verification technology. A test suite checks (1) and (2) for the cases you thought of. A formal proof checks them for all cases — but only for the properties that are decidable. A differential harness checks (3) against a reference. A measurement instrument checks (4). A certification is the discipline of refusing to conflate them, and refusing to claim any of them beyond what its technology can actually see.

The tooling described below took about two weeks of work. What it produced is a report with 2,644 checks across 43 categories, of which every claim is either machine-checked, measured with a stated precision, or explicitly marked not provable. The zero on the last category — nothing unaccounted — is the actual product.

Layer 1: The conformance ledger — the JCK idea, adapted

Java has the JCK: a conformance kit where every normative statement in the specification gets a conformance test, positive and negative. The JCK's pass is the industry's definition of “Java is working as expected.” A young language has no industry, so nobody will build a JCK for you — which is convenient, because you can build a better one: a JCK for your own manual, checked by the same discipline you'd demand of someone else's language.

The structure is simple. Parse the manual into discrete, numbered claims. Every claim gets at least one test. A linter fails the build if any claim has no covering test.

{
  "id": "I002",
  "sec": "identical-to-java",
  "topic": "Control flow",
  "text": "if/else, for, while, do-while, break/continue..."
}

For SuperJ's manual that produced 92 claims in four classes — identical to Java, removed from Java, changed from Java, new in SuperJ. The classification is the interesting part. “Identical to Java” claims are cheap to verify — the JLS oracle exists. “New in SuperJ” claims are the expensive ones, because the only oracle is the manual's own prose — which means the prose has to be normative enough to test against, and the test has to be inverted (run to red) before it counts.

Every claim then gets a provability tier in the ledger:

• A — formally proved. A machine-checked proof covers it.
• B/C — provable, with a proof shape — differential grid, exhaustive small domain, state machine.
• D — descriptive. An environment variable's documentation, a table header, a package listing. Not language semantics; stays in the test tier, and that is fine.

The final count after the campaign: 77 of 92 claims formally proved, zero unassessed, 12 explicitly descriptive, 3 pinned as divergence cells. The divergence cells are the part a marketing page would hide and a certification must show: places where the compiler disagrees with the manual, ticketed with red tests that fail until the compiler catches up. A certification without visible red cells would be lying by omission.

Layer 2: Full-domain proofs — where “works on all inputs” becomes a theorem

Testing samples. For integers, “sampled” and “exhaustive” are the same thing only if your domain is small. For a 32-bit integer, the domain is 2³² — you cannot sample your way to certainty, but z3 can prove it. The trick is to state the language's arithmetic laws as SMT queries over the entire domain:

law('wraparound involution (a+b)-b == a', (a + b) - b != a)
law('overflow rule: INT_MIN / -1 == INT_MIN (JLS 15.17.2)', ...)

unsat over the full bitvector domain means: no counterexample exists among all 4,294,967,296 inputs. Not “we tested a lot of inputs” — the law is a theorem. The numeric kernel that got this treatment:

Domain	Theorems	What “full domain” means
int32	10 laws	all 232 pairs
long, i128, i256, i512	36 laws	all 264…2512 values
float/double sign algebra	4 laws	all 264 bit patterns, NaNs included
SIMD byte lanes	lane law	all 65,536 (a,b) pairs × 16 lanes

Three engineering notes that made the proofs trustworthy rather than theatrical:

First: the model must be differentially checked against the real compiler. The initial formal model of SuperJ arithmetic lacked the JLS 15.17.2 overflow rule that the real compiler correctly implemented — the differential caught it. The language was right, the model was wrong. Without the 1,124-cell compiler-vs-model grid, the proofs would have been proving the wrong thing, beautifully.

Second: know z3's semantics better than you trust them. z3's % is bvsmod — floored division, sign following the divisor. Java's % is irem, sign following the dividend. A naive “verified matching law” produces a false counterexample that looks like a compiler bug and wastes a day. The fix is definitional: build Java's remainder as a - (a/b)*b and then prove the law.

Third: exhaustiveness is a claim about the encoding, not a vibe. “Proved over all 2³² inputs” is only true if the encoding actually ranges over 2³² inputs. The verifier for your verifier is reading the z3 script, and it is you.

The long question: how do you prove a 2⁶⁴ domain?

This is the moment readers of C certification work (CompCert, the ISO C standard's annexes, the LLVM correctness literature) always ask about the big types. long is 64 bits. Its signed range is −9,223,372,036,854,775,808 … +9,223,372,036,854,775,807. You cannot enumerate that in the lifetime of the universe — 2⁶⁴ iterations at a billion per second is 292 years. Testing cannot even name the boundary cases reliably. So how can anyone claim long arithmetic is mathematically correct?

The answer is the same move CompCert uses, borrowed from hardware verification, and it rests on one observation: the numbers never have to be enumerated — only the rules they obey.

long in SuperJ is defined as a 64-bit two's-complement integer whose behavior is fixed by a small set of laws. Each law is a universally quantified statement — “for all a, b in the domain, this identity holds” — and a law over an infinite-looking domain becomes a finite SMT query because of how z3 encodes it: a 64-bit value is a bit vector of exactly 64 cells, so the solver reasons about the bit structure, not the magnitude. Asking z3 whether (a + b) - b != a can ever hold for 64-bit a, b is asking it to find a counterexample bit pattern; if the solver returns unsat, there is no such pattern — which is a proof over all 2⁶⁴ pairs, delivered in about forty seconds on a laptop.

Concretely, the long kernel carries nine laws in three families:

Ring laws (algebra class, on a finite group): (a+b)-b == a and (a*b)*b⁻¹-style wraparound identities. These prove that wrapping is an involution — add-then-subtract returns exactly where you started, for every pair, including at the boundaries. If a compiler ever “optimizes” an overflow check away incorrectly, this law catches the translation.

Division's edge cases — where Java-derived semantics bite:

LONG_MIN / -1 == LONG_MIN        (JLS 15.17.2, the overflow rule)
x % y has the sign of x, not y   (truncated division, not floored)

The first is the famous case: -9223372036854775808L / -1 should be +9,223,372,036,854,775,808 — which does not exist in the domain — so the spec pins it to LONG_MIN itself. A test suite samples around the boundary; the proof pins the entire lattice: every input pair a / b was checked against the spec formula simultaneously. The second is the one that bites porters from C (floored bvsmod) and from Python (floored %): the sign convention is provable, not assumed — the z3 law states it for all a, all b ≠ 0.

Shift and mask laws: a << (s & 63) never escapes the domain, the shift count mask is 63 (not 127 — that's i128's mask; each width carries its own), and masking is idempotent. Each is a one-line quantified identity.

The scaling is the beautiful part. A 512-bit integer has a domain 2⁵¹² — larger than the number of atoms in the observable universe by a factor you cannot write down. The proof does not care. Bitvector laws are width-independent in statement; only the modulus changes. The i128/i256/i512 proofs are the int32 proofs re-run with a different bit width — 36 theorems, same shape, each still exhaustive over its whole domain. This is the payoff of the SMT approach over testing: the cost of certainty is constant in the domain size. The certification of i512 — a type with more values than anything physical could ever count — is as complete as the certification of byte.

And the anchor to reality stays the differential: every law the solver proves is also checked cell-by-cell against the real compiler on the boundary values the laws are about — LONG_MIN, LONG_MIN + 1, -1, 0, +1, LONG_MAX — because a proof over the model plus a differential against the artifact is what makes “the language is mathematically correct” mean the same thing as “this binary computes mathematically correct answers.”

This is exactly the standard the C world aspires to with its formal semantics work (the CompCert kernel, Cerberus's ISO C11 semantics) — small, machine-checked laws over precisely-stated domains. The difference is scope and honesty: CompCert proves the compiler preserves semantics; a young language can get the same confidence cheaper by proving the semantics themselves over full domains and differentially checking the artifact against the model. It is certification at the same mathematical standard, scoped to what a young language can actually sustain.

Layer 3: The compiler itself — translation validation

You cannot prove a closed-source compiler the way CompCert proves its kernel. What you can do is translation validation: prove, per function, that the compiler's output preserves the properties you care about. The SuperJ test corpus compiles to LLVM IR, and every one of the 3,528 emitted functions across 124 files now carries:

• No silent undefined behavior. A symbolic walk from each function's entry block must never reach unreachable except under a dominating no-return call. Dead IR from finally outlining is exempt; constant branches (br i1 1) take only the live edge.
• Bounds guards. Every user array access with a non-constant index is dominated by an explicit check. Constant-folded indices, rodata, and compiler-generated dispatch walks are exempt — with the reason recorded, not hand-waved.
• CFG totality. Every block terminates; every branch target exists.
• Profile equivalence. 89 programs × {debug, release, AVX2} — stdout and exit code byte-identical. The optimizer pipeline is certified on the corpus, not trusted.
• Numeric refinement. 40 generated programs where the formal model independently computes the expected output; model, debug build, and release build agree byte-for-byte.

The honest boundary: this is translation validation, not compiler verification. It checks the compiler's output, not the compiler. The completeness limit is the corpus — which is exactly why the next step, proposed as an upstream ticket, is running the validator inside superj test, so every future test build is validated as it is built and the corpus becomes a moving frontier instead of a snapshot.

Layer 4: Garbage-freedom — the certification a no-GC language owes you

In Java, “does it leak” has a lawyer's answer: the GC will collect it. In SuperJ there is no collector, so the question is existential — and the manual answers it honestly: a leak is memory the program keeps alive that its author did not intend to keep alive, and the one shape the language permits without warning is a deliberately-kept global-arena reference. That definition makes leak-freeness partially a statement about intent — which no tool can prove. So the certification decomposes it into what is provable:

Arena reclamation is a theorem. Every arena {} block drops on every exit path — fall off the end, return, break, continue, throw, labeled break — at any nesting depth, in LIFO order, with drops == creates verified per allocation site. Proved as a pushdown system over the statement grammar, grounded by runtime oracles.

Stack placement safety is a theorem — and its complement is checked. If the compiler says a value dies on the stack, no execution path reads it after death. Stated in z3 over the escape-analysis action algebra, checked UNSAT, with composition soundness (clean callee summaries preserve the verdict). And the theorem's complement is machine-checked too: the witness-completeness pass proves the dump reports exactly the escapes the source exhibits — no false accusations in either direction — over an 18-shape grid that enumerates the action space. (What remains empirical — coverage of unseen syntax — is in the boundary section.)

Flatness is a law with two scales. Run any region at N and 10N iterations. A leak with per-iteration retention r is linear in N and mathematically cannot hide from the ratio test; a genuinely flat region stays at delta 0. This turns the manual's “flat across scale” guideline into a checker with a verdict algebra:

Verdict	Meaning
FLAT	delta 0 at both scales — certified garbage-free
BOUNDED	growth ≤ one 4 MiB chunk — table pre-sizing, by design
LINEAR-RETENTION	scales with N — a leak at a measured rate
INTENTIONAL	documented cost (exception objects: 80 B/throw)

And then: the SDK, method by method. All 2,910 public API methods were enumerated from the SDK stubs, synthesized into flatness probes, compiled, and run at two scales:

Verdict	Count	Meaning
FLAT	1,799	certified garbage-free in canonical shape
BOUNDED	207	growth within one chunk (table sizing)
CARVEOUT	527	flat only in reuse shapes — one systemic cause, ticketed
NEEDS-FIXTURE	52	requires live objects (fixtures, callbacks)
SIDE-EFFECT	541	network/proc/gpu — wrapper-level check

Every one of the 3,126 accounted methods has exactly one verdict in a ledger, and the reconciliation guarantees zero unmeasured. Two real defects fell out of this campaign alone: an SDK carve-out that leaks ~126 B/iteration even inside an arena block (#4790), and — the one that made the whole exercise feel alive — a CRITICAL SIGSEGV: HttpClient.request with null arguments crashes the runtime with a raw segfault instead of throwing NullPointerException (#4814). You do not find that with examples. You find it by refusing to let any method be unaccounted for.

The part certifications usually skip: what we chose NOT to prove

Every claim above came with a boundary, and the boundaries were written down before the results were:

• Escape analysis: the safety property is proved; the catches-everything property is the part that stays empirical. The distinction matters, so here it is in full. What is machine-checked: (a) the safety theorem — every allocation graded -> STACK is only read within its allocating frame, stated over the 5-action summary algebra {return, store-to-static, store-to-array, store-to-global, native-barrier} with composition soundness (a clean callee summary preserves the verdict); (b) witness two-sidedness — every escape the source witnesses appears as non-STACK in the dump, and every non-STACK dump verdict corresponds to a source witness (no false accusations), verified over an 18-shape grid that enumerates the action space; (c) arena reclamation totality — every block drops on every exit path, drops == creates, as a pushdown-system proof. What stays empirical: shape-space completeness — whether the analyzer's inference covers every syntactic way a program can express an escape. The 18 shapes enumerate the action space; a novel syntactic form that both the structural parser and the analyzer miss would be invisible to both, agreeing with each other and both wrong. #4744 (a dead-branch promotion) is exactly this class: a dump verdict that source reasoning says should be STACK. That is why the red cell stays red: not because the safety theorem is weak, but because completeness against unseen syntax is bounded by enumeration, and the boundary is enforced by tickets, not by faith.

• The checker is code too. The translation validator is ~600 lines of Python. Its own soundness rests on LLVM text parsing, which bit us four times (multi-line switch terminators, !dbg metadata, SSA temp reuse, constant branches). Every bite became a test.

• A “certification” without an assessor is a claim. ISO-style conformity assessment needs a third party. What we built is the evidence base that makes such an assessment assessable.

• Two live divergences from javac in definite-assignment and reachability — filed, pinned red, and the formal model deliberately follows the JLS so the pins re-fail until the compiler matches.

A certification without a recorded boundary is marketing. The boundary is what makes it auditable.

The audit: five ways our own certification could quietly lie

The uncomfortable question after building all of the above: who checks the checker? We ran a dedicated audit of the certification framework itself — every gate, every exit code, every denominator — and found five defects that are generic to this kind of campaign. Every one of them had the same shape: a check that reported a number but could not fail.

1. Gates that never gated. The spec-tag linter printed “100.0% contract-cited, 92/92 claims covered” — and exited 0 unconditionally. The numbers were real, but the gate was theater: nothing downstream would ever have noticed a regression. Same story in the metamorphic harness: a program whose compile failed was silently dropped from both numerator and denominator, so a generator bug that broke all 60 programs would have printed “0/0, all identical” and passed. Both now hard-fail. The lesson is a rule: a check without a failing exit code is a dashboard, not a gate.

2. Regex blindness — 1,462 of 1,463 tests invisible. The linter's @Test pattern required the annotation, the modifier, and the method name on one line. The corpus's dominant style puts @Test on its own line — exactly one test method in 1,463 matches the single-line form. The “100% cited” number was computed over a denominator of 885 methods when the true count was 1,113 — the linter was certifying tests it could not see. Worse, the citation regex didn't recognize the test plan's own XX-NNN ID format, so // EXC-013: — a perfectly cited contract — counted as untagged. The report's fallback test enumerator had the same one-line assumption. Both now accept the multi-line form. The generic lesson: when a validator claims “all X”, cross-check its denominator against ground truth by a second, mechanical means (here: the suite runner's own .out files, which list every test it actually ran).

3. Coverage regression without an alarm. An SDK update added 40 public methods. Method coverage silently slid from 2,910/2,910 to 2,870/2,910 — 98.6% — while our own project notes still claimed “100% testable on every package.” Nobody noticed for days. The fix is a ratchet: a baseline file pins the covered total, and the report category fails whenever the SDK grows methods the corpus doesn't mention. After covering the 40 (a new probe with happy path, edge, and error case per method: the *Into allocation-free variants, the Bech32 plain-charset pair, listInto's documented -2 on non-directories, WebSocket's direction-aware bindFromClient/bindFromServer with its masking rules), the baseline was bumped and the ratchet re-armed. Absolute percentages lull; deltas catch.

4. Unwired layers — red but invisible. The metamorphic harness, the spec linter, the method-coverage report, and the profile sweep all ran green standalone, but none of them appeared in the HTML report — so on any day one of them went red, the report (the thing a human actually reads) would have kept saying everything passes. All four are now report categories. Likewise the negative-compile matrix (80 cells) was never collected — different output format, so the collector's parser simply found nothing, and “119 cells, PASS” never mentioned the 80 it didn't know existed.

5. Stale pins and stale binaries. Two negative tests were marked expected-to-fail for bugs that had already been fixed upstream — the matrix was running red on “fix landed, flip the pin” with nobody assigned to see it. And the memory sweep discovered two suite binaries whose source had been deleted; they produced no memlog and the sweep's exit code treated “no log” as fine. Pins must flip when tickets close; verdicts must distinguish “passed” from “instrument absent.”

The audit also shrank a claim, which is the healthiest sign: the memory sweep previously reported 113 suites swept; the honest number is 148, because 37 suites in four projects were silently outside its glob. Same code, same tool — the scope was the bug.

What it cost

• 2,644 checks in the final report, 2,643 green. The one red is a ticketed compiler bug we refuse to stop failing.
• 29 validation layers (plus 14 project suite sets), from full-domain SMT theorems to per-method garbage certificates, all wired into one HTML report with drill-downs.
• Roughly two weeks of agentic time, ~40 seconds for the formal category to re-verify from scratch, and one crash ticket that would otherwise have been a production 3 AM.

The pattern, generalized

If you are certifying any system — a language, a database, a protocol stack — the recipe generalizes:

1. Make the spec countable. Every normative sentence becomes a numbered claim. A spec that cannot be enumerated cannot be conformance-tested.
2. Prove what is decidable, exhaustively. Small domains beat samples. Full domains beat small domains. z3 over bitvectors is the cheapest certainty in software engineering.
3. Differential-test everything you model. The model is wrong until the real system agrees with it. The differential is where the language's own bugs surface.
4. Validate the compiler's output, don't trust its input. For a closed-source compiler, translation validation is the only honest technology — and it composes with every future build.
5. Measure the property the runtime can't hide. For a no-GC language, that is the allocation ledger itself. Flatness across scales is the theorem-shaped version of “no leaks.”
6. Write down what you did not prove. The boundary section is the certification's signature. Everything above it is evidence; everything below it is future work with a ticket number.
7. Audit the certification itself — with failing exit codes. Every gate gets a red-path test: what does it print when the thing it guards actually regresses, and does anything fail? Our audit found five silent-pass defects in a framework we had built precisely to avoid silent passes. The meta-layer is not paranoia; it is the same rule one level up.

“Production ready” is not a badge you receive. It is a ledger you can defend — every line backed by a theorem, a measurement, or a ticket that says precisely why it is still red.

The full evidence trail — 21 formal runners, a 2,910-method SDK ledger, a 2,644-check report — is public in the review repository.