Building verified agent sandboxes: Part 1

Aditya Tewari Harshikaa Agrawal Sami Jawhar Luke Champine Cheru Berhanu† Jason Gross Nickolai Zeldovich

As recent events have demonstrated, reliable sandboxes are a must have in the world. We built a prototype sandbox on xv6, a small teaching operating system, and proved that no program inside the sandbox can change any file outside it. We consider this a first step toward our target of verifying Firecracker with KVM on Linux, a common production setup for agent sandboxes.

The work described here was completed on September 30, 2026.

What we built

To fulfill its intended purpose, a sandbox must be as trustworthy as a cryptographic primitive. Cryptography’s strength comes from its close relation to mathematics. A cryptographic primitive can be precisely modeled as a mathematical object and thus can have particular guarantees formally verified. To achieve similar guarantees for sandboxes, we must extend the practice of formal verification into the messy world of computer systems. While this is a daunting task we believe it is the only viable strategy to security critical software and thus internet infra against agents and malicious actors.

We started from xv6iris, by Frans Kaashoek and Nickolai Zeldovich at MIT-PDOS. xv6iris proved the xv6 kernel correct at the level of its compiled machine code. That proof:

Checks the kernel’s machine code against the official RISC-V specification
Reasons about several processor cores running at the same time
States its final theorem only in terms of what a person can observe from outside the machine

The xv6iris proof is about 1.5 million lines of Rocq. On top of it we added:

A hypervisor inside the xv6 kernel, which plays the role that KVM plays in Linux, using the processor’s virtualization features that xv6iris had switched off;
vmm, a small program that plays the role of Firecracker: it loads an untrusted program, called the guest, and runs it in a virtual machine;
A theorem that the guest cannot change any file on the disk, no matter what its code is.

The verified sandbox: the machine, as the RISC-V Sail
specification defines it, with 8 cores, a console, an interrupt
controller and a disk. Inside it, the proved xv6 kernel with init,
sh and vmm, and inside the kernel the hypervisor, which runs the
guest on one core. No assumptions are made about the guest code,
which may be potentially adversarial. — **The guest can be any code.** This proof assumes 8 cores are fixed, with guests always running on core 1. Our internal versions prove that an updated version of xv6 can run with 1 to 512 cores and run guests on up to 512 cores as well.

Our new proof is about 342,000 additional lines, written nearly entirely by agents across 19 days, and we found a bug in qemu.

What we proved

Following xv6iris, we describe the system in terms of its observables–states that can be observed externally. These include:

If the machine is on or off
What files are stored on disk at power on
The literal characters sent and received over a serial port.

Expressed in these terms, our theorem says:

Assume the machine is powered on and the console shows the prompt $.
If you type vmm --no-output-run, press Enter, and type nothing else,
then every file on the disk stays as it was.

This holds:

For any guest programs
With arbitrary system crashes or going from power on to off at any point.
For any number of boots from the original disk image, as long as only vmm --no-output-run is typed in.

In fact as shown below crashes allow us to precisely examine the filesystem in order to observe its state and are essential to the theorem.

Each row is a file on the disk across one sandbox session: boot, the
prompt, vmm, the guest running any bytes, and vmm's closing lines.
Wherever the power is cut, the reboot finds every file as shipped
and the canary in /sys/vmm still empty. An inset, Power cuts find
changes, shows a change by the guest that would pass a check at the
end but is caught by a cut in the middle. — **Power cuts give the proof strength.** No matter when the power is cut, the file system observer always sees the same disk other than an empty canary under `/sys/vmm`. Below, a change by the guest that a check at the end would miss is caught by a cut in the middle.

Trusting the proof

You don’t have to read the roughly 1.5 million lines of proof behind the theorem to trust it. Rocq checks the proof in order to determine that each step is correct. What you do have to trust is much smaller:

About 5,100 lines of definitions that describe the machine and state the theorem, including about 1,700 lines of hand-written models of the console, the interrupt controller and the disk.
The processor specification: about 81,000 lines of Rocq, generated from the official Sail description of RISC-V as we configured it.
Sail’s floating-point specification, which is not completely modeled in Sail.
The files we run are the files the proof is about. 1 1 The proof is about the exact bytes of the kernel and the disk image. Before a run of the sandbox our build system checks the hashes of the kernel and the files system. If either differs, it refuses to start unless you override it. A build from source on a fresh machine produces the same bytes.
Rocq and its built-in types PrimString and PrimInt.
Function extensionality, a standard function equality axiom. It states that two functions are equal if and only if they agree on all inputs.

The auditing surface: about 1.5 million machine-checked lines
of proof, against what you trust: the RISC-V specification, 80,725
lines, and our definitions, about 5,100 lines. The proof relies on
79 axioms, 12 standard Rocq and 67 floating point, plus 2 sealed
predicates for store-conditional, which the proof covers either
way. — **We examine the definitions and Rocq checks the proof.** Thus, the audit surface is 5,100 lines of definitions and the RISC-V Sail specification. The code itself was about 8,400 lines.

The theorem statements and proofs are published and available here. Feel free to poke around and try the rocq check yourself!

Why this is hard, and what came before

Plenty of software has been verified before. Here is how this work relates to the closest earlier efforts:

