该论文针对安全代币（Security Tokens）标准中监管操作语义不明确的问题，提出了一种机械化（machine-checked）的参考执行语义。安全代币标准通常暴露特权转移、冻结、恢复和合规机制，但机制本身并不标识其执行的法律效果或附带的证据与撤销义务。作者在 Isabelle/HOL 中形式化定义了 ERC-8319 中提出的六种监管行动：FREEZE、SEIZE、CONFISCATE、LIQUIDATE、RESTRICT 和 RECOVER。模型区分了应用（applied）、拒绝（rejected）和操作失败（operational-failure）三种结果，并机械化验证了撤销（reversal）、重放（replay）、纪元（epoch）、框架（frame）、案例局部终态（case-local terminality）和收据（receipt）等性质。构建过程中没有未证明的占位符或额外公理。论文证明了外部事实边界：两个在所有权、结算和权益上存在分歧的具体世界会产生相同的核观察结果，因此这些外部事实不能从受限输入中建立。通过构造性见证和直接变异展示了可达性和故障集的伪造（falsification）。针对一个 ERC-TRUST Solidity/EVM 候选实现，论文分别报告了 Foundry、Certora、Kontrol/KEVM、变异测试、确定性构建和运行时身份的证据。当前发布概况满足全部 7 个证据包、49 个 Core 和 24 个强制性 Supporting 义务，且无部分学分；6 个可选义务未声明。在固定运行时前提下，机械化抽象关系被证明是唯一且函数的，包和行推论从哈希绑定证书产生条件性的、概况范围的细化定理。作者明确声明，这些结果并不构成完整的 Isabelle 到 Solidity 到 EVM 的细化定理、编译器正确性、审计、生产就绪或部署验证。其贡献在于一种机器检查的领域语义，以及一张可证伪的地图，说明对于受监管代币执行标准，什么是已证明的、什么是有界证据、什么是假设的、什么是开放的。该研究面向智能合约形式化验证、安全代币标准和监管科技领域的研究者与工程师。