Turing complete and safe: running untrusted code without a cage

How to hand a coding agent a program it wrote at runtime, let it loop forever if it likes, and still know — prove — that it cannot touch the world. The trick is to move the safety boundary off the edge of the machine and onto the edge of a type.

A few months ago, when I wanted my coding agent to do something I didn’t trust — crunch a file, run some throwaway numeric script, transform a blob of data in a way I hadn’t vetted — I did what everyone does. I fired up a disposable AWS box. If it corrupted itself, deleted the wrong thing, or got its brains eaten by a prompt injection, who cared? Nuke the instance, spin a fresh one. The safety model was: put the untrusted thing in a box so far away that its worst day can’t reach me.

This is a fine, ancient pattern. It is also, when you look at it squarely, a confession. It says: I have no idea what this code will do, so I’ll wrap it in a blast wall and hope the wall holds. The wall is a chroot, or a container, or a VM, or a whole rented machine. The bigger the wall, the more you trust it, the more it costs, and the slower it is to stand up.

I want to tell you about something we built into l3m — a kernel-verified coding agent written in Lean 4 — that replaces the wall with something categorically different. Not a better wall. No wall.

The 1980s, calling home

Start with the humblest possible task, the kind you’d reach for a one-line Python script for: map a function over each line of this file. Uppercase it. Reverse the fields. Parse the number in column three and double it. Compute g(17).

The industry-standard way for an LLM agent to do this is bracing in its honesty: the model writes some Python, and the agent asks “run this?” and you, the human, squint at code you probably don’t fully understand and click yes. That’s the state of the art. eval(untrusted_code) with a human rubber-stamp and, if you’re careful, a sandbox around it that you hope has no holes.

Every part of that sentence is a place safety goes to die. The human doesn’t really read it. The sandbox is a wall, and walls have CVEs — container escape is an entire genre of security research. And the eval is running a Turing-complete language whose whole design lets it open sockets, read your home directory, and phone home.

We wanted the 1980s convenience — just map the function over the file — without the 1980s security posture of “isolate the whole machine and pray.”

The move: make the dangerous thing unsayable

Here is the entire idea, and it is small.

Do not sandbox the code. Change the language so the dangerous thing cannot be expressed.

In Lean, effects live in a type. A function that reads a file, opens a socket, or launches a missile has a type that says so: it returns IO α. A function that merely transforms text has type String → String. And — this is the whole game — there is no way, inside a String → String, to run an IO action and smuggle its result out. Doing so would force the function’s type to become String → IO String. The type system won’t let you lie about it.

So we built a tool, map_lean, that accepts a Lean function as a string, at runtime, elaborates it in-process, and — before it will run a single line — checks one thing: is its type String → String? If yes, it runs. If the type mentions IO anywhere, it is rejected. Not sandboxed. Not permitted-but-watched. Rejected, because it does not typecheck as pure.

The witness is undramatic and that is the point:

map_lean  fun s => s.toUpper            ⇒  runs; file uppercased
map_lean  fun s => IO.println s         ⇒  refused: not String → String

IO.println s is not blocked by a guard that catches it in the act. There is no guard. There is no act. The term simply never makes it past the door, because its type is String → IO Unit, and the door only opens for String → String. The IO isn’t prevented — it’s unspellable.

This is the difference between a prison and a language with no word for escape. A prison holds a prisoner who is trying to leave. What we have is a grammar in which “leave” is not a sentence you can form.

Prison versus grammar

I keep coming back to that distinction because it is the axis every advantage rotates around. The disposable VM, the chroot, the container — all of them draw the safety boundary at the perimeter of the machine. Inside the perimeter, code is trusted to do anything; the wall’s job is to make sure “anything” can’t get out. That boundary is:

We moved the boundary off the machine’s edge and onto the edge of a type. And once it lives there, a whole run of good properties falls out — not as separate features we built, but as consequences of that one move.

Controlled access, not all-or-nothing. A VM is binary: inside, code does everything; outside, nothing. Our pure function reads its one input, writes its one fresh output file, and in the very same process cannot open a network connection — because the type has no IO in it. The granularity is per-capability, not per-machine. The agent doing the transform is the same trusted agent; only the kernel it’s handed is confined, and confined by construction.

No backup ritual. The disposable-box pattern forces “push to git before it self-destructs,” because the blast radius is the entire environment. Here the blast radius is one fresh file, and it’s undoable — the tool refuses to overwrite an existing path, so the worst case is “a new file appeared, and you can delete it.” You don’t perform end-of-the-world backups against a function call the way you do against a machine you’re about to nuke.

Private data cannot exfiltrate. This is the one that makes security people sit up. A VM holding your private data, with a network interface, can leak it — that’s the exfiltration surface, and no amount of good intentions closes it. A String → String cannot open a socket. Your private data goes in, transformed data comes out, and there is no channel to the outside world, because the type in which the transform is written has no way to name a channel. Not “configured not to leak.” Unable to spell the network.