seL4 proved a whole microkernel correct, and for some versions carried the proof down to the compiled binary. Its verified versions run on a single core, its processor model is hand-written, and its proof does not cover the kernel’s handling of caches or the TLB, the processor’s cache of address translations.
SeKVM proved that a multiprocessor version of Linux’s KVM hypervisor on Arm protects the confidentiality and integrity of its guests’ data. Its proofs cover the C code and the assembly separately, against a hand-written machine model, and the two are not linked.
Islaris is closest to us in method: it reasons about machine code against the official Sail processor specifications.
CertiKOS is the closest in overall scope: a concurrent kernel for multicore x86 that can also run Linux guests. It differs in what you have to trust. CertiKOS proves its C code and relies on a verified compiler to carry that proof down to machine code, and its x86 machine model, which its authors wrote, assumes the strictest memory ordering. We prove the machine code itself, against the official RISC-V specification, including the processor’s own page-table walks and Translation Look-Aside Buffer (TLB), under a weaker memory ordering. And CertiKOS proves that its kernel matches its specification, while our theorem is about what a (potentially hostile) guest can do.

Prior work as listed above individually cover part of what a sandbox needs. However to our knowledge no earlier proof puts the pieces together in a single system. Our xv6 sandbox theorem covers any guest on the specific kernel/hypervisor with this sandbox program (vmm), on a hardware model given by the official processor specification with multiple cores and address translation. This project is hard because all three things must hold at once:

Real machine code. The proof is about the exact bytes the processor runs, not the source code, so we don’t have to trust the compiler. The cost is that every recompile can break the proof. When we first added the hypervisor, only 33 of the kernel’s 189 existing functions came out identical, and early on one failing proof held up 923 files that depended on it.
Many cores at once. The model has eight cores running in parallel and taking interrupts. The proof covers every order in which their steps can interleave, under a memory-ordering rule a little stricter than RISC-V’s default.
Two layers of address translation. The guest manages its own page tables, the hypervisor manages a second layer underneath, and the processor caches both. The guest can write anything into its tables.

xv6iris addressed the first two, while our extension had to keep both true while adding the third, plus a guest that can be any program.

The cores are where the cases explode. Two cores that each take four steps can interleave in 70 ways. Three cores: 34,650 ways. Eight cores: about 2.4 × 10²⁴ ways. A naive enumeration of the possibilities would be intractable.

A table of the number of ways c cores
taking s steps each can interleave, from 1 to 8 cores and 1 to 6
steps; 2 cores with 4 steps each give 70 ways, and 8 cores with 6
steps give about 1.7 times 10 to the 38. — **Eight cores can interleave their steps in more ways than could ever be tested. The proof covers all of them.** (cs)! / (s!)^c ways for c cores taking s steps each. Outlined: the 2-core and 8-core cases from the text. In red: eight cores taking six steps each can interleave in 1.7 × 10³⁸ orders; testing every one at a billion per second would take about 5.4 × 10²¹ years, some 400 billion times the age of the universe.

xv6iris’s solution to all the interleavings is called “ghost state”: bookkeeping that exists only inside the proof and records which proof artifact owns which resource. As part of a technique called concurrent separation logic, the proof makes claims about all possible interleavings while only reasoning about one core at a time. Our hypervisor proof uses the same technique. This technique was difficult for agents to leverage unless specifically pointed at the abstraction to use. While we think this may be an artifact of how we set up our proof environment we are investigating to see if it possible to make the process of identifying the right ghost states fully automatic.

Ghost state in four views of the same machine: all the
interleavings, where every core and every step changes at once;
file writes isolated, with one ghost token per disk block that a
write must hold; the guest, which owns its core, its memory and its
TLB but no disk token, so no guest step can write a file; and the
kernel, which keeps the disk's tokens and is the only writer of
files, so all we have to prove is that no file is written there. — **Ghost state lets us reuse xv6iris.** Each disk block has one token, and only its holder can write the block. The guest holds none, so only the kernel writes files. xv6iris already proved the kernel's file system, so we only have to show that a session writes nothing but `vmm`'s empty canary.

What comes next

This is a proof of concept. xv6 is a teaching system with no network, no user accounts, and a 2 MB file system, and the proof is about a precise model of a RISC-V processor that no chip on sale matches exactly. Here is what it does not do–yet:

Already proved in later versions, and coming in our next post: up to 512 virtual CPUs on machines with up to 512 cores, any number of sandbox sessions without rebooting, and a guest loaded from a file.
In progress: liveness, a proof that the system keeps making progress. Today the theorem allows for a program that never finishes.
Talking to the guest: an interactive mode, and a virtual network device that the guest can send results through. Today the guest gets no input, and its output is thrown away.
Secrets: nothing yet about confidentiality. The theorem is about files, not about what a guest can learn, and that is one way that we prove less than seL4 and SeKVM.
Real hardware: closing the gaps between the model and real RISC-V chips, then running on a real board. Our tests so far run on QEMU–an open source machine emulator–which does not behave exactly like the processor our proof describes.

From the physics up. Each layer builds on the one below it. Pick a security property on the side to see which layers it has to cover. Hertzbleed reaches all the way down to the physical specifications. Note that in our diagram we verified xv6's version of firecracker, `vmm`, and showed that its version of glibc retained it's properties, we are not releasing a proof of firecracker in this post.

If you are interested in preventing agent escapes, get in touch!