TL;DR
- An ERC number does not mean the standard was verified: nothing in Ethereum's standards process checks by machine that a standard's text and its code behave alike.
- To make that kind of Solidity formal verification possible, ERC-TRUST changed its own design first: an exact-use ticket in front of legacy forced transfers, one owner for regulatory state, a reference kernel that cannot be upgraded, and ERC-3643 support that counts only with evidence.
- A pilot carried FREEZE from the verified model down to compiled bytecode, and when its first remote proof run passed only 2 of 13 rules, we corrected the model until all 13 passed without weakening any of them.
- That settles the design layer; a proof covering every compiled execution is still ahead.
What an ERC Number Does Not Check
For a security token implementer, the trouble starts with one call. Both ERC-7943 and ERC-3643 define forcedTransfer(from, to, amount) [1, 2]. The calldata does not say whether the tokens are moving into court-ordered custody, being permanently taken in a confiscation, going back to the owner they were stolen from, or being sold off in a liquidation to repay a debt.
Those four have different legal effects. Custody can be released later, the other three close the case, and each one has to leave its own record. On chain they all look like the same balance movement, and neither an indexer nor an auditor can tell from the code which of them happened. ERC-8319 gives names to six such legal effects [3], and ERC-TRUST is the standard proposal that turns those names into typed execution.
An ERC number makes this gap easy to overlook, because many readers assume that a numbered standard was verified somewhere along the way. EIP-1, which defines the standards process, describes a Standards Track proposal as a design document, an implementation, and, where warranted, an update to the formal specification. No step in that process checks by machine that the text and the running code behave alike; implementations are usually checked with tests and audits. ERC-TRUST set out to verify the standard itself. Its normative sentences, machine-readable core, generated interfaces, reference implementation, runtime bytecode, conformance evidence, and remaining assumptions are treated as one auditable chain, an approach we described on Ethereum Research as whole-standard assurance.
The first stretch of that chain, told in Formalizing ERC-TRUST from Normative Rules to Executable Semantics, ended with an abstract model verified in Isabelle/HOL within its declared semantic domain. At that point we had a proved specification and no contract. Most Solidity formal verification starts from the other end: the code already exists, and the verifier writes a specification to fit it. Starting from the proved side changed what counted as a good design. A contract structure now had to be something the tools could prove before it could be something convenient, and five decisions came out differently because of that.
Five Design Changes Made for the Proof
A Legacy Call Does Not Say Which Action It Is
We decided early that the token would never guess a regulatory action from a legacy call. A rule that told seizure from confiscation by function name or argument shape could be written down, but it could never be proved, because the call carries nothing to prove it against. So setFrozenTokens and forcedTransfer left the public authority surface, and both selectors now run only as calls the token makes to itself.
A regulatory action arrives instead as a typed command from the account registered for its authority. The token validates the command in a fixed order, assesses the dependencies bound to it, and records one exact-use ticket: the command identifier, the selector, the calldata hash, and the dependency root and epoch current at preparation. When the token then calls its own sensitive selector in the same transaction, the selector compares every recorded field with the actual call and the current dependency state, and only on a full match does it consume the ticket and apply the transition. Reuse, altered calldata, a direct external call, a wrong selector, or a dependency change in between all revert with TrustRouteMismatch [4].
The ticket did not start out this tight. In the pilot, a prepared route could wait for its matching call; the reference implementation later narrowed it to a ticket that lives only inside one transaction and never becomes standing authority. Because of that narrowing, an implementer can expose the ERC-7943 interface without handing its selectors to anyone. It also turns the route into something a verifier can state and prove: a wrong caller or altered calldata can neither use nor corrupt someone else's ticket.
Regulatory State Has Exactly One Owner
Where regulatory state lives had to be settled before any storage layout, because the answer decides what a proof can say. If a registry and a token each kept a copy of the same frozen amount, no proof could tell which copy is true; a proof can only make statements about one store. So a registry stays upstream, as a source of evidence and policy and as a router, and the token or an adapter is the single owner of regulatory state and receipts.
Two copies of one frozen amount, crossed out: regulatory state got one owner.
Today's native token owns ERC-20 balances, frozen targets and restriction flags, cases and their overlays, custody records, action records and receipts, replay keys, authorities, and dependency bindings, as its architecture document lists. Its four dependencies, for policy, identity, settlement, and entitlement, are read-only. Each binding fixes a dependency's address, runtime code identity, configuration digest, schema, and per-kind epoch, and the four fold in a fixed order into one dependency root; rebinding any of them advances a global epoch by one. A command carrying a stale root or epoch is rejected before any state is read, and a call fails closed when the code, configuration, return length, outcome word, command echo, or binding echo does not match.
A dependency upgrade therefore never slips in quietly. The epoch moves, and commands prepared under the old epoch stop executing. The same rule spares the proofs an awkward assumption, since failures can be classified without guessing how the return values of unresolved external calls relate to one another.
Why the Reference Kernel Cannot Be Upgraded
This decision cost the most. Five candidates were on the table: a single monolithic contract, a minimal immutable core with versioned modules and adapters, a UUPS or transparent proxy, a Diamond, and an interface-only standard with a modular reference implementation. We weighed them on how small the standard surface stays, whether upgrade authority can invalidate proofs, storage and selector risk, what a static prover and symbolic execution can express, compatibility with ERC-7943 and ERC-3643, gas and deployment limits, and the operational load on implementers.
A proxy was the familiar answer, and it stayed on the list until we counted what each upgrade would reopen. Initialization, storage layout, the frame of every function, and the upgrade path itself would all have to be proved again after every upgrade, and one admin key could void what had already been proved. A Diamond widens the proof surface further through dynamic routing and storage aliasing, which a surface this thin cannot justify. The monolith kept pulling policy and identity into the standard surface, and in the end it fit in exactly one place: a small pilot with a narrowed boundary between pure decisions and state application.
What we chose combines two layers. The standard layer is interface-only, so semantics, ABI, and observable results become normative while the structure stays neutral. The reference deployment uses a minimal immutable core, the kernel, with versioned, fail-closed adapters.
This sets the proof cost of the reference implementation and nothing more. It does not require every conforming implementation to be non-upgradeable [4]. A proxy-based implementation can still conform, provided it re-verifies fully after each upgrade before it claims conformance again. Every reference endpoint reports proxySupported = false, and a kernel change means a new deployment.
A Profile Is a Claim That Needs Evidence
ERC-TRUST treats ERC-3643 as an optional interoperability profile rather than a normative dependency. For tokens already issued under ERC-3643, an adapter and a ProfileGovernor form one conformance unit. The governor owns the token and seals, once, the expected token code identity, the Identity Registry, the Compliance contract, the chain, the adapter's exclusive Agent relationship, and the manifest of imported legacy state. After the seal it has no arbitrary-call, Agent-management, or registry-rebinding surface, as the profile document specifies.
Every endpoint reports one profile descriptor through trustProfile(), and the descriptor is only a declaration. Importing these contracts, reusing the function names, or matching an ERC-165 identifier does not confer Full status. When evidence is missing, stale, or contradictory, the classification is Unsupported, which is the safe reading of absent evidence and says nothing about anyone's intent.
The boundary ended up narrower than we first drew it. At design time, the adapter with its sealed governor was meant to be the route to Full. Later evidence showed that an adapter over an existing token cannot block an ordinary inbound transfer within the same transaction, so that route stayed Partial, and Full now opens only for a freshly deployed token with a transfer hook. We wrote the gap into the profile document as a known limitation, so an implementer putting ERC-TRUST on top of T-REX knows before deployment what the deployment can and cannot claim.
Our ERC-TRUST 1.2 update reports how the native token's freeze was later proven for every input on the compiled code, under two declared assumptions. We found no published formal verification of regulatory actions for ERC-3643, ERC-1400, ERC-1404 or ERC-7943, so to our knowledge ERC-TRUST is now the first security-token standard backed by machine-checked proof.
Every Surface Comes from One Machine-Readable Source
The last of the five came with the second version of the kernel. The domain constant, enums, request and receipt structs, hash preimages, the kernel interface with its ERC-165 identifier, shape rules, the case transition table, reason classes, and profile descriptors now live in one JSON source, described in the repository's kernel source notes. The Solidity interface, the JSON ABI, a human-readable rendering, TypeScript types, conformance vectors for six actions and three reversals, and the receipt schema are all generated from it. The generator's check mode rejects any drift between the generated copy and the copy the implementation imports, so changing one normative identifier without regenerating the interface fails the build.
An editor reviewing the standard can rely on the prose and the machine form staying in step, and an implementer can reproduce every identifier, hash, calldata, and receipt hash in the conformance vectors from the specification and the vectors alone.
Mapping Verified Meaning onto Solidity
With the design settled, we wrote the correspondence between the model and the contract. The retrieve relation maps concrete balances, frozen targets, restriction flags, custody records, case terminality, nonces, epochs, and receipts into an abstract state. Under its declared well-formedness and pinned-runtime premises it is unique and functional, and it rejects runtime substitution; its input is the current on-chain state and pinned configuration rather than any assumed execution history [4]. The idea goes back a long way. If a function carries concrete states to abstract ones, the claim that an implementation implements a specification can be argued one step at a time; refinement mappings rest on that idea [5].
Writing the relation also meant writing down the places where it does not translate on its own, and we gave each of them a name: canonical ABI decoding and the rejection of malformed lengths, enum values, addresses, and fixed-width words; storage projection; read-only dependency calls and the classification of their return data; creation, consumption, and deletion of the same-transaction ticket; action and reversal effects with rollback; failure stutter, the rule that a rejected or failed step changes no state at all; event order and the final canonical receipt; and the identity of creation and runtime bytecode, method identifiers, and storage layout [4]. Once every seam had a name, we could ask of each one which tool covered it.
The answers were uneven. In our Solidity formal verification setup, the Certora Prover checks quantified rules over every contract state and input at the Solidity level [6]. Kontrol symbolically executes the compiled bytecode on the KEVM semantics [7], which gives an independent cross-check of the source-level result. Foundry runs concrete and fuzz tests and hosts the falsification mutants. Event order fell through all three, and no tool in this scope proves compiler correctness, deployment identity, or the truth of external facts. So we kept one rule while putting their results together: passing tools do not add up to a stronger cross-layer theorem.
What the FREEZE Pilot Checked
Before building the whole design, we took one action all the way down. The FREEZE pilot joins, in one vertical slice, a native FREEZE command, the staged setFrozenTokens route mentioned above, the frozen floor check on ordinary transfers, and the final canonical receipt [8]. It was the smallest piece of Solidity formal verification we could find that still crossed every layer of the design.
At its own point in time, the pilot left five results:
- The static prover passed all 13 quantified rules and confirmed that none of the nine externally callable state-changing functions falls outside the declared classification.
- Two bytecode proofs passed. The canonical receipt event is the last log, right after the freeze event, and after a policy failure the log holds only the constructor's Transfer while the state fingerprint stays unchanged.
- Thirteen tests and 256 fuzz runs passed.
- We broke the code in five declared ways, and each break was caught by the detector meant for it: removing the frozen floor check, keeping a consumed ticket, swapping the freeze event and the receipt, removing the caller and calldata binding, and letting an operational failure execute.
- Two isolated clean builds produced identical artifact and bytecode hashes.
The only statement attached to these results is pilot conjunct VERIFIED. The pilot does not claim full ERC-7943 compatibility or forcedTransfer, signature-based authorization, full ERC-TRUST refinement, a frozen ABI, or a finished or production-ready reference implementation, and the contract says so itself: it reports its own profile as UNSUPPORTED with only the FREEZE bit set. Of everything the pilot produced, that self-report is the result we find most telling, because the contract declares its own limit.
Where We Got Stuck
Three Tools Had to See the Same Bytes
The design documents fixed only a lower bound on the compiler, and for a while that looked like enough. It was not. Unless the three tools used the same compiler and the same optimizer settings, the code the static prover checked and the code symbolic execution checked would be different bytes, and their results could not support each other. Without a pin, Solidity formal verification by three tools would have described three different programs.
So we pinned the exact compiler commit (solc 0.8.36), 200 optimizer runs, and the IR pipeline, and disabled metadata hashing and CBOR metadata. We also turned on the option that keeps the static prover's command-line tool from swapping in an optimizer sequence of its own. If different implementers are to rerun the same evidence and reach the same conclusion, the compiler pin is part of the evidence.
A Check the Tools Did Not Have
The canonical receipt has to be the last log, and at first we had no way to check that. The test framework's sequential event expectation kept only one expected event, and reading the full recorded log was not yet implemented.
So we wrote the check ourselves, as a K rule module that reads the KEVM log cell directly. It confirms that the last two logs are the freeze event and the receipt event, and that after a policy failure the only log is the constructor's Transfer. The module added something people now have to review, so we recorded it as an assertion adapter rather than a transition summary and listed it in the trusted base. With it, the normative sentence "the receipt is the last log" became a check that can fail on bytecode.
The First Remote Proof Run Passed Two of Thirteen Rules
The first remote proof job passed 2 of the 13 rules. Seven failed, and four tripped the vacuity check, which means those four were true only because nothing could reach them; the first run record still shows it. There is a quick way to turn red rules green, which is to make them say less. We took the slow way and read the counterexamples one at a time, asking each time whether the code was wrong or whether we had written down something we did not mean. In the end the fixes went into the model, and the properties kept their strength:
- The route rules had claimed that all storage stays the same after a call with a wrong caller, wrong calldata, or a stale binding, which was more than we meant. We computed the route key from canonical calldata, so the rules now prove that the exact target ticket and its prepared record survive.
- Arbitrary payloads on inactive paths, which carry no meaning in any real call, were projected to canonical zero values, so only active state is compared.
- Operational failure became a deterministic event, a mismatch between the live policy code identity and the bound one, so no correlation between unresolved external return values has to be assumed.
- The recipient's balance increase was written as checked arithmetic, so modular overflow cannot slip through even from symbolic storage states.
The final configuration has no optimistic arguments and no always-allow summaries. The final gate kept the basic vacuity check. The advanced check we used during diagnosis also flags deterministic postconditions in function bodies as tautological, so it stayed a diagnostic tool. We did not delete the failing run; it stays in the repository as diagnostic evidence. Two days later all 13 rules passed, and "a wrong caller can neither use nor corrupt someone else's ticket" was proved as a statement that means what it says.
The first run record: 2 of 13 rules passed; the fixes went into the model.
Everything Passed, and It Was Still Not Done
Then every technical condition passed, and we still did not mark the work complete. One condition was left: the source, ABI, bytecode, specification, and report had to be bound to the same commit, so the status stayed at "verification passed, commit binding pending." There was a shortcut that would have closed it sooner, writing a predicted hash of the not-yet-created commit into the evidence files, and we did not take it. The enumerated content hashes served as the binding first, and the commit identifier was recorded afterwards as provenance, so anyone reproducing the result can confirm by hash that it is about exactly this code.
What Solidity Formal Verification Established at This Layer
By the end of this stage we could answer the three kinds of readers who usually look hardest at a new ERC.
An ERC editor wants to know whether the normative sentences can be verified at all. Here the identities of six actions and three reversals, the receipt preimage, and the failure classes live in one machine-readable source, every public surface is generated from it, and the build fails when prose and machine form drift apart.
Participants on Ethereum Magicians tend to ask whether existing standards could do the same job more cheaply. Documenting intent next to an existing forcedTransfer does not turn that intent into something a proof can check, and as long as the call does not state its action, no proof can separate seizure from confiscation. What ERC-TRUST adds is a typed action identity, a canonical receipt, and an evidence boundary that states what was proved and what is assumed, and none of that shows up in a count of functions.
A security token implementer asks what they gain and what they take on. The gain is an ERC-7943 surface without standing authority, a single owner for state, dependencies that fail closed, and profile declarations backed by evidence. The price is a new deployment and a new manifest for every kernel change, dependency binding and epoch management, the cost of read-only calls, and, on ERC-3643, a choice between Partial and Full.
The design went on to three ways to adopt the standard: a native token, an adapter over an existing ERC-3643 token, and a hook in a new ERC-3643 deployment. What this layer has not given is a proof that builds the runtime correspondence for every accepted execution in a declared profile, from source and compiler or bytecode semantics, external-call assumptions, and trace observations. A handful of selected proofs cannot stand in for that theorem, and we do not let them.
Questions This Layer Left Open
- Does a standard designed for proof lean toward what today's tools can express? Giving up upgrades was a proof-cost decision for the reference implementation; in a real deployment that needs upgrades, who pays for re-verification?
- How should an ERC state profile claims so that interface detection is never read as conformance? An ERC-165 identifier cannot tell Partial from Full.
- Which should be normative, the machine-readable source or the prose people read? Generating the prose from the source removes drift, but editors still review prose.
Conclusion
The hardest lessons of this stage were about order more than technique. Once verification is an input to the design, the design pays first. We gave up upgrades in the reference implementation, put a ticket in front of sensitive calls, wrote a check the tools did not have, and agreed to claim compatibility only as far as the evidence goes. In return, each normative sentence became something that can be checked, and can fail.
The FREEZE pilot showed that this structure can be proved on compiled code, and the run that stopped at 2 of 13 rules is still in the repository next to the one that passed. This much is proved; a proof for every compiled execution is the next piece of work.
For a standard to say that its code can be checked against its own text, what should it be prepared to give up at design time?
References
- [1] Lo Buglio, D., Martinez Molina, T., & Colceriu, M. (2025). ERC-7943: uRWA, Universal Real World Asset Interface. https://eips.ethereum.org/EIPS/eip-7943
- [2] Lebrun, J., Malghem, T., Thizy, K., Falempin, L., & Boudjemaa, A. (2021). ERC-3643: T-REX, Token for Regulated EXchanges. https://eips.ethereum.org/EIPS/eip-3643
- [3] Kim, J., Viglione, R., & Spuller, D. (2026). ERC-8319: Regulatory Compliance Protocol (Pull Request #1848, ethereum/ERCs). https://github.com/ethereum/ERCs/pull/1848
- [4] Kim, J. (2026). Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence. arXiv:2608.29134. https://arxiv.org/abs/2608.29134
- [5] Abadi, M., & Lamport, L. (1991). The Existence of Refinement Mappings. Theoretical Computer Science, 82(2), 253-284. https://doi.org/10.1016/0304-3975(91)90224-P
- [6] Certora. (2026). Certora Prover Documentation. https://docs.certora.com/
- [7] Hildenbrandt, E., Saxena, M., Rodrigues, N., et al. (2018). KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. IEEE CSF 2018, 204-217. https://daejunpark.github.io/papers/kevm.pdf
- [8] Oraclizer Research. (2026). ERC-TRUST Preserved FREEZE Pilot: Verification Evidence. https://github.com/Oraclizer/erc-trust/blob/767c87c2db03219032bdbeaf8e5b06beac19208e/pilot/evidence/proof-report-v2.md