AI wrote my compiler. A mathematical proof checks its work on every build.

Four months ago I published a claim with weak evidence behind it: that how easy a language is for an AI to write correctly depends on the language's design, not on which model you throw at it. The evidence at the time was one toy language that passed all 8 of my test problems — but took 3x longer than Ruby to get there. My working theory was that the gap was just a training-data problem. Put more of this language's code on the internet, and the model would eventually catch up on its own.

That didn't happen. There's barely more Almide code on the public internet today than there was four months ago. And Claude's current models now solve all 20 of my test problems on the first or second try — faster, and in fewer lines, than mature languages with a decade of training data behind them.

Here's what actually changed instead.

The one metric everything answers to

Almide is a language designed to be written by AI agents, and for the last 4.5 months I've barely touched its compiler's source myself. The commit log's Co-Authored-By: Claude trailers tell that story better than I can.

Steering a fleet of stateless agents through a codebase this size needed a policy that survives the fact that none of them remember the last session. The fix was mundane: a file every agent reads before it does anything. Line one of CLAUDE.md:

Every design decision serves one metric: modification survival rate.

Modification Survival Rate (MSR) is not "did the model get it right on the first try." It's: let the model write code, compile it, and if compilation fails, hand it the raw error message and let it retry — up to 3 times. What gets measured is whether the loop converges on working code, not whether the first draft was perfect.

Model writes code → compile
  succeeds → pass
  fails → show raw compiler error → model retries → compile again
    (after 3 failed retries → fail)

That framing — score the retry loop, not the first draft — turned out to be the single highest-leverage decision in this project. It means every syntax choice, every error message, every stdlib function name gets judged by one question: does this help the model recover from being wrong, not just avoid being wrong in the first place.

Cutting syntax down to what has evidence behind it

Once MSR was the metric, syntax debates stopped being taste and became measurable. The first one: should a lambda be written fn(x) => x + 1 or (x) => x + 1? Two characters, and I was sure the shorter one would be easier for a model to get right.

Asking a model which it prefers is useless — models are sycophantic by default and will validate whichever option you hint you like. So I built grammar-lab: the same code-fixing task, run against both syntaxes, scored by whether the output compiles and passes.

https://github.com/almide/almide/tree/develop/research/grammar-lab/

Model	fn-lambda	paren-lambda	p-value
claude-sonnet-4-6	100% (25/25)	100% (25/25)	1.0
claude-haiku-4-5	86% (26/30)	86% (26/30)	1.0

Sonnet hits a ceiling on both — no signal there. Haiku, the weaker model, is where a real difference would show up if one existed. It didn't: identical pass rates, p=1.0, the flattest possible null result. No evidence of a difference means the extra fn characters were pure noise, so I cut them. Frontier models essentially never get syntax wrong on a language they've never seen before — that's not where the failures live.

So where do the failures actually live

There's a clean way to find out, borrowed from someone else's evaluation of a different AI-targeted language: hand a model one cheatsheet, zero other context, and have it implement something nobody writes casually — a red-black tree — from scratch.

I ran the same setup on Almide: Claude Opus, one CHEATSHEET.md file, two problems (a basic calculator and red-black tree insert/delete), five independent runs each, scored by a separate judge model blind to any target answer. All 10 runs eventually finished. Only 2 of the 10 finished clean on the first try. The other 8 all failed at least once — and the failure category was almost perfectly one-sided:

• Syntax errors: 0
• Semantic errors: 0
• Stdlib hallucinations: 9 of 9 first failures

Frontier models essentially never get a new language's grammar wrong. What they get wrong is guessing at a library they've never seen. io.read_line doesn't return a Result, but the model assumed it did and slapped a ! unwrap on it. int.parse is the real function; the model invented int.from_string because that's what half a dozen other languages call it. Plugging the actual gap was almost insultingly simple — 13 lines added to the cheatsheet under "stdin & parsing" and that class of failure stopped.

The second failure mode was different: habits imported wholesale from other languages. OCaml's let ... in and while ... do, !x for boolean negation, an invented .to_upper() method that doesn't exist. This isn't about not knowing Almide's grammar. It's a model averaging across every language it's ever seen and defaulting to the blend. A dedicated detector catches these and returns a diagnostic that says, plainly, "Almide writes this as ___."

Three failure categories, in order of how they get fixed:

1. Stdlib guesses → fixed by writing the real signature down once
2. Cross-language habits → fixed by a detector plus a diagnostic
3. And the one that took the longest to find: the compiler's own advice lying to the model

Error messages are an API, not a paragraph for a human

In most languages, a compile error is prose aimed at a person. In Almide, the thing reading that error is the same model that wrote the code and is about to write the fix, with no human in the loop. That reframes the error message completely: not documentation, but an API response, and like any API response it can be wrong in ways that actively mislead the caller.

