Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence
Isabelle/HOL formalizes in Isabelle/HOL a reference execution semantics for the six ERC-8319 meanings: FREEZE, SEIZE, CONFISCATE, LIQUIDATE, RESTRICT, and RECOVER, and an indistinguishability theorem shows that bound kernel inputs cannot establish external facts about title, settlement, or entitlement.