Loom

Why Loom exists

LLM-assisted coding has moved through phases. Prompt engineering: coax the right answer. Vibe coding: stop coaxing, let the model run. Spec-driven development: write the requirements down first and have the model implement them. Each phase tightened the front of the pipeline. None of them changed the back: you still read the output and hope.

What comes next has to be guarantees. Not better prompts, not stricter specs — a way to mechanically check that the code does what was claimed, and to surface the parts that were not checked rather than quietly absorb them. Loom exists to provide that.

The idea

Between the prose that states the intent and the code that implements it, Loom inserts a third artifact: a short, structured document — an umbrella — short enough for a person to read end to end, precise enough for a verifier to check the implementation against claim by claim. The output is not pass-or-fail: anything the verifier cannot establish surfaces as an explicit gap, so what hasn't been proved is as visible as what has.

What it is

Loom is a research prototype of the Verifiable Umbrella architecture: a three-layer model for software construction in which

1. Prose captures human intent in durable form,
2. an umbrella of structured formal claims sits as the verified intermediate artifact between prose and code, and
3. siblings of LLM-authored implementation modules are mechanically verified against the umbrella's claims.

The umbrella is small enough for a human to read fully; the implementation is detailed enough for a verifier (Dafny, initially) to check against it. The discipline is bidirectional: obligations flow downward, properties flow upward, and the difference is reified as a gap report — the load-bearing visible artifact of the discipline.

Loom v0 is a single-user research prototype intended to validate the architecture. It is not a general-purpose programming language, and it is not production-grade.

Status

E-0005 (loom-light) turned the seed prototype into a real, growable tool: an opt-in verification overlay a downstream repo can add under one removable directory, plus an external runner (this repo) that verifies umbrellas against two backends — Dafny and a TLC model-checker, added through the same seam — and emits schema-stable gap reports. The runner self-hosts: loom's own trust-critical plumbing (atomic crash safety, dispatch totality, parser totality, under loom/) is verified by loom itself. An authoring loop (loom author) turns prose and examples into a verified umbrella end to end; a recognition command (loom suggest) proposes candidate umbrella stubs from source, closing the loop the other direction. The epic closed with a terminal decision (D-0007): productize now, explicitly alpha — a real release process cut from crates/loom in place, no repository move, since every prospective consumer at this stage is this project's own.

The repository holds:

• crates/loom — the engine.
• PLAN.md — the v0 plan, the seed document that drives everything else.
• project-structure.md — the intended repository layout.
• docs/ — language reference, claims reference, verification internals, bidirectional refinement, LLM operations, spec quality, ADRs, and the four background research documents under docs/research/.
• examples/ — worked umbrellas, including the two-umbrella composition case (05-composition/).

Where to start

• New here? Read docs/research/verifiable-umbrella-paper-v2.md for the architecture, then PLAN.md for what v0 commits to building.
• Looking for the language? docs/reference/language-reference.md and docs/reference/claims-reference.md.
• Looking for the discipline? docs/reference/bidirectional-refinement.md.
• Wondering how far guarantees reach across modules — the "global"/architecture question? docs/reference/compositional-correctness.md, with the worked two-umbrella examples/05-composition/.
• Worried about LLMs gaming the specs? docs/reference/spec-quality.md and docs/research/spec-quality-under-llm-authorship.md.