The safety is legible and provable, not empirical. A container is safe until the next CVE. We can instead point at a theorem. The core claim — call it allPure ⇒ no IO — says: if every constant a term refers to is itself pure, the term performs no effect. It’s checked by the Lean kernel. You can read why the tool is safe, down to a small, named set of assumptions. A wall can only be trusted. This can be audited to the axioms.

No latency or dollar tax. Spinning a cloud box is seconds to minutes, and it costs money. chroot is lighter but still a process spawn and a filesystem dance. map_lean evaluates in-process, in microseconds, with no subprocess and no bill. The “compute g(17)” case is instant — which matters, because if the safe path is slow, people route around it to the fast unsafe path and you’ve lost.

It composes, because the boundary is inside the language. A VM puts the boundary at the OS edge; to combine two operations you shuffle files through a shared mount. Our boundary runs through the type system, so a pure kernel composes with another pure kernel as ordinary function composition. g ∘ f is still String → String, still pure, still provably safe. You cannot compose two chroots. You can always compose two pure functions.

Determinism comes for free. A pure String → String is referentially transparent: same input, same output, forever. A VM carries ambient state — a clock, a network, a drifting filesystem — that quietly makes runs non-reproducible. Purity is reproducibility; we didn’t add it, we couldn’t have avoided it.

“But you could loop forever”

Yes. And I don’t care.

This is worth dwelling on, because it’s the objection everyone raises and it turns out to be a red herring. A pure function is not guaranteed to terminate. Someone can write a String → String that spins the CPU forever, or builds an ever-growing list until it exhausts memory. Turing-completeness gives you that hazard for free.

But look at what that hazard is: it burns a core, or it eats RAM. It does not read your SSH key. It does not POST your database to an anonymous host. It does not rm -rf your home directory. The worst a pure runaway can do is waste your own resources — which is exactly the class of harm a disposable VM was protecting against with a sledgehammer. Burning CPU is tame. It’s your CPU. It stops when you stop it.

So we made a deliberate trade: we accept non-termination and unbounded memory as the price of Turing-completeness, because those are the survivable failure modes, and we spend all our rigor on the one that isn’t survivable — reaching the world. The code is Turing complete (it can loop, it can compute anything computable) and safe (it cannot touch anything outside its type). Those two words usually trade against each other. Here they don’t, because the thing we gave up — a guarantee of halting — is the thing that was never dangerous.

The honest part

I don’t want to oversell this, because the overselling is what makes security claims worthless. We do not claim “safe” as a magic absolute. We claim something more precise and, I think, more trustworthy: safe modulo a small, named, auditable trust base.

Two things sit under the theorem. First, a curated prelude — the set of primitive functions a user term is allowed to name. Real Lean bottoms out in native code (arithmetic, string operations), and a handful of those are @[extern]: implemented in C. We audited the transitive closure of, say, the JSON parser — 796 constants — and found the 45-odd native leaves it touches are all pure value kernels (Nat.add, String.append, and friends), none of them filesystem or network primitives. That curated list of blessed native functions is a trust decision, and it is written down and re-checked on every build — if a toolchain update ever slips an un-blessed native call into the closure, the build fails loudly.

Second, one named assumption of the same flavor as “unlink actually deletes the file”: that our miniature model of the evaluator faithfully mirrors the real interpreter. It’s an axiom, and — crucially — it’s listed by name when you ask what the safety proof rests on. We didn’t hide it. It’s a promissory note we can later discharge, and until we do, it’s visible.

That’s the whole trust base: a written-down list of pure primitives, and one named modeling assumption. Compare that to a container, whose trust base is “the entire Linux kernel’s isolation machinery and every CVE not yet discovered in it.” One of these you can hold in your head. The other you take on faith.

Why this is the win I’m proudest of

Almost anything on our safety list could be reproduced elsewhere with enough work. Confining writes to a directory? Any language plus a chroot. An undo log? Real engineering, but reproducible. Capability flags? Fiddly, but ordinary.

This one is different. I don’t believe you can match it without a language in which purity is a type. That’s why it’s a Lean win, not a general programming win. In Python, “this function is pure” is a comment, a hope, a convention you enforce with code review and crossed fingers. In Lean it is a fact the compiler will not let you falsify. And that single fact — purity as a type, not a promise — is what lets us take a Turing-complete language, hand it code we have never seen, written by a machine at runtime, and say, with a kernel-checked proof rather than a shrug: this cannot hurt you.

The disposable AWS box was perimeter security for code — a wall so far away its collapse couldn’t reach me. What we built is type security for code. The boundary moved from the edge of the machine to the edge of a type, and everything good followed from that one move.

No wall. No cage. Just a grammar with no word for harm.