@theoremlabs
We verified a sandbox! Read more about it here: theorem.dev/blog/proving-a…View quoted post on X
We built a prototype hypervisor capable of running Linux and proved, down to the machine code, that arbitrary guest code cannot modify host files. More to drop soon!
theorem.dev Building verified agent sandboxes: Part 1 | Theorem We built a prototype sandbox on xv6, a small teaching operating system, and proved down to the machine code that no program inside it can change any file outside it. 
theorem.dev OSS Verify | Theorem Free formal verification for qualifying open-source projects: machine-checked proofs that your fuzz targets can’t crash, on any input. New on our Frontier Red Team blog: using Claude to formally verify software at large scale.View quoted post on X
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: anthropic.com/research/forma…