One real case: a model wrote let (value, symbol) = pair — value was meant as a throwaway local name. Almide also ships a stdlib module literally named value. The type checker at the time mishandled this destructuring pattern and misdiagnosed value as undefined, then suggested:

error: undefined variable 'value'
  hint: Add `import value`   ← wrong

The model dutifully added the import and dug itself in deeper. The error didn't just fail to help; it actively lied, and the model trusted it. The fix was to exclude common local-variable names like value and error from the import-suggestion heuristic. Diagnostics that actively steer a model into a worse state go on a running list and get closed out one at a time.

The reference point here is Elm, well known for treating compiler errors as a conversation rather than a verdict:

https://elm-lang.org/news/compiler-errors-for-humans

Almide pushes that a step further by swapping the other side of the conversation from a human to a model. A current diagnostic looks like this:

error[E001]: type mismatch in fn 'sum_digits': expected Int but got Unit
  --> unit_leak.almd:2:25
  in fn 'sum_digits'
  here: let abs_n = int.abs(n)
  hint: Fix the expression type or change the expected type
  try:
      // fn body ends with `let abs_n = ...` (a statement, returns Unit).
      // Add `abs_n` as the trailing expression so the fn returns Int:
      //
      //   let abs_n = <computation>
      //   abs_n                         // <-- add this line

error[E001] is one of 31 error codes, each shipped with its own docs and a repro test. CI rejects a new diagnostic code that lacks either. try: is not a filled-in template; it's a paste-able fix specific to that exact failure. "Type mismatch" is a verdict; "add abs_n on the next line" is an instruction a model can execute without reasoning about it further, and that's the part that actually moves the retry loop forward.

The docs behind each code aren't hosted anywhere external:

almide explain E010

returns the full writeup (common causes, a real diagnostic sample, fix options) straight from the compiler binary. Two reasons for that: a language this new has no Stack Overflow answers to fall back on, and the docs can never drift out of sync with the compiler that's running, because they ship in the same binary.

The next question follows naturally: if try: is literally paste-able code, why is a model pasting it at all?

almide fix app.almd

applies deterministic fixes directly, for the four categories that have exactly one correct rewrite regardless of context:

• Missing imports (json, fs, etc.): added automatically
• Hallucinated comparison functions (int.gt(n, 0)): rewritten to the real operator (n > 0)
• Stray OCaml let ... in: the trailing in is stripped
• Redundant return: removed, since Almide uses trailing-expression returns

almide fix --json emits a machine-readable report, meant to be consumed by an agent's own retry loop rather than read by a person:

Compile fails → almide fix applies deterministic rewrites → recheck
  clean → no model needed
  errors remain → only judgment-requiring fixes reach the model

Every deterministic fix almide fix applies is one fewer round trip through a model, one fewer chance to introduce a new mistake while fixing the old one.

Measuring the effect daily, on purpose-picked weak models

Fixing a diagnostic and feeling like it helped are different things. Almide Dojo is the daily instrument that closes that gap:

https://github.com/almide/almide-dojo

• 31 problems, fizzbuzz through red-black tree, ranked by difficulty
• A GitHub Actions job runs all 31 daily against two models
• Compile failures get up to 3 retries with the raw diagnostic shown
• Results land in a dated commit every day

The models are deliberately not Claude. Dojo runs two Llama models via Cloudflare Workers AI: 3.3 70B and a considerably smaller 3.1 8B. Cost is half the reason. The other half: instrument sensitivity. Claude scored 29/30 the day Dojo launched, and a model pinned at the ceiling can't show you whether a fix moved anything. The same logic that put Haiku in grammar-lab put Llama in Dojo.

Running both sizes side by side surfaces something a single model wouldn't:

• 70B: 16/31 correct on the first try, climbing to 22/31 once retries are allowed.
• 8B: stuck at 10/31 on the first try — and stays there. 21 failed problems × 3 retries = 63 additional attempts, and not one of them converges.

The gap between those two numbers is exactly "can this model read an error and move toward the fix," isolated from everything else. That's why the dashboard's headline metric isn't first-try accuracy: it's the percentage solved within 3 tries. First-try accuracy measures the model. This measures the compiler's side of the conversation.

The dashboard's other load-bearing number is a ranking of which diagnostic codes still block a model after all 3 retries are burned. That ranking is the backlog — it says, directly, which parts of the compiler still need work, ranked by how often they defeat the retry loop.

Daily 12:00 UTC: models solve 31 problems
  → failures logged
  → turned into diagnostic / stdlib fix candidates
  → compiler patched
  → (next day) models solve 31 problems again

Neither Llama model has changed in months. The pass rate has. That's the whole point of running it daily against static models — any movement in the numbers is attributable to the language, not the AI.

Deleting syntax is the hardest call, and the right one

