Efficient Branch-and-Bound Testing and Verification of zkVMs

零知识虚拟机（zkVM）通过把虚拟机语义翻译成执行轨迹上的代数约束，使通用程序能够被可验证地执行。这些约束的正确性至关重要：一条错误的约束可能使系统处于欠约束（under-constrained）状态，从而接受伪造的证明；也可能因过约束（o

历史摘要 · 未重新核验 · arXiv cs.CR