# Coverable

> Coverable builds LMAT, a programming language restricted enough that a compiler can check everything a program does before it runs.

The public site is a declaration tree of 42 nodes. Nothing renders that is not named. Read the tree before the marketing page.

Contact: uzi@coverable.ai

## Pages

- [lmat](https://coverable.ai/): 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.
  - [problem](https://coverable.ai/problem): The problem — Generation got faster. Review did not, and that is measured.
    - [review-gap](https://coverable.ai/review-gap): Generation got faster. Review did not. — Measured at scale by people with no stake in our argument.
    - [after-the-fact](https://coverable.ai/after-the-fact): Every existing answer checks the work after it exists — Evaluations, sandboxes, review, guardrails. All of them run too late.
    - [cost-curve](https://coverable.ai/cost-curve): The asymmetry that is the whole company — Post-hoc verification scales with output size. Pre-hoc does not.
    - [wood-and-steel](https://coverable.ai/wood-and-steel): Python and JavaScript are wood — Steel did not win by being stronger. It won by being knowable.
  - [fit](https://coverable.ai/fit): Who this is for — Where being unable to check the output is the thing that stops the work.
    - [ideal-client](https://coverable.ai/ideal-client): The ideal client — Regulated, document-heavy, and unable to tolerate a wrong field.
    - [not-for](https://coverable.ai/not-for): Who this is not for — A short honest list, because a closed language has real edges.
    - [first-domain](https://coverable.ai/first-domain): Why we started with immigration — The hardest version of the problem, chosen on purpose.
  - [language](https://coverable.ai/language): The language — One property, closure, seen from four sides.
    - [total-checker](https://coverable.ai/total-checker): The checker is total — Model output stops being pass or fail and becomes correctable.
    - [determinism](https://coverable.ai/determinism): Determinism by construction — Nondeterminism is not policed by a rule. It is inexpressible.
    - [bounded-execution](https://coverable.ai/bounded-execution): Bounded execution — There is no argument in which to ask for another customer’s data.
    - [compiled-introspection](https://coverable.ai/compiled-introspection): Compiled introspection — Everything the platform says about a program is derived, never narrated.
  - [reach](https://coverable.ai/reach): What a program may reach — The complete list, and it fits on one screen. That is the point.
    - [capabilities](https://coverable.ai/capabilities): Twenty capabilities — Everything a running program is allowed to touch, and its effect.
    - [modules](https://coverable.ai/modules): Seven importable modules — Calculation libraries with no way out of the process.
    - [sources](https://coverable.ai/sources): Six external sources — A program names a source. It can never name a web address.
  - [refuses](https://coverable.ai/refuses): What the language refuses — Software written in LMAT cannot lie to the person using it.
    - [zero-baseline](https://coverable.ai/zero-baseline): A chart’s scale always starts at zero — There is no setting that turns this off.
    - [absent-vs-empty](https://coverable.ai/absent-vs-empty): Absent and empty are different facts — A field a record does not carry can never draw as zero.
    - [nothing-hidden](https://coverable.ai/nothing-hidden): Nothing is hidden quietly — A search says how many matched out of how many.
    - [screen-displays](https://coverable.ai/screen-displays): The program computes, the screen displays — No expression of any kind reaches a screen.
    - [no-jargon](https://coverable.ai/no-jargon): No jargon on any screen — Not minimal jargon. None.
    - [rehearse-first](https://coverable.ai/rehearse-first): Rehearse first, confirm anything irreversible — A program says what it would do before it does it.
    - [no-escape-hatch](https://coverable.ai/no-escape-hatch): No escape hatch — This one is the whole bet.
  - [measured](https://coverable.ai/measured): Measured — Counted from the repository on 13 September 2026.
    - [surface](https://coverable.ai/surface): The surface, as counts — 21 primitives, 20 capabilities, 7 modules, 113 findings.
    - [pattern-usage](https://coverable.ai/pattern-usage): Every pattern earns its place — Real programs use every one of them. None is dead weight.
    - [corpus](https://coverable.ai/corpus): What fourteen real programs declare — Median: 140.5 lines, 3 collections, 9.5 fields, 6 blocks.
    - [compiler-size](https://coverable.ai/compiler-size): The compiler is large so that programs can be small — We do not claim to compress software. We claim it is written once.
  - [evidence](https://coverable.ai/evidence): The evidence — Every figure carries its sample size and its date.
    - [immigration](https://coverable.ai/immigration): The hardest document domain we could find — Federal immigration filings, and attorneys on the platform today.
    - [author-loop](https://coverable.ai/author-loop): 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.
    - [boundary](https://coverable.ai/boundary): What holds the boundary — 19 hostile programs against the sandbox on every build.
  - [ahead](https://coverable.ai/ahead): Where it goes — The same problem returns, with much worse failure modes.
    - [machine-action](https://coverable.ai/machine-action): When the mistake is a wire transfer — Models are moving from writing code to taking actions.
    - [lmatfs](https://coverable.ai/lmatfs): lmatfs, the substrate — A virtual filesystem so an agent never touches the host’s disk.
  - [who](https://coverable.ai/who): Who is building it — The problem was found in practice, not on a whiteboard.
    - [team](https://coverable.ai/team): The team — Two founders out of Carnegie Mellon, and the advisors around them.
    - [contact](https://coverable.ai/contact): Talk to us — We are raising, hiring, and looking for the next domain.

## Answers

### 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.

## Optional

- [Full tree as plain text](https://coverable.ai/llms-full.txt)
- [Design system](https://coverable.ai/styleguide.html)