Theorem 发布验证沙箱原型，以机器码级形式化验证隔离访客代码

Theorem 团队发布「验证沙箱」系列第一部分，构建可运行 Linux 的原型 hypervisor。该方案基于 MIT 的 xv6iris，以约 150 万行 Rocq 证明验证内核正确性，并在机器码层面证明访客代码无法修改宿主文件。团队称这是迈向生产级可信沙箱的第一步。