Formalizing ERC-TRUST from Normative Rules to Executable Semantics

TL;DR

• Discharging a proof obligation does not show that the obligation constrains any reachable execution. If no reachable state satisfies its premise, the obligation passes vacuously, and the checker will not warn you.
• The design article before this one left three hard questions: expressing SEIZE’s custody and retained ownership non-vacuously over a fungible balance, and keeping LIQUIDATE and RECOVER from pulling external facts into token events while still fixing action identity and the applied condition. This article answers them.
• Applied, rejected, and operational-failure outcomes for the six regulatory actions, the three reversals, ordinary transfer, replay protection, frame preservation, and authority rotation close into one state model. Each rule then had an execution built for it so that the rule is not empty.
• Verification runs in two layers. A separate program re-enumerated the kernel’s own list in reverse and compared, and fifteen deliberately broken variants were fed in and caught fifteen times. Every claim reported here closed down to its foundations without accepting an outside calculator’s answer and without an unproven placeholder anywhere beneath it.
• All of this holds within the declared semantic domain. Solidity code, compiled bytecode, a deployed artifact, and legal fact are not claimed here.

Why Formalize Before Implementation

The design article for this standard started from a problem: on-chain, a reversible freeze and an irreversible confiscation collapse into the same call. It then froze a norm, that the legal effect of the six regulatory actions becomes a set of distinct first-class objects. Freezing a norm means fixing sentences. The next question is a different kind. What survives and what disappears when those sentences are lowered into a form a machine can check?

The reason to do this now is ordering. Move the sentences into Solidity first, discover the norm contradicts itself later, and by then the code, the tests, and the audit target already stand on that contradiction. The cost of backing out scales with the size of the implementation. Find the contradiction at the sentence stage and the thing you fix is one sentence. The three questions the previous article left pointed the same way, because each of them asks whether something is expressible at all. If custody over a fungible balance genuinely cannot be expressed, that is worth knowing before anyone writes a contract.

In one paragraph: the concepts the standard uses were defined as states, commands, and outcomes; what each regulatory action changes and leaves untouched was written as propositions; and a proof assistant checked those propositions one at a time. An executable kernel was then extracted from the same definitions, run, deliberately broken, and re-counted by a separate program. What came out is a confirmation that the obligations of this standard are discharged and that each one constrains an execution that is actually reachable. This is the part of security token formal verification that a green check alone never establishes.

What this work stands on is the regulatory-action composition model that was mechanically checked earlier. What it adds is the relation that the standard’s product meaning uses that verified structure correctly. The two layers prove different things, and the difference matters repeatedly below. This article stops at the checkpoint where the abstract model was frozen and verified; everything below describes what was true at that point.

Figure 1: From a normative sentence to reproducible evidence, with the proof loop and the execution loop that check each other

What a Single Normative Sentence Unfolds Into

“An authorized authority may freeze a given amount in a target account; the freeze is reversible; ownership does not transfer.” One line as prose. To let a machine detect a violation of that line, everything folded inside it has to be pulled out and named.

Which domain and which token. Which version of that token. Which action. Who the subject is and where the destination points. What amount. Which regulatory case it belongs to. What one-time value blocks reuse. Which policy and which authority it binds to. That policy’s code, schema, configuration, provenance, and validity window. And the values observed immediately before and immediately after execution.

A one-line norm unfolds into more than a dozen binding axes. That is the first output of formalization, and for an implementer it becomes the minimum set of facts a conforming design must bind and keep traceable, not necessarily a list of separate storage fields. Omit any one of them and that implementation cannot later answer “under which authority and which policy version was this freeze executed.” Not being able to answer means there is nothing for an auditor or a regulator to point at, and the legal legibility the previous article promised breaks at exactly that point.

One thing became clear here. A standard writing “authority MUST be verified” and a standard defining what authority is, what it binds to, and when it expires are different amounts of work. The first relies on the reader’s good faith. The second makes independent implementers arrive at the same conclusion.

Three worked examples of that descent, each running from the normative phrase to the formal object to what an outside observer can actually see:

• The authority MUST be authorized for this action becomes an authorization record bound to domain, action, subject, and policy version, and becomes observable as the receipt naming which authorization was consumed and retired.
• A freeze MUST be reversible and a confiscation MUST NOT be becomes a case state that admits a reversal transition after FREEZE and admits none after CONFISCATE, and becomes observable as the case state carried on the call.
• A rejected action MUST NOT change state becomes a rejected outcome defined so that every observable equals the pre-state, and becomes observable as the pre and post observation pair recorded for that call.

