该论文处理的是一个在可验证计算工程中常被忽视的信任缺口：GKR 协议的可靠性界只能保证『关于某个算术电路的输出声明是可信的』，却无法保证『该电路确实编码了应用所期望的状态转移』。作者以稀疏 Merkle 树（SMT）的成员证明、非成员证明与状态更新为具体应用载体，在 Isabelle/HOL 证明助手内对这条从状态转移到 GKR 验证的完整信任链进行机器检验。 方法上分为若干层次。首先是编译器模型：它建立了电路接受与状态转移有效性之间的双向关系（而非仅有单向的可靠性蕴含），从而同时覆盖可靠性与完整性两个方向。其次是可复用的协议模型：把层归约（layer reduction）、wiring predicate 扩展，以及从外部导入的 sumcheck 可靠性结论组装起来，形成一个针对某个显式『链事件』的界；其组合定理把语义上的无效性传递到该界上，且 witness 在挑战实验之前就已固定，避免了先看挑战再选证据的隐患。作者特别强调使用具体解释（concrete interpretations）与前提激活（premise activation）来暴露『空洞假设集』——即假设集合在逻辑上被满足但语义上无内容的情况，这是仅靠一次干净编译无法发现的。 进一步的工作构造了精确的四次 KoalaBear 扩域，把基域上的电路对象提升到扩域，并在其陈述的挑战假设下建立分母为 p^4 的装配界。论文还附带了一个可执行的 Rust prover，通过 Creusot/Why3 合约提供部分实现层面的连接，并给出一个条件性定理，把成功的验证者执行轨迹与模型事件关联起来——但该定理依赖一个未被消解的值对应（value-correspondence）前提。作者明确列出未完成的部分：既未建立转录中的在线挑战分布性质，也未建立多轮 Fiat–Shamir 归约。因此其核心贡献是：在单一证明助手内完成编译器正确性与 GKR 装配模型的组合，并显式、诚实地刻画了遗留的实现义务与密码学义务。 适合阅读的人群包括：形式化方法与证明助手研究者、zkVM / 可验证计算与状态承诺（SMT、Rollup 状态根）方向的协议设计者，以及需要对证明系统实现做独立评估的安全审计人员。

该论文提出并实现了一种名为 Unicity 的新型区块链基础设施，其核心目标是支持用户进行链下（off-chain）点对点代币交易，同时防止代币的平行状态（即双重支付），并保持区块链本身的极简复杂度与存储开销。基础设施的关键组件是聚合层（Aggregation Layer），它负责存储代币已花费状态的信息，并向用户提供关于无双重支付的紧凑密码学证明，且无需牺牲任何信任假设。聚合层本质上是一个二层（Layer 2）服务，维护一个仅追加（append-only）的键值存储库，并周期性通过被称为共识层（Consensus Layer）的传统区块链来认证其状态。在每一轮状态变更时，聚合层需向共识层提供密码学证明，以证明键值存储的仅追加一致性。论文采用 Radix 稀疏默克尔树（RSMT）生成每一轮 i 的存储摘要 r_i，并构造特殊类型的认证路径，以证明下一轮摘要 r_{i+1} 仅通过向存储库中添加若干键值对 (k,v) 得到。证明验证代码实现为代数中间表示（AIR）电路，构建在 Plonky3 STARK 工具包之上。该实现无需可信设置，在单台普通消费级 CPU 上可达到每秒 10000 次插入的吞吐量，验证时间在毫秒级范围内。论文的主要贡献在于设计了一个无需信任的聚合层，兼顾可扩展性、安全性和低存储成本，为链下交易提供实用的双重支付防护方案。该研究适合对区块链扩容、二层协议、密码学证明（STARK/Merkle 树）以及去中心化系统安全感兴趣的从业者阅读。