U — The Intermediate Form — Safebots

Safebots · U Language · August 2026

U — The intermediate form.

How a structured language inside attested compute creates a third way between open source and closed corporations. Why "provably" is a different category of claim from "tested." And what that unlocks.

1. The three-way problem

2. The intermediate form

3. What U declares

4. Pinned LLMs on structure

5. The attested analysis chain

6. More trustworthy than humans

7. What this unlocks

8. U vs PHP/Node, layer by layer

9. "Provably" — a different claim

10. .u.meta — proof in the binary

11. M-of-N signing

12. The linker as reasoner

13. The economics

14. The honest boundary

1. The three-way problem.

Open source

Trust the code because you can read it. The flaw: nobody does. The xz backdoor sat for two years. The cost of reading scales with codebase size, and nobody pays it.

Closed corporation

Trust us — reputation, SOC 2, lawyers. The flaw: trust is a promise, not a property. Promises break when incentives change.

The third way

Trust the seal, the compiler, and the reproducible verdict . The compiler proved what the code can do. The proof is in the artifact. Anyone can verify it.

Open source gives you the right to verify but not the ability. Closed corporations give you neither. Safebox proposes a third way: trust the running code because a sealed, attested environment analyzed it — using tools that are themselves pinned, reproducible, and verifiable.

The question is: what makes the analysis good enough to trust?

2. The intermediate form.

There's a pattern in computer science that shows up everywhere: the trick is finding an intermediate representation structured enough to be processed cheaply in both directions.

A B-tree gives O(log n) at write time and O(log n) at read time. A flat array gives O(1) writes but O(n) reads. A fully sorted array gives O(log n) reads but O(n) writes. The B-tree trades a small constant factor for logarithmic performance in both directions.

Unstructured code

Python, JS, PHP. Easy to write. Hard to analyze. The auditor must infer ownership, mutability, nullability, effects, capabilities from conventions. Cost scales with codebase size.

Fully formal specs

TLA+, Coq, Isabelle. Easy to analyze. Hard to write. Cost of writing scales with properties. Practitioners are rare.

U — the intermediate form

Every binding site is a machine-readable declaration. Cost of writing: near zero (auto-filled, safest default). Cost of analyzing: O(1) per binding .

The compiler catches 11 categories of bugs at build time — null dereference, use-after-free, data races, injection, missing error handling, off-by-one, SQL injection, float rounding, forgotten await, lost database update, indentation. These are structurally impossible in well-typed U, not merely unlikely.

The same declared structure that lets the compiler verify correctness also lets an LLM verify intent — at far higher fidelity than with Python or TypeScript, because the properties it needs to reason about are declared, not inferred.

3. What U declares that other languages don't.

annotationdeclareswhat the auditor learns for free<br>-Rvalue never escapes its scopeno aliasing, no UAF, no sharing bugs<br>+Rheap-resident, ARC-managedcheck sharing discipline<br>-Mimmutable through this referenceno TOCTOU, no data race on this path<br>+M(MVCC)mutable with a specific policycheck the policy is appropriate<br>-Nguaranteed non-nullno null dereference — skip it<br>-Eeffect-freesafe to reorder, parallelize, memoize, retry<br>-Ddeterministicsafe to cache; auditor can reproduce any call<br>! ErrorTypeexact failure surfaceerror surface is enumerated, not guessed<br>o { Network.HTTP }module has network capabilityentire capability surface in one scan

In Python, the auditor must infer every one of these from context. In U, they are declared at the binding site and verified by the compiler. The auditor reads facts, not guesses.

4. What a pinned LLM can do with declared structure.

A "pinned LLM" inside a Safebox is a specific model version, with specific weights, running a specific prompt, inside an attested environment. Its output is near-deterministic: same code + same prompt = same verdict.

Capability surface in one scan. U's o declarations enumerate every external capability. A module without o { Network.HTTP } cannot make HTTP calls — the compiler enforces this, and the LLM can trust that enforcement.

Effect boundaries are declared. A function marked -E -D is proven pure and deterministic. The LLM treats it as a mathematical function — verify logic without considering state or timing.

Template injection is structurally impossible. html`…` and sql`…` reject raw strings at compile time. The LLM doesn't audit for injection — the compiler makes it a type error.

The LLM is the only probabilistic layer. Everything beneath it is deterministic. And the LLM's job is vastly easier because the structural noise has been eliminated by the compiler.

5. The...