A normative rule was separated into typed bindings and three observable outcome classes before implementation.

Why Six Actions and Seven Labels Stay Apart

The previous article declared that the six regulatory actions the product exposes and the seven transition labels of the composition model are not the same list. Reversal commands are not RCP action identities, and recovery and liquidation sit in the transfer and settlement layer. The declaration stopped there.

Formalization had to turn that declaration into a checkable proposition, because it forces you to say precisely what breaks if the two lists are treated as one. What the standard requires is preservation of the six action identities and their observable results, and it does not require internal functions to correspond one-to-one with transition labels. That statement holds because the two layers were kept apart. Merge them and the standard starts dictating the internal structure of an implementation, and an implementation with a different internal structure gets pushed out as non-conformant even though it realizes the same regulatory meaning.

For an implementer the separation comes back as freedom. If each of the six actions is separately observable and produces the specified result, the standard does not ask how the internals were assembled. This is why the standard can stay thin, and why it keeps the distinctions while staying thin.

The obvious objection at this point is that ERC-7943 and ERC-3643 already ship freeze and forced transfer, so a prose profile over them would be cheaper than a new proposal. The increment this stage adds is not another mechanism. Both of those standards state their rules in prose, and prose gives you no way to ask whether a stated rule excludes anything. You cannot check a prose rule for vacuity, you cannot enumerate the order effects it implies, and you cannot hand a reviewer a counterexample when it fails. Writing the rules in a form where “does this rule forbid anything” has an answer is the part a profile document cannot supply.

Rules That Pass Every Check and Require Nothing

Formalization has a failure mode that prose does not. The formal-methods literature calls it vacuity: an obligation is discharged and at the same time constrains no reachable execution. If no state satisfying the premise exists, every proposition over that premise is true. Logically true, check passed, nothing guaranteed.

What that means for a standard is not light. Write conformance requirements nobody can satisfy and the checker still turns green. Suppose there is a rule saying no transfer may exceed the frozen amount, and the state where an amount is frozen is itself unreachable. The rule blocks nothing. Claiming to have implemented that standard is then true no matter what you built.

So separately from writing the rules, the existence of executions that trigger them was proved on its own. For each of the six actions, a path where it applies, a path where it is rejected, and a path where it fails operationally were built one by one and confirmed reachable. The three reversal paths, ordinary transfer, and the alternate state path were confirmed the same way. A proof assistant answers whether a proposition follows from its premises. It does not answer whether anything satisfies those premises. That second question is one a person has to ask separately, and in security token formal verification it is the question that decides whether the result means anything.

For a third party this becomes a design requirement for any later conformance check, not a conformance check by itself. When an implementation claims conformance, one thing that has to be checked is whether the executions that trigger those requirements exist inside that implementation. It is also why conformance vectors cannot contain success paths alone. Inputs where rejection and operational failure actually occur have to be there for the vector to be checking anything.

Figure 2: The same rule and the same checker returning the same pass, once over a premise nothing reaches and once over a premise a constructed witness reaches

Where the Line Stops in Front of Legal Fact

The three the previous article called hardest close here. All three have the same shape: decide what to guarantee over on-chain state without the standard pretending to know what that state cannot know.

SEIZE had to express custody over a fungible balance. When part of a commingled account moves into an authority’s custody, who the prior holder was and what encumbrance sits on that amount both have to survive, while holding the boundary that a balance movement alone cannot say legal title moved. After a successful SEIZE, custody state, the declared prior-holder reference, and the encumbrance are all preserved, and that this connects non-vacuously to the model above it was confirmed alongside. What was not proved is the attribution of actual legal title.

LIQUIDATE has its real sale and its real proceeds happening off-chain. So the proof reaches exactly as far as a bound attestation about settlement being tied to the token disposition receipt as one unit. Whether it actually sold, whether proceeds arrived, whether the debt cleared: the model does not say.

RECOVER looks like a problem of judging the rightful owner, and the standard cannot make that judgment. So what was proved is the provider-asserted destination, the commitment behind that assertion, the credit actually reflected at the destination account, and that the commitment is consumed exactly once. Who the rightful owner is falls outside what is proved.

The three share one shape. Take external fact as input without asserting that the input is true, and close only what happens to on-chain state and receipts once that input arrives. For an implementer this line is a line of responsibility. Implementing this standard is not vouching that an external judgment was correct. It is leaving a reproducible record that enforcement after that judgment arrived went as specified.