Almide v0.1.0 used a single keyword, do, for two unrelated jobs: wrapping loop bodies and wrapping effect-fn bodies. One keyword, two meanings — exactly the kind of ambiguity that makes a model hesitate mid-generation and produces inconsistent output. I wrote the removal plan one afternoon and rewrote all 66 do blocks in the repo to while/guard that same night.

I considered a deprecation period with warnings first. I didn't do it — a language that hasn't hit 1.0 doesn't owe anyone a migration window, and every day do stays half-valid is another day a model can generate it. Write do in Almide today and the compiler returns exactly one line:

`do` blocks have been removed — use `while` for loops or remove `do` from effect fn bodies

No fallback, no soft warning. Just a sign pointing at what to write instead.

What was actually being optimized for

Stack these up and the conclusion is uncomfortable at first: trying to make a model never make a mistake is the wrong target. Model output is sampled from a distribution, and some rate of mistakes is a property of how the thing works, not a bug to be patched away. What's actually achievable is three things, and none of them are about making the model smarter:

1. Cut the number of ways to write the same thing. Every syntax choice removed is one fewer place a model can hesitate and diverge. Deleting do wasn't cleanup; it was this principle applied directly.
2. Force every remaining mistake to fail loudly. The dangerous failure doesn't look like a compile error. It looks like code that runs and returns a subtly wrong answer without complaint. Every design choice here is aimed at converting silent wrong-answers into diagnostics that stop the build.
3. Pave the road back from a loud failure to correct code. hint, try, almide explain, almide fix: with all four in place, the 3-retry loop from MSR usually finds its way home. In practice, that's close enough to first-try correctness to matter just as much.

The name of the metric was the answer the whole time. Modification Survival Rate doesn't ask whether the first draft was right. It asks whether the loop, wrong, then corrected, then right, closes. Every decision in this section was aimed at making that loop shorter and more reliable, not at making the first draft perfect.

Running a fleet of agents that don't remember each other

None of this works without a way to run many agents against one codebase without it collapsing into chaos. The starting constraint is structural, not motivational: an agent's memory resets completely between sessions. The next one called doesn't know the last one existed, let alone what it learned. Policy can't live in a conversation — it has to live in a file that gets re-read every single time.

That's what CLAUDE.md actually is. Every real incident, a rejected diff, an agent taking a shortcut that broke something two files away, gets written into that file the moment it happens, not speculatively in advance. The file only grows from things that actually happened.

What that leaves me doing is closer to grading than writing. I set direction, judge diffs, and reject the ones that don't hold up. The one thing I haven't figured out how to externalize is the actual judgment call on any given diff — that still lives only in my head, and I don't have a good story yet for writing it down the way everything else got written down.

Working at this pace needed the codebase itself to be partitioned, not just the policy. The compiler is split into 15 Rust crates, wired like this (trimmed to the crates that matter most; the full graph has more edges than fit legibly in one diagram):

almide-base (symbols, spans, diagnostics)      → almide-syntax, almide-types
almide-syntax (lexer, parser, AST)             → almide-lang
almide-types (type checking, unification)      → almide-lang
almide-lang                                    → almide-ir
almide-ir                                      → almide-frontend, almide-optimize, almide-codegen (~89k lines)
almide-frontend (typecheck, lowering)          → almide-mir (~68k lines), almide-interp
almide-optimize (DCE, optimization passes)     → almide-mir
almide-codegen, almide-mir, almide-interp      → almide CLI

The payoff isn't organizational tidiness for its own sake:

• A crate boundary is a context boundary. "Fix the type checker" scopes an agent to one crate instead of the entire tree — and a narrower context window means fewer opportunities to wander.
• A crate boundary is also an API boundary. A change that reaches across crates shows up immediately in the diff as a change to a public function signature — exactly the kind of thing a reviewer catches at a glance, and exactly the kind of thing that's invisible in a single-crate diff.
• Untouched crates skip the rebuild. At this commit velocity, incremental build time is the actual throughput ceiling, not agent availability.

Code doesn't stay healthy on its own just because tests pass

Splitting the tree into crates doesn't stop entropy from accumulating inside each one. Every day, this compiler tells someone else's code "this is wrong" — a reasonable question is whether the code doing the telling is itself in good shape.

There's a structural reason to expect it isn't. Told to "make it work," an agent takes the fastest path to green, and the fastest path is almost always appending to whatever function is already large rather than restructuring it. Each individual diff passes review — a diff-scoped review can only ever judge one commit at a time, and one commit's worth of "append here" always looks reasonable in isolation. Compound that decision at agent velocity for months and the aggregate outcome is a codebase nobody designed, arrived at without anybody making a single obviously wrong decision.

I built codopsy, a static AST-based code quality scorer, originally for TypeScript/JS, now extended to Rust and to Almide's own .almd files, to check whether that was actually happening here.

