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.
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.
Trust us — reputation, SOC 2, lawyers. The flaw: trust is a promise, not a property. Promises break when incentives change.
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?
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.
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.
TLA+, Coq, Isabelle. Easy to analyze. Hard to write. Cost of writing scales with properties. Practitioners are rare.
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.
| annotation | declares | what the auditor learns for free |
|---|---|---|
-R | value never escapes its scope | no aliasing, no UAF, no sharing bugs |
+R | heap-resident, ARC-managed | check sharing discipline |
-M | immutable through this reference | no TOCTOU, no data race on this path |
+M(MVCC) | mutable with a specific policy | check the policy is appropriate |
-N | guaranteed non-null | no null dereference — skip it |
-E | effect-free | safe to reorder, parallelize, memoize, retry |
-D | deterministic | safe to cache; auditor can reproduce any call |
! ErrorType | exact failure surface | error surface is enumerated, not guessed |
o { Network.HTTP } | module has network capability | entire 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.
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.
Consistency. A pinned LLM produces the same verdict on the same code every time. Two human auditors do not. The same human on different days does not. Consistency makes errors testable and calibratable — inconsistency doesn't.
Coverage. The LLM processes every function, every binding, every modifier. It doesn't tire, skip the boring parts, or assume a well-named function does what its name says.
Uncorrelated failures. The LLM and the U compiler have different failure modes. The compiler doesn't hallucinate. The LLM doesn't miss logic bugs. Neither has the other's blind spots.
A U package's capability surface is declared and compiler-verified. No o { Network.HTTP } = provably cannot phone home. The LLM checks logic for backdoors. The analysis is reproducible. Together they catch what neither catches alone — uncorrelated failure modes.
LLM generates U → compiler catches 11 structural categories → second LLM reviews logic. Three independent checks, two deterministic. In Python, if the LLM writes a data race, the compiler has no idea. In U, it's a type error.
A plugin declaring o { Templates } and nothing else provably cannot access the network. The enforcement is at the language level, not the platform level. No sandbox to escape from — the capability isn't there.
The attested chain runs on every commit. The verdict is reproducible by the regulator. "Was this code reviewed?" has a mechanical answer.
Anyone spins up a Safebox, loads attested code, offers the service. Attestation proves they're running the genuine code. Users trust the chain, not the operator. What blockchain tried — trust the code, not the operator — but fast and private.
A Safebox oracle's U source proves it can only call the approved API and only return the approved type. Attested, compiler-proven, on-chain verifiable.
Don't align the model by surgery on its weights. Install the culture — workflows, policies, scope rules — as an inspectable layer in U. The substrate decides what the model can do. The model can want whatever it wants.
The Safebox enforcement chain we built has 23 test phases and ~643 assertions. Every property is enforced at runtime. U moves the critical properties to compile time. The runtime checks become defence-in-depth.
Scope.check() runs on every call. 71 assertions verify the matcher. Correct because we tested it — not because it's structurally impossible to be wrong.
o { Network.HTTP } is the only import mechanism. Without it, the call doesn't exist in the binary. No runtime check. No bypass. Nothing to test.
Remove process/require/module from the worker global. BUG #71 found 4 escape routes via new Function("return this").
No eval, no Function constructor, no prototype chain. All 8 escape vectors are structurally impossible. The sandbox shrinks to memory/time enforcement.
BUG #76: live CRLF email injection. BUG #74: credential leak via URL userinfo. Both runtime validation failures.
Template tags: html`…`, sql`…`, smtp`…` reject raw strings at compile time. Injection is a type error.
spec._provenance = {...} injected by the orchestrator. Enforcement at runtime via Scope.check.
LLM output is type S. SMTP requires Templates.HTML. The only path between them is the template system. The type IS the provenance.
The deterministic gate is intended to be pure. Nothing proves it. A subtle Date.now() would break caching silently.
-E -D on the gate function. The compiler proves it's deterministic. Adding Time.now() is a compile error. Caching is proven correct.
Tests prove correctness against finitely many shapes. A compiler proves correctness against all possible inputs. That's not a better test. It's a different category of claim, the way a mathematical proof is a different category from an experiment.
When the U compiler enforces o declarations, it doesn't check 71 URL shapes. It proves the call cannot exist — the function isn't in the compilation context. No URL of any shape, including shapes nobody imagined, can be constructed or passed. The 71 assertions become defence-in-depth. The primary evidence is a proof.
The auditors vote on a fact, not on their reading of source. The LLM reasons about semantic implications — "why does a refund processor need HTTP?" — not about whether the code hides a fetch().
In PHP, knowing function A is safe tells you nothing about B. In U, if A is -E -D and B is -E -D, their composition is -E -D — the compiler proves this transitively. Reason about 1,000 functions by reading 1,000 annotations, not 1,000 implementations. That's a sound shortcut.
A compiled U module's symbol table says:
Anyone reading that symbol knows what it can do, what it can't, and what can fail. The source is irrelevant to the safety claim. The claim is in the interface, proven by the compiler.
Traditional closed source: "trust us." You can't verify.
Traditional open source: "read it yourself." You won't.
U: "the compiler proved what the code can do, and the proof is in the artifact."
.u.meta — the proof travels with the binary.
Every binary the U compiler produces contains a .u.meta ELF section: a structured record of every class, function, modifier, error type, and the module's complete capability surface. Emitted by the compiler, covered by the binary's hash, readable by anyone with the binary and nothing else.
A separate manifest can be detached, stale, or forged. Embedding removes the question: one hash covers everything. The unit of deployment is the binary. cp is sufficient.
No U tooling required to extract it — it's a plain ELF section: objcopy --dump-section .u.meta=meta.json ./server.
.u.meta is a claim. A signature is an endorsement of that claim. Different acts, different parties, different times. Conflating them is how signing schemes end up meaning nothing.
An endorser signs a set, and that set need not be everything. "I vouch for Templates and HTTP; I do not vouch for SMTP." Watch it accumulate:
Bob deliberately withheld SMTP. The binary stayed unloadable on that capability until Carol, who had checked SMTP against the spec, signed for it alone. The disagreement is legible in the artifact instead of resolved in a meeting.
| attack | result |
|---|---|
| widen capabilities after signing | all endorsements invalid — meta_hash moved |
recompile code, transplant .u.meta | all endorsements invalid — image_hash moved |
| unauthorized key signs | not counted toward any threshold |
| detached manifest vs tampered binary | does not match |
The linker is the only tool that sees all compiled parts at once. The compiler sees one file. The auditor sees what they're given. Only the linker is present when separate pieces become one program.
The capability surface is a union. A module that renders templates + a module that reads files + a module that opens sockets = a program that can read your files and post them. No single source file says so. The union says so, at link time, in one line.
Cross-module effect violations. A function declared -E that calls a symbol whose .u.meta says +E(Network.HTTP) is a contract violation only the linker can catch. Without that check, separate compilation is a hole in the compositional argument — and it's exactly where an attacker would aim.
Useful before enforcement. A linker that merely prints the capability union already turns whole-program questions into a table lookup. Enforcement comes later. The data is what creates the option.
Traditional SaaS: trust the company → they run the code → you use the service.
Safebox SaaS: trust the attestation → anyone runs the code → you choose whoever offers the best price.
U makes this viable: the compiler catches most bugs for free, the LLM audit is cacheable (same code = same verdict), the analysis scales sublinearly (O(1) per binding, not O(n) per codebase), and .u.meta means the cheap verification path needs no source and no rebuild.
Logic bugs are still possible. The compiler eliminates structural bugs. The LLM catches many logic bugs. Neither catches all. The claim is not "bug-free" — it's "structurally sound, logic-verified to the best of a reproducible, attested analysis."
The LLM can be wrong. But it is consistently wrong — same error, same code, every time — which makes it testable and improvable. Human errors are inconsistent, which means they can't be.
.u.meta is only as trustworthy as the compiler. A modified compiler can emit any declarations it likes. Reproducing the build from source with a known compiler closes the gap. The section records compiler version and source hash precisely so that check is possible.
Signatures bind a claim to a hash, not to reality. An endorsement says a key holder vouched for a pairing of code and declarations. It does not say they were right, or that their key is still under their control.
Sleeper bugs are hard. A sleeper that stays within its declared contract while doing something subtly wrong is the hard case for any analyzer.
The smallest trust surface current technology can achieve: an attested hardware boundary running open-source deterministic tools and a pinned, reproducible LLM, against code whose structural properties are declared, compiler-verified, and carried in the artifact itself. Not zero trust. The minimum trust — and the minimum is small enough that anyone can inspect it.
That's the third way. Not "read the code yourself." Not "trust the company." Trust the proof, and verify it.