Figure 3: Two opposite external legal worlds produce the same kernel observation when the core input is identical

How to Check This Without Taking Our Word for It

Saying the proofs all passed is not verification, because we are the ones saying it. Security token formal verification only means something to a reader if someone else can re-run it, so the time went into leaving it in that form, in two layers.

First, an executable kernel was extracted from the finished definitions and made to enumerate every case it handles. The problem with that is when the enumerator itself is wrong, because a wrong enumerator produces a wrong list consistently. So a separate program re-counted the same kernel in reverse and the two lists were compared. Neither the standard-side list nor the list from the model beneath it was off by a single row.

Second, implementations that deliberately break the rules were fed in. A version that fails to preserve custody, a version missing the settlement binding, a version that never credits the recovery destination, and so on: fifteen ways of breaking it, caught fifteen times out of fifteen. Then the original was restored and confirmed to pass again. A check that only confirms passing rules nothing out. You learn that a check is protecting something by seeing it catch the violation.

One discipline held over the proofs themselves. Every claim reported here closed down to its foundations with no outside calculator’s answer taken as given and no unproven placeholder anywhere beneath it. A proof assistant can open a channel that hands a computation to an external tool and trusts the answer, and using that channel blurs what the final claim rests on. The work closed with that channel shut.

This structure is the input to a conformance vector rather than the vector itself. For a third implementer to say they realized the same meaning, they have to be able to regenerate the same list from their own implementation and compare it, and the same violations have to be caught in their implementation too. Regenerating an identical finite list does not by itself prove that two implementations mean the same thing; it rules out a class of ways they could differ.

Where We Got Stuck

The results above did not arrive in order. The work took three passes, and the middle one ended with nothing gained.

We Took a Shortcut We Had Already Learned About

The fastest way to confirm a concrete execution is to compute the value directly. Closing it that way let the build proceed, but the proof audit flagged twenty-four places. A position closed by computation is not one the logical kernel checked; it is an answer copied down from an external calculator, which blurs what the final claim rests on. Twenty-four of the channels described in the previous section had been left open.

The trouble is that we had already hit this trap once. The same shortcut caught us the same way during the underlying model work, and we had written down that searching the source does not find it. Having the record and having the record fire on the next layer up turned out to be different things. What we backed into is one discipline: no computational automation on load-bearing proofs, and when starting a new layer, read the previous layer’s trap list first.

The Log Would Not Tell Us Where It Failed

With the computational automation stripped out and symbolic normalization in its place, time blew up instead. The full check hit the time limit, and so did an abbreviated diagnostic check. So we moved a deliberate failure point back and forth through the theory to narrow down which proposition was slow.

Five attempts, five identical endings. The time limit applied to the check as a whole rather than to any single proposition. Before reaching the failure point we had planted, the accumulated time of the commands ahead of it used up the limit, and the log left nothing but a timeout each round. Turning on detailed recording did not preserve per-command timing either.

The reason this was bigger than a code problem is that the conclusion that day was not “we did not find the slow proposition” but “the current approach cannot find it.” Continuing to edit was pointless. So the day closed with nothing fixed and only a diagnosis recorded.

The break came from changing how we measured. A fragment of the theory up to a chosen point was copied mechanically, its content pinned by hash, and checked once on its own so the intermediate result could be stored. Checking target propositions one at a time on top of that stored result removed the cost of redoing the front section every round and measured only the individual proof. A place that had taken ten minutes finished in forty-two seconds. What remains is two rules: separate whether the obstacle is the proof or the measurement, and if it is the measurement, move the boundary. And a diagnostic fragment is never promoted into evidence for a verdict, under any circumstances.

We Rolled an Encoding Back

Compressing the observations before and after execution into one large integer makes comparison simple. The initial design took that road, and the arithmetic burden on the checker grew to match. The proofs only came apart after rolling back to a structured observation record, separating the shared precheck, and splitting the work into per-action helpers.

What we gave up here was elegance. The compressed representation is cleaner and it sacrificed checkability. This is another confirmation that the choice of definitions decides what can be proved, which also means that when stuck, suspect the definition before the proof tactic.

Our Own Falsification Set Was Short

After the proofs all passed, twelve rule-breaking versions went in and all twelve were caught. Looking again, though, none of them directly broke the three hard boundaries: custody preservation, settlement binding, and the recovery destination. Things around them were touched, and nothing aimed at the boundaries themselves.