A-F score =
  complexity (35%, branching & nesting)
  + rule violations (40%, 174 lint rules)
  + structure (25%, file size, function density)

Complexity counts cyclomatic branches (flag threshold: 10) and weights nesting depth more heavily under cognitive complexity (flag threshold: 15). The same branch two levels deep costs more than the same branch at the top level, because it costs a reader more to hold in their head. Rule violations run against 174 lint rules: too many parameters, excessive nesting, empty functions, abandoned TODOs. Structure checks whether files and functions have grown past reasonable size.

I wasn't guessing that this would be a problem. A 2026 Carnegie Mellon study tracked open-source projects where the first coding tool introduced was an autonomous agent, the Claude Code category, not autocomplete, and measured what happened to the codebase over time.

https://arxiv.org/abs/2601.13597

Initial velocity jumped, as expected. Static-analysis warnings rose ~18%; cognitive complexity rose ~39%. Critically, the quality regression outlasted the velocity gain and didn't fade once the initial burst of speed did.

Whether the same thing was happening to Almide's own compiler was an empirical question, not an assumption. The reason codopsy exists at all isn't to score once and stop; it's a loop: score, surface the worst offenders, have an agent fix them, score again.

Score → worst-offenders list → agent fixes → score again → …

Running that loop for the first time didn't go the way I expected. Splitting an overly complex function just redistributes the complexity into its children, and the worst-offenders list refills almost as fast as it empties. The mistake was setting the goal as "empty the list." That instruction gives an agent an endless game of whack-a-mole. The goal that actually works is stated as a property of the whole system: "no function in the compiler exceeds the complexity threshold," full stop. Not a list to chase, but a state to reach.

Run properly, the aggregate score across the compiler's crates currently sits at 71/100. What's left is concentrated almost entirely in one place: the legacy almide-codegen path, which is slated for wholesale retirement rather than incremental fixing (more on why that path exists at all in the next section).

Can you trust a compiler's output when AI wrote the compiler?

Tests exist, and they pass. But tests only ever cover the cases someone thought to write, and this compiler is being rewritten at agent velocity by multiple models working in parallel — "the tests pass" stops being a satisfying answer to "is this correct" well before you'd like it to.

The answer that held up was mathematical, and it lives in one crate: almide-mir.

Almide actually has two independent code-generation paths. The older one, almide-codegen (~89k lines), works and has years of runtime behind it — but it's code an agent fleet wrote at a pace no human reviewer tracks line-by-line, and retrofitting a mathematical proof onto code that large, written that fast, after the fact isn't realistic.

So instead of proving the existing path, I built a second one from scratch, designed from day one to be checkable: almide-mir (~68k lines).

Type-checked program → lower to MIR → insert Perceus refcount ops
  → emit wasm / native
  → emit a certificate → proven checker verifies the certificate, every build

A type-checked program lowers into MIR — a mid-level IR, the same concept Rust and Swift's compilers both have a version of — gets Perceus memory-management instructions inserted (next section), then splits two ways: one path renders to wasm or native, the other emits a certificate that a separately-proven checker verifies on every single build.

MIR here isn't designed to be pleasant for a human to read. The only design constraint is how cheaply a machine can check it. It started as an opt-in flag; it's now the default path for both wasm and native output.

No garbage collector, no pauses, no proof burden on the writer

Almide programs ship with no garbage collector — nothing walking the heap at runtime looking for what to free. Instead, the compiler does the lifetime analysis statically, at compile time: it determines exactly where a value's last use is, and inserts reference-count increment/decrement instructions directly into the generated code at those points. There's no runtime process; the moment a value's last use passes, its cleanup is already baked into the instruction stream.

The obvious question: Almide's own compiler is written in Rust, so why not just let Rust's ownership system handle this? For the native backend, it does: Almide emits Rust source and hands it to rustc, so Rust's own borrow checker enforces memory safety on that path already. WASM is the problem: Almide emits WASM bytecode directly, bypassing Rust (and LLVM, and Cranelift) entirely, so there's no borrow checker anywhere near that output. Two backends, two different guarantees, unless one memory scheme covers both identically — which is the whole point of everything else in this article.

The answer is Perceus, the scheme behind Koka's memory management: not just refcounting, but refcounting with reuse. Freed memory gets recycled immediately for the next allocation at the same site, instead of round-tripping through an allocator.

Alex Reinking, Ningning Xie, Leonardo de Moura, Daan Leijen — Perceus: Garbage Free Reference Counting with Reuse (PLDI 2021)
https://www.microsoft.com/en-us/research/publication/perceus-garbage-free-reference-counting-with-reuse/

