零知识虚拟机（zkVM）通过把虚拟机语义翻译成执行轨迹上的代数约束，使通用程序能够被可验证地执行。这些约束的正确性至关重要：一条错误的约束可能使系统处于欠约束（under-constrained）状态，从而接受伪造的证明；也可能因过约束（over-constrained）而拒绝合法执行。现有手段在生产规模下都无法提供有意义的保证——模糊测试和单元测试覆盖不足、SMT 求解器难以应对约束的规模与非线性、定理证明器则需要大量人工投入。 本文提出 ZEBRA，一个全自动的验证与缺陷检测框架。其核心洞察是：对于给定程序与输入，约束系统必须恰好允许一条有效执行轨迹，不多也不少。由此，作者把 zkVM 验证归约为“规范轨迹空间上的解集基数问题”，并在计数之前先消除空行填充（null-row padding）、非确定性置换等结构性冗余。为使基数计算可处理，ZEBRA 将分析从有限域 witness 提升到整数区间格，并利用 zkVM 约束的结构稀疏性——在 5 个真实 zkVM 上，约束平均只使用了其理论连接容量的 14.0%——从而实现紧致的区间传播，并把近似误差控制在有限范围内。在此基础上，ZEBRA 执行并行的分支限界（branch-and-bound）搜索：要么给出一个具体的反例，要么证明在给定有界区域内不存在违规。 在 5 个真实 zkVM 上的评测中，ZEBRA 共发现 11 个零日缺陷，其中 6 个已被独立确认、3 个已被开发者修复；与基于 SMT 的验证相比，ZEBRA 速度快 51.5 倍，可验证的实例多 16.5 个百分点，其范围（区间）验证相比逐输入重复验证最多带来 63 倍的效率提升。该工作面向 zkVM／电路开发者与形式化验证研究者，提供了首个在真实系统上可扩展、可自动化的约束正确性检查路径。

本文提出了一种名为 Prezta（可验证的零信任授权远程执行）的新型架构，旨在解决关键基础设施中运营技术（OT）系统安全现代化面临的挑战。传统的应用网关虽然能执行复杂授权并支持零信任架构，但存在部署和管理负担重、需与远程边缘设备共置、频繁更新补丁等问题。Prezta 通过将授权策略评估移到客户端内的零知识虚拟机（zkVM）中执行，生成简洁的零知识证明，边缘设备只需高效验证该证明即可确认授权结果，从而消除了应用网关，将零信任安全边界扩展至边缘。该系统支持策略和身份管理方案的动态演进，无需更新边缘设备。原型基于 RISC Zero zkVM 实现，兼容 XACML 3.0 策略和 JWT 身份声明。为减轻 zkVM 带来的证明开销，作者将策略编译为 Rust 代码，并预编译正则表达式，同时优化签名验证和 JWT 解析，将证明者时间降低了一个数量级以上。编译器正确实现了 XACML 3.0 一致性测试套件的 83%，在台式机上证明生成耗时数十秒，而验证仅需数十毫秒，足以适应资源受限的边缘设备。该研究展示了零知识证明在零信任远程授权中的可行性，为边缘计算环境下的安全架构提供了新思路。