Adding three and stopping there was not enough. The sequence ran again from the beginning, because proof, list generation, reverse comparison, and violation checking have to flow once over the same source state for the results to point at the same thing. What remains is one criterion: a violation set is counted not by how many were caught but by whether every claimed boundary has a violation aimed straight at it.

What Security Token Formal Verification Established at This Stage

One sentence is permitted, and it is worth quoting exactly. The ERC-TRUST abstract regulatory-action model has been mechanically verified in Isabelle/HOL within its declared semantic domain. That covers applied, rejected, and operational-failure outcomes for the six actions, the three reversals, ordinary transfer, the alternate state, the relationship to existing standard paths, replay protection, frame preservation, authority rotation, and the three boundaries above.

What it does not cover is stated as plainly, and it is stated for this stage. At this stage it does not mean a Solidity implementation is verified. It does not mean compiled bytecode or a deployed artifact is verified. It does not mean legal ownership or the truth of an external event is proved. It has no bearing on standard adoption or editor approval. Prior work has used Isabelle/HOL to reason about Ethereum bytecode; that is precisely a later verification layer this article does not claim. Showing that real code preserves this meaning is a different kind of work, and a separate track carries it.

What an implementer takes on belongs next to what they get. Every regulatory action has to carry a typed context and produce a canonical receipt, which is more calldata to pass and more to bind than a bare forced transfer. Every outcome class needs a reachable execution in the conformance evidence, including the rejections and the operational failures rather than the successes alone. And the trust model for external judgment has to be declared rather than assumed, because the standard takes that judgment as input without asserting that it is true.

This staging is itself part of the claim. Point each claim at the evidence of its own stage and a reviewer can check which sentence rests on what. A claim rolled into one undifferentiated statement is a claim a reviewer cannot check, and a claim that cannot be checked ends up as a request to trust the designer.

Questions This Stage Left Open

At this checkpoint, three questions remained open.

First, when a norm reopens, what part of the formalization reopens with it. A normative layer does not stay frozen forever; a relationship with an adjacent standard can force it open again. Deciding in advance which parts belong to a full reopening and which belong to a comparison-scope reopening is part of designing the formalization. Draw that boundary late and every tremor in the norm holds the whole proof asset hostage.

Second, how much reachability a conformance check has to require to stay meaningful. Require it only for success paths and rejection rules can be vacuous. Require it for every combination and the cost of checking grows without a ceiling.

Third, once a standard declares that it takes external judgment as input, how far it should specify where that input comes from. Leave it unspecified and trust models diverge across implementations. Specify it and the standard is choosing, in advance, among institutions that differ by jurisdiction.

Closing

The largest lesson from lowering a norm into machine-checkable meaning was not a proof technique. It was deciding what to leave unproved. The legal title behind a custody relation, the settlement that happens off-chain, who the rightful owner is. The standard could have pretended to answer all three, and pretending would have looked stronger. Declining to answer and marking the boundary in that spot is what made the rest checkable.

The day that did not pass also left more than the proofs that did. Closing a day with a diagnosis that the failure point cannot be identified looks like nothing gained, and that diagnosis changed the next approach. A green check in security token formal verification is an outcome, not a goal.

The question left for the reader: when a standard says it is self-checkable, what should the minimum condition of that claim be? Is discharging every obligation enough, or does it also have to show that executions triggering those rules exist? We took the second, and that choice accounted for half the work. Related reading is the Regulatory Compliance page in the documentation.

References

1. Kim, J., Viglione, R., Spuller, D. (2026). ERC-8319: Regulatory Compliance Protocol (Pull Request #1848, ethereum/ERCs). https://github.com/ethereum/ERCs/pull/1848
2. Lo Buglio, D., et al. (2026). ERC-7943: uRWA, Universal Real World Asset Interface. https://eips.ethereum.org/EIPS/eip-7943
3. Tokeny, et al. (2021). ERC-3643: T-REX, Token for Regulated EXchanges. https://eips.ethereum.org/EIPS/eip-3643
4. Beer, I., Ben-David, S., Eisner, C., Rodeh, Y. (2001). Efficient Detection of Vacuity in Temporal Model Checking. Formal Methods in System Design, 18, 141–163. https://research.ibm.com/publications/efficient-detection-of-vacuity-in-temporal-model-checking
5. Amani, S., Bégel, M., Bortin, M., Staples, M. (2018). Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL. CPP 2018, 66–77. https://trustworthy.systems/publications/full_text/Amani_BBS_18.pdf
6. Nipkow, T., Paulson, L. C., Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer. https://isabelle.in.tum.de/