Coverable builds LMAT
Coverable builds LMAT, a programming language restricted enough that a compiler can check everything a program does before it runs.
This site is a tree of 42 nodes. Enable JavaScript to walk it as a program, or read the list below.
uzi@coverable.ai
Everything on this site
- AI can write software faster than anyone can check it. — A language restricted enough that a compiler can check everything a program does before it runs.
- The problem — Generation got faster. Review did not, and that is measured.
- Generation got faster. Review did not. — Measured at scale by people with no stake in our argument.
- Every existing answer checks the work after it exists — Evaluations, sandboxes, review, guardrails. All of them run too late.
- The asymmetry that is the whole company — Post-hoc verification scales with output size. Pre-hoc does not.
- Python and JavaScript are wood — Steel did not win by being stronger. It won by being knowable.
- Who this is for — Where being unable to check the output is the thing that stops the work.
- The ideal client — Regulated, document-heavy, and unable to tolerate a wrong field.
- Who this is not for — A short honest list, because a closed language has real edges.
- Why we started with immigration — The hardest version of the problem, chosen on purpose.
- The language — One property, closure, seen from four sides.
- The checker is total — Model output stops being pass or fail and becomes correctable.
- Determinism by construction — Nondeterminism is not policed by a rule. It is inexpressible.
- Bounded execution — There is no argument in which to ask for another customer’s data.
- Compiled introspection — Everything the platform says about a program is derived, never narrated.
- What a program may reach — The complete list, and it fits on one screen. That is the point.
- Twenty capabilities — Everything a running program is allowed to touch, and its effect.
- Seven importable modules — Calculation libraries with no way out of the process.
- Six external sources — A program names a source. It can never name a web address.
- What the language refuses — Software written in LMAT cannot lie to the person using it.
- A chart’s scale always starts at zero — There is no setting that turns this off.
- Absent and empty are different facts — A field a record does not carry can never draw as zero.
- Nothing is hidden quietly — A search says how many matched out of how many.
- The program computes, the screen displays — No expression of any kind reaches a screen.
- No jargon on any screen — Not minimal jargon. None.
- Rehearse first, confirm anything irreversible — A program says what it would do before it does it.
- No escape hatch — This one is the whole bet.
- Measured — Counted from the repository on 13 September 2026.
- The surface, as counts — 21 primitives, 20 capabilities, 7 modules, 113 findings.
- Every pattern earns its place — Real programs use every one of them. None is dead weight.
- What fourteen real programs declare — Median: 140.5 lines, 3 collections, 9.5 fields, 6 blocks.
- The compiler is large so that programs can be small — We do not claim to compress software. We claim it is written once.
- The evidence — Every figure carries its sample size and its date.
- The hardest document domain we could find — Federal immigration filings, and attorneys on the platform today.
- The author loop, measured three times — 5 of 5 on 2026-08-10. 5 of 5 on 2026-08-20. 5 of 6 on 2026-08-25.
- What holds the boundary — 19 hostile programs against the sandbox on every build.
- Where it goes — The same problem returns, with much worse failure modes.
- When the mistake is a wire transfer — Models are moving from writing code to taking actions.
- lmatfs, the substrate — A virtual filesystem so an agent never touches the host’s disk.
- Who is building it — The problem was found in practice, not on a whiteboard.
- The team — Two founders out of Carnegie Mellon, and the advisors around them.
- Talk to us — We are raising, hiring, and looking for the next domain.
Questions
- What is Coverable?
- Coverable builds LMAT, a restricted programming language a machine can write and a compiler can check before the program runs.
- What is LMAT?
- LMAT is a programming language restricted enough that a compiler resolves every reference a program makes before it runs. What a program can name and what it can touch is finite and declared.
- How is LMAT different from Python or JavaScript?
- Python and JavaScript are general-purpose. Any line can reach the outside world, so you can only observe that a program was safe this time. LMAT makes nondeterminism, the network, the filesystem and ambient authority inexpressible.
- Who is Coverable for?
- Teams that need machine-written software they can check: law firms first, then any domain where an unchecked output is what stops the work. Contact uzi@coverable.ai.
- Does software written in LMAT hide missing data?
- No. A field a record does not carry draws as not recorded, never as blank or zero. A search says how many matched out of how many.
- How do I contact Coverable?
- Email uzi@coverable.ai. Coverable is raising, hiring, and looking for the next domain after immigration law.