(de Moura is also one of Lean's authors, relevant a few sections down.)

Scheme	When cleanup is decided	Burden on the code's author	Runtime cost
GC	At runtime, whenever the collector runs	Near zero	Runtime pauses; ships a collector
Rust ownership	At compile time	High: the author proves ownership to satisfy the borrow checker	Near zero, no pauses
Perceus	At compile time	Low: the compiler inserts the proof, not the author	Refcount ops only, no pauses

That middle column is the actual reason Perceus won here, and it's specific to this project: the "author" writing Almide's compiler is a fleet of AI agents, and Rust's ownership model requires the author to construct a proof the borrow checker accepts. Perceus gets compile-time determinism without asking the code's author for anything extra: write the code the way you'd write it in any GC'd language, and the compiler inserts the refcounting itself.

Two side benefits, beyond the main one: no GC runtime shipped inside the WASM binary, which matters directly for binary size, and fully deterministic allocation and free ordering for a given input — same program, same input, identical sequence of allocs and frees, every run. That determinism becomes load-bearing two sections from now.

Don't verify the compiler. Verify its answer sheet.

The compiler inserts every refcount increment and decrement automatically — and the code doing that insertion is written by AI agents, not by me. Get one of those insertions wrong and there are exactly two failure modes: one extra +1 leaks memory that's never freed; one extra -1 frees memory still in use, which either corrupts state silently or crashes on the double-free.

The obvious answer is to formally verify the compiler itself. There's real precedent: CompCert, a fully verified C compiler built primarily by Xavier Leroy at INRIA, proves semantic preservation end-to-end using Rocq (formerly Coq).

Xavier Leroy — Formal verification of a realistic compiler (Communications of the ACM, 2009)
https://xavierleroy.org/publi/compcert-CACM.pdf

CompCert's proof holds because a small team spent decades hand-crafting every line to keep it intact. A proof is only valid for the exact code it was proven against. Almide's compiler gets rewritten daily by multiple agents in parallel; prove it today, and the proof is stale by the next commit. CompCert's approach doesn't transfer to a codebase that changes shape every few hours.

So the target of verification flipped: don't trust the compiler. Verify its answer sheet, every time.

Compiler (untrusted) produces:
  - the generated program
  - a certificate (a ledger of memory ops)
Both go to the checker (proven safe in Rocq):
  accept → ship it
  reject → build fails

Every build, the compiler emits a certificate alongside the generated program: one line per heap allocation, a running ledger of +1/-1 entries. A small checker, proven correct once in Rocq, verifies that ledger sums correctly: never goes negative, ends at exactly zero. Same principle as checking balanced parentheses.

The idea predates this project by almost 30 years. It's Proof-Carrying Code (Necula, POPL 1997), originally designed so a machine could verify code arriving from an untrusted network peer without trusting the sender.

George C. Necula — Proof-Carrying Code (POPL 1997)
https://homes.cs.washington.edu/~mernst/teaching/6.893/readings/necula-popl97.pdf

It applies cleanly to a compiler an AI fleet is writing, and it solves the staleness problem CompCert can't dodge: what's proven is one narrow claim, "a ledger the checker accepts is safe." That doesn't change no matter how much the compiler generating those ledgers changes underneath it. The compiler churns daily. The checker doesn't. Prove the part that doesn't move.

I'll admit I expected this to be closer to a formality than a real safety net, a nice proof that would rarely actually catch anything in practice. It caught something on day one: a real memory leak in code that was already shipping. One branch of an error-handling path forgot to free a string. Tests didn't catch it because the program never crashed; it just leaked, silently, forever. On the ledger, it showed up as a single missing entry in the arithmetic.

Proving the rulebook, not just each day's homework

The Rocq-proven checker verifies that a given build's ledger balances. That leaves one question further back: is the Perceus discipline itself actually sound? A ledger balancing correctly, build after build, doesn't establish that following Perceus's own rules, increment here, decrement there, actually keeps memory safe in every case. That's a claim about the rulebook, not about any single day's arithmetic.

That's what Lean is for. Rocq and Lean are the same category of tool: both let a machine verify that a mathematical proof is actually valid. But they're doing different jobs here. Rocq built the small checker that verifies each build's certificate. Lean proves the underlying discipline that certificate is supposed to be following.

https://lean-lang.org/

In Lean, the heap and the reference-counting semantics are defined formally: what "safe" means, expressed as math. Then it's proven as a theorem that every operation Perceus's discipline prescribes preserves that safety invariant.

	What it proves	When it runs
Lean	The Perceus discipline itself is sound	Once, at design time
Rocq-proven checker	Each individual build followed the discipline	Every build

Neither one is sufficient alone. A discipline that's wrong doesn't become right by checking every build against it perfectly. A correct discipline followed by an unchecked compiler doesn't stay correct once a mistake slips through.

Both proofs are wired into something concrete, not just filed away: Almide keeps a contract ledger, a numbered registry of every promise about observable behavior (like "native and wasm output are byte-identical," which shows up later in this article), and every entry is required to point at evidence. That evidence has a tier system:

documented only → tests → fuzzing → exhaustive case coverage → Lean proof
      (weakest evidence)                              (strongest evidence)

A Lean proof sits at the top of that ladder — the one form of evidence in the whole ledger that doesn't need to be re-earned as the code around it changes.

Borrowing from software that isn't allowed to crash

Perceus, Rocq, Lean — three fairly heavyweight tools for a side project. The honest motivation: I want Almide to eventually be usable in mission-critical domains, the kind where "it mostly works" isn't an acceptable answer. My own dev notes from partway through this project read: "Native and wasm output must be byte-identical. No exceptions. If a mismatch bug is found, fix it." I wrote that as a constraint on myself, specifically to close off the easy way out later.

Industries that already answer "how do you trust software that can't fail" have been doing it for decades, independently: automotive has ISO 26262 (2011), medical devices have IEC 62304 (2006), electrical/electronic systems broadly have IEC 61508 (1998), aviation has DO-178C (1982).

Life-critical software quality standards
  - Aviation: DO-178C (1982)
  - Medical devices: IEC 62304 (2006)
  - Electrical/electronic: IEC 61508 (1998)
    - Automotive: ISO 26262 (2011), built on IEC 61508

These aren't ranked by strictness: DO-178C, ISO 26262, and IEC 61508 all demand roughly the same things, independent verification, bidirectional traceability, structural coverage analysis, qualification of the tools used to build the software. IEC 62304 for medical devices is comparatively the lightest of the four.

I picked aviation as the model not because it's the strictest, but because it's the oldest, and because it already has the framework closest to what Almide is actually doing: DO-330, aviation's standard for qualifying the tools used to build safety-critical software, not just the software itself.

https://en.wikipedia.org/wiki/DO-178C

In aviation, flight-control and engine-control software can't fly without documented evidence that it was built to DO-178C. The bar isn't whether it works. It's whether you can prove, on paper, that it was built correctly. Almide isn't seeking DO-178C certification. It's importing the reasoning.

Traceability is the other half: every requirement has to trace forward to the code implementing it and backward to the test verifying it, in both directions, with nothing left dangling. Almide's contract ledger does exactly this — the "native and wasm output match" promise, for instance, links forward to tests, fuzzing, and the Lean proof, and CI checks that both directions of every link actually exist. A promise linked in only one direction is treated as a hard failure.

DO-330 is where this gets genuinely uncanny. Its core principle: a development tool doesn't need to be fully verified itself if there's a mechanism that checks its output every single time.

https://www.faa.gov/documentLibrary/media/Advisory_Circular/AC_20-115D.pdf

That's Proof-Carrying Code, stated in regulatory language instead of research-paper language, decades apart and arrived at independently. Don't trust the compiler; verify what it produces, every time. Same shape, same reasoning.

Showing only the parts that look good isn't honest, so here's the full gap analysis. I broke DO-178C's actual requirements into 6 pillars and scored Almide against each one myself:

Pillar	Requires	Almide today
1. Artifact safety	Memory safety, bounded resource use, type soundness	Met: the Rocq-proven checker (43 theorems, proven once) verifies every build's certificate
2. Object-code fidelity	The actual binary matches the source program's meaning	Partial: proven for wasm output; not yet connected to the native binary
3. Requirements traceability	Bidirectional requirement↔code↔test links, plus structural test coverage	Not met: safety is proven; correctness-tracing isn't built yet
4. Execution environment qualification	The OS/hardware/runtime is itself qualified, with worst-case timing bounds	Not met: wasmtime is unqualified, no WCET analysis exists
5. Certification artifacts & tool qualification	A submittable evidence package plus qualification of the build tools	Not met: the certificate is a technical artifact, not a certification-grade one
6. Regulatory acceptance & track record	Passing audits, plus operational history	Not met: no regulator anywhere has accepted "prove the checker instead of the compiler" as a model yet

Roughly 1.5 of 6 pillars, honestly scored. The half-pillar that's actually hit goes deep, though: 43 proven theorems standing behind a checker that runs on every single build, not a one-off audit.

What's left splits into three kinds. Some of it closes with pure engineering — the roadmap below covers that. Some of it needs an organization, not a proof: a legal entity that can sign certification documents, a long-term support commitment, a relationship with a regulator, funded and qualified engineers on staff. And some of it only resolves with time: operational history in a less-regulated adjacent domain first (drones, small satellites), building a track record the same way every other safety standard eventually did.

Full writeup in the repo

"Can you trust code an AI wrote" reads like a brand-new question. Underneath it is an old one: how do you trust output from a process you don't fully trust. Aviation spent 40 years answering it. There's no reason to solve it again from scratch.

The roadmap for the part that's still missing

Six honestly-scored pillars, 1.5 of them hit, isn't something to leave as a someday-list: that's exactly how good intentions turn into nothing shipping. So the gap got broken into tracked issues:

https://github.com/almide/almide/issues/586

The part that's pure engineering (no regulator, no legal entity, no waiting required) breaks into four stages, each one a prerequisite for the next:

1. Decouple the spec from the compiler's actual behavior. Right now "correct" is defined by whatever the compiler currently does. Grader and gradee are the same thing, which means the bar quietly bends to match implementation quirks instead of holding still. Everything else in this roadmap chains off this one first step; it's the longest dependency path in the graph below. Once a spec exists independently, every clause gets linked bidirectionally to the contract ledger and to tests: an independent spec nobody checks against is just as useless as no spec.

2. Deliberately shrink what gets guaranteed. Measure test coverage on safety-relevant compiler paths against aviation's structural-coverage bar, then carve out a Critical profile: a restricted subset of the language, with a static-memory mode (allocate everything up front, at startup) and codegen with a computable worst-case execution time. Proving the entire language is unrealistic; proving a narrow, explicitly-scoped subset isn't.

3. Make the evidence heavier. Sign an evidence dossier on every release. Offer swapping rustc for Ferrocene (a Rust toolchain already qualified against ISO 26262, IEC 61508, and IEC 62304 by TÜV SÜD) as an option for native codegen.

https://ferrocene.dev/

And extend the Lean proof past the Perceus discipline itself, down into the actual allocator and refcount implementation it currently stops short of.

4. Build one thing end to end. Run a PID controller kernel — the standard baseline control algorithm for embedded systems — through the entire verification stack, start to finish, as a concrete existence proof that the whole pipeline actually connects.

None of that touches the organizational or track-record items: a legal entity able to sign certification documents, an LTS commitment spanning decades, a relationship with an actual regulator, funded engineers, and eventually a public position on a question nobody has answered yet, how do you certify code a machine wrote. Writing code doesn't move any of those forward. They're on the list anyway, because leaving them off would be lying to myself about where the project actually stands.

The critical path through all of it:

Decouple the spec → qualified code generator → operational track record → signable certification package

The last two stages of that chain are honestly beyond what a one-person side project closes alone. Writing them down anyway is what keeps the map accurate about where things actually stand.

Correctness is proven. Does any of this actually run well?

Everything above answers "can the output be trusted." None of it answers "is the output any good," and a language that's only correct is a much smaller claim than a language that's correct and usable. Almide compiles to two independent targets from the same verified MIR: native, and WebAssembly, and the same source program produces both.

Almide source → almide-mir (verified IR)
  → Rust source → rustc → native binary
  → WASM bytecode (emitted directly)

Both outputs come from the same verified MIR before they diverge — the native path additionally goes through Rust and rustc, the WASM path is emitted by hand — so both carry the same strength of correctness guarantee. What follows is about size and speed, not trust.

Native: inherit Rust's toolchain wholesale

The native backend emits Rust source and hands it to rustc. That's a deliberate choice to inherit, rather than reimplement, everything Rust already does well: a world-class optimizer, mature cross-compilation, and a single static binary with no runtime and no external dependencies to install.

That CLI example is a git-clone-style tool with init/add/commit/log subcommands. Built with dead-code elimination and symbol stripping, it comes out to 413 KB, one file. otool -L on the result shows exactly one linked library: macOS's own libSystem. Nothing else. Copy the file, run it.

There's a second-order benefit worth naming: because the intermediate output is readable Rust, a human can actually review whether the compiler did its job correctly, in a way that's impossible when the intermediate form is opaque machine code. It also leaves a real migration path open later: swapping rustc for a qualified toolchain like Ferrocene without touching Almide's own code generation at all, which is exactly the lever mentioned in the DO-178C roadmap above.

WASM: the toolchain floor forced a rewrite

The WASM backend didn't start this way. Early on, it was the same trick one level deeper: Almide's Rust output, cross-compiled to wasm32 instead of native. It worked. It also meant Hello World shipped at hundreds of kilobytes, because it inherited Rust's entire runtime along with it, the allocator, the panic-unwinding machinery, all of it. No amount of dead-code stripping got under that floor; the floor was the Rust runtime itself, not anything specific to the program being compiled.

A dev note from partway through that phase says it plainly: "You can't win the raw WASM binary size fight without a direct backend." The fix that note points at is the only one that actually works: stop going through Rust, LLVM, and Cranelift entirely, and have the compiler emit WASM bytecode by hand.

Memory management reuses the same Perceus scheme from earlier: a bump allocator underneath the reference-counting instructions the compiler inserts. I/O goes through WASI. Nothing else is linked in: no external runtime to install, no separate allocator crate, one self-contained file.

What's actually inside a module today

Reachability-based dead code elimination runs inside the verified renderer itself, before the module gets assembled (not as a separate cleanup pass afterward), stripping every function, import, and data segment the compiled call graph doesn't reach. Debug info keeps function names (so a runtime trap resolves to a real function name instead of <unknown>), while local-variable names get dropped.

Program	Verified (shipped)	+ wasm-opt
Hello World	703 B	548 B
FizzBuzz 1–100	1,722 B	1,092 B
Fibonacci (recursive)	1,370 B	771 B
Closure + indirect call	2,651 B	1,668 B
Variant match + float display	11,857 B	6,946 B

wasm-opt shrinks every one of those further, but it's a separate rewrite that runs outside the certificate the verified renderer produces — it's not something the checker vouches for on its own. It ships as an explicit --wasm-opt flag, backed by a differential test in CI that confirms its output is behaviorally identical to the verified module before any of this is trusted. Leave the flag off, and what ships is the verified renderer's bytes, unmodified.

Does it actually run fast

Four problems from the classic "benchmarks game" suite: nbody (a 1,000,000-step N-body simulation), spectralnorm (n=1000), binarytrees (depth 16), fannkuchredux (n=10). One machine, 5 runs each, median reported, wasm run through wasmtime.

Benchmark	native	wasm	native size	wasm size
nbody	0.035s	0.036s	476 KB	18.3 KB
spectralnorm	0.028s	0.028s	477 KB	16.4 KB
binarytrees	0.207s	0.057s	459 KB	16.9 KB
fannkuchredux	0.181s	0.182s	508 KB	18.9 KB

wasm binaries land 25x to 30x smaller than native across the board. On raw speed, wasm ties native on three of the four and wins outright on binarytrees, by 3.6x. That benchmark is dominated by allocate/free churn, and Perceus's bump allocator is considerably cheaper there than macOS's OS-backed native allocator. Every one of these four programs produces byte-for-byte identical stdout between native and wasm — confirmed by diffing the actual output, not inferred from the timings.

What Almide deliberately isn't taking from the wasm spec

Wasm 3.0 standardized in September 2025 and opened up a wider surface than Almide actually uses. What's more interesting than the subset it does use is what got explicitly turned down, and why: every rejection below traces back to the same constraint, that nothing is allowed to break the byte-identical guarantee between native and WASM output.

Feature	Why it's rejected
GC	A dual linear-memory / wasm-GC backend means paying a parity tax on every builtin twice over. Self-managed refcounting is the actual foundation the byte-identical guarantee stands on; replacing it with host GC means giving that foundation up.
Relaxed SIMD	The spec explicitly permits implementation-defined results. That's a direct conflict with an equivalence guarantee: "implementation-defined" and "byte-identical across runtimes" can't both be true.
Typed function references (call_ref)	Reference types can't live in linear memory. Closures are stored as linear-memory structs plus a table index, structurally incompatible unless the whole memory model moves to GC, which is the item directly above this one.
memory64	Bounds-check cost goes up for no benefit on any program that fits under 4GB, which is effectively all of them.
Multiple memories	A single linear memory is a deliberate choice, kept for iOS Safari compatibility rather than adopted from spec breadth for its own sake.

Past the core spec, the frontier is WASI and the Component Model. Today's WASM output only speaks WASI preview 1: no sockets, no HTTP client. WASI 0.2 is stable now; 0.3, released February 2026, adds native async (future<T>/stream<T>) at the canonical-ABI level. That's the part worth having: an agent loop written in Almide, compiled once, deployable as a Component to wasmtime, a browser, or an edge runtime, receiving a streamed LLM API response through the standard mechanism instead of a bespoke one.

The rollout isn't a single jump. It's staged: a custom almide_host import ABI first (a minimal http.get/http.post surface, no canonical ABI required), then a p1→p2 adapter, then 0.2's synchronous canonical ABI, and only then 0.3 async once the ecosystem around it is less new.

Try it

No install needed — there's a WASM playground in the browser:

https://almide.github.io/playground/

For local use, one line:

curl -fsSL https://raw.githubusercontent.com/almide/almide/main/tools/install.sh | sh

If you'd rather have an agent write Almide for you than learn the syntax yourself (which is the entire point of the language), there's a standalone reference package built for that: almide-agents. It works as a Claude Code skill or as an AGENTS.md for anything that reads one.

https://github.com/almide/almide-agents

Point an agent at it and ask for a working program; the retry loop described in this article is what makes that actually converge instead of stalling.

Every size number in this article is reproducible from the repo:

https://github.com/almide/almide/blob/develop/docs/WASM-OUTPUT.md

This is a solo project — no company behind it, no funding round. The DO-178C gap analysis earlier in this piece is deliberately not flattering, and it's accurate: 1.5 of 6 pillars, honestly. What I don't have a good answer for yet is the organizational half of that gap: nothing here closes it by writing more code, and I'd genuinely like to hear from anyone who's navigated getting a from-scratch verification approach in front of an actual regulator or safety-standard body. That part of the roadmap is still open.

https://github.com/almide/almide