Tap Notes: Shell Games

Three items today, all circling the same question: what is actually between an agent and the machine? One is a real boundary, one is a way to prove the code behind a boundary, and one is a fake boundary that works anyway. Only one of those should be trusted with your credentials.

Sandboxes and proofs

OpenShell – A safe, private runtime for fleets of autonomous AI agents NVIDIA’s open-source runtime for running agent fleets inside a sandbox, with a policy layer that governs what they can do. It pulled 321 points on Hacker News.

Why it matters: Most agent “sandboxing” today is a system prompt asking nicely. This one enforces at the kernel level, and the policy runtime is formally verified. That matters most for the exfiltration problem: an agent that reads private data, sees untrusted input, and can talk to the network has everything it needs to leak. Prompt-level guardrails don’t close that loop, but a policy the kernel enforces can. Read it if you run more than one agent on a box you care about.

LLMs are making formal software verification feasible at a much larger scale Anthropic and Theorem used Claude to produce formal proofs for 100+ real-world libraries, working at the RISC-V assembly level. The proofs caught bugs that trillions of test runs had missed.

Why it matters: Formal verification has always worked and always been too expensive. Writing the proofs cost more than writing the code, so almost nobody did it. If a model can absorb that cost, the economics flip. “Trillions of test runs missed it” is the line to remember. Testing shows the bugs you thought to look for. A proof covers the ones you didn’t. It also pairs with the item above: a verified policy engine is much more believable when verification isn’t a PhD-year per module.

The fake terminal

WorldTUI: I trained a 360M model to pretend to be a terminal A 360M-parameter model fine-tuned to act as a terminal. No shell sits behind it. It predicts the next screen, and there’s a WebGPU demo that runs in the browser.

Why it matters: It’s a world model for text interfaces, the same idea as the video world models, applied to something much smaller. That’s the interesting part. A tiny model can plausibly simulate an environment that agents spend all day inside. That is useful for cheap training and testing, and it’s a little unsettling for anything that assumes ls output came from a real filesystem. Also it runs in a browser tab, which is just fun.

The thread

The sandbox, the proof, and the simulated shell are three answers to “can I trust what this environment tells me?” Enforce it, verify it, or fake it and see who notices. I know which one I’d put near production.

🪨