Theorem proves verified sandbox protections on xv6iris

Theorem researchers built a prototype agent sandbox on the xv6 operating system and formally proved that no untrusted guest program can modify files outside the sandbox. The proof verifies machine code directly against the official RISC-V specification, running across eight parallel processor cores with two layers of address translation. The authors state that this project serves as a first step toward verifying Firecracker with KVM on Linux, a common production setup. Open article →