ERC-TRUST 1.2, completed in early October, makes ERC-TRUST, to our knowledge, the first security-token standard backed by machine-checked proof. ERC-TRUST is our proposal for a comprehensive and adaptable execution standard for regulatory actions on security tokens. Its proofs now reach the code that actually runs: every registered execution of its six regulatory actions is checked against the exact compiled bytecode, and for the regulatory freeze, the FREEZE action, the proof covers every possible input. A valid order freezes exactly what the rules say, and an invalid one is rejected without touching the asset.
What ERC-TRUST 1.2 Proves
For issuers, custodians and regulators, a regulatory action has to work every time, and an order without valid grounds must never move an asset. Tests show that code behaved correctly in the cases someone wrote down. A proof shows that, under its stated assumptions, no case is left in which it fails.
For the freeze, the proof works on the compiled bytecode itself and covers every input, including edge cases such as a freeze larger than the token's total supply. That is why the word guarantee now applies to it. The proof also has teeth: on a compiled copy with a single safety check removed, the proof's rejection checks failed.
A New Bar for an Ethereum Standard
A standard's name does not mean its behavior has been proven. Under Ethereum's own process, EIP-1, a standards proposal comes with a written specification and an implementation, and implementations are usually checked with tests and audits. The process does not ask for a machine-checked link between the text of a standard and the code that runs it.
ERC-TRUST set itself that harder goal: treating the standard itself as something to verify. Its rules were first written as a machine-checked model, the step described in Formalizing ERC-TRUST from Normative Rules to Executable Semantics, and with ERC-TRUST 1.2 the evidence reaches the compiled code. We set out this approach as whole-standard assurance on Ethereum Research. In our review of the other security-token standards, including ERC-3643, ERC-1400, ERC-1404 and ERC-7943, we found no published formal verification of their regulatory actions.
Six Actions, Three Ways to Adopt
ERC-TRUST 1.2 covers all six regulatory actions (freeze, seize, confiscate, restrict, recover and liquidate) across three ways to adopt the standard: a new native token, an adapter for tokens already issued under ERC-3643, and a hook for new ERC-3643 deployments. We ran the hook against the actual bytecode of T-REX 4.1.3, the reference implementation behind ERC-3643. In all three, the proof kernel of Isabelle/HOL checked each registered execution of the compiled code against the model, and an internal reviewer who took no part in building the evidence checked it again.
The ERC-TRUST 1.2 freeze guarantee rests on two declared technical assumptions about hashing and storage layout, the other executions are checked where they were registered, and proving that every possible execution matches the model remains ongoing research. This is neither a third-party audit nor a verified deployment.
Check It Yourself
“Guarantee” is not a word anyone gets to use lightly, so we back it with public, independently verifiable mathematics. The GitHub repository holds the code and proofs with the commands to replay them, and it records the ERC-TRUST 1.2 results. The paper, arXiv:2608.29134, sets out the model's semantics and how we tried to break it. The work was built with Oraclizer Veri, our in-house tool for observing what compiled contracts actually do: storage, return values, reverts and events.
For anyone who handles security tokens, ERC-TRUST 1.2 changes what can be checked. Whether a regulatory order was carried out exactly as the rules say no longer has to rest on anyone's word. For the freeze, it can be confirmed from the code itself.