为安全代币实现类型化监管动作的机械化：语义、证伪与有界EVM证据
Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence
浏览论文内容
中文总结 AI 辅助
本文在Isabelle/HOL中形式化ERC-8319的六种监管动作语义，为安全代币开发了机械化语义模型，完成多工具验证，明确了已证明内容、有界证据及未解决问题的图谱。
中文摘要 AI 辅助
安全代币标准提供了特权转移、冻结、恢复和合规机制，但机制本身并不能识别所执行的法律效果，也不能识别与之相关的证据和撤销义务。我们在Isabelle/HOL中形式化了ERC-8319提出的六种监管动作含义的参考执行语义：FREEZE（冻结）、SEIZE（扣押）、CONFISCATE（没收）、LIQUIDATE（清算）、RESTRICT（限制）和RECOVER（恢复）。该模型区分了应用、拒绝和操作失败的结果，并机械化了撤销、重放、纪元、帧、案例局部终端性和收据属性；构建过程没有未证明的占位符或额外公理。它证明了外部真理边界：两个关于所有权、结算和权利不一致的具体世界会产生相同的核心观察结果，因此无法从有界输入中确定这些外部事实。建设性见证和直接突变显示了声明故障集的可达性和证伪性。对于一个ERC-TRUST Solidity/EVM候选方案，我们报告了单独范围的Foundry、Certora、Kontrol/KEVM、突变、确定性构建和运行时身份证据。当前的发布配置文件对所有七个证据包以及所有49项核心义务和24项强制性支持义务进行了验证，无部分信用；六项可选义务尚未认领。在固定运行时前提下，机械化抽象关系被证明是唯一且功能性的，而包和行推论从哈希边界证书产生了条件性的、配置文件范围的精化定理。这些结果不构成完整的Isabelle-to-Solidity-to-EVM精化定理、编译器正确性、审计、生产就绪性或部署验证。本研究的贡献是机器验证的领域语义，以及一张可证伪的图谱，标明了已证明的内容、有界证据、假设的内容以及受监管代币执行标准中仍未解决的内容。
英文摘要
Security-token standards expose privileged controls without identifying the legal effect executed or the evidence and reversal obligations it carries. We formalize in Isabelle/HOL a reference execution semantics for the six ERC-8319 meanings: FREEZE, SEIZE, CONFISCATE, LIQUIDATE, RESTRICT, and RECOVER. It distinguishes applied, rejected, and operational-failure outcomes and mechanizes action-specific reversals, replay and epoch rules, complete frames, case-local terminality, and final receipts; the session builds without unproved placeholders or additional axioms. An indistinguishability theorem shows that bound kernel inputs cannot establish external facts about title, settlement, or entitlement. Constructive witnesses and direct mutations establish reachability and sensitivity for the declared fault set. For a successor ERC-TRUST Solidity/EVM candidate, we report separately scoped Foundry, Certora, Kontrol/KEVM, mutation, deterministic-build, runtime-identity, and independent-reproduction evidence. All twelve named evidence lanes pass with none pending, while the 74-row obligation ledger remains conditional: 70 rows are closed, two runtime-link rows remain successor obligations, and two are inapplicable. The Native runtime is bound separately from an ERC-3643 interoperability reference that explicitly reports Partial and full=false, not Verified Full. These results do not establish complete Isabelle-to-Solidity-to-EVM refinement, compiler correctness, audit completion, production readiness, deployment verification, or external legal truth. They provide a machine-checked domain semantics and an explicit map of proved, bounded, assumed, and open results.
发表机构
- Oraclizer Labs（Oraclizer实验室）
- Oraclizer Labs Korea（Oraclizer韩国实验室）
机构由 AI 辅助整理，请以论文原文为准。
