046 · 简化版被证明，原 kernel 就正确了吗？RESOLVE 用逐位测试连接原始 kernel 与低并发版本，再证明后者的代数等价性。这条混合证据链扩大了验证范围，也要求分清：哪些连接经过证明，哪些仍依赖有限执行。