LOOM: a language that proves what AI-written code is allowed to do

▶ Try it live (in your browser): https://umbraaeternaa.github.io/loom/play.html Built solo, in the open, from Ukraine 🇺🇦. The problem nobody can scale their way out of AI now writes a large and growing share of the code that runs in the world. The uncomfortable part isn't that the code is often wrong — it's that the same model frequently writes both the code and the tests that check it. When one intelligence authors the solution and the criteria, "it passed" quietly stops meaning "it's safe." The gate becomes foolable. You can make the model bigger, but a bigger model that grades its own homework is still grading its own homework. The honest answer isn't "trust a smarter model." It's: trust only what can be independently proven — and make that proof mechanical, not a matter of hope. That is the whole idea behind LOOM. What LOOM is LOOM is a small, open-source, effect-typed language that acts as a machine-checked trust layer for AI-written code. It doesn't just run code — it proves, at a gate, exactly what the code is allowed to do, before a single line executes. If the code lies about what it does, the compiler refuses it. The slogan is: AI proposes, the compiler disposes. Today it is a research kernel with 385 self-verifying checks, all green — every feature added only with an adversarial test, so the language can only ever get greener. There's a live browser playground where a stranger can paste a program and watch the checker accept or reject it in under a minute. What it can actually do Effect honesty. Every function declares its effects — Pure, IO, Net, Alloc, FFI, Rand. Declared effects must cover what the code actually does; the lie is caught transitively through calls, branches, recursion — not just straight-line code. Capabilities, not ambient power. A foreign call has no ambient authority — un-wrapped, it's refused. A seam is the only thing that grants authority, so (seam (Pure) (ffi untrusted)) makes that code's I/O physically impossible. Reinterpreting h